|
[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>p1 <U>p2 <U>p3) -> (<U>(p1 p2) <U>(p1 p3) <U>(p2 p3)))
( 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))
|