:: by Agata Darmochwa{\l}

::

:: Received May 25, 1990

:: Copyright (c) 1990-2016 Association of Mizar Users

definition

let Al be QC-alphabet ;

let T be Subset of (CQC-WFF Al);

end;
let T be Subset of (CQC-WFF Al);

attr T is being_a_theory means :: CQC_THE1:def 1

( VERUM Al in T & ( for p, q, r being Element of CQC-WFF Al

for s being QC-formula of Al

for x, y being bound_QC-variable of Al holds

( (('not' p) => p) => p in T & p => (('not' p) => q) in T & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T & (p '&' q) => (q '&' p) in T & ( p in T & p => q in T implies q in T ) & (All (x,p)) => p in T & ( p => q in T & not x in still_not-bound_in p implies p => (All (x,q)) in T ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T implies s . y in T ) ) ) );

( VERUM Al in T & ( for p, q, r being Element of CQC-WFF Al

for s being QC-formula of Al

for x, y being bound_QC-variable of Al holds

( (('not' p) => p) => p in T & p => (('not' p) => q) in T & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T & (p '&' q) => (q '&' p) in T & ( p in T & p => q in T implies q in T ) & (All (x,p)) => p in T & ( p => q in T & not x in still_not-bound_in p implies p => (All (x,q)) in T ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T implies s . y in T ) ) ) );

:: deftheorem defines being_a_theory CQC_THE1:def 1 :

for Al being QC-alphabet

for T being Subset of (CQC-WFF Al) holds

( T is being_a_theory iff ( VERUM Al in T & ( for p, q, r being Element of CQC-WFF Al

for s being QC-formula of Al

for x, y being bound_QC-variable of Al holds

( (('not' p) => p) => p in T & p => (('not' p) => q) in T & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T & (p '&' q) => (q '&' p) in T & ( p in T & p => q in T implies q in T ) & (All (x,p)) => p in T & ( p => q in T & not x in still_not-bound_in p implies p => (All (x,q)) in T ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T implies s . y in T ) ) ) ) );

for Al being QC-alphabet

for T being Subset of (CQC-WFF Al) holds

( T is being_a_theory iff ( VERUM Al in T & ( for p, q, r being Element of CQC-WFF Al

for s being QC-formula of Al

for x, y being bound_QC-variable of Al holds

( (('not' p) => p) => p in T & p => (('not' p) => q) in T & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T & (p '&' q) => (q '&' p) in T & ( p in T & p => q in T implies q in T ) & (All (x,p)) => p in T & ( p => q in T & not x in still_not-bound_in p implies p => (All (x,q)) in T ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T implies s . y in T ) ) ) ) );

::$CT 4

theorem :: CQC_THE1:5

for Al being QC-alphabet

for T, S being Subset of (CQC-WFF Al) st T is being_a_theory & S is being_a_theory holds

T /\ S is being_a_theory

for T, S being Subset of (CQC-WFF Al) st T is being_a_theory & S is being_a_theory holds

T /\ S is being_a_theory

proof end;

:: --------- The consequence operation

definition

let Al be QC-alphabet ;

let X be Subset of (CQC-WFF Al);

ex b_{1} being Subset of (CQC-WFF Al) st

for t being Element of CQC-WFF Al holds

( t in b_{1} iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds

t in T )

for b_{1}, b_{2} being Subset of (CQC-WFF Al) st ( for t being Element of CQC-WFF Al holds

( t in b_{1} iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds

t in T ) ) & ( for t being Element of CQC-WFF Al holds

( t in b_{2} iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds

t in T ) ) holds

b_{1} = b_{2}

end;
let X be Subset of (CQC-WFF Al);

func Cn X -> Subset of (CQC-WFF Al) means :Def2: :: CQC_THE1:def 2

for t being Element of CQC-WFF Al holds

( t in it iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds

t in T );

existence for t being Element of CQC-WFF Al holds

( t in it iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds

t in T );

ex b

for t being Element of CQC-WFF Al holds

( t in b

t in T )

proof end;

uniqueness for b

( t in b

t in T ) ) & ( for t being Element of CQC-WFF Al holds

( t in b

t in T ) ) holds

b

proof end;

:: deftheorem Def2 defines Cn CQC_THE1:def 2 :

for Al being QC-alphabet

for X, b_{3} being Subset of (CQC-WFF Al) holds

( b_{3} = Cn X iff for t being Element of CQC-WFF Al holds

( t in b_{3} iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds

t in T ) );

for Al being QC-alphabet

for X, b

( b

( t in b

t in T ) );

theorem Th3: :: CQC_THE1:7

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al holds (('not' p) => p) => p in Cn X

for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al holds (('not' p) => p) => p in Cn X

proof end;

theorem Th4: :: CQC_THE1:8

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for p, q being Element of CQC-WFF Al holds p => (('not' p) => q) in Cn X

for X being Subset of (CQC-WFF Al)

for p, q being Element of CQC-WFF Al holds p => (('not' p) => q) in Cn X

proof end;

theorem Th5: :: CQC_THE1:9

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for p, q, r being Element of CQC-WFF Al holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X

for X being Subset of (CQC-WFF Al)

for p, q, r being Element of CQC-WFF Al holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X

proof end;

theorem Th6: :: CQC_THE1:10

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for p, q being Element of CQC-WFF Al holds (p '&' q) => (q '&' p) in Cn X

for X being Subset of (CQC-WFF Al)

for p, q being Element of CQC-WFF Al holds (p '&' q) => (q '&' p) in Cn X

proof end;

theorem Th7: :: CQC_THE1:11

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for p, q being Element of CQC-WFF Al st p in Cn X & p => q in Cn X holds

q in Cn X

for X being Subset of (CQC-WFF Al)

for p, q being Element of CQC-WFF Al st p in Cn X & p => q in Cn X holds

q in Cn X

proof end;

theorem Th8: :: CQC_THE1:12

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds (All (x,p)) => p in Cn X

for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds (All (x,p)) => p in Cn X

proof end;

theorem Th9: :: CQC_THE1:13

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for p, q being Element of CQC-WFF Al

for x being bound_QC-variable of Al st p => q in Cn X & not x in still_not-bound_in p holds

p => (All (x,q)) in Cn X

for X being Subset of (CQC-WFF Al)

for p, q being Element of CQC-WFF Al

for x being bound_QC-variable of Al st p => q in Cn X & not x in still_not-bound_in p holds

p => (All (x,q)) in Cn X

proof end;

theorem Th10: :: CQC_THE1:14

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for s being QC-formula of Al

for x, y being bound_QC-variable of Al st s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Cn X holds

s . y in Cn X

for X being Subset of (CQC-WFF Al)

for s being QC-formula of Al

for x, y being bound_QC-variable of Al st s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Cn X holds

s . y in Cn X

proof end;

theorem Th12: :: CQC_THE1:16

for Al being QC-alphabet

for T, X being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds

Cn X c= T by Def2;

for T, X being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds

Cn X c= T by Def2;

Lm1: for Al being QC-alphabet

for X being Subset of (CQC-WFF Al) holds Cn (Cn X) c= Cn X

proof end;

theorem :: CQC_THE1:19

theorem Th16: :: CQC_THE1:20

for Al being QC-alphabet

for T being Subset of (CQC-WFF Al) holds

( T is being_a_theory iff Cn T = T )

for T being Subset of (CQC-WFF Al) holds

( T is being_a_theory iff Cn T = T )

proof end;

:: ---------- The notion of proof

:: deftheorem defines Proof_Step_Kinds CQC_THE1:def 3 :

Proof_Step_Kinds = { k where k is Nat : k <= 9 } ;

Proof_Step_Kinds = { k where k is Nat : k <= 9 } ;

registration
end;

theorem Th19: :: CQC_THE1:23

for Al being QC-alphabet

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]

for n being Nat st 1 <= n & n <= len f holds

not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]

for n being Nat st 1 <= n & n <= len f holds

not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9

proof end;

definition

let Al be QC-alphabet ;

let PR be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:];

let n be Nat;

let X be Subset of (CQC-WFF Al);

( ( (PR . n) `2 = 0 & (PR . n) `2 = 1 implies ( (PR . n) `1 in X iff (PR . n) `1 = VERUM Al ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 2 implies ( (PR . n) `1 in X iff ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 3 implies ( (PR . n) `1 in X iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 4 implies ( (PR . n) `1 in X iff ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 5 implies ( (PR . n) `1 in X iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 6 implies ( (PR . n) `1 in X iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 7 implies ( (PR . n) `1 in X iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 8 implies ( (PR . n) `1 in X iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 9 implies ( (PR . n) `1 in X iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 2 implies ( (PR . n) `1 = VERUM Al iff ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 3 implies ( (PR . n) `1 = VERUM Al iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 4 implies ( (PR . n) `1 = VERUM Al iff ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 5 implies ( (PR . n) `1 = VERUM Al iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 6 implies ( (PR . n) `1 = VERUM Al iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 7 implies ( (PR . n) `1 = VERUM Al iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 8 implies ( (PR . n) `1 = VERUM Al iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 9 implies ( (PR . n) `1 = VERUM Al iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 3 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 4 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 5 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 6 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 7 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 8 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 9 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 4 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 5 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 6 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 7 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 8 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 9 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 5 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 6 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 7 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 8 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 9 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 6 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 7 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 8 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 9 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 7 implies ( ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 8 implies ( ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 9 implies ( ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 8 implies ( ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 9 implies ( ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 8 & (PR . n) `2 = 9 implies ( ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) ) ;

end;
let PR be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:];

let n be Nat;

let X be Subset of (CQC-WFF Al);

pred PR,n is_a_correct_step_wrt X means :Def4: :: CQC_THE1:def 4

(PR . n) `1 in X if (PR . n) `2 = 0

(PR . n) `1 = VERUM Al if (PR . n) `2 = 1

ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p if (PR . n) `2 = 2

ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) if (PR . n) `2 = 3

ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) if (PR . n) `2 = 4

ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) if (PR . n) `2 = 5

ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p if (PR . n) `2 = 6

ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) if (PR . n) `2 = 7

ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) if (PR . n) `2 = 8

ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) if (PR . n) `2 = 9

;

consistency (PR . n) `1 in X if (PR . n) `2 = 0

(PR . n) `1 = VERUM Al if (PR . n) `2 = 1

ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p if (PR . n) `2 = 2

ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) if (PR . n) `2 = 3

ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) if (PR . n) `2 = 4

ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) if (PR . n) `2 = 5

ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p if (PR . n) `2 = 6

ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) if (PR . n) `2 = 7

ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) if (PR . n) `2 = 8

ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) if (PR . n) `2 = 9

;

( ( (PR . n) `2 = 0 & (PR . n) `2 = 1 implies ( (PR . n) `1 in X iff (PR . n) `1 = VERUM Al ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 2 implies ( (PR . n) `1 in X iff ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 3 implies ( (PR . n) `1 in X iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 4 implies ( (PR . n) `1 in X iff ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 5 implies ( (PR . n) `1 in X iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 6 implies ( (PR . n) `1 in X iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 7 implies ( (PR . n) `1 in X iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 8 implies ( (PR . n) `1 in X iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 9 implies ( (PR . n) `1 in X iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 2 implies ( (PR . n) `1 = VERUM Al iff ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 3 implies ( (PR . n) `1 = VERUM Al iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 4 implies ( (PR . n) `1 = VERUM Al iff ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 5 implies ( (PR . n) `1 = VERUM Al iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 6 implies ( (PR . n) `1 = VERUM Al iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 7 implies ( (PR . n) `1 = VERUM Al iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 8 implies ( (PR . n) `1 = VERUM Al iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 9 implies ( (PR . n) `1 = VERUM Al iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 3 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 4 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 5 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 6 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 7 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 8 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 9 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 4 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 5 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 6 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 7 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 8 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 9 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 5 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 6 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 7 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 8 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 9 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 6 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 7 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 8 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 9 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 7 implies ( ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 8 implies ( ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 9 implies ( ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 8 implies ( ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 9 implies ( ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 8 & (PR . n) `2 = 9 implies ( ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) ) ;

:: deftheorem Def4 defines is_a_correct_step_wrt CQC_THE1:def 4 :

for Al being QC-alphabet

for PR being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]

for n being Nat

for X being Subset of (CQC-WFF Al) holds

( ( (PR . n) `2 = 0 implies ( PR,n is_a_correct_step_wrt X iff (PR . n) `1 in X ) ) & ( (PR . n) `2 = 1 implies ( PR,n is_a_correct_step_wrt X iff (PR . n) `1 = VERUM Al ) ) & ( (PR . n) `2 = 2 implies ( PR,n is_a_correct_step_wrt X iff ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p ) ) & ( (PR . n) `2 = 3 implies ( PR,n is_a_correct_step_wrt X iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 4 implies ( PR,n is_a_correct_step_wrt X iff ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 5 implies ( PR,n is_a_correct_step_wrt X iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 6 implies ( PR,n is_a_correct_step_wrt X iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 7 implies ( PR,n is_a_correct_step_wrt X iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 8 implies ( PR,n is_a_correct_step_wrt X iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 9 implies ( PR,n is_a_correct_step_wrt X iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) );

for Al being QC-alphabet

for PR being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]

for n being Nat

for X being Subset of (CQC-WFF Al) holds

( ( (PR . n) `2 = 0 implies ( PR,n is_a_correct_step_wrt X iff (PR . n) `1 in X ) ) & ( (PR . n) `2 = 1 implies ( PR,n is_a_correct_step_wrt X iff (PR . n) `1 = VERUM Al ) ) & ( (PR . n) `2 = 2 implies ( PR,n is_a_correct_step_wrt X iff ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p ) ) & ( (PR . n) `2 = 3 implies ( PR,n is_a_correct_step_wrt X iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 4 implies ( PR,n is_a_correct_step_wrt X iff ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 5 implies ( PR,n is_a_correct_step_wrt X iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 6 implies ( PR,n is_a_correct_step_wrt X iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 7 implies ( PR,n is_a_correct_step_wrt X iff ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 8 implies ( PR,n is_a_correct_step_wrt X iff ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 9 implies ( PR,n is_a_correct_step_wrt X iff ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) );

definition

let Al be QC-alphabet ;

let X be Subset of (CQC-WFF Al);

let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:];

end;
let X be Subset of (CQC-WFF Al);

let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:];

pred f is_a_proof_wrt X means :: CQC_THE1:def 5

( f <> {} & ( for n being Nat st 1 <= n & n <= len f holds

f,n is_a_correct_step_wrt X ) );

( f <> {} & ( for n being Nat st 1 <= n & n <= len f holds

f,n is_a_correct_step_wrt X ) );

:: deftheorem defines is_a_proof_wrt CQC_THE1:def 5 :

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] holds

( f is_a_proof_wrt X iff ( f <> {} & ( for n being Nat st 1 <= n & n <= len f holds

f,n is_a_correct_step_wrt X ) ) );

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] holds

( f is_a_proof_wrt X iff ( f <> {} & ( for n being Nat st 1 <= n & n <= len f holds

f,n is_a_correct_step_wrt X ) ) );

theorem :: CQC_THE1:24

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds

rng f <> {} by RELAT_1:41;

for X being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds

rng f <> {} by RELAT_1:41;

theorem Th21: :: CQC_THE1:25

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds

1 <= len f

for X being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds

1 <= len f

proof end;

theorem :: CQC_THE1:26

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds

not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 6

for X being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds

not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 6

proof end;

theorem Th23: :: CQC_THE1:27

for Al being QC-alphabet

for n being Nat

for X being Subset of (CQC-WFF Al)

for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len f holds

( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X )

for n being Nat

for X being Subset of (CQC-WFF Al)

for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len f holds

( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X )

proof end;

theorem Th24: :: CQC_THE1:28

for Al being QC-alphabet

for n being Nat

for X being Subset of (CQC-WFF Al)

for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt X holds

f ^ g,n + (len f) is_a_correct_step_wrt X

for n being Nat

for X being Subset of (CQC-WFF Al)

for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt X holds

f ^ g,n + (len f) is_a_correct_step_wrt X

proof end;

theorem Th25: :: CQC_THE1:29

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & g is_a_proof_wrt X holds

f ^ g is_a_proof_wrt X

for X being Subset of (CQC-WFF Al)

for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & g is_a_proof_wrt X holds

f ^ g is_a_proof_wrt X

proof end;

theorem :: CQC_THE1:30

for Al being QC-alphabet

for X, Y being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & X c= Y holds

f is_a_proof_wrt Y

for X, Y being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & X c= Y holds

f is_a_proof_wrt Y

proof end;

theorem Th27: :: CQC_THE1:31

for Al being QC-alphabet

for l being Nat

for X being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & 1 <= l & l <= len f holds

(f . l) `1 in Cn X

for l being Nat

for X being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & 1 <= l & l <= len f holds

(f . l) `1 in Cn X

proof end;

definition

let Al be QC-alphabet ;

let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:];

assume A1: f <> {} ;

coherence

(f . (len f)) `1 is Element of CQC-WFF Al

end;
let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:];

assume A1: f <> {} ;

coherence

(f . (len f)) `1 is Element of CQC-WFF Al

proof end;

:: deftheorem Def6 defines Effect CQC_THE1:def 6 :

for Al being QC-alphabet

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f <> {} holds

Effect f = (f . (len f)) `1 ;

for Al being QC-alphabet

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f <> {} holds

Effect f = (f . (len f)) `1 ;

theorem Th28: :: CQC_THE1:32

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds

Effect f in Cn X

for X being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds

Effect f in Cn X

proof end;

Lm2: for Al being QC-alphabet

for X being Subset of (CQC-WFF Al) holds { p where p is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) } c= CQC-WFF Al

proof end;

theorem Th29: :: CQC_THE1:33

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al) holds X c= { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) }

for X being Subset of (CQC-WFF Al) holds X c= { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) }

proof end;

Lm3: for Al being QC-alphabet

for X being Subset of (CQC-WFF Al) holds VERUM Al in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) }

proof end;

Lm4: for Al being QC-alphabet

for p being Element of CQC-WFF Al

for X being Subset of (CQC-WFF Al) holds (('not' p) => p) => p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) }

proof end;

Lm5: for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for X being Subset of (CQC-WFF Al) holds p => (('not' p) => q) in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) }

proof end;

Lm6: for Al being QC-alphabet

for p, q, r being Element of CQC-WFF Al

for X being Subset of (CQC-WFF Al) holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) }

proof end;

Lm7: for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for X being Subset of (CQC-WFF Al) holds (p '&' q) => (q '&' p) in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) }

proof end;

Lm8: for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for X being Subset of (CQC-WFF Al) st p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } & p => q in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = G ) } holds

q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = H ) }

proof end;

Lm9: for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for X being Subset of (CQC-WFF Al) holds (All (x,p)) => p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) }

proof end;

Lm10: for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for X being Subset of (CQC-WFF Al) st p => q in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } & not x in still_not-bound_in p holds

p => (All (x,q)) in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = G ) }

proof end;

Lm11: for Al being QC-alphabet

for s being QC-formula of Al

for x, y being bound_QC-variable of Al

for X being Subset of (CQC-WFF Al) st s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } holds

s . y in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = G ) }

proof end;

theorem Th30: :: CQC_THE1:34

for Al being QC-alphabet

for Y, X being Subset of (CQC-WFF Al) st Y = { p where p is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) } holds

Y is being_a_theory by Lm3, Lm4, Lm5, Lm6, Lm7, Lm8, Lm9, Lm10, Lm11;

for Y, X being Subset of (CQC-WFF Al) st Y = { p where p is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) } holds

Y is being_a_theory by Lm3, Lm4, Lm5, Lm6, Lm7, Lm8, Lm9, Lm10, Lm11;

Lm12: for Al being QC-alphabet

for X being Subset of (CQC-WFF Al) holds { p where p is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) } c= Cn X

proof end;

theorem Th31: :: CQC_THE1:35

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al) holds { p where p is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) } = Cn X

for X being Subset of (CQC-WFF Al) holds { p where p is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) } = Cn X

proof end;

theorem Th32: :: CQC_THE1:36

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al holds

( p in Cn X iff ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) )

for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al holds

( p in Cn X iff ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) )

proof end;

theorem :: CQC_THE1:37

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al st p in Cn X holds

ex Y being Subset of (CQC-WFF Al) st

( Y c= X & Y is finite & p in Cn Y )

for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al st p in Cn X holds

ex Y being Subset of (CQC-WFF Al) st

( Y c= X & Y is finite & p in Cn Y )

proof end;

:: --------- TAUT(Al) - the set of all tautologies

definition
end;

:: deftheorem defines TAUT CQC_THE1:def 7 :

for Al being QC-alphabet holds TAUT Al = Cn ({} (CQC-WFF Al));

for Al being QC-alphabet holds TAUT Al = Cn ({} (CQC-WFF Al));

theorem Th34: :: CQC_THE1:38

for Al being QC-alphabet

for T being Subset of (CQC-WFF Al) st T is being_a_theory holds

TAUT Al c= T

for T being Subset of (CQC-WFF Al) st T is being_a_theory holds

TAUT Al c= T

proof end;

theorem :: CQC_THE1:39

theorem :: CQC_THE1:43

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al holds p => (('not' p) => q) in TAUT Al

for p, q being Element of CQC-WFF Al holds p => (('not' p) => q) in TAUT Al

proof end;

theorem :: CQC_THE1:44

for Al being QC-alphabet

for p, q, r being Element of CQC-WFF Al holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in TAUT Al

for p, q, r being Element of CQC-WFF Al holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in TAUT Al

proof end;

theorem :: CQC_THE1:45

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al holds (p '&' q) => (q '&' p) in TAUT Al

for p, q being Element of CQC-WFF Al holds (p '&' q) => (q '&' p) in TAUT Al

proof end;

theorem :: CQC_THE1:46

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al st p in TAUT Al & p => q in TAUT Al holds

q in TAUT Al

for p, q being Element of CQC-WFF Al st p in TAUT Al & p => q in TAUT Al holds

q in TAUT Al

proof end;

theorem :: CQC_THE1:47

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds (All (x,p)) => p in TAUT Al by Th8;

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds (All (x,p)) => p in TAUT Al by Th8;

theorem :: CQC_THE1:48

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for x being bound_QC-variable of Al st p => q in TAUT Al & not x in still_not-bound_in p holds

p => (All (x,q)) in TAUT Al by Th9;

for p, q being Element of CQC-WFF Al

for x being bound_QC-variable of Al st p => q in TAUT Al & not x in still_not-bound_in p holds

p => (All (x,q)) in TAUT Al by Th9;

theorem :: CQC_THE1:49

for Al being QC-alphabet

for s being QC-formula of Al

for x, y being bound_QC-variable of Al st s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in TAUT Al holds

s . y in TAUT Al by Th10;

for s being QC-formula of Al

for x, y being bound_QC-variable of Al st s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in TAUT Al holds

s . y in TAUT Al by Th10;

:: --------- Relation of consequence of a set of formulas

:: deftheorem Def8 defines |- CQC_THE1:def 8 :

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for s being QC-formula of Al holds

( X |- s iff s in Cn X );

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for s being QC-formula of Al holds

( X |- s iff s in Cn X );

theorem :: CQC_THE1:50

theorem :: CQC_THE1:51

theorem :: CQC_THE1:52

theorem :: CQC_THE1:53

theorem :: CQC_THE1:54

theorem :: CQC_THE1:55

theorem :: CQC_THE1:56

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds X |- (All (x,p)) => p by Th8;

for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds X |- (All (x,p)) => p by Th8;

theorem :: CQC_THE1:57

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for p, q being Element of CQC-WFF Al

for x being bound_QC-variable of Al st X |- p => q & not x in still_not-bound_in p holds

X |- p => (All (x,q)) by Th9;

for X being Subset of (CQC-WFF Al)

for p, q being Element of CQC-WFF Al

for x being bound_QC-variable of Al st X |- p => q & not x in still_not-bound_in p holds

X |- p => (All (x,q)) by Th9;

theorem :: CQC_THE1:58

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for s being QC-formula of Al

for x, y being bound_QC-variable of Al st s . y in CQC-WFF Al & not x in still_not-bound_in s & X |- s . x holds

X |- s . y by Th10;

for X being Subset of (CQC-WFF Al)

for s being QC-formula of Al

for x, y being bound_QC-variable of Al st s . y in CQC-WFF Al & not x in still_not-bound_in s & X |- s . x holds

X |- s . y by Th10;

:: deftheorem defines valid CQC_THE1:def 9 :

for Al being QC-alphabet

for s being QC-formula of Al holds

( s is valid iff {} (CQC-WFF Al) |- s );

for Al being QC-alphabet

for s being QC-formula of Al holds

( s is valid iff {} (CQC-WFF Al) |- s );

definition

let Al be QC-alphabet ;

let s be QC-formula of Al;

compatibility

( s is valid iff s in TAUT Al ) by Def8;

end;
let s be QC-formula of Al;

compatibility

( s is valid iff s in TAUT Al ) by Def8;

:: deftheorem defines valid CQC_THE1:def 10 :

for Al being QC-alphabet

for s being QC-formula of Al holds

( s is valid iff s in TAUT Al );

for Al being QC-alphabet

for s being QC-formula of Al holds

( s is valid iff s in TAUT Al );

theorem :: CQC_THE1:59

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al st p is valid holds

X |- p

for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al st p is valid holds

X |- p

proof end;

theorem :: CQC_THE1:63

for Al being QC-alphabet

for p, q, r being Element of CQC-WFF Al holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) is valid

for p, q, r being Element of CQC-WFF Al holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) is valid

proof end;

theorem :: CQC_THE1:65

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al st p is valid & p => q is valid holds

q is valid

for p, q being Element of CQC-WFF Al st p is valid & p => q is valid holds

q is valid

proof end;

theorem :: CQC_THE1:66

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds (All (x,p)) => p is valid by Th8;

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds (All (x,p)) => p is valid by Th8;

theorem :: CQC_THE1:67

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for x being bound_QC-variable of Al st p => q is valid & not x in still_not-bound_in p holds

p => (All (x,q)) is valid by Th9;

for p, q being Element of CQC-WFF Al

for x being bound_QC-variable of Al st p => q is valid & not x in still_not-bound_in p holds

p => (All (x,q)) is valid by Th9;

theorem :: CQC_THE1:68

for Al being QC-alphabet

for s being QC-formula of Al

for x, y being bound_QC-variable of Al st s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x is valid holds

s . y is valid by Th10;

for s being QC-formula of Al

for x, y being bound_QC-variable of Al st s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x is valid holds

s . y is valid by Th10;