Goal
J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- Jm3
Linearized Gentzen Proof
- m3; J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3 by Axiom
- J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3; ~m3 by =>not
- m2; J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3 by Axiom
- J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3; ~m2 by =>not
- J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3; (~m2 & ~m3) by =>&
- m1; J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3 by Axiom
- J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3; ~m1 by =>not
- J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3; (~m1 & (~m2 & ~m3)) by =>&
- ~(~m1 & (~m2 & ~m3)); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3 by not=>
- J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m2; m3 by []=>
- ~m2; J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m3 by not=>
- J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1; m3 by []=>
- ~m3; J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1 by not=>
- J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3 >- m1 by []=>
- ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K1~m3; K2~m3 >- m2; m3; K1m1; K1~m1 by =>[1]
- m3; ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1m3; K1~m2; K2~m3 >- m2; m3; K1m1; K1~m1 by Axiom
- ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1m3; K1~m2; K2~m3 >- m2; m3; K1m1; K1~m1 by []=>
- ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m3 ∨ K1~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m2; K2~m3 >- m2; m3; K1m1; K1~m1 by or=>
- m2; ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m3 ∨ K1~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1m2; K2~m3 >- m2; m3; K1m1; K1~m1 by Axiom
- ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m3 ∨ K1~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1m2; K2~m3 >- m2; m3; K1m1; K1~m1 by []=>
- ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m2 ∨ K1~m2); (K1m3 ∨ K1~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2; m3; K1m1; K1~m1 by or=>
- ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m2 ∨ K1~m2); (K1m3 ∨ K1~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2; m3; (K1m1 ∨ K1~m1) by =>or
- ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m2 ∨ K1~m2); (K1m3 ∨ K1~m3); ~(K1m1 ∨ K1~m1); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2; m3 by not=>
- ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m2 ∨ K1~m2); (K1m3 ∨ K1~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2; m3 by []=>
- ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))); (K1m2 ∨ K1~m2); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2; m3 by &=>
- ((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2; m3 by &=>
- J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2; m3 by []=>
- ~m3; J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2 by not=>
- J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K2~m3 >- m2 by []=>
- (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m3; K2~m3 >- m3; K2m2; K2~m2 by =>[2]
- m3; (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m3; K2m3 >- m3; K2m2; K2~m2 by Axiom
- (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m3; K2m3 >- m3; K2m2; K2~m2 by []=>
- (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); (K2m3 ∨ K2~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m3 >- m3; K2m2; K2~m2 by or=>
- (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); (K2m3 ∨ K2~m3); ~m3; J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m3 >- m3; K2m2; K2~m2 by not=>
- (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); (K2m3 ∨ K2~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1~m3 >- m3; K2m2; K2~m2 by []=>
- m3; (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); (K2m3 ∨ K2~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1m3 >- m3; K2m2; K2~m2 by Axiom
- (K1m2 ∨ K1~m2); (K2m1 ∨ K2~m1); (K2m3 ∨ K2~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2); K1m3 >- m3; K2m2; K2~m2 by []=>
- (K1m2 ∨ K1~m2); (K1m3 ∨ K1~m3); (K2m1 ∨ K2~m1); (K2m3 ∨ K2~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3; K2m2; K2~m2 by or=>
- ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)); (K1m2 ∨ K1~m2); (K1m3 ∨ K1~m3); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3; K2m2; K2~m2 by &=>
- ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))); (K1m2 ∨ K1~m2); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3; K2m2; K2~m2 by &=>
- ((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3; K2m2; K2~m2 by &=>
- J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3; K2m2; K2~m2 by []=>
- J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3; (K2m2 ∨ K2~m2) by =>or
- ~(K2m2 ∨ K2~m2); J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3 by not=>
- J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- m3 by []=>
- J((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))); J~(~m1 & (~m2 & ~m3)); J~(K1m1 ∨ K1~m1); J~(K2m2 ∨ K2~m2) >- Jm3 by =>[0]
Complexity
Actual Gentzen proof: 40 rules, root sequent size 57, total length 3439
Number of rules and external term size should be O(1600..9409..11826721), the total hilbert proof length should be O(4096000000..1654219191218281803361)
Actual Hilbert proof: 1519 rules, external term size - 760, total length - 572811
Hilbert Proof
-
- 1. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- V3:(~(K2m2 ∨ K2~m2)) Hyp 0
- 2. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- V2:(~(K1m1 ∨ K1~m1)) Hyp 1
- 3. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- V1:(~(~m1 & (~m2 & ~m3))) Hyp 2
- 4. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) Hyp 3
- 5. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))))) Axiom 5
- 6. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- (V1:(~(~m1 & (~m2 & ~m3))) → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 4 and 5
- 7. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) MP on 3 and 6
- 8. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- ((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (V2:(~(K1m1 ∨ K1~m1)) → ((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) Axiom 5
- 9. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- (V2:(~(K1m1 ∨ K1~m1)) → ((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 7 and 8
- 10. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- ((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) MP on 2 and 9
- 11. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- (((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (V3:(~(K2m2 ∨ K2~m2)) → ((C5 ((C5 ((C5 !V0) !V1)) !V2)) !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 5
- 12. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- (V3:(~(K2m2 ∨ K2~m2)) → ((C5 ((C5 ((C5 !V0) !V1)) !V2)) !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 10 and 11
- 13. V3:(~(K2m2 ∨ K2~m2)); V2:(~(K1m1 ∨ K1~m1)); V1:(~(~m1 & (~m2 & ~m3))); V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) |- ((C5 ((C5 ((C5 !V0) !V1)) !V2)) !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 1 and 12
- 14. |- (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (V2:(~(K1m1 ∨ K1~m1)) → (V3:(~(K2m2 ∨ K2~m2)) → ((C5 ((C5 ((C5 !V0) !V1)) !V2)) !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))))) 4 times Deduction
- 15. |- Tt:(((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (V2:(~(K1m1 ∨ K1~m1)) → (V3:(~(K2m2 ∨ K2~m2)) → ((C5 ((C5 ((C5 !V0) !V1)) !V2)) !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))))) → ((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((C5 ((C5 ((C5 !V0) !V1)) !V2)) !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))))) CS for classical tautology or t:A->A
- 16. |- (Tt:(((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (V2:(~(K1m1 ∨ K1~m1)) → (V3:(~(K2m2 ∨ K2~m2)) → ((C5 ((C5 ((C5 !V0) !V1)) !V2)) !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))))) → ((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((C5 ((C5 ((C5 !V0) !V1)) !V2)) !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))))) → ((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (V2:(~(K1m1 ∨ K1~m1)) → (V3:(~(K2m2 ∨ K2~m2)) → ((C5 ((C5 ((C5 !V0) !V1)) !V2)) !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))))) → ((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((C5 ((C5 ((C5 !V0) !V1)) !V2)) !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))))) Axiom 13
- 17. |- ((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (V2:(~(K1m1 ∨ K1~m1)) → (V3:(~(K2m2 ∨ K2~m2)) → ((C5 ((C5 ((C5 !V0) !V1)) !V2)) !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))))) → ((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((C5 ((C5 ((C5 !V0) !V1)) !V2)) !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) MP on 15 and 16
- 18. |- ((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((C5 ((C5 ((C5 !V0) !V1)) !V2)) !V3):((((V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 14 and 17
-
- 20. K2K2~m3 |- K2K2~m3 Hyp 0
- 21. K2K2~m3 |- (K2~m3 → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) Axiom 5
- 22. K2K2~m3 |- K2(K2~m3 → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) Nec
- 23. K2K2~m3 |- (K2(K2~m3 → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → (K2K2~m3 → K2(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) Axiom 17
- 24. K2K2~m3 |- (K2K2~m3 → K2(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) MP on 22 and 23
- 25. K2K2~m3 |- K2(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 20 and 24
- 26. K2K2~m3 |- (K2(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → (K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) Axiom 17
- 27. K2K2~m3 |- (K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 25 and 26
- 28. |- (K2K2~m3 → (K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) 1 times Deduction
- 29. |- Tt:(((K2K2~m3 → (K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) CS for classical tautology or t:A->A
- 30. |- (Tt:(((K2K2~m3 → (K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) → ((K2K2~m3 → (K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) Axiom 13
- 31. |- ((K2K2~m3 → (K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) MP on 29 and 30
- 32. |- ((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 28 and 31
- 33. |- Tt:((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3))))))) CS for classical tautology or t:A->A
- 34. |- (Tt:((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3))))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 13
- 35. |- (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))))) MP on 33 and 34
- 36. |- (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3))))) MP on 32 and 35
- 37. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) Hyp 0
- 38. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (V1:(~(~m1 & (~m2 & ~m3))) → ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) Axiom 5
- 39. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (V1:(~(~m1 & (~m2 & ~m3))) → ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) Nec
- 40. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (V1:(~(~m1 & (~m2 & ~m3))) → ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(V1:(~(~m1 & (~m2 & ~m3))) → ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 17
- 41. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K2(V1:(~(~m1 & (~m2 & ~m3))) → ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 39 and 40
- 42. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- K2(V1:(~(~m1 & (~m2 & ~m3))) → ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 37 and 41
- 43. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K2(V1:(~(~m1 & (~m2 & ~m3))) → ((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → (K2V1:(~(~m1 & (~m2 & ~m3))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) Axiom 17
- 44. K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K2V1:(~(~m1 & (~m2 & ~m3))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 42 and 43
- 45. |- (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K2V1:(~(~m1 & (~m2 & ~m3))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) 1 times Deduction
- 46. |- Tt:(((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K2V1:(~(~m1 & (~m2 & ~m3))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) CS for classical tautology or t:A->A
- 47. |- (Tt:(((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K2V1:(~(~m1 & (~m2 & ~m3))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K2V1:(~(~m1 & (~m2 & ~m3))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 13
- 48. |- ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K2V1:(~(~m1 & (~m2 & ~m3))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 46 and 47
- 49. |- ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 45 and 48
- 50. |- (((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 1
- 51. |- (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 49 and 50
- 52. |- ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → ((K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 2
- 53. |- ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → (K2(K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3))))) → (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 51 and 52
- 54. |- (((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 36 and 53
- 55. |- Tt:(((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1)))))) CS for classical tautology or t:A->A
- 56. |- (Tt:(((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1)))))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1)))))) Axiom 13
- 57. |- ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) → K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))))) MP on 55 and 56
- 58. |- ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1)))) MP on 54 and 57
- 59. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) Hyp 0
- 60. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (V2:(~(K1m1 ∨ K1~m1)) → (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) Axiom 5
- 61. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (V2:(~(K1m1 ∨ K1~m1)) → (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) Nec
- 62. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (V2:(~(K1m1 ∨ K1~m1)) → (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → K2(V2:(~(K1m1 ∨ K1~m1)) → (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 17
- 63. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → K2(V2:(~(K1m1 ∨ K1~m1)) → (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 61 and 62
- 64. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- K2(V2:(~(K1m1 ∨ K1~m1)) → (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 59 and 63
- 65. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K2(V2:(~(K1m1 ∨ K1~m1)) → (((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → (K2V2:(~(K1m1 ∨ K1~m1)) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) Axiom 17
- 66. K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K2V2:(~(K1m1 ∨ K1~m1)) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 64 and 65
- 67. |- (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K2V2:(~(K1m1 ∨ K1~m1)) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) 1 times Deduction
- 68. |- Tt:(((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K2V2:(~(K1m1 ∨ K1~m1)) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) CS for classical tautology or t:A->A
- 69. |- (Tt:(((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K2V2:(~(K1m1 ∨ K1~m1)) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K2V2:(~(K1m1 ∨ K1~m1)) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 13
- 70. |- ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K2V2:(~(K1m1 ∨ K1~m1)) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 68 and 69
- 71. |- ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 67 and 70
- 72. |- (((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 1
- 73. |- ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 71 and 72
- 74. |- (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → ((K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1)))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 2
- 75. |- (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → (K2((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1)))) → ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 73 and 74
- 76. |- ((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 58 and 75
- 77. |- Tt:((((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2)))))) CS for classical tautology or t:A->A
- 78. |- (Tt:((((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2)))))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2)))))) Axiom 13
- 79. |- (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) → K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))))) MP on 77 and 78
- 80. |- (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2)))) MP on 76 and 79
- 81. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) Hyp 0
- 82. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (V3:(~(K2m2 ∨ K2~m2)) → ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) Axiom 5
- 83. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (V3:(~(K2m2 ∨ K2~m2)) → ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) Nec
- 84. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (V3:(~(K2m2 ∨ K2~m2)) → ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → K2(V3:(~(K2m2 ∨ K2~m2)) → ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 17
- 85. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → K2(V3:(~(K2m2 ∨ K2~m2)) → ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 83 and 84
- 86. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- K2(V3:(~(K2m2 ∨ K2~m2)) → ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 81 and 85
- 87. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K2(V3:(~(K2m2 ∨ K2~m2)) → ((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) → (K2V3:(~(K2m2 ∨ K2~m2)) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) Axiom 17
- 88. K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K2V3:(~(K2m2 ∨ K2~m2)) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 86 and 87
- 89. |- (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K2V3:(~(K2m2 ∨ K2~m2)) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) 1 times Deduction
- 90. |- Tt:(((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K2V3:(~(K2m2 ∨ K2~m2)) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) CS for classical tautology or t:A->A
- 91. |- (Tt:(((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K2V3:(~(K2m2 ∨ K2~m2)) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K2V3:(~(K2m2 ∨ K2~m2)) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 13
- 92. |- ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K2V3:(~(K2m2 ∨ K2~m2)) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 90 and 91
- 93. |- ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 89 and 92
- 94. |- (((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 1
- 95. |- (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 93 and 94
- 96. |- ((((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → ((K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2)))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 2
- 97. |- ((((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → (K2(((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2)))) → (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 95 and 96
- 98. |- (((((K2K2~m3 & K2V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K2V1:(~(~m1 & (~m2 & ~m3)))) & K2V2:(~(K1m1 ∨ K1~m1))) & K2V3:(~(K2m2 ∨ K2~m2))) → K2((((K2~m3 & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 80 and 97
-
- 100. K1K1~m2 |- K1K1~m2 Hyp 0
- 101. K1K1~m2 |- (K1~m2 → (K1~m3 → (K1~m2 & K1~m3))) Axiom 5
- 102. K1K1~m2 |- K1(K1~m2 → (K1~m3 → (K1~m2 & K1~m3))) Nec
- 103. K1K1~m2 |- (K1(K1~m2 → (K1~m3 → (K1~m2 & K1~m3))) → (K1K1~m2 → K1(K1~m3 → (K1~m2 & K1~m3)))) Axiom 17
- 104. K1K1~m2 |- (K1K1~m2 → K1(K1~m3 → (K1~m2 & K1~m3))) MP on 102 and 103
- 105. K1K1~m2 |- K1(K1~m3 → (K1~m2 & K1~m3)) MP on 100 and 104
- 106. K1K1~m2 |- (K1(K1~m3 → (K1~m2 & K1~m3)) → (K1K1~m3 → K1(K1~m2 & K1~m3))) Axiom 17
- 107. K1K1~m2 |- (K1K1~m3 → K1(K1~m2 & K1~m3)) MP on 105 and 106
- 108. |- (K1K1~m2 → (K1K1~m3 → K1(K1~m2 & K1~m3))) 1 times Deduction
- 109. |- Tt:(((K1K1~m2 → (K1K1~m3 → K1(K1~m2 & K1~m3))) → ((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)))) CS for classical tautology or t:A->A
- 110. |- (Tt:(((K1K1~m2 → (K1K1~m3 → K1(K1~m2 & K1~m3))) → ((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)))) → ((K1K1~m2 → (K1K1~m3 → K1(K1~m2 & K1~m3))) → ((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)))) Axiom 13
- 111. |- ((K1K1~m2 → (K1K1~m3 → K1(K1~m2 & K1~m3))) → ((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3))) MP on 109 and 110
- 112. |- ((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)) MP on 108 and 111
- 113. |- Tt:((((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)) → (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) CS for classical tautology or t:A->A
- 114. |- (Tt:((((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)) → (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) → (((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)) → (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) Axiom 13
- 115. |- (((K1K1~m2 & K1K1~m3) → K1(K1~m2 & K1~m3)) → (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) MP on 113 and 114
- 116. |- (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 112 and 115
- 117. K1(K1~m2 & K1~m3) |- K1(K1~m2 & K1~m3) Hyp 0
- 118. K1(K1~m2 & K1~m3) |- ((K1~m2 & K1~m3) → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → ((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) Axiom 5
- 119. K1(K1~m2 & K1~m3) |- K1((K1~m2 & K1~m3) → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → ((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) Nec
- 120. K1(K1~m2 & K1~m3) |- (K1((K1~m2 & K1~m3) → (V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → ((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → (K1(K1~m2 & K1~m3) → K1(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → ((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) Axiom 17
- 121. K1(K1~m2 & K1~m3) |- (K1(K1~m2 & K1~m3) → K1(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → ((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) MP on 119 and 120
- 122. K1(K1~m2 & K1~m3) |- K1(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → ((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 117 and 121
- 123. K1(K1~m2 & K1~m3) |- (K1(V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → ((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) Axiom 17
- 124. K1(K1~m2 & K1~m3) |- (K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 122 and 123
- 125. |- (K1(K1~m2 & K1~m3) → (K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) 1 times Deduction
- 126. |- Tt:(((K1(K1~m2 & K1~m3) → (K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) CS for classical tautology or t:A->A
- 127. |- (Tt:(((K1(K1~m2 & K1~m3) → (K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) → ((K1(K1~m2 & K1~m3) → (K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) Axiom 13
- 128. |- ((K1(K1~m2 & K1~m3) → (K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) MP on 126 and 127
- 129. |- ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 125 and 128
- 130. |- (((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) Axiom 1
- 131. |- (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) MP on 129 and 130
- 132. |- ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → ((K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))))) Axiom 2
- 133. |- ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1(K1~m2 & K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))))) MP on 131 and 132
- 134. |- (((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) MP on 116 and 133
- 135. |- Tt:(((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3))))))) CS for classical tautology or t:A->A
- 136. |- (Tt:(((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3))))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 13
- 137. |- ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3))))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))))) MP on 135 and 136
- 138. |- ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3))))) MP on 134 and 137
- 139. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) Hyp 0
- 140. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) Axiom 5
- 141. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) Nec
- 142. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (V1:(~(~m1 & (~m2 & ~m3))) → (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1(V1:(~(~m1 & (~m2 & ~m3))) → (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 17
- 143. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → K1(V1:(~(~m1 & (~m2 & ~m3))) → (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 141 and 142
- 144. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- K1(V1:(~(~m1 & (~m2 & ~m3))) → (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 139 and 143
- 145. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K1(V1:(~(~m1 & (~m2 & ~m3))) → (((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → (K1V1:(~(~m1 & (~m2 & ~m3))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) Axiom 17
- 146. K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) |- (K1V1:(~(~m1 & (~m2 & ~m3))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 144 and 145
- 147. |- (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1V1:(~(~m1 & (~m2 & ~m3))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) 1 times Deduction
- 148. |- Tt:(((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1V1:(~(~m1 & (~m2 & ~m3))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) CS for classical tautology or t:A->A
- 149. |- (Tt:(((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1V1:(~(~m1 & (~m2 & ~m3))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1V1:(~(~m1 & (~m2 & ~m3))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 13
- 150. |- ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) → (K1V1:(~(~m1 & (~m2 & ~m3))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 148 and 149
- 151. |- ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 147 and 150
- 152. |- (((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 1
- 153. |- ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 151 and 152
- 154. |- (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → ((K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))))) Axiom 2
- 155. |- (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → (K1((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3))))) → ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))))) MP on 153 and 154
- 156. |- ((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) MP on 138 and 155
- 157. |- Tt:((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1)))))) CS for classical tautology or t:A->A
- 158. |- (Tt:((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1)))))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1)))))) Axiom 13
- 159. |- (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) → K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3))))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))))) MP on 157 and 158
- 160. |- (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1)))) MP on 156 and 159
- 161. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) Hyp 0
- 162. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (V2:(~(K1m1 ∨ K1~m1)) → ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) Axiom 5
- 163. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (V2:(~(K1m1 ∨ K1~m1)) → ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) Nec
- 164. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (V2:(~(K1m1 ∨ K1~m1)) → ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → K1(V2:(~(K1m1 ∨ K1~m1)) → ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 17
- 165. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → K1(V2:(~(K1m1 ∨ K1~m1)) → ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 163 and 164
- 166. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- K1(V2:(~(K1m1 ∨ K1~m1)) → ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 161 and 165
- 167. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K1(V2:(~(K1m1 ∨ K1~m1)) → ((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → (K1V2:(~(K1m1 ∨ K1~m1)) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) Axiom 17
- 168. K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) |- (K1V2:(~(K1m1 ∨ K1~m1)) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 166 and 167
- 169. |- (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K1V2:(~(K1m1 ∨ K1~m1)) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) 1 times Deduction
- 170. |- Tt:(((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K1V2:(~(K1m1 ∨ K1~m1)) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) CS for classical tautology or t:A->A
- 171. |- (Tt:(((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K1V2:(~(K1m1 ∨ K1~m1)) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K1V2:(~(K1m1 ∨ K1~m1)) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 13
- 172. |- ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) → (K1V2:(~(K1m1 ∨ K1~m1)) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 170 and 171
- 173. |- ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 169 and 172
- 174. |- (((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 1
- 175. |- (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 173 and 174
- 176. |- ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → ((K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1)))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))))) Axiom 2
- 177. |- ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → (K1(((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1)))) → (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))))) MP on 175 and 176
- 178. |- (((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) MP on 160 and 177
- 179. |- Tt:(((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2)))))) CS for classical tautology or t:A->A
- 180. |- (Tt:(((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2)))))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2)))))) Axiom 13
- 181. |- ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) → K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1)))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))))) MP on 179 and 180
- 182. |- ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2)))) MP on 178 and 181
- 183. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) Hyp 0
- 184. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (V3:(~(K2m2 ∨ K2~m2)) → (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) Axiom 5
- 185. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (V3:(~(K2m2 ∨ K2~m2)) → (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) Nec
- 186. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (V3:(~(K2m2 ∨ K2~m2)) → (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → K1(V3:(~(K2m2 ∨ K2~m2)) → (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 17
- 187. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → K1(V3:(~(K2m2 ∨ K2~m2)) → (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 185 and 186
- 188. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- K1(V3:(~(K2m2 ∨ K2~m2)) → (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 183 and 187
- 189. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K1(V3:(~(K2m2 ∨ K2~m2)) → (((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) → (K1V3:(~(K2m2 ∨ K2~m2)) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) Axiom 17
- 190. K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) |- (K1V3:(~(K2m2 ∨ K2~m2)) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 188 and 189
- 191. |- (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K1V3:(~(K2m2 ∨ K2~m2)) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) 1 times Deduction
- 192. |- Tt:(((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K1V3:(~(K2m2 ∨ K2~m2)) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) CS for classical tautology or t:A->A
- 193. |- (Tt:(((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K1V3:(~(K2m2 ∨ K2~m2)) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K1V3:(~(K2m2 ∨ K2~m2)) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 13
- 194. |- ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) → (K1V3:(~(K2m2 ∨ K2~m2)) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 192 and 193
- 195. |- ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 191 and 194
- 196. |- (((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 1
- 197. |- ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 195 and 196
- 198. |- (((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → ((K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) → (((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2)))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))))) Axiom 2
- 199. |- (((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → (K1((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2)))) → ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))))) MP on 197 and 198
- 200. |- ((((((K1K1~m2 & K1K1~m3) & K1V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & K1V1:(~(~m1 & (~m2 & ~m3)))) & K1V2:(~(K1m1 ∨ K1~m1))) & K1V3:(~(K2m2 ∨ K2~m2))) → K1(((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2)))) MP on 182 and 199
-
- 202. |- Tt:((((((((m3 & K1~m2) & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((m1 ∨ m2) ∨ m3))) CS for classical tautology or t:A->A
-
- 204. |- Tt:(((((((((m3 & K1~m2) & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → ((m1 ∨ m2) ∨ m3)) → ((((((K1~m2 & K1~m3) & V0:(((K1m2 ∨ K1~m2) & ((K1m3 ∨ K1~m3) & ((K2m1 ∨ K2~m1) & (K2m3 ∨ K2~m3)))))) & V1:(~(~m1 & (~m2 & ~m3)))) & V2:(~(K1m1 ∨ K1~m1))) & V3:(~(K2m2 ∨ K2~m2))) → (((m1 ∨ m2) ∨ m3) ∨ ~m3)))) CS for classical tautology or t:A->A
- 205. |- (Tt:(((((((((m3 & K1~m2) & K1~m3) & V0:(((K1m2