|
|
(  p -> p)
(p -> p)
((p -> p)  (p -> p))
((p -> p)  (p -> p))
((p -> p) -> p)
(c ->  c)
((p q) p q)
(p -> p)
(p -> p)
(p -> p)
(p -> p)
((q p) q p)
(p2 (p1 p2) p1)
(p -> [U]p)
((<U>p1 <U>p2 <U>p3) -> (<U>(p1 p2) <U>(p1 p3) <U>(p2 p3)))
(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)))
K45: (((( (p q r)) -> ((p -> q) (q -> p) r)) -> (p ((p -> r) (q -> r) (p -> q)))) -> p)
(p -> [U]p)
<U>
<U>
[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)))
(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)
(((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 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 -> 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))
|