============================== prooftrans (BV) ======================= Prover9 (64) version Aug-2007, Aug 2007. Process 26230 was started by veroff on titan, Sat Jan 19 14:18:43 2008 The command was "prover9 -f 4.3.in". ============================== end of head =========================== op(400,infix,[^,v,"->","=>",*]). op(200,prefix,[~,-]). ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 0.04 (+ 0.00) seconds: "(Lemma 4.3, 4 parts)". % Length of proof is 32. % Level of proof is 10. % Maximum clause weight is 35. % Given clauses 53. 3 x v y = y v x # label("(D3)"). [assumption]. 4 x ^ y = y ^ x # label("(D4)"). [assumption]. 8 1 => x = x # label("(BCK2)"). [assumption]. 15 x ^ 1 = x # label("(D10)"). [assumption]. 16 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 19 x -> y = x => (x => y) # label("(-> def)"). [assumption]. 20 x => (x => y) = x -> y. [copy(19),flip(a)]. 21 ~ x = x => 0 # label("(~ def)"). [assumption]. 22 x => 0 = ~ x. [copy(21),flip(a)]. 28 ~ ~ x = x # label("(DN)"). [assumption]. 32 x => x = 1 # label("(3.16)"). [assumption]. 33 x => (y => x) = 1 # label("(3.17)"). [assumption]. 34 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 38 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. 40 (A => B) ^ B != B | (A v B) => B != A => B | A -> (B => C) != B => (A -> C) | A ^ (~ A => B) != A # answer("(Lemma 4.3, 4 parts)"). [assumption]. 104 1 ^ x = x. [para(15(a,1),4(a,1)),flip(a)]. 242 ~ x => 0 = x. [para(28(a,1),22(a,2))]. 364 x => (y => (x => z)) = y => (x -> z). [para(20(a,1),34(a,1,2)),flip(a)]. 365 x => (y => 0) = y => ~ x. [para(22(a,1),34(a,1,2)),flip(a)]. 520 (x v y) => x = 1 ^ (y => x). [para(32(a,1),38(a,1,1)),flip(a)]. 641 ~ x => ~ y = y => x. [para(242(a,1),365(a,1,2)),flip(a)]. 659 ~ x => y = ~ y => x. [para(28(a,1),641(a,1,2))]. 706 x => (~ x => y) = 1. [para(659(a,1),33(a,1,2))]. 729 x ^ (1 => (~ x => y)) = x. [para(706(a,1),16(a,1,2,1))]. 756 x ^ (~ x => y) = x # label("(4.8)"). [para(8(a,1),729(a,1,2))]. 783 x ^ (y => x) = x. [para(641(a,1),756(a,1,2))]. 787 (x => y) ^ y = y # label("(3.13)"). [para(783(a,1),4(a,1)),flip(a)]. 873 (x v y) => x = y => x. [para(520(a,2),104(a,1))]. 888 (x v y) => y = x => y # label("(4.6)"). [para(3(a,1),873(a,1,1))]. 1050 x => (x => (y => z)) = y => (x -> z). [para(34(a,1),364(a,1,2))]. 1109 x -> (y => z) = y => (x -> z) # label("(4.7)"). [para(1050(a,1),20(a,1)),flip(a)]. 1168 $F # answer("(Lemma 4.3, 4 parts)"). [hyper(40,a,787,a,b,888,a,c,1109,a,d,756,a)]. ============================== end of proof ==========================