============================== prooftrans (BV) ======================= Prover9 (64) version Aug-2007, Aug 2007. Process 32327 was started by veroff on io, Mon Jan 21 11:14:29 2008 The command was "prover9 -f 3.1.in". ============================== end of head =========================== op(400,infix,[^,v,"->","=>",*]). op(200,prefix,[~,-]). ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 0.10 (+ 0.02) seconds: "(Lemma 3.1, 5 parts)". % Length of proof is 71. % Level of proof is 13. % Maximum clause weight is 39. % Given clauses 87. 1 (x v y) v z = x v (y v z) # label("(D1)"). [assumption]. 2 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. 3 x v y = y v x # label("(D3)"). [assumption]. 4 x ^ y = y ^ x # label("(D4)"). [assumption]. 5 x v (x ^ y) = x # label("(D5)"). [assumption]. 6 x ^ (x v y) = x # label("(D6)"). [assumption]. 10 x ^ 1 = x # label("(D10)"). [assumption]. 12 ~ x v ~ y = ~ (x ^ y) # label("(DM1)"). [assumption]. 14 ~ ~ x = x # label("(DN)"). [assumption]. 17 x -> x = 1 # label("(N2)"). [assumption]. 19 x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). [assumption]. 20 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. 21 (x ^ y) -> z = x -> (y -> z) # label("(N6)"). [assumption]. 26 x => y = (x -> y) ^ (~ y -> ~ x) # label("(=> def)"). [assumption]. 27 (x -> y) ^ (~ y -> ~ x) = x => y. [copy(26),flip(a)]. 28 x -> 1 = 1 # label("(3.1)"). [assumption]. 29 1 -> x = x # label("(3.2)"). [assumption]. 32 x -> (x -> y) = x -> y # label("(3.5)"). [assumption]. 33 (x -> y) ^ (z -> y) = (x v z) -> y # label("(3.6)"). [assumption]. 40 (A ^ B) -> B != 1 | (A ^ B) => B != 1 | ~ A => ~ B != B => A | (A => B) ^ B != B | A => (A ^ B) != A => B # answer("(Lemma 3.1, 5 parts)"). [assumption]. 60 x v (y ^ x) = x. [para(4(a,1),5(a,1,2))]. 65 x ^ (y v x) = x. [para(3(a,1),6(a,1,2))]. 113 1 ^ x = x. [para(10(a,1),4(a,1)),flip(a)]. 204 x ^ (y v ~ x) = x ^ (x -> y). [para(3(a,1),19(a,1,2))]. 229 (x -> y) ^ (x -> 1) = x -> y. [para(10(a,1),20(a,2,2))]. 234 1 ^ (x -> y) = x -> (x ^ y). [para(17(a,1),20(a,1,1))]. 288 (x -> y) ^ ((~ y -> ~ x) ^ z) = (x => y) ^ z. [para(27(a,1),2(a,1,1)),flip(a)]. 290 (~ x -> ~ y) ^ (y -> x) = y => x. [para(27(a,1),4(a,1)),flip(a)]. 296 (x -> ~ y) ^ (y -> ~ x) = x => ~ y. [para(14(a,1),27(a,1,2,1))]. 407 1 ^ (x -> y) = (y v x) -> y. [para(17(a,1),33(a,1,1))]. 424 x ^ (y -> x) = (1 v y) -> x. [para(29(a,1),33(a,1,1))]. 534 1 v x = 1. [para(113(a,1),5(a,1,2))]. 580 x ^ (y v (z v x)) = x. [para(1(a,1),65(a,1,2))]. 602 x ^ (y v (x v z)) = x. [para(3(a,1),580(a,1,2,2))]. 725 x -> (x ^ y) = x -> y. [para(234(a,1),113(a,1))]. 736 x -> (x v y) = x -> x. [para(6(a,1),725(a,1,2)),flip(a)]. 752 (x -> y) ^ (~ (x ^ y) -> ~ x) = x => (x ^ y). [para(725(a,1),27(a,1,1))]. 765 x -> (x ^ (x -> y)) = x -> y. [para(32(a,1),725(a,2))]. 789 x -> (x v y) = 1. [para(17(a,1),736(a,2))]. 822 x -> (y v x) = 1. [para(3(a,1),789(a,1,2))]. 824 ~ x -> ~ (x ^ y) = 1. [para(12(a,1),789(a,1,2))]. 874 (x ^ y) -> y = 1 # label("(3.10)"). [para(60(a,1),822(a,1,2))]. 931 ((x ^ y) -> x) ^ 1 = (x ^ y) => x. [para(824(a,1),27(a,1,2))]. 1006 (x v y) -> x = y -> x. [para(407(a,1),113(a,1))]. 1030 ~ (x ^ y) -> ~ x = ~ y -> ~ x. [para(12(a,1),1006(a,1,1))]. 1135 x ^ (y -> x) = 1 -> x. [para(534(a,1),424(a,2,1))]. 1179 x ^ (y -> x) = x. [para(29(a,1),1135(a,2))]. 1205 (x -> y) ^ y = y. [para(1179(a,1),4(a,1)),flip(a)]. 1215 (x -> y) v y = x -> y. [para(1179(a,1),60(a,1,2))]. 1220 x -> (y -> x) = 1. [para(1179(a,1),874(a,1,1))]. 1267 (x -> (y -> x)) ^ (x -> 1) = 1. [para(1220(a,1),229(a,2))]. 1309 x ^ (y -> (x v z)) = x. [para(1215(a,1),602(a,1,2))]. 1446 (x -> (y -> x)) ^ 1 = 1. [para(28(a,1),1267(a,1,2))]. 1525 x -> (x ^ (x -> y)) = x -> (y v ~ x). [para(204(a,1),725(a,1,2))]. 1548 (x -> ~ y) ^ (y -> ~ x) = y => ~ x. [para(14(a,1),290(a,1,1,1))]. 1620 (x -> (y -> x)) ^ 1 = (x ^ y) => x. [para(21(a,1),931(a,1,1))]. 1808 (x ^ y) => x = 1. [para(1620(a,1),1446(a,1))]. 1819 (x ^ y) => y = 1 # label("(3.11)"). [para(4(a,1),1808(a,1,1))]. 1985 x -> (y v ~ x) = x -> y. [para(1525(a,1),765(a,1))]. 1995 x -> (~ x v y) = x -> y. [para(3(a,1),1985(a,1,2))]. 2122 ~ x ^ (x -> y) = ~ x. [para(1995(a,1),1309(a,1,2))]. 2143 x ^ (~ x -> y) = ~ ~ x. [para(14(a,1),2122(a,1,1))]. 2180 x ^ (~ x -> y) = x. [para(14(a,1),2143(a,2))]. 2207 (~ x -> y) ^ x = x. [para(2180(a,1),4(a,1)),flip(a)]. 2295 x => ~ y = y => ~ x. [para(1548(a,1),296(a,1))]. 2296 ~ x => ~ y = y => x # label("(3.12)"). [para(14(a,1),2295(a,1,2)),flip(a)]. 2417 (x -> y) ^ y = (x => y) ^ y. [para(2207(a,1),288(a,1,2))]. 2462 (x => y) ^ y = y # label("(3.13)"). [para(2417(a,1),1205(a,1))]. 2601 (x -> y) ^ (~ y -> ~ x) = x => (x ^ y). [para(1030(a,1),752(a,1,2))]. 2655 x => (x ^ y) = x => y # label("(3.14)"). [para(2601(a,1),27(a,1))]. 2724 $F # answer("(Lemma 3.1, 5 parts)"). [hyper(40,a,874,a,b,1819,a,c,2296,a,d,2462,a,e,2655,a)]. ============================== end of proof ==========================