====
Not
====

--x

---

(proof (block
  (expression
    (not (not (variable))))))


====
And
====

a ^ b ^ c

---

(proof (block
  (expression
    (and
      (and
        (variable)
        (variable))
      (variable)))))


====
Or
====

a _ b _ c

---

(proof (block
  (expression
    (or
      (or
        (variable)
        (variable))
      (variable)))))


====
Implies
====

a -> b -> c

---

(proof (block
  (expression
    (implies
      (variable)
      (implies
        (variable)
        (variable))))))


====
Iff
====

a <-> b <-> c

---

(proof (block
  (expression
    (iff
      (variable)
      (iff
        (variable)
        (variable))))))


====
Forall
====

A x . A y . x
A x x ^ A y y
A x A y y ^ z

---

(proof (block
  (expression
    (forall
      (variable)
      (forall
        (variable)
        (variable))))
  (expression
    (and
      (forall
        (variable)
        (variable))
      (forall
        (variable)
        (variable))))
  (expression
    (and
      (forall
        (variable)
        (forall (variable) (variable)))
      (variable)))))


====
Exists
====

E x . E y . x
E x E y x

---

(proof (block
  (expression
    (exists
      (variable)
      (exists
        (variable)
        (variable))))
  (expression
    (exists
      (variable)
      (exists
        (variable)
        (variable))))))


====
Not & And
====

-a ^ b
a ^ -b

---

(proof (block
  (expression
    (and
      (not (variable))
      (variable)))
  (expression
    (and
      (variable)
      (not (variable))))))


====
And & Or
====

a ^ b _ c
a _ b ^ c
a ^ b _ c ^ d
a _ b ^ c _ d

---

(proof (block
  (expression
    (or
      (and (variable) (variable))
      (variable)))
  (expression
    (or
      (variable)
      (and (variable) (variable))))
  (expression
    (or
      (and (variable) (variable))
      (and (variable) (variable))))
  (expression
    (or
      (or
        (variable)
        (and (variable) (variable)))
      (variable)))))


====
Or & Implies
====

a _ b -> c
a -> b _ c
a _ b -> c _ d
a -> b _ c -> d

---

(proof (block
  (expression
    (implies
      (or (variable) (variable))
      (variable)))
  (expression
    (implies
      (variable)
      (or (variable) (variable))))
  (expression
    (implies
      (or (variable) (variable))
      (or (variable) (variable))))
  (expression
    (implies
      (variable)
      (implies
        (or (variable) (variable))
        (variable))))))

====
Implies & Iff
====

a -> b <-> c
a <-> b -> c
a -> b <-> c -> d
a <-> b -> c <-> d

---

(proof (block
  (expression
    (iff
      (implies (variable) (variable))
      (variable)))
  (expression
    (iff
      (variable)
      (implies (variable) (variable))))
  (expression
    (iff
      (implies (variable) (variable))
      (implies (variable) (variable))))
  (expression
    (iff
      (variable)
      (iff
        (implies (variable) (variable))
        (variable))))))


====
Iff & Forall
====

a <-> A x . x
A x . x <-> a
A x . x <-> A y . y
x <-> A y . y <-> x
A x x <-> a

---

(proof (block
  (expression
    (iff
      (variable)
      (forall (variable) (variable))))
  (expression
    (forall
      (variable)
      (iff (variable) (variable))))
  (expression
    (forall
      (variable)
      (iff
        (variable)
        (forall (variable) (variable)))))
  (expression
    (iff
      (variable)
      (forall
        (variable)
        (iff (variable) (variable)))))
  (expression
    (iff
      (forall (variable) (variable))
      (variable)))))


====
Not & Forall
====

-A x -x

---

(proof (block
  (expression
    (not
      (forall (variable) (not (variable)))))))