SQEMA Samples


[3]([1]p, [2](p, q), <1>[1]q)


[2]([1]([1]p  p), ([1]  p))


(((p -> q), r) -> ((p, r) -> (q, r)))


((p, (q -> r)) -> ((p, q) -> (p, r)))


((p, (q -> r)) -> ((p, q) -> (q, r)))


(T -> C(1, 1))


((0 != p) -> C(p, 1))


((0 != p) -> C(p, p))


(C(p, q) -> C(q, p))


(C(p, q) -> (C(p, r)  C(-r, q)))


(((0 != p)  (0 != -p)) -> C(p, -p))


(((0 == (p * q))  (1 == (p + q))) -> (C(p, p)  C(q, q)))


((0 != (p * -q)) -> (C(p, -q)  C(q, -q)))


(p -> [U]p)

<U>

<U>


(p -> [U]p)


((<U>p₁  <U>p₂  <U>p₃) -> (<U>(p₁  p₂)  <U>(p₁  p₃)  <U>(p₂  p₃)))


(p -> [U]p)


(p -> [U]p)


((<U>p  p) -> p)


((p  p) -> [U]p)


((<U>p  p) -> [U]p)


([U]p -> p)


([U](p -> p) -> p)


((p <-> q) <-> p)


(p <-> (((  (p  q  r)) -> ((p -> q)  (q -> p)  r)) -> (p  ((p -> r)  (q -> r)  (p -> q)))))


((p -> p)  (p -> p))


(((ci  p) -> <U>(ci  p))  ((ci  p) -> ci))


(([U]p -> p) -> [U]p)


([1][2]^-1p -> [3]p)


(((p  q)  (p <-> q)) -> (p  q))


(((  p) -> p) -> p)


(p -> p)


((p -> p)  (p -> p))


((p  q) -> (p  q))


(((p  q  r)  (p  q  r)  (p  r  q)  (p  q  r)  (q  r  p)  (q  p  r)  (r  p  q)  (p  q  r)) -> )


(((p  r)  q)  p)


(p  q)


(((p -> q)  p) -> q)


(p -> p)


(p -> p)


(p -> p)


((p -> p) -> p)


((p -> q)  (q -> p))


((p <-> q) -> p)


((p  p  q)  (p  p  q)  p)


(((p  q)  q) -> (p  q))


((p -> q)  (p -> p))


((p  p) -> q)


(p -> p)


(p -> p)


((p  q) -> (p -> q))


(((p  q)  (p  q)) -> (p  q))


(((p  q) -> (p -> q))  (((p  q)  (p  q)) -> (p  q)))


((p  p  q)  (p  p  q))