:: PROCAL_1 semantic presentation begin theorem Th1: :: PROCAL_1:1 for A being QC-alphabet for p being Element of CQC-WFF A holds 'not' (p '&' ('not' p)) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds 'not' (p '&' ('not' p)) in TAUT A let p be Element of CQC-WFF A; ::_thesis: 'not' (p '&' ('not' p)) in TAUT A p => p in TAUT A by LUKASI_1:4; hence 'not' (p '&' ('not' p)) in TAUT A by QC_LANG2:def_2; ::_thesis: verum end; Lm1: for A being QC-alphabet for p, q being Element of CQC-WFF A holds p 'or' q = ('not' p) => q proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds p 'or' q = ('not' p) => q let p, q be Element of CQC-WFF A; ::_thesis: p 'or' q = ('not' p) => q ('not' p) => q = 'not' (('not' p) '&' ('not' q)) by QC_LANG2:def_2; hence p 'or' q = ('not' p) => q by QC_LANG2:def_3; ::_thesis: verum end; theorem Th2: :: PROCAL_1:2 for A being QC-alphabet for p being Element of CQC-WFF A holds p 'or' ('not' p) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds p 'or' ('not' p) in TAUT A let p be Element of CQC-WFF A; ::_thesis: p 'or' ('not' p) in TAUT A ('not' p) => ('not' p) in TAUT A by LUKASI_1:4; hence p 'or' ('not' p) in TAUT A by Lm1; ::_thesis: verum end; theorem Th3: :: PROCAL_1:3 for A being QC-alphabet for p, q being Element of CQC-WFF A holds p => (p 'or' q) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds p => (p 'or' q) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: p => (p 'or' q) in TAUT A p => (('not' p) => q) in TAUT A by CQC_THE1:43; hence p => (p 'or' q) in TAUT A by Lm1; ::_thesis: verum end; theorem Th4: :: PROCAL_1:4 for A being QC-alphabet for q, p being Element of CQC-WFF A holds q => (p 'or' q) in TAUT A proof let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A holds q => (p 'or' q) in TAUT A let q, p be Element of CQC-WFF A; ::_thesis: q => (p 'or' q) in TAUT A q => (('not' p) => q) in TAUT A by LUKASI_1:5; hence q => (p 'or' q) in TAUT A by Lm1; ::_thesis: verum end; theorem Th5: :: PROCAL_1:5 for A being QC-alphabet for p, q being Element of CQC-WFF A holds (p 'or' q) => (('not' p) => q) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p 'or' q) => (('not' p) => q) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (p 'or' q) => (('not' p) => q) in TAUT A (('not' p) => q) => (('not' p) => q) in TAUT A by LUKASI_1:4; hence (p 'or' q) => (('not' p) => q) in TAUT A by Lm1; ::_thesis: verum end; theorem Th6: :: PROCAL_1:6 for A being QC-alphabet for p, q being Element of CQC-WFF A holds ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) in TAUT A 'not' (p 'or' q) = 'not' ('not' (('not' p) '&' ('not' q))) by QC_LANG2:def_3; hence ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) in TAUT A by LUKASI_1:25; ::_thesis: verum end; theorem Th7: :: PROCAL_1:7 for A being QC-alphabet for p, q being Element of CQC-WFF A holds (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) in TAUT A 'not' (p 'or' q) = 'not' ('not' (('not' p) '&' ('not' q))) by QC_LANG2:def_3; hence (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) in TAUT A by LUKASI_1:27; ::_thesis: verum end; theorem Th8: :: PROCAL_1:8 for A being QC-alphabet for p, q being Element of CQC-WFF A holds (p 'or' q) => (q 'or' p) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p 'or' q) => (q 'or' p) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (p 'or' q) => (q 'or' p) in TAUT A (('not' p) => q) => (('not' q) => p) in TAUT A by LUKASI_1:31; then (p 'or' q) => (('not' q) => p) in TAUT A by Lm1; hence (p 'or' q) => (q 'or' p) in TAUT A by Lm1; ::_thesis: verum end; theorem :: PROCAL_1:9 for A being QC-alphabet for p being Element of CQC-WFF A holds ('not' p) 'or' p in TAUT A proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds ('not' p) 'or' p in TAUT A let p be Element of CQC-WFF A; ::_thesis: ('not' p) 'or' p in TAUT A (p 'or' ('not' p)) => (('not' p) 'or' p) in TAUT A by Th8; hence ('not' p) 'or' p in TAUT A by Th2, CQC_THE1:46; ::_thesis: verum end; theorem :: PROCAL_1:10 for A being QC-alphabet for p, q being Element of CQC-WFF A holds ('not' (p 'or' q)) => ('not' p) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ('not' (p 'or' q)) => ('not' p) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: ('not' (p 'or' q)) => ('not' p) in TAUT A ( (p => (p 'or' q)) => (('not' (p 'or' q)) => ('not' p)) in TAUT A & p => (p 'or' q) in TAUT A ) by Th3, LUKASI_1:26; hence ('not' (p 'or' q)) => ('not' p) in TAUT A by CQC_THE1:46; ::_thesis: verum end; theorem Th11: :: PROCAL_1:11 for A being QC-alphabet for p being Element of CQC-WFF A holds (p 'or' p) => p in TAUT A proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds (p 'or' p) => p in TAUT A let p be Element of CQC-WFF A; ::_thesis: (p 'or' p) => p in TAUT A ( (p 'or' p) => (('not' p) => p) in TAUT A & (('not' p) => p) => p in TAUT A ) by Th5, CQC_THE1:42; hence (p 'or' p) => p in TAUT A by LUKASI_1:3; ::_thesis: verum end; theorem :: PROCAL_1:12 for A being QC-alphabet for p being Element of CQC-WFF A holds p => (p 'or' p) in TAUT A by Th3; theorem :: PROCAL_1:13 for A being QC-alphabet for p, q being Element of CQC-WFF A holds (p '&' ('not' p)) => q in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p '&' ('not' p)) => q in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (p '&' ('not' p)) => q in TAUT A ('not' q) => ('not' (p '&' ('not' p))) in TAUT A by Th1, LUKASI_1:13; hence (p '&' ('not' p)) => q in TAUT A by LUKASI_1:35; ::_thesis: verum end; theorem :: PROCAL_1:14 for A being QC-alphabet for p, q being Element of CQC-WFF A holds (p => q) => (('not' p) 'or' q) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p => q) => (('not' p) 'or' q) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (p => q) => (('not' p) 'or' q) in TAUT A A1: (('not' ('not' p)) => p) => ((p => q) => (('not' ('not' p)) => q)) in TAUT A by LUKASI_1:1; ( ('not' ('not' p)) => q = ('not' p) 'or' q & ('not' ('not' p)) => p in TAUT A ) by Lm1, LUKASI_1:25; hence (p => q) => (('not' p) 'or' q) in TAUT A by A1, CQC_THE1:46; ::_thesis: verum end; Lm2: for A being QC-alphabet for p, q being Element of CQC-WFF A holds (p '&' q) => (('not' ('not' p)) '&' q) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p '&' q) => (('not' ('not' p)) '&' q) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (p '&' q) => (('not' ('not' p)) '&' q) in TAUT A ( (p => ('not' ('not' p))) => (('not' (('not' ('not' p)) '&' q)) => ('not' (p '&' q))) in TAUT A & p => ('not' ('not' p)) in TAUT A ) by CQC_THE1:44, LUKASI_1:27; then ('not' (('not' ('not' p)) '&' q)) => ('not' (p '&' q)) in TAUT A by CQC_THE1:46; hence (p '&' q) => (('not' ('not' p)) '&' q) in TAUT A by LUKASI_1:35; ::_thesis: verum end; Lm3: for A being QC-alphabet for p, q being Element of CQC-WFF A holds (('not' ('not' p)) '&' q) => (p '&' q) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (('not' ('not' p)) '&' q) => (p '&' q) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (('not' ('not' p)) '&' q) => (p '&' q) in TAUT A ( (('not' ('not' p)) => p) => (('not' (p '&' q)) => ('not' (('not' ('not' p)) '&' q))) in TAUT A & ('not' ('not' p)) => p in TAUT A ) by CQC_THE1:44, LUKASI_1:25; then ('not' (p '&' q)) => ('not' (('not' ('not' p)) '&' q)) in TAUT A by CQC_THE1:46; hence (('not' ('not' p)) '&' q) => (p '&' q) in TAUT A by LUKASI_1:35; ::_thesis: verum end; theorem Th15: :: PROCAL_1:15 for A being QC-alphabet for p, q being Element of CQC-WFF A holds (p '&' q) => ('not' (p => ('not' q))) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p '&' q) => ('not' (p => ('not' q))) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (p '&' q) => ('not' (p => ('not' q))) in TAUT A A1: (p '&' ('not' ('not' q))) => ('not' ('not' (p '&' ('not' ('not' q))))) in TAUT A by LUKASI_1:27; ( (q '&' p) => (('not' ('not' q)) '&' p) in TAUT A & (p '&' q) => (q '&' p) in TAUT A ) by Lm2, CQC_THE1:45; then A2: (p '&' q) => (('not' ('not' q)) '&' p) in TAUT A by LUKASI_1:3; (('not' ('not' q)) '&' p) => (p '&' ('not' ('not' q))) in TAUT A by CQC_THE1:45; then (p '&' q) => (p '&' ('not' ('not' q))) in TAUT A by A2, LUKASI_1:3; then (p '&' q) => ('not' ('not' (p '&' ('not' ('not' q))))) in TAUT A by A1, LUKASI_1:3; hence (p '&' q) => ('not' (p => ('not' q))) in TAUT A by QC_LANG2:def_2; ::_thesis: verum end; theorem Th16: :: PROCAL_1:16 for A being QC-alphabet for p, q being Element of CQC-WFF A holds ('not' (p => ('not' q))) => (p '&' q) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ('not' (p => ('not' q))) => (p '&' q) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: ('not' (p => ('not' q))) => (p '&' q) in TAUT A A1: ('not' ('not' (p '&' ('not' ('not' q))))) => (p '&' ('not' ('not' q))) in TAUT A by LUKASI_1:25; ( (p '&' ('not' ('not' q))) => (('not' ('not' q)) '&' p) in TAUT A & (('not' ('not' q)) '&' p) => (q '&' p) in TAUT A ) by Lm3, CQC_THE1:45; then A2: (p '&' ('not' ('not' q))) => (q '&' p) in TAUT A by LUKASI_1:3; (q '&' p) => (p '&' q) in TAUT A by CQC_THE1:45; then (p '&' ('not' ('not' q))) => (p '&' q) in TAUT A by A2, LUKASI_1:3; then ('not' ('not' (p '&' ('not' ('not' q))))) => (p '&' q) in TAUT A by A1, LUKASI_1:3; hence ('not' (p => ('not' q))) => (p '&' q) in TAUT A by QC_LANG2:def_2; ::_thesis: verum end; theorem Th17: :: PROCAL_1:17 for A being QC-alphabet for p, q being Element of CQC-WFF A holds ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) in TAUT A ( ('not' ('not' p)) => p in TAUT A & (('not' ('not' p)) => p) => ((p => ('not' q)) => (('not' ('not' p)) => ('not' q))) in TAUT A ) by LUKASI_1:1, LUKASI_1:25; then A1: (p => ('not' q)) => (('not' ('not' p)) => ('not' q)) in TAUT A by CQC_THE1:46; ('not' (p => ('not' q))) => (p '&' q) in TAUT A by Th16; then A2: ('not' (p '&' q)) => ('not' ('not' (p => ('not' q)))) in TAUT A by LUKASI_1:34; ('not' ('not' (p => ('not' q)))) => (p => ('not' q)) in TAUT A by LUKASI_1:25; then ('not' (p '&' q)) => (p => ('not' q)) in TAUT A by A2, LUKASI_1:3; then ('not' (p '&' q)) => (('not' ('not' p)) => ('not' q)) in TAUT A by A1, LUKASI_1:3; hence ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) in TAUT A by Lm1; ::_thesis: verum end; theorem Th18: :: PROCAL_1:18 for A being QC-alphabet for p, q being Element of CQC-WFF A holds (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) in TAUT A A1: (p => ('not' ('not' p))) => ((('not' ('not' p)) => ('not' q)) => (p => ('not' q))) in TAUT A by LUKASI_1:1; (p '&' q) => ('not' (p => ('not' q))) in TAUT A by Th15; then A2: ('not' ('not' (p => ('not' q)))) => ('not' (p '&' q)) in TAUT A by LUKASI_1:34; (p => ('not' q)) => ('not' ('not' (p => ('not' q)))) in TAUT A by LUKASI_1:27; then A3: (p => ('not' q)) => ('not' (p '&' q)) in TAUT A by A2, LUKASI_1:3; ( ('not' p) 'or' ('not' q) = ('not' ('not' p)) => ('not' q) & p => ('not' ('not' p)) in TAUT A ) by Lm1, LUKASI_1:27; then (('not' p) 'or' ('not' q)) => (p => ('not' q)) in TAUT A by A1, CQC_THE1:46; hence (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) in TAUT A by A3, LUKASI_1:3; ::_thesis: verum end; theorem Th19: :: PROCAL_1:19 for A being QC-alphabet for p, q being Element of CQC-WFF A holds (p '&' q) => p in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p '&' q) => p in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (p '&' q) => p in TAUT A ('not' p) => (('not' p) 'or' ('not' q)) in TAUT A by Th3; then A1: ('not' (('not' p) 'or' ('not' q))) => ('not' ('not' p)) in TAUT A by LUKASI_1:34; (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) in TAUT A by Th18; then A2: ('not' ('not' (p '&' q))) => ('not' (('not' p) 'or' ('not' q))) in TAUT A by LUKASI_1:34; (p '&' q) => ('not' ('not' (p '&' q))) in TAUT A by LUKASI_1:27; then A3: (p '&' q) => ('not' (('not' p) 'or' ('not' q))) in TAUT A by A2, LUKASI_1:3; ('not' ('not' p)) => p in TAUT A by LUKASI_1:25; then ('not' (('not' p) 'or' ('not' q))) => p in TAUT A by A1, LUKASI_1:3; hence (p '&' q) => p in TAUT A by A3, LUKASI_1:3; ::_thesis: verum end; theorem Th20: :: PROCAL_1:20 for A being QC-alphabet for p, q being Element of CQC-WFF A holds (p '&' q) => (p 'or' q) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p '&' q) => (p 'or' q) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (p '&' q) => (p 'or' q) in TAUT A ( p => (p 'or' q) in TAUT A & (p '&' q) => p in TAUT A ) by Th3, Th19; hence (p '&' q) => (p 'or' q) in TAUT A by LUKASI_1:3; ::_thesis: verum end; theorem Th21: :: PROCAL_1:21 for A being QC-alphabet for p, q being Element of CQC-WFF A holds (p '&' q) => q in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p '&' q) => q in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (p '&' q) => q in TAUT A ( (q '&' p) => q in TAUT A & (p '&' q) => (q '&' p) in TAUT A ) by Th19, CQC_THE1:45; hence (p '&' q) => q in TAUT A by LUKASI_1:3; ::_thesis: verum end; theorem :: PROCAL_1:22 for A being QC-alphabet for p being Element of CQC-WFF A holds p => (p '&' p) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds p => (p '&' p) in TAUT A let p be Element of CQC-WFF A; ::_thesis: p => (p '&' p) in TAUT A ( ('not' (p '&' p)) => (('not' p) 'or' ('not' p)) in TAUT A & (('not' p) 'or' ('not' p)) => ('not' p) in TAUT A ) by Th11, Th17; then ('not' (p '&' p)) => ('not' p) in TAUT A by LUKASI_1:3; hence p => (p '&' p) in TAUT A by LUKASI_1:35; ::_thesis: verum end; theorem :: PROCAL_1:23 for A being QC-alphabet for p, q being Element of CQC-WFF A holds (p <=> q) => (p => q) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p <=> q) => (p => q) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (p <=> q) => (p => q) in TAUT A p <=> q = (p => q) '&' (q => p) by QC_LANG2:def_4; hence (p <=> q) => (p => q) in TAUT A by Th19; ::_thesis: verum end; theorem :: PROCAL_1:24 for A being QC-alphabet for p, q being Element of CQC-WFF A holds (p <=> q) => (q => p) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p <=> q) => (q => p) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (p <=> q) => (q => p) in TAUT A p <=> q = (p => q) '&' (q => p) by QC_LANG2:def_4; hence (p <=> q) => (q => p) in TAUT A by Th21; ::_thesis: verum end; theorem Th25: :: PROCAL_1:25 for A being QC-alphabet for p, q, r being Element of CQC-WFF A holds ((p 'or' q) 'or' r) => (p 'or' (q 'or' r)) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ((p 'or' q) 'or' r) => (p 'or' (q 'or' r)) in TAUT A let p, q, r be Element of CQC-WFF A; ::_thesis: ((p 'or' q) 'or' r) => (p 'or' (q 'or' r)) in TAUT A ( ('not' p) => ((('not' r) => q) => (('not' q) => r)) in TAUT A & (('not' p) => ((('not' r) => q) => (('not' q) => r))) => ((('not' p) => (('not' r) => q)) => (('not' p) => (('not' q) => r))) in TAUT A ) by LUKASI_1:11, LUKASI_1:13, LUKASI_1:31; then A1: (('not' p) => (('not' r) => q)) => (('not' p) => (('not' q) => r)) in TAUT A by CQC_THE1:46; ( ((p 'or' q) 'or' r) => (r 'or' (p 'or' q)) in TAUT A & (r 'or' (p 'or' q)) => (('not' r) => (p 'or' q)) in TAUT A ) by Th5, Th8; then ((p 'or' q) 'or' r) => (('not' r) => (p 'or' q)) in TAUT A by LUKASI_1:3; then A2: ((p 'or' q) 'or' r) => (('not' r) => (('not' p) => q)) in TAUT A by Lm1; (('not' r) => (('not' p) => q)) => (('not' p) => (('not' r) => q)) in TAUT A by LUKASI_1:8; then ((p 'or' q) 'or' r) => (('not' p) => (('not' r) => q)) in TAUT A by A2, LUKASI_1:3; then ((p 'or' q) 'or' r) => (('not' p) => (('not' q) => r)) in TAUT A by A1, LUKASI_1:3; then ((p 'or' q) 'or' r) => (('not' p) => (q 'or' r)) in TAUT A by Lm1; hence ((p 'or' q) 'or' r) => (p 'or' (q 'or' r)) in TAUT A by Lm1; ::_thesis: verum end; theorem :: PROCAL_1:26 for A being QC-alphabet for p, q, r being Element of CQC-WFF A holds ((p '&' q) '&' r) => (p '&' (q '&' r)) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ((p '&' q) '&' r) => (p '&' (q '&' r)) in TAUT A let p, q, r be Element of CQC-WFF A; ::_thesis: ((p '&' q) '&' r) => (p '&' (q '&' r)) in TAUT A A1: (('not' p) 'or' (('not' r) 'or' ('not' q))) => ((('not' r) 'or' ('not' q)) 'or' ('not' p)) in TAUT A by Th8; ( ('not' (q '&' r)) => (('not' q) 'or' ('not' r)) in TAUT A & (('not' q) 'or' ('not' r)) => (('not' r) 'or' ('not' q)) in TAUT A ) by Th8, Th17; then ('not' (q '&' r)) => (('not' r) 'or' ('not' q)) in TAUT A by LUKASI_1:3; then A2: ('not' ('not' p)) => (('not' (q '&' r)) => (('not' r) 'or' ('not' q))) in TAUT A by LUKASI_1:13; (('not' ('not' p)) => (('not' (q '&' r)) => (('not' r) 'or' ('not' q)))) => ((('not' ('not' p)) => ('not' (q '&' r))) => (('not' ('not' p)) => (('not' r) 'or' ('not' q)))) in TAUT A by LUKASI_1:11; then (('not' ('not' p)) => ('not' (q '&' r))) => (('not' ('not' p)) => (('not' r) 'or' ('not' q))) in TAUT A by A2, CQC_THE1:46; then (('not' p) 'or' ('not' (q '&' r))) => (('not' ('not' p)) => (('not' r) 'or' ('not' q))) in TAUT A by Lm1; then A3: (('not' p) 'or' ('not' (q '&' r))) => (('not' p) 'or' (('not' r) 'or' ('not' q))) in TAUT A by Lm1; ('not' (p '&' (q '&' r))) => (('not' p) 'or' ('not' (q '&' r))) in TAUT A by Th17; then ('not' (p '&' (q '&' r))) => (('not' p) 'or' (('not' r) 'or' ('not' q))) in TAUT A by A3, LUKASI_1:3; then A4: ('not' (p '&' (q '&' r))) => ((('not' r) 'or' ('not' q)) 'or' ('not' p)) in TAUT A by A1, LUKASI_1:3; A5: (('not' (p '&' q)) 'or' ('not' r)) => ('not' ((p '&' q) '&' r)) in TAUT A by Th18; ( (('not' q) 'or' ('not' p)) => (('not' p) 'or' ('not' q)) in TAUT A & (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) in TAUT A ) by Th8, Th18; then (('not' q) 'or' ('not' p)) => ('not' (p '&' q)) in TAUT A by LUKASI_1:3; then A6: ('not' ('not' r)) => ((('not' q) 'or' ('not' p)) => ('not' (p '&' q))) in TAUT A by LUKASI_1:13; (('not' ('not' r)) => ((('not' q) 'or' ('not' p)) => ('not' (p '&' q)))) => ((('not' ('not' r)) => (('not' q) 'or' ('not' p))) => (('not' ('not' r)) => ('not' (p '&' q)))) in TAUT A by LUKASI_1:11; then (('not' ('not' r)) => (('not' q) 'or' ('not' p))) => (('not' ('not' r)) => ('not' (p '&' q))) in TAUT A by A6, CQC_THE1:46; then (('not' r) 'or' (('not' q) 'or' ('not' p))) => (('not' ('not' r)) => ('not' (p '&' q))) in TAUT A by Lm1; then A7: (('not' r) 'or' (('not' q) 'or' ('not' p))) => (('not' r) 'or' ('not' (p '&' q))) in TAUT A by Lm1; (('not' r) 'or' ('not' (p '&' q))) => (('not' (p '&' q)) 'or' ('not' r)) in TAUT A by Th8; then (('not' r) 'or' (('not' q) 'or' ('not' p))) => (('not' (p '&' q)) 'or' ('not' r)) in TAUT A by A7, LUKASI_1:3; then A8: (('not' r) 'or' (('not' q) 'or' ('not' p))) => ('not' ((p '&' q) '&' r)) in TAUT A by A5, LUKASI_1:3; ((('not' r) 'or' ('not' q)) 'or' ('not' p)) => (('not' r) 'or' (('not' q) 'or' ('not' p))) in TAUT A by Th25; then ('not' (p '&' (q '&' r))) => (('not' r) 'or' (('not' q) 'or' ('not' p))) in TAUT A by A4, LUKASI_1:3; then ('not' (p '&' (q '&' r))) => ('not' ((p '&' q) '&' r)) in TAUT A by A8, LUKASI_1:3; hence ((p '&' q) '&' r) => (p '&' (q '&' r)) in TAUT A by LUKASI_1:35; ::_thesis: verum end; theorem Th27: :: PROCAL_1:27 for A being QC-alphabet for p, q, r being Element of CQC-WFF A holds (p 'or' (q 'or' r)) => ((p 'or' q) 'or' r) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds (p 'or' (q 'or' r)) => ((p 'or' q) 'or' r) in TAUT A let p, q, r be Element of CQC-WFF A; ::_thesis: (p 'or' (q 'or' r)) => ((p 'or' q) 'or' r) in TAUT A A1: (('not' p) => (('not' r) => q)) => (('not' r) => (('not' p) => q)) in TAUT A by LUKASI_1:8; ( ('not' p) => ((('not' q) => r) => (('not' r) => q)) in TAUT A & (('not' p) => ((('not' q) => r) => (('not' r) => q))) => ((('not' p) => (('not' q) => r)) => (('not' p) => (('not' r) => q))) in TAUT A ) by LUKASI_1:11, LUKASI_1:13, LUKASI_1:31; then A2: (('not' p) => (('not' q) => r)) => (('not' p) => (('not' r) => q)) in TAUT A by CQC_THE1:46; (p 'or' (q 'or' r)) => (('not' p) => (q 'or' r)) in TAUT A by Th5; then (p 'or' (q 'or' r)) => (('not' p) => (('not' q) => r)) in TAUT A by Lm1; then (p 'or' (q 'or' r)) => (('not' p) => (('not' r) => q)) in TAUT A by A2, LUKASI_1:3; then (p 'or' (q 'or' r)) => (('not' r) => (('not' p) => q)) in TAUT A by A1, LUKASI_1:3; then A3: (p 'or' (q 'or' r)) => (r 'or' (('not' p) => q)) in TAUT A by Lm1; (r 'or' (('not' p) => q)) => ((('not' p) => q) 'or' r) in TAUT A by Th8; then (p 'or' (q 'or' r)) => ((('not' p) => q) 'or' r) in TAUT A by A3, LUKASI_1:3; hence (p 'or' (q 'or' r)) => ((p 'or' q) 'or' r) in TAUT A by Lm1; ::_thesis: verum end; theorem Th28: :: PROCAL_1:28 for A being QC-alphabet for p, q being Element of CQC-WFF A holds p => (q => (p '&' q)) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds p => (q => (p '&' q)) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: p => (q => (p '&' q)) in TAUT A A1: (((p '&' q) 'or' ('not' p)) 'or' ('not' q)) => (('not' q) 'or' ((p '&' q) 'or' ('not' p))) in TAUT A by Th8; ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) in TAUT A by Th17; then A2: (p '&' q) 'or' (('not' p) 'or' ('not' q)) in TAUT A by Lm1; ((p '&' q) 'or' (('not' p) 'or' ('not' q))) => (((p '&' q) 'or' ('not' p)) 'or' ('not' q)) in TAUT A by Th27; then ((p '&' q) 'or' ('not' p)) 'or' ('not' q) in TAUT A by A2, CQC_THE1:46; then ('not' q) 'or' ((p '&' q) 'or' ('not' p)) in TAUT A by A1, CQC_THE1:46; then A3: ('not' ('not' q)) => ((p '&' q) 'or' ('not' p)) in TAUT A by Lm1; ( q => (((p '&' q) 'or' ('not' p)) => (('not' p) 'or' (p '&' q))) in TAUT A & (q => (((p '&' q) 'or' ('not' p)) => (('not' p) 'or' (p '&' q)))) => ((q => ((p '&' q) 'or' ('not' p))) => (q => (('not' p) 'or' (p '&' q)))) in TAUT A ) by Th8, LUKASI_1:11, LUKASI_1:13; then A4: (q => ((p '&' q) 'or' ('not' p))) => (q => (('not' p) 'or' (p '&' q))) in TAUT A by CQC_THE1:46; q => ('not' ('not' q)) in TAUT A by LUKASI_1:27; then q => ((p '&' q) 'or' ('not' p)) in TAUT A by A3, LUKASI_1:3; then q => (('not' p) 'or' (p '&' q)) in TAUT A by A4, CQC_THE1:46; then q => (('not' ('not' p)) => (p '&' q)) in TAUT A by Lm1; then A5: ('not' ('not' p)) => (q => (p '&' q)) in TAUT A by LUKASI_1:15; p => ('not' ('not' p)) in TAUT A by LUKASI_1:27; hence p => (q => (p '&' q)) in TAUT A by A5, LUKASI_1:3; ::_thesis: verum end; theorem :: PROCAL_1:29 for A being QC-alphabet for p, q being Element of CQC-WFF A holds (p => q) => ((q => p) => (p <=> q)) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p => q) => ((q => p) => (p <=> q)) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (p => q) => ((q => p) => (p <=> q)) in TAUT A (p => q) => ((q => p) => ((p => q) '&' (q => p))) in TAUT A by Th28; hence (p => q) => ((q => p) => (p <=> q)) in TAUT A by QC_LANG2:def_4; ::_thesis: verum end; Lm4: for A being QC-alphabet for p, q being Element of CQC-WFF A st p in TAUT A & q in TAUT A holds p '&' q in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p in TAUT A & q in TAUT A holds p '&' q in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: ( p in TAUT A & q in TAUT A implies p '&' q in TAUT A ) assume that A1: p in TAUT A and A2: q in TAUT A ; ::_thesis: p '&' q in TAUT A p => (q => (p '&' q)) in TAUT A by Th28; then q => (p '&' q) in TAUT A by A1, CQC_THE1:46; hence p '&' q in TAUT A by A2, CQC_THE1:46; ::_thesis: verum end; theorem :: PROCAL_1:30 for A being QC-alphabet for p, q being Element of CQC-WFF A holds (p 'or' q) <=> (q 'or' p) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p 'or' q) <=> (q 'or' p) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (p 'or' q) <=> (q 'or' p) in TAUT A set P = p 'or' q; set Q = q 'or' p; ( (p 'or' q) => (q 'or' p) in TAUT A & (q 'or' p) => (p 'or' q) in TAUT A ) by Th8; then ((p 'or' q) => (q 'or' p)) '&' ((q 'or' p) => (p 'or' q)) in TAUT A by Lm4; hence (p 'or' q) <=> (q 'or' p) in TAUT A by QC_LANG2:def_4; ::_thesis: verum end; theorem :: PROCAL_1:31 for A being QC-alphabet for p, q, r being Element of CQC-WFF A holds ((p '&' q) => r) => (p => (q => r)) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ((p '&' q) => r) => (p => (q => r)) in TAUT A let p, q, r be Element of CQC-WFF A; ::_thesis: ((p '&' q) => r) => (p => (q => r)) in TAUT A ( p => ((q => (p '&' q)) => (((p '&' q) => r) => (q => r))) in TAUT A & p => (q => (p '&' q)) in TAUT A ) by Th28, LUKASI_1:1, LUKASI_1:13; then A1: p => (((p '&' q) => r) => (q => r)) in TAUT A by LUKASI_1:20; (p => (((p '&' q) => r) => (q => r))) => (((p '&' q) => r) => (p => (q => r))) in TAUT A by LUKASI_1:8; hence ((p '&' q) => r) => (p => (q => r)) in TAUT A by A1, CQC_THE1:46; ::_thesis: verum end; theorem Th32: :: PROCAL_1:32 for A being QC-alphabet for p, q, r being Element of CQC-WFF A holds (p => (q => r)) => ((p '&' q) => r) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds (p => (q => r)) => ((p '&' q) => r) in TAUT A let p, q, r be Element of CQC-WFF A; ::_thesis: (p => (q => r)) => ((p '&' q) => r) in TAUT A A1: (p => ((p '&' q) => r)) => ((p '&' q) => (p => r)) in TAUT A by LUKASI_1:8; ((p '&' q) => (p => r)) => (((p '&' q) => p) => ((p '&' q) => r)) in TAUT A by LUKASI_1:11; then A2: ((p '&' q) => (p => r)) => ((p '&' q) => r) in TAUT A by Th19, LUKASI_1:16; ( (p '&' q) => q in TAUT A & ((p '&' q) => q) => ((q => r) => ((p '&' q) => r)) in TAUT A ) by Th21, LUKASI_1:1; then (q => r) => ((p '&' q) => r) in TAUT A by CQC_THE1:46; then A3: p => ((q => r) => ((p '&' q) => r)) in TAUT A by LUKASI_1:13; (p => ((q => r) => ((p '&' q) => r))) => ((p => (q => r)) => (p => ((p '&' q) => r))) in TAUT A by LUKASI_1:11; then (p => (q => r)) => (p => ((p '&' q) => r)) in TAUT A by A3, CQC_THE1:46; then (p => (q => r)) => ((p '&' q) => (p => r)) in TAUT A by A1, LUKASI_1:3; hence (p => (q => r)) => ((p '&' q) => r) in TAUT A by A2, LUKASI_1:3; ::_thesis: verum end; theorem Th33: :: PROCAL_1:33 for A being QC-alphabet for r, p, q being Element of CQC-WFF A holds (r => p) => ((r => q) => (r => (p '&' q))) in TAUT A proof let A be QC-alphabet ; ::_thesis: for r, p, q being Element of CQC-WFF A holds (r => p) => ((r => q) => (r => (p '&' q))) in TAUT A let r, p, q be Element of CQC-WFF A; ::_thesis: (r => p) => ((r => q) => (r => (p '&' q))) in TAUT A ( r => (p => (q => (p '&' q))) in TAUT A & (r => (p => (q => (p '&' q)))) => ((r => p) => (r => (q => (p '&' q)))) in TAUT A ) by Th28, LUKASI_1:11, LUKASI_1:13; then A1: (r => p) => (r => (q => (p '&' q))) in TAUT A by CQC_THE1:46; (r => (q => (p '&' q))) => ((r => q) => (r => (p '&' q))) in TAUT A by LUKASI_1:11; hence (r => p) => ((r => q) => (r => (p '&' q))) in TAUT A by A1, LUKASI_1:3; ::_thesis: verum end; theorem :: PROCAL_1:34 for A being QC-alphabet for p, q, r being Element of CQC-WFF A holds ((p 'or' q) => r) => ((p => r) 'or' (q => r)) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ((p 'or' q) => r) => ((p => r) 'or' (q => r)) in TAUT A let p, q, r be Element of CQC-WFF A; ::_thesis: ((p 'or' q) => r) => ((p => r) 'or' (q => r)) in TAUT A ( q => (p 'or' q) in TAUT A & (q => (p 'or' q)) => (((p 'or' q) => r) => (q => r)) in TAUT A ) by Th4, LUKASI_1:1; then ((p 'or' q) => r) => (q => r) in TAUT A by CQC_THE1:46; then ('not' (p => r)) => (((p 'or' q) => r) => (q => r)) in TAUT A by LUKASI_1:13; then ((p 'or' q) => r) => (('not' (p => r)) => (q => r)) in TAUT A by LUKASI_1:15; hence ((p 'or' q) => r) => ((p => r) 'or' (q => r)) in TAUT A by Lm1; ::_thesis: verum end; theorem Th35: :: PROCAL_1:35 for A being QC-alphabet for p, r, q being Element of CQC-WFF A holds (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, r, q being Element of CQC-WFF A holds (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT A let p, r, q be Element of CQC-WFF A; ::_thesis: (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT A set AA = ('not' r) => ('not' p); set B = ('not' r) => ('not' q); set C = ('not' r) => (('not' p) '&' ('not' q)); set D = (p 'or' q) => r; set E = q => r; A1: (('not' r) => ('not' p)) => ((('not' r) => ('not' q)) => (('not' r) => (('not' p) '&' ('not' q)))) in TAUT A by Th33; (('not' r) => (('not' p) '&' ('not' q))) => (('not' (('not' p) '&' ('not' q))) => r) in TAUT A by LUKASI_1:31; then (('not' r) => (('not' p) '&' ('not' q))) => ((p 'or' q) => r) in TAUT A by QC_LANG2:def_3; then A2: (('not' r) => ('not' q)) => ((('not' r) => (('not' p) '&' ('not' q))) => ((p 'or' q) => r)) in TAUT A by LUKASI_1:13; ((('not' r) => ('not' q)) => ((('not' r) => (('not' p) '&' ('not' q))) => ((p 'or' q) => r))) => (((('not' r) => ('not' q)) => (('not' r) => (('not' p) '&' ('not' q)))) => ((('not' r) => ('not' q)) => ((p 'or' q) => r))) in TAUT A by LUKASI_1:11; then ((('not' r) => ('not' q)) => (('not' r) => (('not' p) '&' ('not' q)))) => ((('not' r) => ('not' q)) => ((p 'or' q) => r)) in TAUT A by A2, CQC_THE1:46; then (('not' r) => ('not' p)) => ((('not' r) => ('not' q)) => ((p 'or' q) => r)) in TAUT A by A1, LUKASI_1:3; then A3: (('not' r) => ('not' q)) => ((('not' r) => ('not' p)) => ((p 'or' q) => r)) in TAUT A by LUKASI_1:15; (q => r) => (('not' r) => ('not' q)) in TAUT A by LUKASI_1:26; then (q => r) => ((('not' r) => ('not' p)) => ((p 'or' q) => r)) in TAUT A by A3, LUKASI_1:3; then A4: (('not' r) => ('not' p)) => ((q => r) => ((p 'or' q) => r)) in TAUT A by LUKASI_1:15; (p => r) => (('not' r) => ('not' p)) in TAUT A by LUKASI_1:26; hence (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT A by A4, LUKASI_1:3; ::_thesis: verum end; theorem Th36: :: PROCAL_1:36 for A being QC-alphabet for p, r, q being Element of CQC-WFF A holds ((p => r) '&' (q => r)) => ((p 'or' q) => r) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, r, q being Element of CQC-WFF A holds ((p => r) '&' (q => r)) => ((p 'or' q) => r) in TAUT A let p, r, q be Element of CQC-WFF A; ::_thesis: ((p => r) '&' (q => r)) => ((p 'or' q) => r) in TAUT A set P = p => r; set Q = q => r; set R = (p 'or' q) => r; ( (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT A & ((p => r) => ((q => r) => ((p 'or' q) => r))) => (((p => r) '&' (q => r)) => ((p 'or' q) => r)) in TAUT A ) by Th32, Th35; hence ((p => r) '&' (q => r)) => ((p 'or' q) => r) in TAUT A by CQC_THE1:46; ::_thesis: verum end; theorem :: PROCAL_1:37 for A being QC-alphabet for p, q being Element of CQC-WFF A holds (p => (q '&' ('not' q))) => ('not' p) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p => (q '&' ('not' q))) => ('not' p) in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: (p => (q '&' ('not' q))) => ('not' p) in TAUT A p => ('not' (q '&' ('not' q))) in TAUT A by Th1, LUKASI_1:13; then A1: ('not' ('not' (q '&' ('not' q)))) => ('not' p) in TAUT A by LUKASI_1:34; (q '&' ('not' q)) => ('not' ('not' (q '&' ('not' q)))) in TAUT A by LUKASI_1:27; then (q '&' ('not' q)) => ('not' p) in TAUT A by A1, LUKASI_1:3; then A2: p => ((q '&' ('not' q)) => ('not' p)) in TAUT A by LUKASI_1:13; ( ('not' ('not' p)) => p in TAUT A & (('not' ('not' p)) => p) => ((p => ('not' p)) => (('not' ('not' p)) => ('not' p))) in TAUT A ) by LUKASI_1:1, LUKASI_1:25; then ( (('not' ('not' p)) => ('not' p)) => ('not' p) in TAUT A & (p => ('not' p)) => (('not' ('not' p)) => ('not' p)) in TAUT A ) by CQC_THE1:42, CQC_THE1:46; then A3: (p => ('not' p)) => ('not' p) in TAUT A by LUKASI_1:3; (p => ((q '&' ('not' q)) => ('not' p))) => ((p => (q '&' ('not' q))) => (p => ('not' p))) in TAUT A by LUKASI_1:11; then (p => (q '&' ('not' q))) => (p => ('not' p)) in TAUT A by A2, CQC_THE1:46; hence (p => (q '&' ('not' q))) => ('not' p) in TAUT A by A3, LUKASI_1:3; ::_thesis: verum end; theorem :: PROCAL_1:38 for A being QC-alphabet for p, q, r being Element of CQC-WFF A holds ((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)) in TAUT A let p, q, r be Element of CQC-WFF A; ::_thesis: ((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)) in TAUT A (('not' p) => q) => ((('not' p) => r) => (('not' p) => (q '&' r))) in TAUT A by Th33; then (p 'or' q) => ((('not' p) => r) => (('not' p) => (q '&' r))) in TAUT A by Lm1; then (p 'or' q) => ((p 'or' r) => (('not' p) => (q '&' r))) in TAUT A by Lm1; then A1: (p 'or' q) => ((p 'or' r) => (p 'or' (q '&' r))) in TAUT A by Lm1; ((p 'or' q) => ((p 'or' r) => (p 'or' (q '&' r)))) => (((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r))) in TAUT A by Th32; hence ((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)) in TAUT A by A1, CQC_THE1:46; ::_thesis: verum end; theorem :: PROCAL_1:39 for A being QC-alphabet for p, q, r being Element of CQC-WFF A holds (p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r)) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds (p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r)) in TAUT A let p, q, r be Element of CQC-WFF A; ::_thesis: (p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r)) in TAUT A A1: ('not' ((p '&' q) 'or' (p '&' r))) => (('not' (p '&' q)) '&' ('not' (p '&' r))) in TAUT A by Th6; ( ('not' (p => ('not' q))) => (p '&' q) in TAUT A & (('not' (p => ('not' q))) => (p '&' q)) => (('not' (p '&' q)) => (p => ('not' q))) in TAUT A ) by Th16, LUKASI_1:31; then A2: ('not' (p '&' q)) => (p => ('not' q)) in TAUT A by CQC_THE1:46; ( ('not' (p => ('not' r))) => (p '&' r) in TAUT A & (('not' (p => ('not' r))) => (p '&' r)) => (('not' (p '&' r)) => (p => ('not' r))) in TAUT A ) by Th16, LUKASI_1:31; then A3: ('not' (p '&' r)) => (p => ('not' r)) in TAUT A by CQC_THE1:46; ( (p => ('not' q)) => ((p => ('not' r)) => (p => (('not' q) '&' ('not' r)))) in TAUT A & p => (('not' q) '&' ('not' r)) = 'not' (p '&' ('not' (('not' q) '&' ('not' r)))) ) by Th33, QC_LANG2:def_2; then (p => ('not' q)) => ((p => ('not' r)) => ('not' (p '&' (q 'or' r)))) in TAUT A by QC_LANG2:def_3; then ('not' (p '&' q)) => ((p => ('not' r)) => ('not' (p '&' (q 'or' r)))) in TAUT A by A2, LUKASI_1:3; then (p => ('not' r)) => (('not' (p '&' q)) => ('not' (p '&' (q 'or' r)))) in TAUT A by LUKASI_1:15; then ('not' (p '&' r)) => (('not' (p '&' q)) => ('not' (p '&' (q 'or' r)))) in TAUT A by A3, LUKASI_1:3; then A4: ('not' (p '&' q)) => (('not' (p '&' r)) => ('not' (p '&' (q 'or' r)))) in TAUT A by LUKASI_1:15; (('not' (p '&' q)) => (('not' (p '&' r)) => ('not' (p '&' (q 'or' r))))) => ((('not' (p '&' q)) '&' ('not' (p '&' r))) => ('not' (p '&' (q 'or' r)))) in TAUT A by Th32; then (('not' (p '&' q)) '&' ('not' (p '&' r))) => ('not' (p '&' (q 'or' r))) in TAUT A by A4, CQC_THE1:46; then ('not' ((p '&' q) 'or' (p '&' r))) => ('not' (p '&' (q 'or' r))) in TAUT A by A1, LUKASI_1:3; hence (p '&' (q 'or' r)) => ((p '&' q) 'or' (p '&' r)) in TAUT A by LUKASI_1:35; ::_thesis: verum end; theorem Th40: :: PROCAL_1:40 for A being QC-alphabet for p, r, q being Element of CQC-WFF A holds ((p 'or' r) '&' (q 'or' r)) => ((p '&' q) 'or' r) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, r, q being Element of CQC-WFF A holds ((p 'or' r) '&' (q 'or' r)) => ((p '&' q) 'or' r) in TAUT A let p, r, q be Element of CQC-WFF A; ::_thesis: ((p 'or' r) '&' (q 'or' r)) => ((p '&' q) 'or' r) in TAUT A ((('not' p) => r) '&' (('not' q) => r)) => ((('not' p) 'or' ('not' q)) => r) in TAUT A by Th36; then ((p 'or' r) '&' (('not' q) => r)) => ((('not' p) 'or' ('not' q)) => r) in TAUT A by Lm1; then A1: ((p 'or' r) '&' (q 'or' r)) => ((('not' p) 'or' ('not' q)) => r) in TAUT A by Lm1; ( ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) in TAUT A & (('not' (p '&' q)) => (('not' p) 'or' ('not' q))) => (((('not' p) 'or' ('not' q)) => r) => (('not' (p '&' q)) => r)) in TAUT A ) by Th17, LUKASI_1:1; then ((('not' p) 'or' ('not' q)) => r) => (('not' (p '&' q)) => r) in TAUT A by CQC_THE1:46; then ((p 'or' r) '&' (q 'or' r)) => (('not' (p '&' q)) => r) in TAUT A by A1, LUKASI_1:3; hence ((p 'or' r) '&' (q 'or' r)) => ((p '&' q) 'or' r) in TAUT A by Lm1; ::_thesis: verum end; Lm5: for A being QC-alphabet for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds (r '&' p) => (r '&' q) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds (r '&' p) => (r '&' q) in TAUT A let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A implies (r '&' p) => (r '&' q) in TAUT A ) A1: ('not' (r => ('not' q))) => (r '&' q) in TAUT A by Th16; assume p => q in TAUT A ; ::_thesis: (r '&' p) => (r '&' q) in TAUT A then ('not' q) => ('not' p) in TAUT A by LUKASI_1:34; then A2: r => (('not' q) => ('not' p)) in TAUT A by LUKASI_1:13; (r => (('not' q) => ('not' p))) => ((r => ('not' q)) => (r => ('not' p))) in TAUT A by LUKASI_1:11; then (r => ('not' q)) => (r => ('not' p)) in TAUT A by A2, CQC_THE1:46; then A3: ('not' (r => ('not' p))) => ('not' (r => ('not' q))) in TAUT A by LUKASI_1:34; (r '&' p) => ('not' (r => ('not' p))) in TAUT A by Th15; then (r '&' p) => ('not' (r => ('not' q))) in TAUT A by A3, LUKASI_1:3; hence (r '&' p) => (r '&' q) in TAUT A by A1, LUKASI_1:3; ::_thesis: verum end; Lm6: for A being QC-alphabet for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds (p 'or' r) => (q 'or' r) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds (p 'or' r) => (q 'or' r) in TAUT A let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A implies (p 'or' r) => (q 'or' r) in TAUT A ) assume p => q in TAUT A ; ::_thesis: (p 'or' r) => (q 'or' r) in TAUT A then A1: ('not' q) => ('not' p) in TAUT A by LUKASI_1:34; (('not' q) => ('not' p)) => ((('not' p) => r) => (('not' q) => r)) in TAUT A by LUKASI_1:1; then (('not' p) => r) => (('not' q) => r) in TAUT A by A1, CQC_THE1:46; then (p 'or' r) => (('not' q) => r) in TAUT A by Lm1; hence (p 'or' r) => (q 'or' r) in TAUT A by Lm1; ::_thesis: verum end; Lm7: for A being QC-alphabet for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds (r 'or' p) => (r 'or' q) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds (r 'or' p) => (r 'or' q) in TAUT A let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A implies (r 'or' p) => (r 'or' q) in TAUT A ) assume p => q in TAUT A ; ::_thesis: (r 'or' p) => (r 'or' q) in TAUT A then A1: ('not' r) => (p => q) in TAUT A by LUKASI_1:13; (('not' r) => (p => q)) => ((('not' r) => p) => (('not' r) => q)) in TAUT A by LUKASI_1:11; then (('not' r) => p) => (('not' r) => q) in TAUT A by A1, CQC_THE1:46; then (r 'or' p) => (('not' r) => q) in TAUT A by Lm1; hence (r 'or' p) => (r 'or' q) in TAUT A by Lm1; ::_thesis: verum end; theorem :: PROCAL_1:41 for A being QC-alphabet for p, q, r being Element of CQC-WFF A holds ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT A let p, q, r be Element of CQC-WFF A; ::_thesis: ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT A A1: ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) => (('not' (('not' p) 'or' ('not' r))) 'or' ('not' (('not' q) 'or' ('not' r)))) in TAUT A by Th17; ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r))) => ((('not' p) '&' ('not' q)) 'or' ('not' r)) in TAUT A by Th40; then A2: ('not' ((('not' p) '&' ('not' q)) 'or' ('not' r))) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) in TAUT A by LUKASI_1:34; (('not' (('not' p) '&' ('not' q))) '&' ('not' ('not' r))) => ('not' ((('not' p) '&' ('not' q)) 'or' ('not' r))) in TAUT A by Th7; then (('not' (('not' p) '&' ('not' q))) '&' ('not' ('not' r))) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) in TAUT A by A2, LUKASI_1:3; then A3: ((p 'or' q) '&' ('not' ('not' r))) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) in TAUT A by QC_LANG2:def_3; ( ('not' (p '&' r)) => (('not' p) 'or' ('not' r)) in TAUT A & (('not' (p '&' r)) => (('not' p) 'or' ('not' r))) => (('not' (('not' p) 'or' ('not' r))) => (p '&' r)) in TAUT A ) by Th17, LUKASI_1:31; then ('not' (('not' p) 'or' ('not' r))) => (p '&' r) in TAUT A by CQC_THE1:46; then A4: (('not' (('not' p) 'or' ('not' r))) 'or' ('not' (('not' q) 'or' ('not' r)))) => ((p '&' r) 'or' ('not' (('not' q) 'or' ('not' r)))) in TAUT A by Lm6; ( ('not' (q '&' r)) => (('not' q) 'or' ('not' r)) in TAUT A & (('not' (q '&' r)) => (('not' q) 'or' ('not' r))) => (('not' (('not' q) 'or' ('not' r))) => (q '&' r)) in TAUT A ) by Th17, LUKASI_1:31; then ('not' (('not' q) 'or' ('not' r))) => (q '&' r) in TAUT A by CQC_THE1:46; then A5: ((p '&' r) 'or' ('not' (('not' q) 'or' ('not' r)))) => ((p '&' r) 'or' (q '&' r)) in TAUT A by Lm7; r => ('not' ('not' r)) in TAUT A by LUKASI_1:27; then ((p 'or' q) '&' r) => ((p 'or' q) '&' ('not' ('not' r))) in TAUT A by Lm5; then ((p 'or' q) '&' r) => ('not' ((('not' p) 'or' ('not' r)) '&' (('not' q) 'or' ('not' r)))) in TAUT A by A3, LUKASI_1:3; then ((p 'or' q) '&' r) => (('not' (('not' p) 'or' ('not' r))) 'or' ('not' (('not' q) 'or' ('not' r)))) in TAUT A by A1, LUKASI_1:3; then ((p 'or' q) '&' r) => ((p '&' r) 'or' ('not' (('not' q) 'or' ('not' r)))) in TAUT A by A4, LUKASI_1:3; hence ((p 'or' q) '&' r) => ((p '&' r) 'or' (q '&' r)) in TAUT A by A5, LUKASI_1:3; ::_thesis: verum end; theorem :: PROCAL_1:42 for A being QC-alphabet for p, q being Element of CQC-WFF A st p in TAUT A holds p 'or' q in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p in TAUT A holds p 'or' q in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: ( p in TAUT A implies p 'or' q in TAUT A ) assume A1: p in TAUT A ; ::_thesis: p 'or' q in TAUT A p => (p 'or' q) in TAUT A by Th3; hence p 'or' q in TAUT A by A1, CQC_THE1:46; ::_thesis: verum end; theorem :: PROCAL_1:43 for A being QC-alphabet for q, p being Element of CQC-WFF A st q in TAUT A holds p 'or' q in TAUT A proof let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A st q in TAUT A holds p 'or' q in TAUT A let q, p be Element of CQC-WFF A; ::_thesis: ( q in TAUT A implies p 'or' q in TAUT A ) assume A1: q in TAUT A ; ::_thesis: p 'or' q in TAUT A q => (p 'or' q) in TAUT A by Th4; hence p 'or' q in TAUT A by A1, CQC_THE1:46; ::_thesis: verum end; theorem :: PROCAL_1:44 for A being QC-alphabet for p, q being Element of CQC-WFF A st p '&' q in TAUT A holds p in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p '&' q in TAUT A holds p in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: ( p '&' q in TAUT A implies p in TAUT A ) assume A1: p '&' q in TAUT A ; ::_thesis: p in TAUT A (p '&' q) => p in TAUT A by Th19; hence p in TAUT A by A1, CQC_THE1:46; ::_thesis: verum end; theorem :: PROCAL_1:45 for A being QC-alphabet for p, q being Element of CQC-WFF A st p '&' q in TAUT A holds q in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p '&' q in TAUT A holds q in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: ( p '&' q in TAUT A implies q in TAUT A ) assume A1: p '&' q in TAUT A ; ::_thesis: q in TAUT A (p '&' q) => q in TAUT A by Th21; hence q in TAUT A by A1, CQC_THE1:46; ::_thesis: verum end; theorem :: PROCAL_1:46 for A being QC-alphabet for p, q being Element of CQC-WFF A st p '&' q in TAUT A holds p 'or' q in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p '&' q in TAUT A holds p 'or' q in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: ( p '&' q in TAUT A implies p 'or' q in TAUT A ) assume A1: p '&' q in TAUT A ; ::_thesis: p 'or' q in TAUT A (p '&' q) => (p 'or' q) in TAUT A by Th20; hence p 'or' q in TAUT A by A1, CQC_THE1:46; ::_thesis: verum end; theorem :: PROCAL_1:47 for A being QC-alphabet for p, q being Element of CQC-WFF A st p in TAUT A & q in TAUT A holds p '&' q in TAUT A by Lm4; theorem :: PROCAL_1:48 for A being QC-alphabet for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds (p 'or' r) => (q 'or' r) in TAUT A by Lm6; theorem :: PROCAL_1:49 for A being QC-alphabet for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds (r 'or' p) => (r 'or' q) in TAUT A by Lm7; theorem :: PROCAL_1:50 for A being QC-alphabet for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds (r '&' p) => (r '&' q) in TAUT A by Lm5; theorem Th51: :: PROCAL_1:51 for A being QC-alphabet for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds (p '&' r) => (q '&' r) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds (p '&' r) => (q '&' r) in TAUT A let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A implies (p '&' r) => (q '&' r) in TAUT A ) A1: (p => q) => ((q => ('not' r)) => (p => ('not' r))) in TAUT A by LUKASI_1:1; assume p => q in TAUT A ; ::_thesis: (p '&' r) => (q '&' r) in TAUT A then (q => ('not' r)) => (p => ('not' r)) in TAUT A by A1, CQC_THE1:46; then A2: ('not' (p => ('not' r))) => ('not' (q => ('not' r))) in TAUT A by LUKASI_1:34; A3: ('not' (q => ('not' r))) => (q '&' r) in TAUT A by Th16; (p '&' r) => ('not' (p => ('not' r))) in TAUT A by Th15; then (p '&' r) => ('not' (q => ('not' r))) in TAUT A by A2, LUKASI_1:3; hence (p '&' r) => (q '&' r) in TAUT A by A3, LUKASI_1:3; ::_thesis: verum end; theorem :: PROCAL_1:52 for A being QC-alphabet for r, p, q being Element of CQC-WFF A st r => p in TAUT A & r => q in TAUT A holds r => (p '&' q) in TAUT A proof let A be QC-alphabet ; ::_thesis: for r, p, q being Element of CQC-WFF A st r => p in TAUT A & r => q in TAUT A holds r => (p '&' q) in TAUT A let r, p, q be Element of CQC-WFF A; ::_thesis: ( r => p in TAUT A & r => q in TAUT A implies r => (p '&' q) in TAUT A ) assume that A1: r => p in TAUT A and A2: r => q in TAUT A ; ::_thesis: r => (p '&' q) in TAUT A (r => p) => ((r => q) => (r => (p '&' q))) in TAUT A by Th33; then (r => q) => (r => (p '&' q)) in TAUT A by A1, CQC_THE1:46; hence r => (p '&' q) in TAUT A by A2, CQC_THE1:46; ::_thesis: verum end; theorem :: PROCAL_1:53 for A being QC-alphabet for p, r, q being Element of CQC-WFF A st p => r in TAUT A & q => r in TAUT A holds (p 'or' q) => r in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, r, q being Element of CQC-WFF A st p => r in TAUT A & q => r in TAUT A holds (p 'or' q) => r in TAUT A let p, r, q be Element of CQC-WFF A; ::_thesis: ( p => r in TAUT A & q => r in TAUT A implies (p 'or' q) => r in TAUT A ) assume ( p => r in TAUT A & q => r in TAUT A ) ; ::_thesis: (p 'or' q) => r in TAUT A then A1: (p => r) '&' (q => r) in TAUT A by Lm4; ((p => r) '&' (q => r)) => ((p 'or' q) => r) in TAUT A by Th36; hence (p 'or' q) => r in TAUT A by A1, CQC_THE1:46; ::_thesis: verum end; theorem :: PROCAL_1:54 for A being QC-alphabet for p, q being Element of CQC-WFF A st p 'or' q in TAUT A & 'not' p in TAUT A holds q in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p 'or' q in TAUT A & 'not' p in TAUT A holds q in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: ( p 'or' q in TAUT A & 'not' p in TAUT A implies q in TAUT A ) assume that A1: p 'or' q in TAUT A and A2: 'not' p in TAUT A ; ::_thesis: q in TAUT A (p 'or' q) => (('not' p) => q) in TAUT A by Th5; then ('not' p) => q in TAUT A by A1, CQC_THE1:46; hence q in TAUT A by A2, CQC_THE1:46; ::_thesis: verum end; theorem :: PROCAL_1:55 for A being QC-alphabet for p, q being Element of CQC-WFF A st p 'or' q in TAUT A & 'not' q in TAUT A holds p in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p 'or' q in TAUT A & 'not' q in TAUT A holds p in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: ( p 'or' q in TAUT A & 'not' q in TAUT A implies p in TAUT A ) assume that A1: p 'or' q in TAUT A and A2: 'not' q in TAUT A ; ::_thesis: p in TAUT A ( (q 'or' p) => (('not' q) => p) in TAUT A & (p 'or' q) => (q 'or' p) in TAUT A ) by Th5, Th8; then (p 'or' q) => (('not' q) => p) in TAUT A by LUKASI_1:3; then ('not' q) => p in TAUT A by A1, CQC_THE1:46; hence p in TAUT A by A2, CQC_THE1:46; ::_thesis: verum end; theorem :: PROCAL_1:56 for A being QC-alphabet for p, q, r, s being Element of CQC-WFF A st p => q in TAUT A & r => s in TAUT A holds (p '&' r) => (q '&' s) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p => q in TAUT A & r => s in TAUT A holds (p '&' r) => (q '&' s) in TAUT A let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A & r => s in TAUT A implies (p '&' r) => (q '&' s) in TAUT A ) assume ( p => q in TAUT A & r => s in TAUT A ) ; ::_thesis: (p '&' r) => (q '&' s) in TAUT A then ( (p '&' r) => (q '&' r) in TAUT A & (q '&' r) => (q '&' s) in TAUT A ) by Lm5, Th51; hence (p '&' r) => (q '&' s) in TAUT A by LUKASI_1:3; ::_thesis: verum end; theorem :: PROCAL_1:57 for A being QC-alphabet for p, q, r, s being Element of CQC-WFF A st p => q in TAUT A & r => s in TAUT A holds (p 'or' r) => (q 'or' s) in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p => q in TAUT A & r => s in TAUT A holds (p 'or' r) => (q 'or' s) in TAUT A let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A & r => s in TAUT A implies (p 'or' r) => (q 'or' s) in TAUT A ) assume ( p => q in TAUT A & r => s in TAUT A ) ; ::_thesis: (p 'or' r) => (q 'or' s) in TAUT A then ( (p 'or' r) => (q 'or' r) in TAUT A & (q 'or' r) => (q 'or' s) in TAUT A ) by Lm6, Lm7; hence (p 'or' r) => (q 'or' s) in TAUT A by LUKASI_1:3; ::_thesis: verum end; theorem :: PROCAL_1:58 for A being QC-alphabet for p, q being Element of CQC-WFF A st (p '&' ('not' q)) => ('not' p) in TAUT A holds p => q in TAUT A proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st (p '&' ('not' q)) => ('not' p) in TAUT A holds p => q in TAUT A let p, q be Element of CQC-WFF A; ::_thesis: ( (p '&' ('not' q)) => ('not' p) in TAUT A implies p => q in TAUT A ) A1: 'not' (p '&' ('not' q)) = p => q by QC_LANG2:def_2; assume (p '&' ('not' q)) => ('not' p) in TAUT A ; ::_thesis: p => q in TAUT A then A2: ('not' ('not' p)) => ('not' (p '&' ('not' q))) in TAUT A by LUKASI_1:34; p => ('not' ('not' p)) in TAUT A by LUKASI_1:27; then p => ('not' (p '&' ('not' q))) in TAUT A by A2, LUKASI_1:3; hence p => q in TAUT A by A1, LUKASI_1:18; ::_thesis: verum end;