:: Propositional Calculus
::  by Grzegorz Bancerek, Agata Darmochwa\l and Andrzej Trybulec
::
:: Received September 26, 1990
:: Copyright (c) 1990-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies SUBSET_1, CQC_LANG, XBOOLEAN, CQC_THE1, QC_LANG1;
 notations SUBSET_1, QC_LANG1, CQC_LANG, CQC_THE1;
 constructors CQC_THE1;
 registrations CQC_LANG;
 definitions CQC_THE1;
 expansions CQC_THE1;
 theorems CQC_THE1, QC_LANG2;

begin

reserve A for QC-alphabet;
reserve p, q, r, s, t for Element of CQC-WFF(A);
reserve X for Subset of CQC-WFF(A);

theorem Th1:
  (p => q) => ((q => r) => (p => r)) in TAUT(A)
proof
  (p => q) => ('not'(q '&' 'not' r) => 'not'(p '&' 'not' r)) in TAUT(A) by
CQC_THE1:44;
  then (p => q) => ((q => r) => 'not'(p '&' 'not' r)) in TAUT(A)
  by QC_LANG2:def 2;
  hence thesis by QC_LANG2:def 2;
end;

theorem Th2:
  p => q in TAUT(A) implies (q => r) => (p => r) in TAUT(A)
proof
  assume
A1: p => q in TAUT(A);
  (p => q) => ((q => r) => (p => r)) in TAUT(A) by Th1;
  hence thesis by A1,CQC_THE1:46;
end;

theorem Th3:
  p => q in TAUT(A) & q => r in TAUT(A) implies p => r in TAUT(A)
proof
  assume that
A1: p => q in TAUT(A) and
A2: q => r in TAUT(A);
  (p => q) => ((q => r) => (p => r)) in TAUT(A) by Th1;
  then (q => r) => (p => r) in TAUT(A) by A1,CQC_THE1:46;
  hence thesis by A2,CQC_THE1:46;
end;

theorem Th4: :: Identity law
  p => p in TAUT(A)
proof
  ('not' p => p) => p in TAUT(A) & p => ('not' p => p) in TAUT(A)
     by CQC_THE1:42,43;
  hence thesis by Th3;
end;

Lm1: (((q => r) => (p => r)) => s) => ((p => q) => s) in TAUT(A)
proof
  (p => q) => ((q => r) => (p => r)) in TAUT(A) by Th1;
  hence thesis by Th2;
end;

Lm2: (p => (q => r)) => ((s => q) => (p => (s => r))) in TAUT(A)
proof
  ((((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s =>
r))) ) => ((p => (q => r)) => ((s => q) => (p => (s => r)))) in TAUT(A)&
(((q =>
r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r))) in TAUT(A)
by Lm1;
  hence thesis by CQC_THE1:46;
end;

Lm3: (p => q) => (((p => r) => s) => ((q => r) => s)) in TAUT(A)
proof
  ((q => r) => (p => r)) => (((p => r) => s) => ((q => r) => s)) in
TAUT(A) &
((( q => r) => (p => r)) => (((p => r) => s) => ((q => r) => s))) => ((p => q)
  => ( ((p => r) => s) => ((q => r) => s))) in TAUT(A) by Lm1,Th1;
  hence thesis by CQC_THE1:46;
end;

Lm4: (t => ((p => r) => s)) => ((p => q) => (t => ((q => r) => s))) in TAUT(A)
proof
  ((p => q) => (((p => r) => s) => ((q => r) => s))) in TAUT(A) & ((p => q)
=> (( (p => r) => s) => ((q => r) => s))) => ((t => ((p => r) => s)) => ((p =>
  q) => (t => ((q => r) => s)))) in TAUT(A) by Lm2,Lm3;
  hence thesis by CQC_THE1:46;
end;

Lm5: (('not' p => q) => r) => (p => r) in TAUT(A)
proof
  p => ('not' p => q) in TAUT(A) by CQC_THE1:43;
  hence thesis by Th2;
end;

Lm6: p => ((('not' p => r) => s) => ((q => r) => s)) in TAUT(A)
proof
  ('not' p => q) => ((('not' p => r) => s) => ((q => r) => s)) in TAUT(A) & (
  (( 'not' p => q) => ((('not' p => r) => s) => ((q => r) => s)) ) => (p => (((
  'not' p => r) => s) => ((q => r) => s)))) in TAUT(A) by Lm3,Lm5;
  hence thesis by CQC_THE1:46;
end;

Lm7: (q => (('not' p => p) => p)) => (('not' p => p) => p) in TAUT(A)
proof
  ('not' p => p) => p in TAUT(A) & (('not' p => p) => p) => ((('not'(('not' p
  => p) => p) => (('not' p => p) => p)) => (('not' p => p) => p)) => ((q => ((
  'not' p => p) => p)) => (('not' p => p) => p))) in TAUT(A)
  by Lm6,CQC_THE1:42;
  then
  ('not'(('not' p => p) => p) => (('not' p => p) => p)) => (('not' p => p)
  => p ) in TAUT(A) & (('not'(('not' p => p) => p) =>
(('not' p => p) => p)) => ((
'not' p => p) => p)) => ((q => (('not' p => p) => p)) => (('not' p => p) => p))
  in TAUT(A) by CQC_THE1:42,46;
  hence thesis by CQC_THE1:46;
end;

Lm8: t => (('not' p => p) => p) in TAUT(A)
proof
  ('not' t => (('not' p => p) => p)) => (('not' p => p) => p) in TAUT(A) & ((
'not' t => (('not' p => p) => p)) => (('not' p => p) => p)) => (t => ( ('not' p
  => p) => p)) in TAUT(A) by Lm5,Lm7;
  hence thesis by CQC_THE1:46;
end;

Lm9: ('not' p => q) => (t => ((q => p) => p)) in TAUT(A)
proof
  t => (('not' p => p) => p) in TAUT(A) & (t => (('not' p => p) => p)) => ((
  'not' p => q) => (t => ((q => p) => p) )) in TAUT(A) by Lm4,Lm8;
  hence thesis by CQC_THE1:46;
end;

Lm10: ((t => ((q => p) => p)) => r) => (('not' p => q) => r) in TAUT(A)
proof
  ('not' p => q) => (t => ((q => p) => p)) in TAUT(A) & (('not' p => q) => (t
=> ((q => p) => p))) => (((t => ((q => p) => p)) => r) => (('not' p => q) => r)
  ) in TAUT(A) by Lm9,Th1;
  hence thesis by CQC_THE1:46;
end;

Lm11: ('not' p => q) => ((q => p) => p) in TAUT(A)
proof
  ('not'((q => p) => p) => ((q => p) => p)) => ((q => p) => p) in TAUT(A) & (
( 'not'((q => p) => p) => ((q => p) => p)) => ((q => p) => p)) => (( 'not' p =>
  q ) => ((q => p) => p)) in TAUT(A) by Lm10,CQC_THE1:42;
  hence thesis by CQC_THE1:46;
end;

Lm12: p => ((q => p) => p) in TAUT(A)
proof
  ('not' p => q) => ((q => p) => p) in TAUT(A) & (('not' p => q) => ((q => p)
  => p)) => (p => ((q => p) => p)) in TAUT(A) by Lm5,Lm11;
  hence thesis by CQC_THE1:46;
end;

theorem Th5:
  q => (p => q) in TAUT(A)
proof
  q => (('not' p => q) => q) in TAUT(A) & (q => (('not' p => q) => q)) => ((p
  => ('not' p => q)) => (q => (p => q))) in TAUT(A) by Lm2,Lm12;
  then p => ('not' p => q) in TAUT(A) & (p => ('not' p => q)) =>
(q => (p => q))
  in TAUT(A) by CQC_THE1:43,46;
  hence thesis by CQC_THE1:46;
end;

theorem Th6:
  ((p => q) => r) => (q => r) in TAUT(A)
proof
  q => (p => q) in TAUT(A) & (q => (p => q)) => (((p => q) => r) => (q => r))
  in TAUT(A) by Th1,Th5;
  hence thesis by CQC_THE1:46;
end;

theorem Th7:
  q => ((q => p) => p) in TAUT(A)
proof
  ('not' p => q) => ((q => p) => p) in TAUT(A) & (('not' p => q) => ((q => p)
  => p)) => (q => ((q => p) => p)) in TAUT(A) by Lm11,Th6;
  hence thesis by CQC_THE1:46;
end;

theorem Th8:
  (s => (q => p)) => (q => (s => p)) in TAUT(A)
proof
  q => ((q => p) => p) in TAUT(A) & (q => ((q => p) => p)) => ((s => (q => p)
  ) => (q => (s => p))) in TAUT(A) by Lm2,Th7;
  hence thesis by CQC_THE1:46;
end;

theorem Th9:
  (q => r) => ((p => q) => (p => r)) in TAUT(A)
proof
  (p => q) => ((q => r) => (p => r)) in TAUT(A) & ((p => q) => ((q => r) => (
  p => r))) => ((q => r) => ((p => q) => (p => r))) in TAUT(A) by Th1,Th8;
  hence thesis by CQC_THE1:46;
end;

Lm13: ((q => (s => p)) => r) => ((s => (q => p)) => r) in TAUT(A)
proof
  (s => (q => p)) => (q => (s => p)) in TAUT(A) & ((s => (q => p)) => (q => (
s => p))) => (((q => (s => p)) => r) => ((s => (q => p)) => r)) in TAUT(A)
by Th1,Th8;
  hence thesis by CQC_THE1:46;
end;

Lm14: ((p => q) => p) => p in TAUT(A)
proof
  ('not' p => (p => q)) => (((p => q) => p) => p) in TAUT(A) & (('not' p => (
p => q)) => (((p => q) => p) => p)) => ((p => ('not' p => q)) => (((p => q) =>
  p) => p)) in TAUT(A) by Lm11,Lm13;
  then
  p => ('not' p => q) in TAUT(A) & (p => ('not' p => q)) => (((p => q) => p)
  => p ) in TAUT(A) by CQC_THE1:43,46;
  hence thesis by CQC_THE1:46;
end;

Lm15: ((p => r) => s) => ((p => q) => ((q => r) => s)) in TAUT(A)
proof
  (p => q) => (((p => r) => s) => ((q => r) => s)) in TAUT(A) & ((p => q) =>
  (((p => r) => s) => ((q => r) => s))) => (((p => r) => s) => ((p => q) => ((q
  => r) => s))) in TAUT(A) by Lm3,Th8;
  hence thesis by CQC_THE1:46;
end;

Lm16: ((p => q) => r) => ((r => p) => p) in TAUT(A)
proof
  ((p => q) => p) => p in TAUT(A) & (((p => q) => p) => p) => (((p => q) => r
  ) => ((r => p) => p)) in TAUT(A) by Lm14,Lm15;
  hence thesis by CQC_THE1:46;
end;

Lm17: (((r => p) => p) => s) => (((p => q) => r) => s) in TAUT(A)
proof
  ((p => q) => r) => ((r => p) => p) in TAUT(A) & (((p => q) => r) => ((r =>
p) => p)) => ((((r => p) => p) => s) => (((p => q) => r) => s)) in TAUT(A)
by Lm16,Th1;
  hence thesis by CQC_THE1:46;
end;

Lm18: ((q => r) => p) => ((q => p) => p) in TAUT(A)
proof
  ((p => q) => q) => ((q => p) => p) in TAUT(A) & (((p => q) => q) => ((q =>
  p) => p)) => (((q => r) => p) => ((q => p) => p)) in TAUT(A) by Lm16,Lm17;
  hence thesis by CQC_THE1:46;
end;

theorem Th10:
  (q => (q => r)) => (q => r) in TAUT(A)
proof
  (q => r) => (q => r) in TAUT(A) & ((q => r) => (q => r)) => ((q => (q => r)
  ) => (q => r)) in TAUT(A) by Lm18,Th4;
  hence thesis by CQC_THE1:46;
end;

Lm19: (q => s) => (((q => r) => p) => ((s => p) => p)) in TAUT(A)
proof
  ((q => r) => p) => ((q => p) => p) in TAUT(A) & (((q => r) => p) => ((q =>
p) => p)) => ((q => s) => (((q => r) => p) => ((s => p) => p))) in TAUT(A)
by Lm4,Lm18;
  hence thesis by CQC_THE1:46;
end;

Lm20: ((q => r) => p) => ((q => s) => ((s => p) => p)) in TAUT(A)
proof
  (q => s) => (((q => r) => p) => ((s => p) => p)) in TAUT(A) & ((q => s) =>
  (((q => r) => p) => ((s => p) => p))) => (((q => r) => p) => ((q => s) => ((s
  => p) => p))) in TAUT(A) by Lm19,Th8;
  hence thesis by CQC_THE1:46;
end;

Lm21: (q => s) => ((s => (p => (q => r))) => (p => (q => r))) in TAUT(A)
proof
  (q => r) => (p => (q => r)) in TAUT(A) & ((q => r) => (p => (q => r))) => (
  (q => s) => ((s => (p => (q => r))) => (p => (q => r)))) in TAUT(A)
  by Lm20,Th5;
  hence thesis by CQC_THE1:46;
end;

Lm22: (s => (p => (q => r))) => ((q => s) => (p => (q => r))) in TAUT(A)
proof
  (q => s) => ((s => (p => (q => r))) => (p => (q => r))) in TAUT(A) & ((q =>
  s) => ((s => (p => (q => r))) => (p => (q => r)))) => ((s => (p => (q => r)))
  => ( (q => s) => (p => (q => r)))) in TAUT(A) by Lm21,Th8;
  hence thesis by CQC_THE1:46;
end;

theorem Th11:
  (p => (q => r)) => ((p => q) => (p => r)) in TAUT(A)
proof
  (q => r) => ((p => q) => (p => r)) in TAUT(A) & ((q => r) => ((p => q) => (
  p => r))) => ((p => (q => r)) => ((p => q) => (p => r))) in TAUT(A)
  by Lm22,Th9;
  hence thesis by CQC_THE1:46;
end;

theorem Th12:
  'not' VERUM(A) => p in TAUT(A)
proof
  VERUM(A) => ('not' VERUM(A) => p) in TAUT(A) by CQC_THE1:43;
  hence thesis by CQC_THE1:41,46;
end;

theorem Th13:
  q in TAUT(A) implies p => q in TAUT(A)
proof
  q => (p => q) in TAUT(A) by Th5;
  hence thesis by CQC_THE1:46;
end;

theorem
  p in TAUT(A) implies (p => q) => q in TAUT(A)
proof
  assume
A1: p in TAUT(A);
  p => ((p => q) => q) in TAUT(A) by Th7;
  hence thesis by A1,CQC_THE1:46;
end;

theorem Th15:
  s => (q => p) in TAUT(A) implies q => (s => p) in TAUT(A)
proof
  assume
A1: s => (q => p) in TAUT(A);
  (s => (q => p)) => (q => (s => p)) in TAUT(A) by Th8;
  hence thesis by A1,CQC_THE1:46;
end;

theorem Th16:
  s => (q => p) in TAUT(A) & q in TAUT(A) implies s => p in TAUT(A)
proof
  assume s => (q => p) in TAUT(A);
  then q => (s => p) in TAUT(A) by Th15;
  hence thesis by CQC_THE1:46;
end;

theorem
  s => (q => p) in TAUT(A) & q in TAUT(A) & s in TAUT(A) implies p in TAUT(A)
proof
  assume s => (q => p) in TAUT(A) & q in TAUT(A);
  then s => p in TAUT(A) by Th16;
  hence thesis by CQC_THE1:46;
end;

theorem
  q => (q => r) in TAUT(A) implies q => r in TAUT(A)
proof
  (q => (q => r)) => (q => r) in TAUT(A) by Th10;
  hence thesis by CQC_THE1:46;
end;

theorem Th19:
  (p => (q => r)) in TAUT(A) implies (p => q) => (p => r) in TAUT(A)
proof
  assume
A1: p => (q => r) in TAUT(A);
  (p => (q => r)) => ((p => q) => (p => r)) in TAUT(A) by Th11;
  hence thesis by A1,CQC_THE1:46;
end;

theorem Th20:
  (p => (q => r)) in TAUT(A) & p => q in TAUT(A) implies p => r in TAUT(A)
proof
  assume (p => (q => r)) in TAUT(A);
  then (p => q) => (p => r) in TAUT(A) by Th19;
  hence thesis by CQC_THE1:46;
end;

theorem
  (p => (q => r)) in TAUT(A) & p => q in TAUT(A) & p in TAUT(A) implies
  r in TAUT(A)
proof
  assume (p => (q => r)) in TAUT(A) & p => q in TAUT(A);
  then p => r in TAUT(A) by Th20;
  hence thesis by CQC_THE1:46;
end;

theorem Th22:
  p => (q => r) in TAUT(A) & p => (r => s ) in TAUT(A) implies
   p => (q => s) in TAUT(A)
proof
  assume that
A1: p => (q => r) in TAUT(A) and
A2: p => (r => s ) in TAUT(A);
  p => ((q => r) => ((r => s) => (q => s))) in TAUT(A) by Th1,Th13;
  then p => ((r => s) => (q => s)) in TAUT(A) by A1,Th20;
  hence thesis by A2,Th20;
end;

theorem
  p => VERUM(A) in TAUT(A) by Th13,CQC_THE1:41;

Lm23: 'not' p => (p => 'not' VERUM(A)) in TAUT(A)
proof
  p => ('not' p => 'not' VERUM(A)) in TAUT(A) by CQC_THE1:43;
  hence thesis by Th15;
end;

Lm24: ('not' p => 'not' VERUM(A)) => p in TAUT(A)
proof
  'not' p => ('not' VERUM(A) => p) in TAUT(A) &
('not' p => ('not' VERUM(A) => p))
  => ( ('not' p => 'not' VERUM(A)) => ('not' p => p)) in TAUT(A)
by Th11,Th12,Th13;
  then
A1: ('not' p => 'not' VERUM(A)) => ('not' p => p) in TAUT(A)
  by CQC_THE1:46;
  ('not' p => p) => p in TAUT(A) by CQC_THE1:42;
  hence thesis by A1,Th3;
end;

theorem Th24:
  ('not' p => 'not' q) => (q => p) in TAUT(A)
proof
  q => ('not' q => 'not' VERUM(A)) in TAUT(A) &
  ('not' q => 'not' VERUM(A)) => ((
  'not' p => 'not' q) => ('not' p => 'not' VERUM(A))) in TAUT(A)
  by Th9,CQC_THE1:43;
  then
A1: q => (('not' p => 'not' q) => ('not' p => 'not' VERUM(A))) in TAUT(A)
  by Th3;
  q => (('not' p => 'not' VERUM(A)) => p) in TAUT(A) by Lm24,Th13;
  then q => (('not' p => 'not' q) => p) in TAUT(A) by A1,Th22;
  hence thesis by Th15;
end;

theorem Th25:
  'not' 'not' p => p in TAUT(A)
proof
  'not' 'not' p => ('not' p => 'not' VERUM(A)) in TAUT(A) & ('not' p =>
'not'
  VERUM(A)) => (VERUM(A) => p) in TAUT(A) by Lm23,Th24;
  then 'not' 'not' p => (VERUM(A) => p) in TAUT(A) by Th3;
  then VERUM(A) => ('not' 'not' p => p) in TAUT(A) by Th15;
  hence thesis by CQC_THE1:41,46;
end;

Lm25: now
  let A,p;
  'not' 'not' p => p in TAUT(A) by Th25;
  then
A1: (p => 'not' VERUM(A)) => ('not' 'not' p => 'not' VERUM(A))
  in TAUT(A) by Th2;
  ('not' 'not' p => 'not' VERUM(A)) => 'not' p in TAUT(A) by Lm24;
  hence (p => 'not' VERUM(A)) => 'not' p in TAUT(A) by A1,Th3;
end;

theorem Th26:
  (p => q) => ('not' q => 'not' p) in TAUT(A)
proof
  'not' q => (q => 'not' VERUM(A)) in TAUT(A) &
(q => 'not' VERUM(A)) => ((p
=> q)
  => ( p => 'not' VERUM(A))) in TAUT(A) by Lm23,Th9;
  then
A1: 'not' q => ((p => q) => (p => 'not' VERUM(A))) in TAUT(A) by Th3;
  'not' q => ((p => 'not' VERUM(A)) => 'not' p) in TAUT(A) by Lm25,Th13;
  then 'not' q => ((p => q) => 'not' p) in TAUT(A) by A1,Th22;
  hence thesis by Th15;
end;

theorem Th27:
  p => 'not' 'not' p in TAUT(A)
proof
  (VERUM(A) => p) => ('not' p => 'not' VERUM(A)) in TAUT(A) &
('not' p => 'not'
  VERUM(A)) => 'not' 'not' p in TAUT(A) by Lm25,Th26;
  then
A1: (VERUM(A) => p) => 'not' 'not' p in TAUT(A) by Th3;
  p => (VERUM(A) => p) in TAUT(A) by Th5;
  hence thesis by A1,Th3;
end;

theorem Th28:
  ('not' 'not' p => q) => (p => q) in TAUT(A) & (p => q) => ('not'
  'not' p => q) in TAUT(A)
proof
  p => 'not' 'not' p in TAUT(A) by Th27;
  hence ('not' 'not' p => q) => (p => q) in TAUT(A) by Th2;
  'not' 'not' p => p in TAUT(A) by Th25;
  hence thesis by Th2;
end;

theorem Th29:
  (p => 'not' 'not' q) => (p => q) in TAUT(A) & (p => q) => (p =>
  'not' 'not' q) in TAUT(A)
proof
  (p => ('not' 'not' q => q)) => ((p => 'not' 'not' q) => (p => q)) in
  TAUT(A) & p => ('not' 'not' q => q) in TAUT(A) by Th11,Th13,Th25;
  hence (p => 'not' 'not' q) => (p => q) in TAUT(A) by CQC_THE1:46;
  (p => (q => 'not' 'not' q)) => ((p => q) => (p => 'not' 'not' q)) in
  TAUT(A) & p => (q => 'not' 'not' q) in TAUT(A) by Th11,Th13,Th27;
  hence thesis by CQC_THE1:46;
end;

theorem Th30:
  (p => 'not' q) => (q => 'not' p) in TAUT(A)
proof
  (p => 'not' q) => ('not' 'not' q => 'not' p) in TAUT(A) & ('not' 'not' q =>
  'not' p) => (q => 'not' p) in TAUT(A) by Th26,Th28;
  hence thesis by Th3;
end;

theorem Th31:
  ('not' p => q) => ('not' q => p) in TAUT(A)
proof
  ('not' p => q) => ('not' q => 'not' 'not' p) in TAUT(A) & ('not' q => 'not'
  'not' p) => ('not' q => p) in TAUT(A) by Th26,Th29;
  hence thesis by Th3;
end;

theorem
  (p => 'not' p) => 'not' p in TAUT(A)
proof
  ('not' 'not' p => 'not' p) => 'not' p in TAUT(A) & (p => 'not' p) => ('not'
  'not' p => 'not' p) in TAUT(A) by Th28,CQC_THE1:42;
  hence thesis by Th3;
end;

theorem
  'not' p => (p => q) in TAUT(A)
proof
  'not' p => ('not' 'not' p => q) in TAUT(A) & ('not' 'not' p => q) => (p =>
  q) in TAUT(A) by Th28,CQC_THE1:43;
  hence thesis by Th3;
end;

theorem Th34:
  p => q in TAUT(A) iff 'not' q => 'not' p in TAUT(A)
proof
  (p => q) => ('not' q => 'not' p) in TAUT(A) by Th26;
  hence p => q in TAUT(A) implies 'not' q => 'not' p in TAUT(A) by CQC_THE1:46;
  ('not' q => 'not' p) => (p => q) in TAUT(A) by Th24;
  hence 'not' q => 'not' p in TAUT(A) implies p => q in TAUT(A) by CQC_THE1:46;
end;

theorem
  'not' p => 'not' q in TAUT(A) implies q => p in TAUT(A) by Th34;

theorem
  p in TAUT(A) iff 'not' 'not' p in TAUT(A)
proof
  thus p in TAUT(A) implies 'not' 'not' p in TAUT(A)
  proof
    assume
A1: p in TAUT(A);
    p => 'not' 'not' p in TAUT(A) by Th27;
    hence thesis by A1,CQC_THE1:46;
  end;
  assume
A2: 'not' 'not' p in TAUT(A);
  'not' 'not' p => p in TAUT(A) by Th25;
  hence thesis by A2,CQC_THE1:46;
end;

theorem
  (p => q) in TAUT(A) iff (p => 'not' 'not' q) in TAUT(A)
proof
  thus (p => q) in TAUT(A) implies (p => 'not' 'not' q) in TAUT(A)
  proof
    assume
A1: p => q in TAUT(A);
    (p => q) => (p => 'not' 'not' q) in TAUT(A) by Th29;
    hence thesis by A1,CQC_THE1:46;
  end;
  assume
A2: p => 'not' 'not' q in TAUT(A);
  (p => 'not' 'not' q) => (p => q) in TAUT(A) by Th29;
  hence thesis by A2,CQC_THE1:46;
end;

theorem
  (p => q) in TAUT(A) iff ('not' 'not' p => q) in TAUT(A)
proof
  thus (p => q) in TAUT(A) implies ('not' 'not' p => q) in TAUT(A)
  proof
    assume
A1: p => q in TAUT(A);
    (p => q) => ('not' 'not' p => q) in TAUT(A) by Th28;
    hence thesis by A1,CQC_THE1:46;
  end;
  assume
A2: 'not' 'not' p => q in TAUT(A);
  ('not' 'not' p => q) => (p => q) in TAUT(A) by Th28;
  hence thesis by A2,CQC_THE1:46;
end;

theorem
  p => 'not' q in TAUT(A) implies q => 'not' p in TAUT(A)
proof
  assume
A1: p => 'not' q in TAUT(A);
  (p => 'not' q) => (q => 'not' p) in TAUT(A) by Th30;
  hence thesis by A1,CQC_THE1:46;
end;

theorem
  'not' p => q in TAUT(A) implies 'not' q => p in TAUT(A)
proof
  assume
A1: 'not' p => q in TAUT(A);
  ('not' p => q) => ('not' q => p) in TAUT(A) by Th31;
  hence thesis by A1,CQC_THE1:46;
end;

:: predykat |- i schematy konsekwencji

registration
  let A,p,q,r;
  cluster (p => q) => ((q => r) => (p => r)) -> valid;
coherence
by Th1;
end;

theorem
  p => q is valid implies (q => r) => (p => r) is valid
proof
  assume
A1: p => q is valid;
  (p => q) => ((q => r) => (p => r)) is valid;
  hence thesis by A1,CQC_THE1:65;
end;

theorem Th42:
  p => q is valid & q => r is valid implies p => r is valid
by Th3;

registration
  let A,p;
  cluster p => p -> valid;
coherence
by Th4;
end;

registration
  let A,p,q;
  cluster p => (q => p) -> valid;
coherence
by Th5;
end;

theorem
  p is valid implies q => p is valid
by Th13;

registration
  let A,p,q,s;
  cluster (s => (q => p)) => (q => (s => p)) -> valid;
coherence
by Th8;
end;

theorem Th44:
  p => (q => r) is valid implies q => (p => r) is valid
by Th15;

theorem
  p => (q => r) is valid & q is valid implies p => r is valid
proof
  assume p => (q => r) is valid;
  then q => (p => r) is valid by Th44;
  hence thesis by CQC_THE1:65;
end;

theorem
  p => VERUM(A) is valid & 'not' VERUM(A) => p is valid
by Th13,CQC_THE1:41,Th12;

registration
  let A,p,q;
  cluster p => ((p => q) => q) -> valid;
coherence
by Th7;
end;

registration
  let A,q,r;
  cluster (q => (q => r)) => (q => r) -> valid;
coherence
by Th10;
end;

theorem
  q => (q => r) is valid implies q => r is valid
proof
  assume
A1: q => (q => r) is valid;
  (q => (q => r)) => (q => r) is valid;
  hence thesis by A1,CQC_THE1:65;
end;

registration
  let A,p,q,r;
  cluster (p => (q => r)) => ((p => q) => (p => r)) -> valid;
coherence
by Th11;
end;

theorem Th48:
  p => (q => r) is valid implies (p => q) => (p => r) is valid
proof
  assume
A1: p => (q => r) is valid;
  (p => (q => r)) => ((p => q) => (p => r)) is valid;
  hence thesis by A1,CQC_THE1:65;
end;

theorem
  p => (q => r) is valid & p => q is valid implies p => r is valid
proof
  assume that
A1: p => (q => r) is valid and
A2: p => q is valid;
  (p => q) => (p => r) is valid by A1,Th48;
  hence thesis by A2,CQC_THE1:65;
end;

registration
  let A,p,q,r;
  cluster ((p => q) => r) => (q => r) -> valid;
coherence
by Th6;
end;

theorem
  (p => q) => r is valid implies q => r is valid
proof
  assume
A1: (p => q) => r is valid;
  ((p => q) => r) => (q => r) is valid;
  hence thesis by A1,CQC_THE1:65;
end;

registration
  let A,p,q,r;
  cluster (p => q) => ((r => p) => (r => q)) -> valid;
coherence
by Th9;
end;

theorem
  p => q is valid implies (r => p) => (r => q) is valid
proof
  assume
A1: p => q is valid;
  (p => q) => ((r => p) => (r => q)) is valid;
  hence thesis by A1,CQC_THE1:65;
end;

registration
  let A,p,q;
  cluster (p => q) => ('not' q => 'not' p) -> valid;
coherence
by Th26;
end;

registration
  let A,p,q;
  cluster ('not' p => 'not' q) => (q => p) ->  valid;
coherence
by Th24;
end;

theorem
  'not' p => 'not' q is valid iff q => p is valid
proof
  thus 'not' p => 'not' q is valid implies q => p is valid
  proof
    assume
A1: 'not' p => 'not' q is valid;
    ('not' p => 'not' q) => (q => p) is valid;
    hence thesis by A1,CQC_THE1:65;
  end;
  assume
A2: q => p is valid;
  (q => p) => ('not' p => 'not' q) is valid;
  hence thesis by A2,CQC_THE1:65;
end;

registration
  let A,p;
  cluster p => 'not' 'not' p -> valid;
coherence
by Th27;
end;

registration
  let A,p;
  cluster 'not' 'not' p => p -> valid;
coherence
by Th25;
end;

theorem
  'not' 'not' p is valid iff p is valid
proof
  thus 'not' 'not' p is valid implies p is valid
  proof
    assume
A1: 'not' 'not' p is valid;
    'not' 'not' p => p is valid;
    hence thesis by A1,CQC_THE1:65;
  end;
  assume
A2: p is valid;
  p => 'not' 'not' p is valid;
  hence thesis by A2,CQC_THE1:65;
end;

registration
  let A,p,q;
  cluster ('not' 'not' p => q) => (p => q) -> valid;
coherence
by Th28;
end;

theorem
  'not' 'not' p => q is valid iff p => q is valid
proof
  thus 'not' 'not' p => q is valid implies p => q is valid
  proof
    assume
A1: 'not' 'not' p => q is valid;
    ('not' 'not' p => q) => (p => q) is valid;
    hence thesis by A1,CQC_THE1:65;
  end;
  assume
A2: p => q is valid;
  'not' 'not' p => p is valid;
  hence thesis by A2,Th42;
end;

registration
  let A,p,q;
  cluster (p => 'not' 'not' q) => (p => q) -> valid;
coherence
by Th29;
end;

theorem
  p => 'not' 'not' q is valid iff p => q is valid
proof
  thus p => 'not' 'not' q is valid implies p => q is valid
  proof
    assume
A1: p => 'not' 'not' q is valid;
    (p => 'not' 'not' q) => (p => q) is valid;
    hence thesis by A1,CQC_THE1:65;
  end;
  assume
A2: p => q is valid;
  q => 'not' 'not' q is valid;
  hence thesis by A2,Th42;
end;

registration
  let A,p,q;
  cluster (p => 'not' q) => (q => 'not' p) -> valid;
coherence
by Th30;
end;

theorem
  p => 'not' q is valid implies q => 'not' p is valid
proof
  assume
A1: p => 'not' q is valid;
  (p => 'not' q) => (q => 'not' p) is valid;
  hence thesis by A1,CQC_THE1:65;
end;

registration
  let A,p,q;
  cluster ('not' p => q) => ('not' q => p) -> valid;
coherence
by Th31;
end;

theorem
  'not' p => q is valid implies 'not' q => p is valid
proof
  assume
A1: 'not' p => q is valid;
  ('not' p => q) => ('not' q => p) is valid;
  hence thesis by A1,CQC_THE1:65;
end;

theorem
  X|- p => q implies X|- (q => r) => (p => r)
proof
  assume
A1: X|- p => q;
  X|- (p => q) => ((q => r) => (p => r)) by CQC_THE1:59;
  hence thesis by A1,CQC_THE1:55;
end;

theorem Th59:
  X|- p => q & X|- q => r implies X|- p => r
proof
  assume that
A1: X|- p => q and
A2: X|- q => r;
  X|- (p => q) => ((q => r) => (p => r)) by CQC_THE1:59;
  then X|- (q => r) => (p => r) by A1,CQC_THE1:55;
  hence thesis by A2,CQC_THE1:55;
end;

theorem
  X|- p => p by CQC_THE1:59;

theorem
  X|- p implies X|- q => p
proof
  assume
A1: X|- p;
  X|- p => (q => p) by CQC_THE1:59;
  hence thesis by A1,CQC_THE1:55;
end;

theorem
  X |- p implies X |- (p => q) => q
proof
  assume
A1: X |- p;
  X |- p => ((p => q) => q) by CQC_THE1:59;
  hence thesis by A1,CQC_THE1:55;
end;

theorem Th63:
  X |- p => (q => r) implies X |- q => (p => r)
proof
  assume
A1: X |- p => (q => r);
  X|- (p => (q => r)) => (q => (p => r)) by CQC_THE1:59;
  hence thesis by A1,CQC_THE1:55;
end;

theorem
  X |- p => (q => r) & X |- q implies X |- p => r
proof
  assume X |- p => (q => r);
  then X |- q => (p => r) by Th63;
  hence thesis by CQC_THE1:55;
end;

theorem
  X |- p => (p => q) implies X |- p => q
proof
  assume
A1: X |- p => (p => q);
  X|- (p => (p => q)) => (p => q) by CQC_THE1:59;
  hence thesis by A1,CQC_THE1:55;
end;

theorem
  X |- (p => q) => r implies X |- q => r
proof
  assume
A1: X |- (p => q) => r;
  X|- ((p => q) => r) => (q => r) by CQC_THE1:59;
  hence thesis by A1,CQC_THE1:55;
end;

theorem Th67:
  X |- p => (q => r) implies X |- (p => q) => (p =>r)
proof
  assume
A1: X|- p => (q => r);
  X |- (p => (q => r)) => ((p => q) => (p =>r)) by CQC_THE1:59;
  hence thesis by A1,CQC_THE1:55;
end;

theorem
  X |- p => (q => r) & X|- p => q implies X |- p => r
proof
  assume X|- p => (q => r);
  then X |- (p => q) => (p =>r) by Th67;
  hence thesis by CQC_THE1:55;
end;

theorem
  X|- 'not' p => 'not' q iff X|- q => p
proof
  thus X|- 'not' p => 'not' q implies X|- q => p
  proof
    assume
A1: X|- 'not' p => 'not' q;
    X|- ('not' p => 'not' q) => (q => p) by CQC_THE1:59;
    hence thesis by A1,CQC_THE1:55;
  end;
  assume
A2: X|- q => p;
  X|- (q => p) => ('not' p => 'not' q) by CQC_THE1:59;
  hence thesis by A2,CQC_THE1:55;
end;

theorem
  X|- 'not' 'not' p iff X|- p
proof
  thus X|- 'not' 'not' p implies X|- p
  proof
    assume
A1: X|- 'not' 'not' p;
    X|- 'not' 'not' p => p by CQC_THE1:59;
    hence thesis by A1,CQC_THE1:55;
  end;
  assume
A2: X|- p;
  X|- p => 'not' 'not' p by CQC_THE1:59;
  hence thesis by A2,CQC_THE1:55;
end;

theorem
  X|- p => 'not' 'not' q iff X|- p => q
proof
  thus X|- p => 'not' 'not' q implies X|- p => q
  proof
    assume
A1: X|- p => 'not' 'not' q;
    X|- (p => 'not' 'not' q) => (p => q) by CQC_THE1:59;
    hence thesis by A1,CQC_THE1:55;
  end;
  assume
A2: X|- p => q;
  X|- q => 'not' 'not' q by CQC_THE1:59;
  hence thesis by A2,Th59;
end;

theorem
  X|- 'not' 'not' p => q iff X|- p => q
proof
  thus X|- 'not' 'not' p => q implies X|- p => q
  proof
    assume
A1: X|- 'not' 'not' p => q;
    X|- ('not' 'not' p => q) => (p => q) by CQC_THE1:59;
    hence thesis by A1,CQC_THE1:55;
  end;
  assume
A2: X|- p => q;
  X|- 'not' 'not' p => p by CQC_THE1:59;
  hence thesis by A2,Th59;
end;

theorem Th73:
  X|- p => 'not' q implies X|- q => 'not' p
proof
  assume
A1: X|- p => 'not' q;
  X|- (p => 'not' q) => (q => 'not' p) by CQC_THE1:59;
  hence thesis by A1,CQC_THE1:55;
end;

theorem Th74:
  X|- 'not' p => q implies X|- 'not' q => p
proof
  assume
A1: X|- 'not' p => q;
  X|- ('not' p => q) => ('not' q => p) by CQC_THE1:59;
  hence thesis by A1,CQC_THE1:55;
end;

theorem
  X|- p => 'not' q & X |- q implies X|- 'not' p
proof
  assume X|- p => 'not' q;
  then X |- q => 'not' p by Th73;
  hence thesis by CQC_THE1:55;
end;

theorem
  X|- 'not' p => q & X |- 'not' q implies X|- p
proof
  assume X|- 'not' p => q;
  then X |- 'not' q => p by Th74;
  hence thesis by CQC_THE1:55;
end;