:: CALCUL_1 semantic presentation

registration
let c1 be FinSequence;
let c2 be set ;
cluster a1 | a2 -> FinSubsequence-like ;
coherence
c1 | c2 is FinSubsequence-like by FINSEQ_1:69;
end;

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

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

definition
let c1 be non empty set ;
let c2 be FinSequence of c1;
assume E2: len c2 > 0 ;
func Suc c2 -> Element of a1 equals :Def2: :: CALCUL_1:def 2
a2 . (len a2);
coherence
c2 . (len c2) is Element of c1
proof end;
end;

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

definition
let c1 be non empty set ;
let c2 be Element of c1;
let c3 be FinSequence of c1;
pred c2 is_tail_of c3 means :Def3: :: CALCUL_1:def 3
ex b1 being Nat st
( b1 in dom a3 & a3 . b1 = a2 );
end;

:: deftheorem Def3 defines is_tail_of CALCUL_1:def 3 :
for b1 being non empty set
for b2 being Element of b1
for b3 being FinSequence of b1 holds
( b2 is_tail_of b3 iff ex b4 being Nat st
( b4 in dom b3 & b3 . b4 = b2 ) );

definition
let c1, c2 be FinSequence of CQC-WFF ;
pred c1 is_Subsequence_of c2 means :Def4: :: CALCUL_1:def 4
ex b1 being Subset of NAT st a1 c= Seq (a2 | b1);
end;

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

theorem Th1: :: CALCUL_1:1
for b1, b2 being FinSequence of CQC-WFF st b1 is_Subsequence_of b2 holds
( rng b1 c= rng b2 & ex b3 being Subset of NAT st rng b1 c= rng (b2 | b3) )
proof end;

theorem Th2: :: CALCUL_1:2
for b1 being FinSequence of CQC-WFF st len b1 > 0 holds
( (len (Ant b1)) + 1 = len b1 & len (Ant b1) < len b1 )
proof end;

theorem Th3: :: CALCUL_1:3
for b1 being FinSequence of CQC-WFF st len b1 > 0 holds
( b1 = (Ant b1) ^ <*(Suc b1)*> & rng b1 = (rng (Ant b1)) \/ {(Suc b1)} )
proof end;

theorem Th4: :: CALCUL_1:4
for b1 being FinSequence of CQC-WFF st len b1 > 1 holds
len (Ant b1) > 0
proof end;

theorem Th5: :: CALCUL_1:5
for b1 being Element of CQC-WFF
for b2 being FinSequence of CQC-WFF holds
( Suc (b2 ^ <*b1*>) = b1 & Ant (b2 ^ <*b1*>) = b2 )
proof end;

theorem Th6: :: CALCUL_1:6
for b1, b2 being FinSequence holds
( len b1 <= len (b1 ^ b2) & len b2 <= len (b1 ^ b2) & ( b1 <> {} implies ( 1 <= len b1 & len b2 < len (b2 ^ b1) ) ) )
proof end;

theorem Th7: :: CALCUL_1:7
for b1, b2 being FinSequence of CQC-WFF holds Seq ((b1 ^ b2) | (dom b1)) = (b1 ^ b2) | (dom b1)
proof end;

theorem Th8: :: CALCUL_1:8
for b1, b2 being FinSequence of CQC-WFF holds b1 is_Subsequence_of b1 ^ b2
proof end;

theorem Th9: :: CALCUL_1:9
for b1, b2 being set
for b3 being FinSequence holds 1 < len ((b3 ^ <*b1*>) ^ <*b2*>)
proof end;

theorem Th10: :: CALCUL_1:10
for b1 being set
for b2 being FinSequence holds
( 1 <= len (b2 ^ <*b1*>) & len (b2 ^ <*b1*>) in dom (b2 ^ <*b1*>) )
proof end;

theorem Th11: :: CALCUL_1:11
for b1, b2 being Nat st 0 < b1 holds
len (Sgm ((Seg b2) \/ {(b2 + b1)})) = b2 + 1
proof end;

theorem Th12: :: CALCUL_1:12
for b1, b2 being Nat st 0 < b1 holds
dom (Sgm ((Seg b2) \/ {(b2 + b1)})) = Seg (b2 + 1)
proof end;

theorem Th13: :: CALCUL_1:13
for b1, b2 being FinSequence of CQC-WFF st 0 < len b1 holds
b1 is_Subsequence_of ((Ant b1) ^ b2) ^ <*(Suc b1)*>
proof end;

theorem Th14: :: CALCUL_1:14
for b1, b2 being set
for b3 being FinSequence of CQC-WFF holds
( 1 in dom <*b1,b2*> & 2 in dom <*b1,b2*> & (b3 ^ <*b1,b2*>) . ((len b3) + 1) = b1 & (b3 ^ <*b1,b2*>) . ((len b3) + 2) = b2 )
proof end;

definition
let c1 be FinSequence of CQC-WFF ;
func still_not-bound_in c1 -> Subset of bound_QC-variables means :Def5: :: CALCUL_1:def 5
for b1 being set holds
( b1 in a2 iff ex b2 being Natex b3 being Element of CQC-WFF st
( b2 in dom a1 & b3 = a1 . b2 & b1 in still_not-bound_in b3 ) );
existence
ex b1 being Subset of bound_QC-variables st
for b2 being set holds
( b2 in b1 iff ex b3 being Natex b4 being Element of CQC-WFF st
( b3 in dom c1 & b4 = c1 . b3 & b2 in still_not-bound_in b4 ) )
proof end;
uniqueness
for b1, b2 being Subset of bound_QC-variables st ( for b3 being set holds
( b3 in b1 iff ex b4 being Natex b5 being Element of CQC-WFF st
( b4 in dom c1 & b5 = c1 . b4 & b3 in still_not-bound_in b5 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4 being Natex b5 being Element of CQC-WFF st
( b4 in dom c1 & b5 = c1 . b4 & b3 in still_not-bound_in b5 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines still_not-bound_in CALCUL_1:def 5 :
for b1 being FinSequence of CQC-WFF
for b2 being Subset of bound_QC-variables holds
( b2 = still_not-bound_in b1 iff for b3 being set holds
( b3 in b2 iff ex b4 being Natex b5 being Element of CQC-WFF st
( b4 in dom b1 & b5 = b1 . b4 & b3 in still_not-bound_in b5 ) ) );

definition
func set_of_CQC-WFF-seq -> set means :Def6: :: CALCUL_1:def 6
for b1 being set holds
( b1 in a1 iff b1 is FinSequence of CQC-WFF );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff b2 is FinSequence of CQC-WFF )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff b3 is FinSequence of CQC-WFF ) ) & ( for b3 being set holds
( b3 in b2 iff b3 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 b2 being set holds
( b2 in b1 iff b2 is FinSequence of CQC-WFF ) );

definition
let c1 be FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :];
let c2 be Nat;
pred c1,c2 is_a_correct_step means :Def7: :: CALCUL_1:def 7
ex b1 being FinSequence of CQC-WFF st
( Suc b1 is_tail_of Ant b1 & (a1 . a2) `1 = b1 ) if (a1 . a2) `2 = 0
ex b1 being FinSequence of CQC-WFF st (a1 . a2) `1 = b1 ^ <*VERUM *> if (a1 . a2) `2 = 1
ex b1 being Natex b2, b3 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < a2 & Ant b2 is_Subsequence_of Ant b3 & Suc b2 = Suc b3 & (a1 . b1) `1 = b2 & (a1 . a2) `1 = b3 ) if (a1 . a2) `2 = 2
ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < a2 & 1 <= b2 & b2 < b1 & len b3 > 1 & len b4 > 1 & Ant (Ant b3) = Ant (Ant b4) & 'not' (Suc (Ant b3)) = Suc (Ant b4) & Suc b3 = Suc b4 & b3 = (a1 . b2) `1 & b4 = (a1 . b1) `1 & (Ant (Ant b3)) ^ <*(Suc b3)*> = (a1 . a2) `1 ) if (a1 . a2) `2 = 3
ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF ex b5 being Element of CQC-WFF st
( 1 <= b1 & b1 < a2 & 1 <= b2 & b2 < b1 & len b3 > 1 & Ant b3 = Ant b4 & Suc (Ant b3) = 'not' b5 & 'not' (Suc b3) = Suc b4 & b3 = (a1 . b2) `1 & b4 = (a1 . b1) `1 & (Ant (Ant b3)) ^ <*b5*> = (a1 . a2) `1 ) if (a1 . a2) `2 = 4
ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < a2 & 1 <= b2 & b2 < b1 & Ant b3 = Ant b4 & b3 = (a1 . b2) `1 & b4 = (a1 . b1) `1 & (Ant b3) ^ <*((Suc b3) '&' (Suc b4))*> = (a1 . a2) `1 ) if (a1 . a2) `2 = 5
ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < a2 & b3 '&' b4 = Suc b2 & b2 = (a1 . b1) `1 & (Ant b2) ^ <*b3*> = (a1 . a2) `1 ) if (a1 . a2) `2 = 6
ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < a2 & b3 '&' b4 = Suc b2 & b2 = (a1 . b1) `1 & (Ant b2) ^ <*b4*> = (a1 . a2) `1 ) if (a1 . a2) `2 = 7
ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < a2 & Suc b2 = All b4,b3 & b2 = (a1 . b1) `1 & (Ant b2) ^ <*(b3 . b4,b5)*> = (a1 . a2) `1 ) if (a1 . a2) `2 = 8
ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < a2 & Suc b2 = b3 . b4,b5 & not b5 in still_not-bound_in (Ant b2) & not b5 in still_not-bound_in (All b4,b3) & b2 = (a1 . b1) `1 & (Ant b2) ^ <*(All b4,b3)*> = (a1 . a2) `1 ) if (a1 . a2) `2 = 9
;
consistency
( ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 1 implies ( ex b1 being FinSequence of CQC-WFF st
( Suc b1 is_tail_of Ant b1 & (c1 . c2) `1 = b1 ) iff ex b1 being FinSequence of CQC-WFF st (c1 . c2) `1 = b1 ^ <*VERUM *> ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 2 implies ( ex b1 being FinSequence of CQC-WFF st
( Suc b1 is_tail_of Ant b1 & (c1 . c2) `1 = b1 ) iff ex b1 being Natex b2, b3 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & Ant b2 is_Subsequence_of Ant b3 & Suc b2 = Suc b3 & (c1 . b1) `1 = b2 & (c1 . c2) `1 = b3 ) ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 3 implies ( ex b1 being FinSequence of CQC-WFF st
( Suc b1 is_tail_of Ant b1 & (c1 . c2) `1 = b1 ) iff ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & len b4 > 1 & Ant (Ant b3) = Ant (Ant b4) & 'not' (Suc (Ant b3)) = Suc (Ant b4) & Suc b3 = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*(Suc b3)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 4 implies ( ex b1 being FinSequence of CQC-WFF st
( Suc b1 is_tail_of Ant b1 & (c1 . c2) `1 = b1 ) iff ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF ex b5 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & Ant b3 = Ant b4 & Suc (Ant b3) = 'not' b5 & 'not' (Suc b3) = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*b5*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 5 implies ( ex b1 being FinSequence of CQC-WFF st
( Suc b1 is_tail_of Ant b1 & (c1 . c2) `1 = b1 ) iff ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & Ant b3 = Ant b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant b3) ^ <*((Suc b3) '&' (Suc b4))*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 6 implies ( ex b1 being FinSequence of CQC-WFF st
( Suc b1 is_tail_of Ant b1 & (c1 . c2) `1 = b1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b3*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 7 implies ( ex b1 being FinSequence of CQC-WFF st
( Suc b1 is_tail_of Ant b1 & (c1 . c2) `1 = b1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b4*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 8 implies ( ex b1 being FinSequence of CQC-WFF st
( Suc b1 is_tail_of Ant b1 & (c1 . c2) `1 = b1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = All b4,b3 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(b3 . b4,b5)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 0 & (c1 . c2) `2 = 9 implies ( ex b1 being FinSequence of CQC-WFF st
( Suc b1 is_tail_of Ant b1 & (c1 . c2) `1 = b1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = b3 . b4,b5 & not b5 in still_not-bound_in (Ant b2) & not b5 in still_not-bound_in (All b4,b3) & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(All b4,b3)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 2 implies ( ex b1 being FinSequence of CQC-WFF st (c1 . c2) `1 = b1 ^ <*VERUM *> iff ex b1 being Natex b2, b3 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & Ant b2 is_Subsequence_of Ant b3 & Suc b2 = Suc b3 & (c1 . b1) `1 = b2 & (c1 . c2) `1 = b3 ) ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 3 implies ( ex b1 being FinSequence of CQC-WFF st (c1 . c2) `1 = b1 ^ <*VERUM *> iff ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & len b4 > 1 & Ant (Ant b3) = Ant (Ant b4) & 'not' (Suc (Ant b3)) = Suc (Ant b4) & Suc b3 = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*(Suc b3)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 4 implies ( ex b1 being FinSequence of CQC-WFF st (c1 . c2) `1 = b1 ^ <*VERUM *> iff ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF ex b5 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & Ant b3 = Ant b4 & Suc (Ant b3) = 'not' b5 & 'not' (Suc b3) = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*b5*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 5 implies ( ex b1 being FinSequence of CQC-WFF st (c1 . c2) `1 = b1 ^ <*VERUM *> iff ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & Ant b3 = Ant b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant b3) ^ <*((Suc b3) '&' (Suc b4))*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 6 implies ( ex b1 being FinSequence of CQC-WFF st (c1 . c2) `1 = b1 ^ <*VERUM *> iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b3*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 7 implies ( ex b1 being FinSequence of CQC-WFF st (c1 . c2) `1 = b1 ^ <*VERUM *> iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b4*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 8 implies ( ex b1 being FinSequence of CQC-WFF st (c1 . c2) `1 = b1 ^ <*VERUM *> iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = All b4,b3 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(b3 . b4,b5)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 1 & (c1 . c2) `2 = 9 implies ( ex b1 being FinSequence of CQC-WFF st (c1 . c2) `1 = b1 ^ <*VERUM *> iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = b3 . b4,b5 & not b5 in still_not-bound_in (Ant b2) & not b5 in still_not-bound_in (All b4,b3) & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(All b4,b3)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 2 & (c1 . c2) `2 = 3 implies ( ex b1 being Natex b2, b3 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & Ant b2 is_Subsequence_of Ant b3 & Suc b2 = Suc b3 & (c1 . b1) `1 = b2 & (c1 . c2) `1 = b3 ) iff ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & len b4 > 1 & Ant (Ant b3) = Ant (Ant b4) & 'not' (Suc (Ant b3)) = Suc (Ant b4) & Suc b3 = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*(Suc b3)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 2 & (c1 . c2) `2 = 4 implies ( ex b1 being Natex b2, b3 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & Ant b2 is_Subsequence_of Ant b3 & Suc b2 = Suc b3 & (c1 . b1) `1 = b2 & (c1 . c2) `1 = b3 ) iff ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF ex b5 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & Ant b3 = Ant b4 & Suc (Ant b3) = 'not' b5 & 'not' (Suc b3) = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*b5*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 2 & (c1 . c2) `2 = 5 implies ( ex b1 being Natex b2, b3 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & Ant b2 is_Subsequence_of Ant b3 & Suc b2 = Suc b3 & (c1 . b1) `1 = b2 & (c1 . c2) `1 = b3 ) iff ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & Ant b3 = Ant b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant b3) ^ <*((Suc b3) '&' (Suc b4))*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 2 & (c1 . c2) `2 = 6 implies ( ex b1 being Natex b2, b3 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & Ant b2 is_Subsequence_of Ant b3 & Suc b2 = Suc b3 & (c1 . b1) `1 = b2 & (c1 . c2) `1 = b3 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b3*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 2 & (c1 . c2) `2 = 7 implies ( ex b1 being Natex b2, b3 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & Ant b2 is_Subsequence_of Ant b3 & Suc b2 = Suc b3 & (c1 . b1) `1 = b2 & (c1 . c2) `1 = b3 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b4*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 2 & (c1 . c2) `2 = 8 implies ( ex b1 being Natex b2, b3 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & Ant b2 is_Subsequence_of Ant b3 & Suc b2 = Suc b3 & (c1 . b1) `1 = b2 & (c1 . c2) `1 = b3 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = All b4,b3 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(b3 . b4,b5)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 2 & (c1 . c2) `2 = 9 implies ( ex b1 being Natex b2, b3 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & Ant b2 is_Subsequence_of Ant b3 & Suc b2 = Suc b3 & (c1 . b1) `1 = b2 & (c1 . c2) `1 = b3 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = b3 . b4,b5 & not b5 in still_not-bound_in (Ant b2) & not b5 in still_not-bound_in (All b4,b3) & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(All b4,b3)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 3 & (c1 . c2) `2 = 4 implies ( ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & len b4 > 1 & Ant (Ant b3) = Ant (Ant b4) & 'not' (Suc (Ant b3)) = Suc (Ant b4) & Suc b3 = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*(Suc b3)*> = (c1 . c2) `1 ) iff ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF ex b5 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & Ant b3 = Ant b4 & Suc (Ant b3) = 'not' b5 & 'not' (Suc b3) = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*b5*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 3 & (c1 . c2) `2 = 5 implies ( ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & len b4 > 1 & Ant (Ant b3) = Ant (Ant b4) & 'not' (Suc (Ant b3)) = Suc (Ant b4) & Suc b3 = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*(Suc b3)*> = (c1 . c2) `1 ) iff ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & Ant b3 = Ant b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant b3) ^ <*((Suc b3) '&' (Suc b4))*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 3 & (c1 . c2) `2 = 6 implies ( ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & len b4 > 1 & Ant (Ant b3) = Ant (Ant b4) & 'not' (Suc (Ant b3)) = Suc (Ant b4) & Suc b3 = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*(Suc b3)*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b3*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 3 & (c1 . c2) `2 = 7 implies ( ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & len b4 > 1 & Ant (Ant b3) = Ant (Ant b4) & 'not' (Suc (Ant b3)) = Suc (Ant b4) & Suc b3 = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*(Suc b3)*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b4*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 3 & (c1 . c2) `2 = 8 implies ( ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & len b4 > 1 & Ant (Ant b3) = Ant (Ant b4) & 'not' (Suc (Ant b3)) = Suc (Ant b4) & Suc b3 = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*(Suc b3)*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = All b4,b3 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(b3 . b4,b5)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 3 & (c1 . c2) `2 = 9 implies ( ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & len b4 > 1 & Ant (Ant b3) = Ant (Ant b4) & 'not' (Suc (Ant b3)) = Suc (Ant b4) & Suc b3 = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*(Suc b3)*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = b3 . b4,b5 & not b5 in still_not-bound_in (Ant b2) & not b5 in still_not-bound_in (All b4,b3) & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(All b4,b3)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 4 & (c1 . c2) `2 = 5 implies ( ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF ex b5 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & Ant b3 = Ant b4 & Suc (Ant b3) = 'not' b5 & 'not' (Suc b3) = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*b5*> = (c1 . c2) `1 ) iff ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & Ant b3 = Ant b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant b3) ^ <*((Suc b3) '&' (Suc b4))*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 4 & (c1 . c2) `2 = 6 implies ( ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF ex b5 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & Ant b3 = Ant b4 & Suc (Ant b3) = 'not' b5 & 'not' (Suc b3) = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*b5*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b3*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 4 & (c1 . c2) `2 = 7 implies ( ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF ex b5 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & Ant b3 = Ant b4 & Suc (Ant b3) = 'not' b5 & 'not' (Suc b3) = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*b5*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b4*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 4 & (c1 . c2) `2 = 8 implies ( ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF ex b5 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & Ant b3 = Ant b4 & Suc (Ant b3) = 'not' b5 & 'not' (Suc b3) = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*b5*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = All b4,b3 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(b3 . b4,b5)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 4 & (c1 . c2) `2 = 9 implies ( ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF ex b5 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & len b3 > 1 & Ant b3 = Ant b4 & Suc (Ant b3) = 'not' b5 & 'not' (Suc b3) = Suc b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant (Ant b3)) ^ <*b5*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = b3 . b4,b5 & not b5 in still_not-bound_in (Ant b2) & not b5 in still_not-bound_in (All b4,b3) & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(All b4,b3)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 5 & (c1 . c2) `2 = 6 implies ( ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & Ant b3 = Ant b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant b3) ^ <*((Suc b3) '&' (Suc b4))*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b3*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 5 & (c1 . c2) `2 = 7 implies ( ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & Ant b3 = Ant b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant b3) ^ <*((Suc b3) '&' (Suc b4))*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b4*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 5 & (c1 . c2) `2 = 8 implies ( ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & Ant b3 = Ant b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant b3) ^ <*((Suc b3) '&' (Suc b4))*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = All b4,b3 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(b3 . b4,b5)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 5 & (c1 . c2) `2 = 9 implies ( ex b1, b2 being Natex b3, b4 being FinSequence of CQC-WFF st
( 1 <= b1 & b1 < c2 & 1 <= b2 & b2 < b1 & Ant b3 = Ant b4 & b3 = (c1 . b2) `1 & b4 = (c1 . b1) `1 & (Ant b3) ^ <*((Suc b3) '&' (Suc b4))*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = b3 . b4,b5 & not b5 in still_not-bound_in (Ant b2) & not b5 in still_not-bound_in (All b4,b3) & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(All b4,b3)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 6 & (c1 . c2) `2 = 7 implies ( ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b3*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b4*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 6 & (c1 . c2) `2 = 8 implies ( ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b3*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = All b4,b3 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(b3 . b4,b5)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 6 & (c1 . c2) `2 = 9 implies ( ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b3*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = b3 . b4,b5 & not b5 in still_not-bound_in (Ant b2) & not b5 in still_not-bound_in (All b4,b3) & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(All b4,b3)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 7 & (c1 . c2) `2 = 8 implies ( ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b4*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = All b4,b3 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(b3 . b4,b5)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 7 & (c1 . c2) `2 = 9 implies ( ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3, b4 being Element of CQC-WFF st
( 1 <= b1 & b1 < c2 & b3 '&' b4 = Suc b2 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*b4*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = b3 . b4,b5 & not b5 in still_not-bound_in (Ant b2) & not b5 in still_not-bound_in (All b4,b3) & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(All b4,b3)*> = (c1 . c2) `1 ) ) ) & ( (c1 . c2) `2 = 8 & (c1 . c2) `2 = 9 implies ( ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = All b4,b3 & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(b3 . b4,b5)*> = (c1 . c2) `1 ) iff ex b1 being Natex b2 being FinSequence of CQC-WFF ex b3 being Element of CQC-WFF ex b4, b5 being bound_QC-variable st
( 1 <= b1 & b1 < c2 & Suc b2 = b3 . b4,b5 & not b5 in still_not-bound_in (Ant b2) & not b5 in still_not-bound_in (All b4,b3) & b2 = (c1 . b1) `1 & (Ant b2) ^ <*(All b4,b3)*> = (c1 . c2) `1 ) ) ) ) ;
end;

:: deftheorem Def7 defines is_a_correct_step CALCUL_1:def 7 :
for b1 being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :]
for b2 being Nat holds
( ( (b1 . b2) `2 = 0 implies ( b1,b2 is_a_correct_step iff ex b3 being FinSequence of CQC-WFF st
( Suc b3 is_tail_of Ant b3 & (b1 . b2) `1 = b3 ) ) ) & ( (b1 . b2) `2 = 1 implies ( b1,b2 is_a_correct_step iff ex b3 being FinSequence of CQC-WFF st (b1 . b2) `1 = b3 ^ <*VERUM *> ) ) & ( (b1 . b2) `2 = 2 implies ( b1,b2 is_a_correct_step iff ex b3 being Natex b4, b5 being FinSequence of CQC-WFF st
( 1 <= b3 & b3 < b2 & Ant b4 is_Subsequence_of Ant b5 & Suc b4 = Suc b5 & (b1 . b3) `1 = b4 & (b1 . b2) `1 = b5 ) ) ) & ( (b1 . b2) `2 = 3 implies ( b1,b2 is_a_correct_step iff ex b3, b4 being Natex b5, b6 being FinSequence of CQC-WFF st
( 1 <= b3 & b3 < b2 & 1 <= b4 & b4 < b3 & len b5 > 1 & len b6 > 1 & Ant (Ant b5) = Ant (Ant b6) & 'not' (Suc (Ant b5)) = Suc (Ant b6) & Suc b5 = Suc b6 & b5 = (b1 . b4) `1 & b6 = (b1 . b3) `1 & (Ant (Ant b5)) ^ <*(Suc b5)*> = (b1 . b2) `1 ) ) ) & ( (b1 . b2) `2 = 4 implies ( b1,b2 is_a_correct_step iff ex b3, b4 being Natex b5, b6 being FinSequence of CQC-WFF ex b7 being Element of CQC-WFF st
( 1 <= b3 & b3 < b2 & 1 <= b4 & b4 < b3 & len b5 > 1 & Ant b5 = Ant b6 & Suc (Ant b5) = 'not' b7 & 'not' (Suc b5) = Suc b6 & b5 = (b1 . b4) `1 & b6 = (b1 . b3) `1 & (Ant (Ant b5)) ^ <*b7*> = (b1 . b2) `1 ) ) ) & ( (b1 . b2) `2 = 5 implies ( b1,b2 is_a_correct_step iff ex b3, b4 being Natex b5, b6 being FinSequence of CQC-WFF st
( 1 <= b3 & b3 < b2 & 1 <= b4 & b4 < b3 & Ant b5 = Ant b6 & b5 = (b1 . b4) `1 & b6 = (b1 . b3) `1 & (Ant b5) ^ <*((Suc b5) '&' (Suc b6))*> = (b1 . b2) `1 ) ) ) & ( (b1 . b2) `2 = 6 implies ( b1,b2 is_a_correct_step iff ex b3 being Natex b4 being FinSequence of CQC-WFF ex b5, b6 being Element of CQC-WFF st
( 1 <= b3 & b3 < b2 & b5 '&' b6 = Suc b4 & b4 = (b1 . b3) `1 & (Ant b4) ^ <*b5*> = (b1 . b2) `1 ) ) ) & ( (b1 . b2) `2 = 7 implies ( b1,b2 is_a_correct_step iff ex b3 being Natex b4 being FinSequence of CQC-WFF ex b5, b6 being Element of CQC-WFF st
( 1 <= b3 & b3 < b2 & b5 '&' b6 = Suc b4 & b4 = (b1 . b3) `1 & (Ant b4) ^ <*b6*> = (b1 . b2) `1 ) ) ) & ( (b1 . b2) `2 = 8 implies ( b1,b2 is_a_correct_step iff ex b3 being Natex b4 being FinSequence of CQC-WFF ex b5 being Element of CQC-WFF ex b6, b7 being bound_QC-variable st
( 1 <= b3 & b3 < b2 & Suc b4 = All b6,b5 & b4 = (b1 . b3) `1 & (Ant b4) ^ <*(b5 . b6,b7)*> = (b1 . b2) `1 ) ) ) & ( (b1 . b2) `2 = 9 implies ( b1,b2 is_a_correct_step iff ex b3 being Natex b4 being FinSequence of CQC-WFF ex b5 being Element of CQC-WFF ex b6, b7 being bound_QC-variable st
( 1 <= b3 & b3 < b2 & Suc b4 = b5 . b6,b7 & not b7 in still_not-bound_in (Ant b4) & not b7 in still_not-bound_in (All b6,b5) & b4 = (b1 . b3) `1 & (Ant b4) ^ <*(All b6,b5)*> = (b1 . b2) `1 ) ) ) );

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

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

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

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

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

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

definition
let c1 be Subset of CQC-WFF ;
let c2 be non empty set ;
let c3 be interpretation of c2;
let c4 be Element of Valuations_in c2;
pred c3,c4 |= c1 means :Def11: :: CALCUL_1:def 11
for b1 being Element of CQC-WFF st b1 in a1 holds
a3,a4 |= b1;
end;

:: deftheorem Def11 defines |= CALCUL_1:def 11 :
for b1 being Subset of CQC-WFF
for b2 being non empty set
for b3 being interpretation of b2
for b4 being Element of Valuations_in b2 holds
( b3,b4 |= b1 iff for b5 being Element of CQC-WFF st b5 in b1 holds
b3,b4 |= b5 );

definition
let c1 be Subset of CQC-WFF ;
let c2 be Element of CQC-WFF ;
pred c1 |= c2 means :: CALCUL_1:def 12
for b1 being non empty set
for b2 being interpretation of b1
for b3 being Element of Valuations_in b1 st b2,b3 |= a1 holds
b2,b3 |= a2;
end;

:: deftheorem Def12 defines |= CALCUL_1:def 12 :
for b1 being Subset of CQC-WFF
for b2 being Element of CQC-WFF holds
( b1 |= b2 iff for b3 being non empty set
for b4 being interpretation of b3
for b5 being Element of Valuations_in b3 st b4,b5 |= b1 holds
b4,b5 |= b2 );

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

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

definition
let c1 be FinSequence of CQC-WFF ;
let c2 be non empty set ;
let c3 be interpretation of c2;
let c4 be Element of Valuations_in c2;
pred c3,c4 |= c1 means :Def14: :: CALCUL_1:def 14
a3,a4 |= rng a1;
end;

:: deftheorem Def14 defines |= CALCUL_1:def 14 :
for b1 being FinSequence of CQC-WFF
for b2 being non empty set
for b3 being interpretation of b2
for b4 being Element of Valuations_in b2 holds
( b3,b4 |= b1 iff b3,b4 |= rng b1 );

definition
let c1 be FinSequence of CQC-WFF ;
let c2 be Element of CQC-WFF ;
pred c1 |= c2 means :Def15: :: CALCUL_1:def 15
for b1 being non empty set
for b2 being interpretation of b1
for b3 being Element of Valuations_in b1 st b2,b3 |= a1 holds
b2,b3 |= a2;
end;

:: deftheorem Def15 defines |= CALCUL_1:def 15 :
for b1 being FinSequence of CQC-WFF
for b2 being Element of CQC-WFF holds
( b1 |= b2 iff for b3 being non empty set
for b4 being interpretation of b3
for b5 being Element of Valuations_in b3 st b4,b5 |= b1 holds
b4,b5 |= b2 );

theorem Th15: :: CALCUL_1:15
for b1 being FinSequence of CQC-WFF st Suc b1 is_tail_of Ant b1 holds
Ant b1 |= Suc b1
proof end;

theorem Th16: :: CALCUL_1:16
for b1, b2 being FinSequence of CQC-WFF st Ant b1 is_Subsequence_of Ant b2 & Suc b1 = Suc b2 & Ant b1 |= Suc b1 holds
Ant b2 |= Suc b2
proof end;

theorem Th17: :: CALCUL_1:17
for b1 being non empty set
for b2 being interpretation of b1
for b3 being Element of Valuations_in b1
for b4 being FinSequence of CQC-WFF st len b4 > 0 holds
( ( b2,b3 |= Ant b4 & b2,b3 |= Suc b4 ) iff b2,b3 |= b4 )
proof end;

theorem Th18: :: CALCUL_1:18
for b1, b2 being FinSequence of CQC-WFF st len b1 > 1 & len b2 > 1 & Ant (Ant b1) = Ant (Ant b2) & 'not' (Suc (Ant b1)) = Suc (Ant b2) & Suc b1 = Suc b2 & Ant b1 |= Suc b1 & Ant b2 |= Suc b2 holds
Ant (Ant b1) |= Suc b1
proof end;

theorem Th19: :: CALCUL_1:19
for b1 being Element of CQC-WFF
for b2, b3 being FinSequence of CQC-WFF st len b2 > 1 & Ant b2 = Ant b3 & 'not' b1 = Suc (Ant b2) & 'not' (Suc b2) = Suc b3 & Ant b2 |= Suc b2 & Ant b3 |= Suc b3 holds
Ant (Ant b2) |= b1
proof end;

theorem Th20: :: CALCUL_1:20
for b1, b2 being FinSequence of CQC-WFF st Ant b1 = Ant b2 & Ant b1 |= Suc b1 & Ant b2 |= Suc b2 holds
Ant b1 |= (Suc b1) '&' (Suc b2)
proof end;

theorem Th21: :: CALCUL_1:21
for b1, b2 being Element of CQC-WFF
for b3 being FinSequence of CQC-WFF st Suc b3 = b1 '&' b2 & Ant b3 |= b1 '&' b2 holds
Ant b3 |= b1
proof end;

theorem Th22: :: CALCUL_1:22
for b1, b2 being Element of CQC-WFF
for b3 being FinSequence of CQC-WFF st Suc b3 = b1 '&' b2 & Ant b3 |= b1 '&' b2 holds
Ant b3 |= b2
proof end;

theorem Th23: :: CALCUL_1:23
for b1 being Element of CQC-WFF
for b2 being non empty set
for b3 being interpretation of b2
for b4 being Element of Valuations_in b2
for b5 being CQC_Substitution holds
( b3,b4 |= [b1,b5] iff b3,b4 |= b1 )
proof end;

theorem Th24: :: CALCUL_1:24
for b1 being Element of CQC-WFF
for b2, b3 being bound_QC-variable
for b4 being non empty set
for b5 being interpretation of b4
for b6 being Element of Valuations_in b4 holds
( b5,b6 |= b1 . b2,b3 iff ex b7 being Element of b4 st
( b6 . b3 = b7 & b5,b6 . (b2 | b7) |= b1 ) )
proof end;

theorem Th25: :: CALCUL_1:25
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable
for b3 being FinSequence of CQC-WFF st Suc b3 = All b2,b1 & Ant b3 |= Suc b3 holds
for b4 being bound_QC-variable holds Ant b3 |= b1 . b2,b4
proof end;

theorem Th26: :: CALCUL_1:26
for b1 being bound_QC-variable
for b2 being non empty set
for b3 being Element of Valuations_in b2
for b4 being Element of b2
for b5 being set st b5 c= bound_QC-variables & not b1 in b5 holds
(b3 . (b1 | b4)) | b5 = b3 | b5
proof end;

theorem Th27: :: CALCUL_1:27
for b1 being non empty set
for b2 being interpretation of b1
for b3 being FinSequence of CQC-WFF
for b4, b5 being Element of Valuations_in b1 st b4 | (still_not-bound_in b3) = b5 | (still_not-bound_in b3) holds
( b2,b4 |= b3 iff b2,b5 |= b3 )
proof end;

theorem Th28: :: CALCUL_1:28
for b1 being Element of CQC-WFF
for b2, b3 being bound_QC-variable
for b4 being non empty set
for b5 being Element of Valuations_in b4
for b6 being Element of b4 st not b2 in still_not-bound_in (All b3,b1) holds
((b5 . (b2 | b6)) . (b3 | b6)) | (still_not-bound_in b1) = (b5 . (b3 | b6)) | (still_not-bound_in b1)
proof end;

theorem Th29: :: CALCUL_1:29
for b1 being Element of CQC-WFF
for b2, b3 being bound_QC-variable
for b4 being FinSequence of CQC-WFF st Suc b4 = b1 . b2,b3 & Ant b4 |= Suc b4 & not b3 in still_not-bound_in (Ant b4) & not b3 in still_not-bound_in (All b2,b1) holds
Ant b4 |= All b2,b1
proof end;

theorem Th30: :: CALCUL_1:30
for b1 being FinSequence of CQC-WFF holds Ant (b1 ^ <*VERUM *>) |= Suc (b1 ^ <*VERUM *>)
proof end;

theorem Th31: :: CALCUL_1:31
for b1 being Nat
for b2 being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] st 1 <= b1 & b1 <= len b2 & not (b2 . b1) `2 = 0 & not (b2 . b1) `2 = 1 & not (b2 . b1) `2 = 2 & not (b2 . b1) `2 = 3 & not (b2 . b1) `2 = 4 & not (b2 . b1) `2 = 5 & not (b2 . b1) `2 = 6 & not (b2 . b1) `2 = 7 & not (b2 . b1) `2 = 8 holds
(b2 . b1) `2 = 9
proof end;

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

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

theorem Th32: :: CALCUL_1:32
for b1 being Element of CQC-WFF
for b2 being Subset of CQC-WFF st b1 is_formal_provable_from b2 holds
b2 |= b1
proof end;

theorem Th33: :: CALCUL_1:33
for b1 being FinSequence of CQC-WFF st Suc b1 is_tail_of Ant b1 holds
|- b1
proof end;

theorem Th34: :: CALCUL_1:34
for b1 being Nat
for b2, b3 being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] st 1 <= b1 & b1 <= len b2 holds
( b2,b1 is_a_correct_step iff b2 ^ b3,b1 is_a_correct_step )
proof end;

theorem Th35: :: CALCUL_1:35
for b1 being Nat
for b2, b3 being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] st 1 <= b1 & b1 <= len b2 & b2,b1 is_a_correct_step holds
b3 ^ b2,b1 + (len b3) is_a_correct_step
proof end;

theorem Th36: :: CALCUL_1:36
for b1, b2 being FinSequence of CQC-WFF st Ant b1 is_Subsequence_of Ant b2 & Suc b1 = Suc b2 & |- b1 holds
|- b2
proof end;

theorem Th37: :: CALCUL_1:37
for b1, b2 being FinSequence of CQC-WFF st 1 < len b1 & 1 < len b2 & Ant (Ant b1) = Ant (Ant b2) & 'not' (Suc (Ant b1)) = Suc (Ant b2) & Suc b1 = Suc b2 & |- b1 & |- b2 holds
|- (Ant (Ant b1)) ^ <*(Suc b1)*>
proof end;

theorem Th38: :: CALCUL_1:38
for b1 being Element of CQC-WFF
for b2, b3 being FinSequence of CQC-WFF st len b2 > 1 & Ant b2 = Ant b3 & Suc (Ant b2) = 'not' b1 & 'not' (Suc b2) = Suc b3 & |- b2 & |- b3 holds
|- (Ant (Ant b2)) ^ <*b1*>
proof end;

theorem Th39: :: CALCUL_1:39
for b1, b2 being FinSequence of CQC-WFF st Ant b1 = Ant b2 & |- b1 & |- b2 holds
|- (Ant b1) ^ <*((Suc b1) '&' (Suc b2))*>
proof end;

theorem Th40: :: CALCUL_1:40
for b1, b2 being Element of CQC-WFF
for b3 being FinSequence of CQC-WFF st b1 '&' b2 = Suc b3 & |- b3 holds
|- (Ant b3) ^ <*b1*>
proof end;

theorem Th41: :: CALCUL_1:41
for b1, b2 being Element of CQC-WFF
for b3 being FinSequence of CQC-WFF st b1 '&' b2 = Suc b3 & |- b3 holds
|- (Ant b3) ^ <*b2*>
proof end;

theorem Th42: :: CALCUL_1:42
for b1 being Element of CQC-WFF
for b2, b3 being bound_QC-variable
for b4 being FinSequence of CQC-WFF st Suc b4 = All b2,b1 & |- b4 holds
|- (Ant b4) ^ <*(b1 . b2,b3)*>
proof end;

theorem Th43: :: CALCUL_1:43
for b1 being Element of CQC-WFF
for b2, b3 being bound_QC-variable
for b4 being FinSequence of CQC-WFF st Suc b4 = b1 . b2,b3 & not b3 in still_not-bound_in (Ant b4) & not b3 in still_not-bound_in (All b2,b1) & |- b4 holds
|- (Ant b4) ^ <*(All b2,b1)*>
proof end;

theorem Th44: :: CALCUL_1:44
for b1 being Element of CQC-WFF
for b2 being FinSequence of CQC-WFF st |- b2 & |- (Ant b2) ^ <*('not' (Suc b2))*> holds
|- (Ant b2) ^ <*b1*>
proof end;

theorem Th45: :: CALCUL_1:45
for b1 being Element of CQC-WFF
for b2 being FinSequence of CQC-WFF st 1 <= len b2 & |- b2 & |- b2 ^ <*b1*> holds
|- (Ant b2) ^ <*b1*>
proof end;

theorem Th46: :: CALCUL_1:46
for b1, b2 being Element of CQC-WFF
for b3 being FinSequence of CQC-WFF st |- (b3 ^ <*b1*>) ^ <*b2*> holds
|- (b3 ^ <*('not' b2)*>) ^ <*('not' b1)*>
proof end;

theorem Th47: :: CALCUL_1:47
for b1, b2 being Element of CQC-WFF
for b3 being FinSequence of CQC-WFF st |- (b3 ^ <*('not' b1)*>) ^ <*('not' b2)*> holds
|- (b3 ^ <*b2*>) ^ <*b1*>
proof end;

theorem Th48: :: CALCUL_1:48
for b1, b2 being Element of CQC-WFF
for b3 being FinSequence of CQC-WFF st |- (b3 ^ <*('not' b1)*>) ^ <*b2*> holds
|- (b3 ^ <*('not' b2)*>) ^ <*b1*>
proof end;

theorem Th49: :: CALCUL_1:49
for b1, b2 being Element of CQC-WFF
for b3 being FinSequence of CQC-WFF st |- (b3 ^ <*b1*>) ^ <*('not' b2)*> holds
|- (b3 ^ <*b2*>) ^ <*('not' b1)*>
proof end;

theorem Th50: :: CALCUL_1:50
for b1, b2, b3 being Element of CQC-WFF
for b4 being FinSequence of CQC-WFF st |- (b4 ^ <*b1*>) ^ <*b2*> & |- (b4 ^ <*b3*>) ^ <*b2*> holds
|- (b4 ^ <*(b1 'or' b3)*>) ^ <*b2*>
proof end;

theorem Th51: :: CALCUL_1:51
for b1, b2 being Element of CQC-WFF
for b3 being FinSequence of CQC-WFF st |- b3 ^ <*b1*> holds
|- b3 ^ <*(b1 'or' b2)*>
proof end;

theorem Th52: :: CALCUL_1:52
for b1, b2 being Element of CQC-WFF
for b3 being FinSequence of CQC-WFF st |- b3 ^ <*b1*> holds
|- b3 ^ <*(b2 'or' b1)*>
proof end;

theorem Th53: :: CALCUL_1:53
for b1, b2, b3 being Element of CQC-WFF
for b4 being FinSequence of CQC-WFF st |- (b4 ^ <*b1*>) ^ <*b2*> & |- (b4 ^ <*b3*>) ^ <*b2*> holds
|- (b4 ^ <*(b1 'or' b3)*>) ^ <*b2*>
proof end;

theorem Th54: :: CALCUL_1:54
for b1 being Element of CQC-WFF
for b2 being FinSequence of CQC-WFF st |- b2 ^ <*b1*> holds
|- b2 ^ <*('not' ('not' b1))*>
proof end;

theorem Th55: :: CALCUL_1:55
for b1 being Element of CQC-WFF
for b2 being FinSequence of CQC-WFF st |- b2 ^ <*('not' ('not' b1))*> holds
|- b2 ^ <*b1*>
proof end;

theorem Th56: :: CALCUL_1:56
for b1, b2 being Element of CQC-WFF
for b3 being FinSequence of CQC-WFF st |- b3 ^ <*(b1 => b2)*> & |- b3 ^ <*b1*> holds
|- b3 ^ <*b2*>
proof end;

theorem Th57: :: CALCUL_1:57
for b1 being Element of CQC-WFF
for b2, b3 being bound_QC-variable holds ('not' b1) . b2,b3 = 'not' (b1 . b2,b3)
proof end;

theorem Th58: :: CALCUL_1:58
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable
for b3 being FinSequence of CQC-WFF st ex b4 being bound_QC-variable st |- b3 ^ <*(b1 . b2,b4)*> holds
|- b3 ^ <*(Ex b2,b1)*>
proof end;

theorem Th59: :: CALCUL_1:59
for b1, b2 being FinSequence of CQC-WFF holds still_not-bound_in (b1 ^ b2) = (still_not-bound_in b1) \/ (still_not-bound_in b2)
proof end;

theorem Th60: :: CALCUL_1:60
for b1 being Element of CQC-WFF holds still_not-bound_in <*b1*> = still_not-bound_in b1
proof end;

theorem Th61: :: CALCUL_1:61
for b1, b2 being Element of CQC-WFF
for b3, b4 being bound_QC-variable
for b5 being FinSequence of CQC-WFF st |- (b5 ^ <*(b1 . b3,b4)*>) ^ <*b2*> & not b4 in still_not-bound_in ((b5 ^ <*(Ex b3,b1)*>) ^ <*b2*>) holds
|- (b5 ^ <*(Ex b3,b1)*>) ^ <*b2*>
proof end;

theorem Th62: :: CALCUL_1:62
for b1 being FinSequence of CQC-WFF holds still_not-bound_in b1 = union { (still_not-bound_in b2) where B is Element of CQC-WFF : ex b1 being Nat st
( b3 in dom b1 & b2 = b1 . b3 ) }
proof end;

theorem Th63: :: CALCUL_1:63
for b1 being FinSequence of CQC-WFF holds still_not-bound_in b1 is finite
proof end;

theorem Th64: :: CALCUL_1:64
( Card bound_QC-variables = alef 0 & not bound_QC-variables is finite )
proof end;

theorem Th65: :: CALCUL_1:65
for b1 being FinSequence of CQC-WFF holds
not for b2 being bound_QC-variable holds b2 in still_not-bound_in b1
proof end;

theorem Th66: :: CALCUL_1:66
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable
for b3 being FinSequence of CQC-WFF st |- b3 ^ <*(All b2,b1)*> holds
|- b3 ^ <*(All b2,('not' ('not' b1)))*>
proof end;

theorem Th67: :: CALCUL_1:67
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable
for b3 being FinSequence of CQC-WFF st |- b3 ^ <*(All b2,('not' ('not' b1)))*> holds
|- b3 ^ <*(All b2,b1)*>
proof end;

theorem Th68: :: CALCUL_1:68
for b1 being Element of CQC-WFF
for b2 being bound_QC-variable
for b3 being FinSequence of CQC-WFF holds
( |- b3 ^ <*(All b2,b1)*> iff |- b3 ^ <*('not' (Ex b2,('not' b1)))*> )
proof end;