:: CQC_THE1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: CQC_THE1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number holds
( not n <= 1 or n = 0 or n = 1 )
proof end;

theorem :: CQC_THE1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number holds
( not n <= 2 or n = 0 or n = 1 or n = 2 )
proof end;

theorem :: CQC_THE1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number holds
( not n <= 3 or n = 0 or n = 1 or n = 2 or n = 3 )
proof end;

theorem :: CQC_THE1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number holds
( not n <= 4 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 )
proof end;

theorem :: CQC_THE1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number holds
( not n <= 5 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 )
proof end;

theorem :: CQC_THE1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number holds
( not n <= 6 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 )
proof end;

theorem :: CQC_THE1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number holds
( not n <= 7 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 )
proof end;

theorem :: CQC_THE1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number holds
( not n <= 8 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 or n = 8 )
proof end;

theorem Th10: :: CQC_THE1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number holds
( not n <= 9 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 or n = 8 or n = 9 )
proof end;

theorem Th11: :: CQC_THE1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds { k where k is Nat : k <= n + 1 } = { i where i is Nat : i <= n } \/ {(n + 1)}
proof end;

theorem Th12: :: CQC_THE1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds { k where k is Nat : k <= n } is finite
proof end;

deffunc H1( set ) -> set = $1 `1 ;

theorem :: CQC_THE1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z being set st X is finite & X c= [:Y,Z:] holds
ex A, B being set st
( A is finite & A c= Y & B is finite & B c= Z & X c= [:A,B:] )
proof end;

theorem Th14: :: CQC_THE1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Z, Y being set st X is finite & Z is finite & X c= [:Y,Z:] holds
ex A being set st
( A is finite & A c= Y & X c= [:A,Z:] )
proof end;

definition
let T be Subset of CQC-WFF ;
attr T is being_a_theory means :Def1: :: CQC_THE1:def 1
( VERUM in T & ( for p, q, r being Element of CQC-WFF
for s being QC-formula
for x, y being bound_QC-variable 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 & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in T implies s . y in T ) ) ) );
end;

:: deftheorem Def1 defines being_a_theory CQC_THE1:def 1 :
for T being Subset of CQC-WFF holds
( T is being_a_theory iff ( VERUM in T & ( for p, q, r being Element of CQC-WFF
for s being QC-formula
for x, y being bound_QC-variable 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 & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in T implies s . y in T ) ) ) ) );

notation
let T be Subset of CQC-WFF ;
synonym T is_a_theory for being_a_theory T;
end;

theorem :: CQC_THE1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S being Subset of CQC-WFF st T is_a_theory & S is_a_theory holds
T /\ S is_a_theory
proof end;

definition
let X be Subset of CQC-WFF ;
func Cn X -> Subset of CQC-WFF means :Def2: :: CQC_THE1:def 2
for t being Element of CQC-WFF holds
( t in it iff for T being Subset of CQC-WFF st T is_a_theory & X c= T holds
t in T );
existence
ex b1 being Subset of CQC-WFF st
for t being Element of CQC-WFF holds
( t in b1 iff for T being Subset of CQC-WFF st T is_a_theory & X c= T holds
t in T )
proof end;
uniqueness
for b1, b2 being Subset of CQC-WFF st ( for t being Element of CQC-WFF holds
( t in b1 iff for T being Subset of CQC-WFF st T is_a_theory & X c= T holds
t in T ) ) & ( for t being Element of CQC-WFF holds
( t in b2 iff for T being Subset of CQC-WFF st T is_a_theory & X c= T holds
t in T ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Cn CQC_THE1:def 2 :
for X, b2 being Subset of CQC-WFF holds
( b2 = Cn X iff for t being Element of CQC-WFF holds
( t in b2 iff for T being Subset of CQC-WFF st T is_a_theory & X c= T holds
t in T ) );

theorem :: CQC_THE1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th27: :: CQC_THE1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF holds VERUM in Cn X
proof end;

theorem Th28: :: CQC_THE1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p being Element of CQC-WFF holds (('not' p) => p) => p in Cn X
proof end;

theorem Th29: :: CQC_THE1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p, q being Element of CQC-WFF holds p => (('not' p) => q) in Cn X
proof end;

theorem Th30: :: CQC_THE1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p, q, r being Element of CQC-WFF holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X
proof end;

theorem Th31: :: CQC_THE1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p, q being Element of CQC-WFF holds (p '&' q) => (q '&' p) in Cn X
proof end;

theorem Th32: :: CQC_THE1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p, q being Element of CQC-WFF st p in Cn X & p => q in Cn X holds
q in Cn X
proof end;

theorem Th33: :: CQC_THE1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p being Element of CQC-WFF
for x being bound_QC-variable holds (All x,p) => p in Cn X
proof end;

theorem Th34: :: CQC_THE1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p, q being Element of CQC-WFF
for x being bound_QC-variable 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 Th35: :: CQC_THE1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for s being QC-formula
for x, y being bound_QC-variable st s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Cn X holds
s . y in Cn X
proof end;

theorem Th36: :: CQC_THE1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF holds Cn X is_a_theory
proof end;

theorem Th37: :: CQC_THE1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, X being Subset of CQC-WFF st T is_a_theory & X c= T holds
Cn X c= T
proof end;

theorem Th38: :: CQC_THE1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF holds X c= Cn X
proof end;

theorem Th39: :: CQC_THE1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being Subset of CQC-WFF st X c= Y holds
Cn X c= Cn Y
proof end;

Lm1: for X being Subset of CQC-WFF holds Cn (Cn X) c= Cn X
proof end;

theorem :: CQC_THE1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF holds Cn (Cn X) = Cn X
proof end;

theorem Th41: :: CQC_THE1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Subset of CQC-WFF holds
( T is_a_theory iff Cn T = T )
proof end;

definition
func Proof_Step_Kinds -> set equals :: CQC_THE1:def 3
{ k where k is Nat : k <= 9 } ;
coherence
{ k where k is Nat : k <= 9 } is set ;
end;

:: deftheorem defines Proof_Step_Kinds CQC_THE1:def 3 :
Proof_Step_Kinds = { k where k is Nat : k <= 9 } ;

registration
cluster Proof_Step_Kinds -> non empty ;
coherence
not Proof_Step_Kinds is empty
proof end;
end;

theorem :: CQC_THE1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th43: :: CQC_THE1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 0 in Proof_Step_Kinds & 1 in Proof_Step_Kinds & 2 in Proof_Step_Kinds & 3 in Proof_Step_Kinds & 4 in Proof_Step_Kinds & 5 in Proof_Step_Kinds & 6 in Proof_Step_Kinds & 7 in Proof_Step_Kinds & 8 in Proof_Step_Kinds & 9 in Proof_Step_Kinds ) ;

theorem :: CQC_THE1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Proof_Step_Kinds is finite by Th12;

theorem Th45: :: CQC_THE1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st 1 <= n & n <= len f & not (f . n) `2 = 0 & not (f . n) `2 = 1 & not (f . n) `2 = 2 & not (f . n) `2 = 3 & not (f . n) `2 = 4 & not (f . n) `2 = 5 & not (f . n) `2 = 6 & not (f . n) `2 = 7 & not (f . n) `2 = 8 holds
(f . n) `2 = 9
proof end;

definition
let PR be FinSequence of [:CQC-WFF ,Proof_Step_Kinds :];
let n be Nat;
let X be Subset of CQC-WFF ;
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 if (PR . n) `2 = 1
ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p if (PR . n) `2 = 2
ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) if (PR . n) `2 = 3
ex p, q, r being Element of CQC-WFF 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 st (PR . n) `1 = (p '&' q) => (q '&' p) if (PR . n) `2 = 5
ex p being Element of CQC-WFF ex x being bound_QC-variable 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 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 ex x being bound_QC-variable 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 ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & 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) `2 = 0 & (PR . n) `2 = 1 implies ( (PR . n) `1 in X iff (PR . n) `1 = VERUM ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 2 implies ( (PR . n) `1 in X iff ex p being Element of CQC-WFF 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 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 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 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 ex x being bound_QC-variable 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 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 ex x being bound_QC-variable 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 ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & 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 iff ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 3 implies ( (PR . n) `1 = VERUM iff ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 4 implies ( (PR . n) `1 = VERUM iff ex p, q, r being Element of CQC-WFF 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 iff ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 6 implies ( (PR . n) `1 = VERUM iff ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 7 implies ( (PR . n) `1 = VERUM iff ex i, j being Nat ex p, q being Element of CQC-WFF 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 iff ex i being Nat ex p, q being Element of CQC-WFF ex x being bound_QC-variable 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 iff ex i being Nat ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & 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 st (PR . n) `1 = (('not' p) => p) => p iff ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 4 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff ex p, q, r being Element of CQC-WFF 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 st (PR . n) `1 = (('not' p) => p) => p iff ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 6 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 7 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff ex i, j being Nat ex p, q being Element of CQC-WFF 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 st (PR . n) `1 = (('not' p) => p) => p iff ex i being Nat ex p, q being Element of CQC-WFF ex x being bound_QC-variable 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 st (PR . n) `1 = (('not' p) => p) => p iff ex i being Nat ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & 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 st (PR . n) `1 = p => (('not' p) => q) iff ex p, q, r being Element of CQC-WFF 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 st (PR . n) `1 = p => (('not' p) => q) iff ex p, q being Element of CQC-WFF 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 st (PR . n) `1 = p => (('not' p) => q) iff ex p being Element of CQC-WFF ex x being bound_QC-variable 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 st (PR . n) `1 = p => (('not' p) => q) iff ex i, j being Nat ex p, q being Element of CQC-WFF 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 st (PR . n) `1 = p => (('not' p) => q) iff ex i being Nat ex p, q being Element of CQC-WFF ex x being bound_QC-variable 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 st (PR . n) `1 = p => (('not' p) => q) iff ex i being Nat ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & 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 st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex p, q being Element of CQC-WFF 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 st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex p being Element of CQC-WFF ex x being bound_QC-variable 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 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 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 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 ex x being bound_QC-variable 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 st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex i being Nat ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & 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 st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex p being Element of CQC-WFF ex x being bound_QC-variable 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 st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex i, j being Nat ex p, q being Element of CQC-WFF 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 st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex i being Nat ex p, q being Element of CQC-WFF ex x being bound_QC-variable 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 st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex i being Nat ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & 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 ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p iff ex i, j being Nat ex p, q being Element of CQC-WFF 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 ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p iff ex i being Nat ex p, q being Element of CQC-WFF ex x being bound_QC-variable 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 ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p iff ex i being Nat ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & 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 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 ex x being bound_QC-variable 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 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 ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & 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 ex x being bound_QC-variable 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 ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) ) ;
end;

:: deftheorem Def4 defines is_a_correct_step_wrt CQC_THE1:def 4 :
for PR being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :]
for n being Nat
for X being Subset of CQC-WFF 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 ) ) & ( (PR . n) `2 = 2 implies ( PR,n is_a_correct_step_wrt X iff ex p being Element of CQC-WFF 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 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 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 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 ex x being bound_QC-variable 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 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 ex x being bound_QC-variable 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 ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) );

definition
let X be Subset of CQC-WFF ;
let f be FinSequence of [:CQC-WFF ,Proof_Step_Kinds :];
pred f is_a_proof_wrt X means :Def5: :: CQC_THE1:def 5
( f <> {} & ( for n being Nat st 1 <= n & n <= len f holds
f,n is_a_correct_step_wrt X ) );
end;

:: deftheorem Def5 defines is_a_proof_wrt CQC_THE1:def 5 :
for X being Subset of CQC-WFF
for f being FinSequence of [:CQC-WFF ,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:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st f is_a_proof_wrt X holds
rng f <> {}
proof end;

theorem Th58: :: CQC_THE1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st f is_a_proof_wrt X holds
1 <= len f
proof end;

theorem :: CQC_THE1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] holds
( not f is_a_proof_wrt X or (f . 1) `2 = 0 or (f . 1) `2 = 1 or (f . 1) `2 = 2 or (f . 1) `2 = 3 or (f . 1) `2 = 4 or (f . 1) `2 = 5 or (f . 1) `2 = 6 )
proof end;

theorem Th60: :: CQC_THE1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for X being Subset of CQC-WFF
for f, g being FinSequence of [:CQC-WFF ,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 Th61: :: CQC_THE1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for X being Subset of CQC-WFF
for g, f being FinSequence of [:CQC-WFF ,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 Th62: :: CQC_THE1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for f, g being FinSequence of [:CQC-WFF ,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:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being Subset of CQC-WFF
for f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st f is_a_proof_wrt X & X c= Y holds
f is_a_proof_wrt Y
proof end;

theorem Th64: :: CQC_THE1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l being Nat
for X being Subset of CQC-WFF
for f being FinSequence of [:CQC-WFF ,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 f be FinSequence of [:CQC-WFF ,Proof_Step_Kinds :];
assume A1: f <> {} ;
func Effect f -> Element of CQC-WFF equals :Def6: :: CQC_THE1:def 6
(f . (len f)) `1 ;
coherence
(f . (len f)) `1 is Element of CQC-WFF
proof end;
end;

:: deftheorem Def6 defines Effect CQC_THE1:def 6 :
for f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st f <> {} holds
Effect f = (f . (len f)) `1 ;

theorem :: CQC_THE1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th66: :: CQC_THE1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st f is_a_proof_wrt X holds
Effect f in Cn X
proof end;

Lm2: for X being Subset of CQC-WFF holds { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = p ) } c= CQC-WFF
proof end;

theorem Th67: :: CQC_THE1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF holds X c= { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) }
proof end;

Lm3: for X being Subset of CQC-WFF holds VERUM in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) }
proof end;

Lm4: for p being Element of CQC-WFF
for X being Subset of CQC-WFF holds (('not' p) => p) => p in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) }
proof end;

Lm5: for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF holds p => (('not' p) => q) in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) }
proof end;

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

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

Lm8: for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st p in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) } & p => q in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = G ) } holds
q in { H where H is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = H ) }
proof end;

Lm9: for p being Element of CQC-WFF
for x being bound_QC-variable
for X being Subset of CQC-WFF holds (All x,p) => p in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) }
proof end;

Lm10: for p, q being Element of CQC-WFF
for x being bound_QC-variable
for X being Subset of CQC-WFF st p => q in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,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 : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = G ) }
proof end;

Lm11: for s being QC-formula
for x, y being bound_QC-variable
for X being Subset of CQC-WFF st s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,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 : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = G ) }
proof end;

theorem Th68: :: CQC_THE1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being Subset of CQC-WFF st Y = { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = p ) } holds
Y is_a_theory
proof end;

Lm12: for X being Subset of CQC-WFF holds { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = p ) } c= Cn X
proof end;

theorem Th69: :: CQC_THE1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF holds { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = p ) } = Cn X
proof end;

theorem Th70: :: CQC_THE1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p being Element of CQC-WFF holds
( p in Cn X iff ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = p ) )
proof end;

theorem :: CQC_THE1:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p being Element of CQC-WFF st p in Cn X holds
ex Y being Subset of CQC-WFF st
( Y c= X & Y is finite & p in Cn Y )
proof end;

definition
canceled;
func TAUT -> Subset of CQC-WFF equals :: CQC_THE1:def 8
 Cn ({} CQC-WFF );
correctness
coherence
Cn ({} CQC-WFF ) is Subset of CQC-WFF ;
;
end;

:: deftheorem CQC_THE1:def 7 :
canceled;

:: deftheorem defines TAUT CQC_THE1:def 8 :
TAUT = Cn ({} CQC-WFF );

theorem :: CQC_THE1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th74: :: CQC_THE1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Subset of CQC-WFF st T is_a_theory holds
TAUT c= T
proof end;

theorem Th75: :: CQC_THE1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF holds TAUT c= Cn X
proof end;

theorem Th76: :: CQC_THE1:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
TAUT is_a_theory by Th36;

theorem Th77: :: CQC_THE1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
VERUM in TAUT by Def1, Th76;

theorem :: CQC_THE1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF holds (('not' p) => p) => p in TAUT by Def1, Th76;

theorem :: CQC_THE1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF holds p => (('not' p) => q) in TAUT by Def1, Th76;

theorem :: CQC_THE1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being Element of CQC-WFF holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in TAUT by Def1, Th76;

theorem :: CQC_THE1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF holds (p '&' q) => (q '&' p) in TAUT by Def1, Th76;

theorem :: CQC_THE1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF st p in TAUT & p => q in TAUT holds
q in TAUT by Def1, Th76;

theorem :: CQC_THE1:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable holds (All x,p) => p in TAUT by Th33;

theorem :: CQC_THE1:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF
for x being bound_QC-variable st p => q in TAUT & not x in still_not-bound_in p holds
p => (All x,q) in TAUT by Th34;

theorem :: CQC_THE1:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being QC-formula
for x, y being bound_QC-variable st s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in TAUT holds
s . y in TAUT by Th35;

definition
let X be Subset of CQC-WFF ;
let s be QC-formula;
pred X |- s means :Def9: :: CQC_THE1:def 9
s in Cn X;
end;

:: deftheorem Def9 defines |- CQC_THE1:def 9 :
for X being Subset of CQC-WFF
for s being QC-formula holds
( X |- s iff s in Cn X );

theorem :: CQC_THE1:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF holds X |- VERUM
proof end;

theorem :: CQC_THE1:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p being Element of CQC-WFF holds X |- (('not' p) => p) => p
proof end;

theorem :: CQC_THE1:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p, q being Element of CQC-WFF holds X |- p => (('not' p) => q)
proof end;

theorem :: CQC_THE1:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p, q, r being Element of CQC-WFF holds X |- (p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))
proof end;

theorem :: CQC_THE1:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p, q being Element of CQC-WFF holds X |- (p '&' q) => (q '&' p)
proof end;

theorem :: CQC_THE1:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p, q being Element of CQC-WFF st X |- p & X |- p => q holds
X |- q
proof end;

theorem :: CQC_THE1:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p being Element of CQC-WFF
for x being bound_QC-variable holds X |- (All x,p) => p
proof end;

theorem :: CQC_THE1:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p, q being Element of CQC-WFF
for x being bound_QC-variable st X |- p => q & not x in still_not-bound_in p holds
X |- p => (All x,q)
proof end;

theorem :: CQC_THE1:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for s being QC-formula
for x, y being bound_QC-variable st s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & X |- s . x holds
X |- s . y
proof end;

definition
let s be QC-formula;
attr s is valid means :Def10: :: CQC_THE1:def 10
 {} CQC-WFF |- s;
end;

:: deftheorem Def10 defines valid CQC_THE1:def 10 :
for s being QC-formula holds
( s is valid iff {} CQC-WFF |- s );

notation
let s be QC-formula;
synonym |- s for valid s;
end;

Lm13: for s being QC-formula holds
( |-|- s valid s iff s in TAUT )
proof end;

definition
let s be QC-formula;
redefine attr s is valid means :: CQC_THE1:def 11
s in TAUT ;
compatibility
( s is valid iff s in TAUT ) by Lm13;
end;

:: deftheorem defines valid CQC_THE1:def 11 :
for s being QC-formula holds
( s is valid iff s in TAUT );

theorem :: CQC_THE1:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_THE1:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p being Element of CQC-WFF st |-|- p valid p holds
X |- p
proof end;

theorem :: CQC_THE1:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
|-|- VERUM valid VERUM by Lm13, Th77;

theorem :: CQC_THE1:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF holds |-|- (('not' p) => p) => p valid (('not' p) => p) => p
proof end;

theorem :: CQC_THE1:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF holds |-|- p => (('not' p) => q) valid p => (('not' p) => q)
proof end;

theorem :: CQC_THE1:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being Element of CQC-WFF holds |-|- (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) valid (p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))
proof end;

theorem :: CQC_THE1:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF holds |-|- (p '&' q) => (q '&' p) valid (p '&' q) => (q '&' p)
proof end;

theorem :: CQC_THE1:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF st |-|- p valid p & |-|- p => q valid p => q holds
|-|- q valid q
proof end;

theorem :: CQC_THE1:105  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable holds |-|- (All x,p) => p valid (All x,p) => p
proof end;

theorem :: CQC_THE1:106  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF
for x being bound_QC-variable st |-|- p => q valid p => q & not x in still_not-bound_in p holds
|-|- p => (All x,q) valid p => (All x,q)
proof end;

theorem :: CQC_THE1:107  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being QC-formula
for x, y being bound_QC-variable st s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & |-|- s . x valid s . x holds
|-|- s . y valid s . y
proof end;