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

registration
let g be FinSequence;
let N be set ;
cluster g | N -> FinSubsequence-like ;
coherence
g | N is FinSubsequence-like by FINSEQ_1:69;
end;

definition
let D be non empty set ;
let f be FinSequence of D;
func Ant f -> FinSequence of D means :Def1: :: CALCUL_1:def 1
for i being Nat st len f = i + 1 holds
it = f | (Seg i) if len f > 0
otherwise it = {} ;
existence
( ( len f > 0 implies ex b1 being FinSequence of D st
for i being Nat st len f = i + 1 holds
b1 = f | (Seg i) ) & ( not len f > 0 implies ex b1 being FinSequence of D st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being FinSequence of D holds
( ( len f > 0 & ( for i being Nat st len f = i + 1 holds
b1 = f | (Seg i) ) & ( for i being Nat st len f = i + 1 holds
b2 = f | (Seg i) ) implies b1 = b2 ) & ( not len f > 0 & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
consistency
for b1 being FinSequence of D holds verum ;
end;

:: deftheorem Def1 defines Ant CALCUL_1:def 1 :
for D being non empty set
for f, b3 being FinSequence of D holds
( ( len f > 0 implies ( b3 = Ant f iff for i being Nat st len f = i + 1 holds
b3 = f | (Seg i) ) ) & ( not len f > 0 implies ( b3 = Ant f iff b3 = {} ) ) );

definition
let D be non empty set ;
let f be FinSequence of D;
assume A1: len f > 0 ;
func Suc f -> Element of D equals :Def2: :: CALCUL_1:def 2
f . (len f);
coherence
f . (len f) is Element of D
proof end;
end;

:: deftheorem Def2 defines Suc CALCUL_1:def 2 :
for D being non empty set
for f being FinSequence of D st len f > 0 holds
Suc f = f . (len f);

definition
let D be non empty set ;
let p be Element of D;
let f be FinSequence of D;
pred p is_tail_of f means :Def3: :: CALCUL_1:def 3
 ex i being Nat st
( i in dom f & f . i = p );
end;

:: deftheorem Def3 defines is_tail_of CALCUL_1:def 3 :
for D being non empty set
for p being Element of D
for f being FinSequence of D holds
( p is_tail_of f iff ex i being Nat st
( i in dom f & f . i = p ) );

definition
let f, g be FinSequence of CQC-WFF ;
pred f is_Subsequence_of g means :Def4: :: CALCUL_1:def 4
 ex N being Subset of NAT st f c= Seq (g | N);
end;

:: deftheorem Def4 defines is_Subsequence_of CALCUL_1:def 4 :
for f, g being FinSequence of CQC-WFF holds
( f is_Subsequence_of g iff ex N being Subset of NAT st f c= Seq (g | N) );

theorem Th1: :: CALCUL_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of CQC-WFF st f is_Subsequence_of g holds
( rng f c= rng g & ex N being Subset of NAT st rng f c= rng (g | N) )
proof end;

theorem Th2: :: CALCUL_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of CQC-WFF st len f > 0 holds
( (len (Ant f)) + 1 = len f & len (Ant f) < len f )
proof end;

theorem Th3: :: CALCUL_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of CQC-WFF st len f > 0 holds
( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} )
proof end;

theorem Th4: :: CALCUL_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of CQC-WFF st len f > 1 holds
len (Ant f) > 0
proof end;

theorem Th5: :: CALCUL_1:5  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 f being FinSequence of CQC-WFF holds
( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f )
proof end;

theorem Th6: :: CALCUL_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fin, fin1 being FinSequence holds
( len fin <= len (fin ^ fin1) & len fin1 <= len (fin ^ fin1) & ( fin <> {} implies ( 1 <= len fin & len fin1 < len (fin1 ^ fin) ) ) )
proof end;

theorem Th7: :: CALCUL_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of CQC-WFF holds Seq ((f ^ g) | (dom f)) = (f ^ g) | (dom f)
proof end;

theorem Th8: :: CALCUL_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of CQC-WFF holds f is_Subsequence_of f ^ g
proof end;

theorem Th9: :: CALCUL_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b, c being set
for fin being FinSequence holds 1 < len ((fin ^ <*b*>) ^ <*c*>)
proof end;

theorem Th10: :: CALCUL_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b being set
for fin being FinSequence holds
( 1 <= len (fin ^ <*b*>) & len (fin ^ <*b*>) in dom (fin ^ <*b*>) )
proof end;

theorem Th11: :: CALCUL_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat st 0 < m holds
len (Sgm ((Seg n) \/ {(n + m)})) = n + 1
proof end;

theorem Th12: :: CALCUL_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat st 0 < m holds
dom (Sgm ((Seg n) \/ {(n + m)})) = Seg (n + 1)
proof end;

theorem Th13: :: CALCUL_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of CQC-WFF st 0 < len f holds
f is_Subsequence_of ((Ant f) ^ g) ^ <*(Suc f)*>
proof end;

theorem Th14: :: CALCUL_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c, d being set
for f being FinSequence of CQC-WFF holds
( 1 in dom <*c,d*> & 2 in dom <*c,d*> & (f ^ <*c,d*>) . ((len f) + 1) = c & (f ^ <*c,d*>) . ((len f) + 2) = d )
proof end;

definition
let f be FinSequence of CQC-WFF ;
func still_not-bound_in f -> Subset of bound_QC-variables means :Def5: :: CALCUL_1:def 5
for a being set holds
( a in it iff ex i being Nat ex p being Element of CQC-WFF st
( i in dom f & p = f . i & a in still_not-bound_in p ) );
existence
ex b1 being Subset of bound_QC-variables st
for a being set holds
( a in b1 iff ex i being Nat ex p being Element of CQC-WFF st
( i in dom f & p = f . i & a in still_not-bound_in p ) )
proof end;
uniqueness
for b1, b2 being Subset of bound_QC-variables st ( for a being set holds
( a in b1 iff ex i being Nat ex p being Element of CQC-WFF st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) & ( for a being set holds
( a in b2 iff ex i being Nat ex p being Element of CQC-WFF st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines still_not-bound_in CALCUL_1:def 5 :
for f being FinSequence of CQC-WFF
for b2 being Subset of bound_QC-variables holds
( b2 = still_not-bound_in f iff for a being set holds
( a in b2 iff ex i being Nat ex p being Element of CQC-WFF st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) );

definition
func set_of_CQC-WFF-seq -> set means :Def6: :: CALCUL_1:def 6
for a being set holds
( a in it iff a is FinSequence of CQC-WFF );
existence
ex b1 being set st
for a being set holds
( a in b1 iff a is FinSequence of CQC-WFF )
proof end;
uniqueness
for b1, b2 being set st ( for a being set holds
( a in b1 iff a is FinSequence of CQC-WFF ) ) & ( for a being set holds
( a in b2 iff a is FinSequence of CQC-WFF ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines set_of_CQC-WFF-seq CALCUL_1:def 6 :
for b1 being set holds
( b1 = set_of_CQC-WFF-seq iff for a being set holds
( a in b1 iff a is FinSequence of CQC-WFF ) );

definition
let PR be FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :];
let n be Nat;
pred PR,n is_a_correct_step means :Def7: :: CALCUL_1:def 7
 ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) if (PR . n) `2 = 0
ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> if (PR . n) `2 = 1
ex i being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) if (PR . n) `2 = 2
ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) if (PR . n) `2 = 3
ex i, j being Nat ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) if (PR . n) `2 = 4
ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) if (PR . n) `2 = 5
ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) if (PR . n) `2 = 6
ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) if (PR . n) `2 = 7
ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) if (PR . n) `2 = 8
ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) if (PR . n) `2 = 9
;
consistency
( ( (PR . n) `2 = 0 & (PR . n) `2 = 1 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 2 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 3 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 4 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 5 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 6 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 7 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 8 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 9 implies ( ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 2 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 3 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 4 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 5 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 6 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 7 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 8 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 9 implies ( ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 3 implies ( ex i being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 4 implies ( ex i being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 5 implies ( ex i being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 6 implies ( ex i being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 7 implies ( ex i being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 8 implies ( ex i being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 9 implies ( ex i being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 4 implies ( ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 5 implies ( ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 6 implies ( ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 7 implies ( ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 8 implies ( ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 9 implies ( ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 5 implies ( ex i, j being Nat ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 6 implies ( ex i, j being Nat ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 7 implies ( ex i, j being Nat ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 8 implies ( ex i, j being Nat ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 9 implies ( ex i, j being Nat ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 6 implies ( ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 7 implies ( ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 8 implies ( ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 9 implies ( ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 7 implies ( ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 8 implies ( ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 9 implies ( ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 8 implies ( ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 9 implies ( ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 8 & (PR . n) `2 = 9 implies ( ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) ) ;
end;

:: deftheorem Def7 defines is_a_correct_step CALCUL_1:def 7 :
for PR being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :]
for n being Nat holds
( ( (PR . n) `2 = 0 implies ( PR,n is_a_correct_step iff ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) ) ) & ( (PR . n) `2 = 1 implies ( PR,n is_a_correct_step iff ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> ) ) & ( (PR . n) `2 = 2 implies ( PR,n is_a_correct_step iff ex i being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) ) ) & ( (PR . n) `2 = 3 implies ( PR,n is_a_correct_step iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 implies ( PR,n is_a_correct_step iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 implies ( PR,n is_a_correct_step iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 6 implies ( PR,n is_a_correct_step iff ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 7 implies ( PR,n is_a_correct_step iff ex i being Nat ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 8 implies ( PR,n is_a_correct_step iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 9 implies ( PR,n is_a_correct_step iff ex i being Nat ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) ) ) );

definition
let PR be FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :];
attr PR is a_proof means :Def8: :: CALCUL_1:def 8
( PR <> {} & ( for n being Nat st 1 <= n & n <= len PR holds
PR,n is_a_correct_step ) );
end;

:: deftheorem Def8 defines a_proof CALCUL_1:def 8 :
for PR being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] holds
( PR is a_proof iff ( PR <> {} & ( for n being Nat st 1 <= n & n <= len PR holds
PR,n is_a_correct_step ) ) );

definition
let f be FinSequence of CQC-WFF ;
pred |- f means :Def9: :: CALCUL_1:def 9
 ex PR being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] st
( PR is a_proof & f = (PR . (len PR)) `1 );
end;

:: deftheorem Def9 defines |- CALCUL_1:def 9 :
for f being FinSequence of CQC-WFF holds
( |- f iff ex PR being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] st
( PR is a_proof & f = (PR . (len PR)) `1 ) );

definition
let p be Element of CQC-WFF ;
let X be Subset of CQC-WFF ;
pred p is_formal_provable_from X means :Def10: :: CALCUL_1:def 10
 ex f being FinSequence of CQC-WFF st
( rng (Ant f) c= X & Suc f = p & |- f );
end;

:: deftheorem Def10 defines is_formal_provable_from CALCUL_1:def 10 :
for p being Element of CQC-WFF
for X being Subset of CQC-WFF holds
( p is_formal_provable_from X iff ex f being FinSequence of CQC-WFF st
( rng (Ant f) c= X & Suc f = p & |- f ) );

definition
let X be Subset of CQC-WFF ;
let A be non empty set ;
let J be interpretation of A;
let v be Element of Valuations_in A;
pred J,v |= X means :Def11: :: CALCUL_1:def 11
for p being Element of CQC-WFF st p in X holds
J,v |= p;
end;

:: deftheorem Def11 defines |= CALCUL_1:def 11 :
for X being Subset of CQC-WFF
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A holds
( J,v |= X iff for p being Element of CQC-WFF st p in X holds
J,v |= p );

definition
let X be Subset of CQC-WFF ;
let p be Element of CQC-WFF ;
pred X |= p means :: CALCUL_1:def 12
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A st J,v |= X holds
J,v |= p;
end;

:: deftheorem defines |= CALCUL_1:def 12 :
for X being Subset of CQC-WFF
for p being Element of CQC-WFF holds
( X |= p iff for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A st J,v |= X holds
J,v |= p );

definition
let p be Element of CQC-WFF ;
pred |= p means :: CALCUL_1:def 13
 {} CQC-WFF |= p;
end;

:: deftheorem defines |= CALCUL_1:def 13 :
for p being Element of CQC-WFF holds
( |= p iff {} CQC-WFF |= p );

definition
let f be FinSequence of CQC-WFF ;
let A be non empty set ;
let J be interpretation of A;
let v be Element of Valuations_in A;
pred J,v |= f means :Def14: :: CALCUL_1:def 14
J,v |= rng f;
end;

:: deftheorem Def14 defines |= CALCUL_1:def 14 :
for f being FinSequence of CQC-WFF
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A holds
( J,v |= f iff J,v |= rng f );

definition
let f be FinSequence of CQC-WFF ;
let p be Element of CQC-WFF ;
pred f |= p means :Def15: :: CALCUL_1:def 15
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A st J,v |= f holds
J,v |= p;
end;

:: deftheorem Def15 defines |= CALCUL_1:def 15 :
for f being FinSequence of CQC-WFF
for p being Element of CQC-WFF holds
( f |= p iff for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A st J,v |= f holds
J,v |= p );

theorem Th15: :: CALCUL_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of CQC-WFF st Suc f is_tail_of Ant f holds
Ant f |= Suc f
proof end;

theorem Th16: :: CALCUL_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of CQC-WFF st Ant f is_Subsequence_of Ant g & Suc f = Suc g & Ant f |= Suc f holds
Ant g |= Suc g
proof end;

theorem Th17: :: CALCUL_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A
for f being FinSequence of CQC-WFF st len f > 0 holds
( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )
proof end;

theorem Th18: :: CALCUL_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of CQC-WFF st len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & Ant f |= Suc f & Ant g |= Suc g holds
Ant (Ant f) |= Suc f
proof end;

theorem Th19: :: CALCUL_1:19  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 f, g being FinSequence of CQC-WFF st len f > 1 & Ant f = Ant g & 'not' p = Suc (Ant f) & 'not' (Suc f) = Suc g & Ant f |= Suc f & Ant g |= Suc g holds
Ant (Ant f) |= p
proof end;

theorem Th20: :: CALCUL_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of CQC-WFF st Ant f = Ant g & Ant f |= Suc f & Ant g |= Suc g holds
Ant f |= (Suc f) '&' (Suc g)
proof end;

theorem Th21: :: CALCUL_1:21  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 f being FinSequence of CQC-WFF st Suc f = p '&' q & Ant f |= p '&' q holds
Ant f |= p
proof end;

theorem Th22: :: CALCUL_1:22  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 f being FinSequence of CQC-WFF st Suc f = p '&' q & Ant f |= p '&' q holds
Ant f |= q
proof end;

theorem Th23: :: CALCUL_1:23  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 A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A
for Sub being CQC_Substitution holds
( J,v |= [p,Sub] iff J,v |= p )
proof end;

theorem Th24: :: CALCUL_1:24  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, y being bound_QC-variable
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A holds
( J,v |= p . x,y iff ex a being Element of A st
( v . y = a & J,v . (x | a) |= p ) )
proof end;

theorem Th25: :: CALCUL_1:25  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
for f being FinSequence of CQC-WFF st Suc f = All x,p & Ant f |= Suc f holds
for y being bound_QC-variable holds Ant f |= p . x,y
proof end;

theorem Th26: :: CALCUL_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for a being Element of A
for X being set st X c= bound_QC-variables & not x in X holds
(v . (x | a)) | X = v | X
proof end;

theorem Th27: :: CALCUL_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for J being interpretation of A
for f being FinSequence of CQC-WFF
for v, w being Element of Valuations_in A st v | (still_not-bound_in f) = w | (still_not-bound_in f) holds
( J,v |= f iff J,w |= f )
proof end;

theorem Th28: :: CALCUL_1:28  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 y, x being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for a being Element of A st not y in still_not-bound_in (All x,p) holds
((v . (y | a)) . (x | a)) | (still_not-bound_in p) = (v . (x | a)) | (still_not-bound_in p)
proof end;

theorem Th29: :: CALCUL_1:29  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, y being bound_QC-variable
for f being FinSequence of CQC-WFF st Suc f = p . x,y & Ant f |= Suc f & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) holds
Ant f |= All x,p
proof end;

theorem Th30: :: CALCUL_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of CQC-WFF holds Ant (f ^ <*VERUM *>) |= Suc (f ^ <*VERUM *>)
proof end;

theorem Th31: :: CALCUL_1:31  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 PR being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] st 1 <= n & n <= len PR & not (PR . n) `2 = 0 & not (PR . n) `2 = 1 & not (PR . n) `2 = 2 & not (PR . n) `2 = 3 & not (PR . n) `2 = 4 & not (PR . n) `2 = 5 & not (PR . n) `2 = 6 & not (PR . n) `2 = 7 & not (PR . n) `2 = 8 holds
(PR . n) `2 = 9
proof end;

Lm1: for f being FinSequence st f <> {} holds
1 <= len f
by GRAPH_5:8;

Lm2: for n being Nat
for PR being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] st 1 <= n & n <= len PR holds
(PR . n) `1 is FinSequence of CQC-WFF
proof end;

theorem :: CALCUL_1:32  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 Subset of CQC-WFF st p is_formal_provable_from X holds
X |= p
proof end;

theorem Th33: :: CALCUL_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of CQC-WFF st Suc f is_tail_of Ant f holds
|- f
proof end;

theorem Th34: :: CALCUL_1:34  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 PR, PR1 being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] st 1 <= n & n <= len PR holds
( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step )
proof end;

theorem Th35: :: CALCUL_1:35  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 PR1, PR being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] st 1 <= n & n <= len PR1 & PR1,n is_a_correct_step holds
PR ^ PR1,n + (len PR) is_a_correct_step
proof end;

theorem Th36: :: CALCUL_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of CQC-WFF st Ant f is_Subsequence_of Ant g & Suc f = Suc g & |- f holds
|- g
proof end;

theorem Th37: :: CALCUL_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of CQC-WFF st 1 < len f & 1 < len g & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & |- f & |- g holds
|- (Ant (Ant f)) ^ <*(Suc f)*>
proof end;

theorem Th38: :: CALCUL_1:38  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 f, g being FinSequence of CQC-WFF st len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & |- f & |- g holds
|- (Ant (Ant f)) ^ <*p*>
proof end;

theorem Th39: :: CALCUL_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of CQC-WFF st Ant f = Ant g & |- f & |- g holds
|- (Ant f) ^ <*((Suc f) '&' (Suc g))*>
proof end;

theorem Th40: :: CALCUL_1:40  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 f being FinSequence of CQC-WFF st p '&' q = Suc f & |- f holds
|- (Ant f) ^ <*p*>
proof end;

theorem Th41: :: CALCUL_1:41  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 f being FinSequence of CQC-WFF st p '&' q = Suc f & |- f holds
|- (Ant f) ^ <*q*>
proof end;

theorem Th42: :: CALCUL_1:42  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, y being bound_QC-variable
for f being FinSequence of CQC-WFF st Suc f = All x,p & |- f holds
|- (Ant f) ^ <*(p . x,y)*>
proof end;

theorem Th43: :: CALCUL_1:43  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, y being bound_QC-variable
for f being FinSequence of CQC-WFF st Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & |- f holds
|- (Ant f) ^ <*(All x,p)*>
proof end;

theorem Th44: :: CALCUL_1:44  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 f being FinSequence of CQC-WFF st |- f & |- (Ant f) ^ <*('not' (Suc f))*> holds
|- (Ant f) ^ <*p*>
proof end;

theorem Th45: :: CALCUL_1:45  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 f being FinSequence of CQC-WFF st 1 <= len f & |- f & |- f ^ <*p*> holds
|- (Ant f) ^ <*p*>
proof end;

theorem Th46: :: CALCUL_1:46  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 f being FinSequence of CQC-WFF st |- (f ^ <*p*>) ^ <*q*> holds
|- (f ^ <*('not' q)*>) ^ <*('not' p)*>
proof end;

theorem :: CALCUL_1:47  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 f being FinSequence of CQC-WFF st |- (f ^ <*('not' p)*>) ^ <*('not' q)*> holds
|- (f ^ <*q*>) ^ <*p*>
proof end;

theorem Th48: :: CALCUL_1:48  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 f being FinSequence of CQC-WFF st |- (f ^ <*('not' p)*>) ^ <*q*> holds
|- (f ^ <*('not' q)*>) ^ <*p*>
proof end;

theorem Th49: :: CALCUL_1:49  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 f being FinSequence of CQC-WFF st |- (f ^ <*p*>) ^ <*('not' q)*> holds
|- (f ^ <*q*>) ^ <*('not' p)*>
proof end;

theorem :: CALCUL_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, r, q being Element of CQC-WFF
for f being FinSequence of CQC-WFF st |- (f ^ <*p*>) ^ <*r*> & |- (f ^ <*q*>) ^ <*r*> holds
|- (f ^ <*(p 'or' q)*>) ^ <*r*>
proof end;

theorem :: CALCUL_1:51  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 f being FinSequence of CQC-WFF st |- f ^ <*p*> holds
|- f ^ <*(p 'or' q)*>
proof end;

theorem :: CALCUL_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p being Element of CQC-WFF
for f being FinSequence of CQC-WFF st |- f ^ <*q*> holds
|- f ^ <*(p 'or' q)*>
proof end;

theorem Th53: :: CALCUL_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, r, q being Element of CQC-WFF
for f being FinSequence of CQC-WFF st |- (f ^ <*p*>) ^ <*r*> & |- (f ^ <*q*>) ^ <*r*> holds
|- (f ^ <*(p 'or' q)*>) ^ <*r*>
proof end;

theorem Th54: :: CALCUL_1:54  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 f being FinSequence of CQC-WFF st |- f ^ <*p*> holds
|- f ^ <*('not' ('not' p))*>
proof end;

theorem Th55: :: CALCUL_1:55  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 f being FinSequence of CQC-WFF st |- f ^ <*('not' ('not' p))*> holds
|- f ^ <*p*>
proof end;

theorem :: CALCUL_1:56  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 f being FinSequence of CQC-WFF st |- f ^ <*(p => q)*> & |- f ^ <*p*> holds
|- f ^ <*q*>
proof end;

theorem Th57: :: CALCUL_1:57  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, y being bound_QC-variable holds ('not' p) . x,y = 'not' (p . x,y)
proof end;

theorem :: CALCUL_1:58  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
for f being FinSequence of CQC-WFF st ex y being bound_QC-variable st |- f ^ <*(p . x,y)*> holds
|- f ^ <*(Ex x,p)*>
proof end;

theorem Th59: :: CALCUL_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of CQC-WFF holds still_not-bound_in (f ^ g) = (still_not-bound_in f) \/ (still_not-bound_in g)
proof end;

theorem Th60: :: CALCUL_1:60  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 still_not-bound_in <*p*> = still_not-bound_in p
proof end;

theorem :: CALCUL_1:61  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, y being bound_QC-variable
for f being FinSequence of CQC-WFF st |- (f ^ <*(p . x,y)*>) ^ <*q*> & not y in still_not-bound_in ((f ^ <*(Ex x,p)*>) ^ <*q*>) holds
|- (f ^ <*(Ex x,p)*>) ^ <*q*>
proof end;

theorem Th62: :: CALCUL_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of CQC-WFF holds still_not-bound_in f = union { (still_not-bound_in p) where p is Element of CQC-WFF : ex i being Nat st
( i in dom f & p = f . i ) }
proof end;

theorem Th63: :: CALCUL_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of CQC-WFF holds still_not-bound_in f is finite
proof end;

theorem Th64: :: CALCUL_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( Card bound_QC-variables = alef 0 & not bound_QC-variables is finite )
proof end;

theorem Th65: :: CALCUL_1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of CQC-WFF holds
not for x being bound_QC-variable holds x in still_not-bound_in f
proof end;

theorem Th66: :: CALCUL_1:66  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
for f being FinSequence of CQC-WFF st |- f ^ <*(All x,p)*> holds
|- f ^ <*(All x,('not' ('not' p)))*>
proof end;

theorem Th67: :: CALCUL_1:67  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
for f being FinSequence of CQC-WFF st |- f ^ <*(All x,('not' ('not' p)))*> holds
|- f ^ <*(All x,p)*>
proof end;

theorem :: CALCUL_1:68  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
for f being FinSequence of CQC-WFF holds
( |- f ^ <*(All x,p)*> iff |- f ^ <*('not' (Ex x,('not' p)))*> )
proof end;