:: by Patrick Braselmann and Peter Koepke

::

:: Received September 25, 2004

:: Copyright (c) 2004-2019 Association of Mizar Users

definition

let D be non empty set ;

let f be FinSequence of D;

( ( len f > 0 implies ex b_{1} being FinSequence of D st

for i being Nat st len f = i + 1 holds

b_{1} = f | (Seg i) ) & ( not len f > 0 implies ex b_{1} being FinSequence of D st b_{1} = {} ) )

for b_{1}, b_{2} being FinSequence of D holds

( ( len f > 0 & ( for i being Nat st len f = i + 1 holds

b_{1} = f | (Seg i) ) & ( for i being Nat st len f = i + 1 holds

b_{2} = f | (Seg i) ) implies b_{1} = b_{2} ) & ( not len f > 0 & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )

for b_{1} being FinSequence of D holds verum
;

end;
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 for i being Nat st len f = i + 1 holds

it = f | (Seg i) if len f > 0

otherwise it = {} ;

( ( len f > 0 implies ex b

for i being Nat st len f = i + 1 holds

b

proof end;

uniqueness for b

( ( len f > 0 & ( for i being Nat st len f = i + 1 holds

b

b

proof end;

consistency for b

:: deftheorem Def1 defines Ant CALCUL_1:def 1 :

for D being non empty set

for f, b_{3} being FinSequence of D holds

( ( len f > 0 implies ( b_{3} = Ant f iff for i being Nat st len f = i + 1 holds

b_{3} = f | (Seg i) ) ) & ( not len f > 0 implies ( b_{3} = Ant f iff b_{3} = {} ) ) );

for D being non empty set

for f, b

( ( len f > 0 implies ( b

b

definition

let Al be QC-alphabet ;

let f be FinSequence of CQC-WFF Al;

( ( len f > 0 implies f . (len f) is Element of CQC-WFF Al ) & ( not len f > 0 implies VERUM Al is Element of CQC-WFF Al ) )

for b_{1} being Element of CQC-WFF Al holds verum
;

end;
let f be FinSequence of CQC-WFF Al;

func Suc f -> Element of CQC-WFF Al equals :Def2: :: CALCUL_1:def 2

f . (len f) if len f > 0

otherwise VERUM Al;

coherence f . (len f) if len f > 0

otherwise VERUM Al;

( ( len f > 0 implies f . (len f) is Element of CQC-WFF Al ) & ( not len f > 0 implies VERUM Al is Element of CQC-WFF Al ) )

proof end;

consistency for b

:: deftheorem Def2 defines Suc CALCUL_1:def 2 :

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al holds

( ( len f > 0 implies Suc f = f . (len f) ) & ( not len f > 0 implies Suc f = VERUM Al ) );

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al holds

( ( len f > 0 implies Suc f = f . (len f) ) & ( not len f > 0 implies Suc f = VERUM Al ) );

definition
end;

:: deftheorem defines is_tail_of CALCUL_1:def 3 :

for f being Relation

for p being set holds

( p is_tail_of f iff p in rng f );

for f being Relation

for p being set holds

( p is_tail_of f iff p in rng f );

Lm1: now :: thesis: for f being FinSequence

for p being set st p is_tail_of f holds

ex i being Nat st

( i in dom f & f . i = p )

for p being set st p is_tail_of f holds

ex i being Nat st

( i in dom f & f . i = p )

let f be FinSequence; :: thesis: for p being set st p is_tail_of f holds

ex i being Nat st

( i in dom f & f . i = p )

let p be set ; :: thesis: ( p is_tail_of f implies ex i being Nat st

( i in dom f & f . i = p ) )

assume p is_tail_of f ; :: thesis: ex i being Nat st

( i in dom f & f . i = p )

then p in rng f ;

then consider i being object such that

A1: i in dom f and

A2: f . i = p by FUNCT_1:def 3;

reconsider i = i as Nat by A1;

take i = i; :: thesis: ( i in dom f & f . i = p )

thus ( i in dom f & f . i = p ) by A1, A2; :: thesis: verum

end;
ex i being Nat st

( i in dom f & f . i = p )

let p be set ; :: thesis: ( p is_tail_of f implies ex i being Nat st

( i in dom f & f . i = p ) )

assume p is_tail_of f ; :: thesis: ex i being Nat st

( i in dom f & f . i = p )

then p in rng f ;

then consider i being object such that

A1: i in dom f and

A2: f . i = p by FUNCT_1:def 3;

reconsider i = i as Nat by A1;

take i = i; :: thesis: ( i in dom f & f . i = p )

thus ( i in dom f & f . i = p ) by A1, A2; :: thesis: verum

Lm2: for f being FinSequence

for p being set st ex i being Element of NAT st

( i in dom f & f . i = p ) holds

p is_tail_of f

by FUNCT_1:def 3;

:: deftheorem defines is_Subsequence_of CALCUL_1:def 4 :

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al holds

( f is_Subsequence_of g iff ex N being Subset of NAT st f c= Seq (g | N) );

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al holds

( f is_Subsequence_of g iff ex N being Subset of NAT st f c= Seq (g | N) );

theorem Th1: :: CALCUL_1:1

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al 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) )

for f, g being FinSequence of CQC-WFF Al 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

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al st len f > 0 holds

( (len (Ant f)) + 1 = len f & len (Ant f) < len f )

for f being FinSequence of CQC-WFF Al st len f > 0 holds

( (len (Ant f)) + 1 = len f & len (Ant f) < len f )

proof end;

theorem Th3: :: CALCUL_1:3

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al st len f > 0 holds

( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} )

for f being FinSequence of CQC-WFF Al st len f > 0 holds

( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} )

proof end;

theorem Th5: :: CALCUL_1:5

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al holds

( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f )

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al holds

( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f )

proof end;

theorem Th6: :: CALCUL_1:6

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) ) ) )

( 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

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al holds Seq ((f ^ g) | (dom f)) = (f ^ g) | (dom f)

for f, g being FinSequence of CQC-WFF Al holds Seq ((f ^ g) | (dom f)) = (f ^ g) | (dom f)

proof end;

theorem Th10: :: CALCUL_1:10

for b being object

for fin being FinSequence holds

( 1 <= len (fin ^ <*b*>) & len (fin ^ <*b*>) in dom (fin ^ <*b*>) )

for fin being FinSequence holds

( 1 <= len (fin ^ <*b*>) & len (fin ^ <*b*>) in dom (fin ^ <*b*>) )

proof end;

theorem Th13: :: CALCUL_1:13

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al st 0 < len f holds

f is_Subsequence_of ((Ant f) ^ g) ^ <*(Suc f)*>

for f, g being FinSequence of CQC-WFF Al st 0 < len f holds

f is_Subsequence_of ((Ant f) ^ g) ^ <*(Suc f)*>

proof end;

theorem Th14: :: CALCUL_1:14

for Al being QC-alphabet

for c, d being object

for f being FinSequence of CQC-WFF Al 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 )

for c, d being object

for f being FinSequence of CQC-WFF Al 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 Al be QC-alphabet ;

let f be FinSequence of CQC-WFF Al;

ex b_{1} being Subset of (bound_QC-variables Al) st

for a being object holds

( a in b_{1} iff ex i being Nat ex p being Element of CQC-WFF Al st

( i in dom f & p = f . i & a in still_not-bound_in p ) )

for b_{1}, b_{2} being Subset of (bound_QC-variables Al) st ( for a being object holds

( a in b_{1} iff ex i being Nat ex p being Element of CQC-WFF Al st

( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) & ( for a being object holds

( a in b_{2} iff ex i being Nat ex p being Element of CQC-WFF Al st

( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) holds

b_{1} = b_{2}

end;
let f be FinSequence of CQC-WFF Al;

func still_not-bound_in f -> Subset of (bound_QC-variables Al) means :Def5: :: CALCUL_1:def 5

for a being object holds

( a in it iff ex i being Nat ex p being Element of CQC-WFF Al st

( i in dom f & p = f . i & a in still_not-bound_in p ) );

existence for a being object holds

( a in it iff ex i being Nat ex p being Element of CQC-WFF Al st

( i in dom f & p = f . i & a in still_not-bound_in p ) );

ex b

for a being object holds

( a in b

( i in dom f & p = f . i & a in still_not-bound_in p ) )

proof end;

uniqueness for b

( a in b

( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) & ( for a being object holds

( a in b

( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) holds

b

proof end;

:: deftheorem Def5 defines still_not-bound_in CALCUL_1:def 5 :

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al

for b_{3} being Subset of (bound_QC-variables Al) holds

( b_{3} = still_not-bound_in f iff for a being object holds

( a in b_{3} iff ex i being Nat ex p being Element of CQC-WFF Al st

( i in dom f & p = f . i & a in still_not-bound_in p ) ) );

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al

for b

( b

( a in b

( i in dom f & p = f . i & a in still_not-bound_in p ) ) );

definition

let Al be QC-alphabet ;

ex b_{1} being set st

for a being object holds

( a in b_{1} iff a is FinSequence of CQC-WFF Al )

for b_{1}, b_{2} being set st ( for a being object holds

( a in b_{1} iff a is FinSequence of CQC-WFF Al ) ) & ( for a being object holds

( a in b_{2} iff a is FinSequence of CQC-WFF Al ) ) holds

b_{1} = b_{2}

end;
func set_of_CQC-WFF-seq Al -> set means :Def6: :: CALCUL_1:def 6

for a being object holds

( a in it iff a is FinSequence of CQC-WFF Al );

existence for a being object holds

( a in it iff a is FinSequence of CQC-WFF Al );

ex b

for a being object holds

( a in b

proof end;

uniqueness for b

( a in b

( a in b

b

proof end;

:: deftheorem Def6 defines set_of_CQC-WFF-seq CALCUL_1:def 6 :

for Al being QC-alphabet

for b_{2} being set holds

( b_{2} = set_of_CQC-WFF-seq Al iff for a being object holds

( a in b_{2} iff a is FinSequence of CQC-WFF Al ) );

for Al being QC-alphabet

for b

( b

( a in b

definition

let Al be QC-alphabet ;

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

let n be Nat;

( ( (PR . n) `2 = 0 & (PR . n) `2 = 1 implies ( ex f being FinSequence of CQC-WFF Al st

( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*> ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 2 implies ( ex f being FinSequence of CQC-WFF Al 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 Al 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 Al 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 Al 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 Al 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 Al ex p being Element of CQC-WFF Al 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 Al 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 Al 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 Al st

( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al 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 Al st

( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al 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 Al st

( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al st

( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i being Nat ex f, g being FinSequence of CQC-WFF Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al 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 Al 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 Al 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 Al ex p being Element of CQC-WFF Al 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 Al 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 Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al 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 Al ex p being Element of CQC-WFF Al 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 Al 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 Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p being Element of CQC-WFF Al 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 Al 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 Al ex p being Element of CQC-WFF Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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;
let PR be FinSequence of [:(set_of_CQC-WFF-seq Al),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 Al st

( Suc f is_tail_of Ant f & (PR . n) `1 = f ) if (PR . n) `2 = 0

ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*> if (PR . n) `2 = 1

ex i being Nat ex f, g being FinSequence of CQC-WFF Al 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 Al 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 Al ex p being Element of CQC-WFF Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 ex f being FinSequence of CQC-WFF Al st

( Suc f is_tail_of Ant f & (PR . n) `1 = f ) if (PR . n) `2 = 0

ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*> if (PR . n) `2 = 1

ex i being Nat ex f, g being FinSequence of CQC-WFF Al 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 Al 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 Al ex p being Element of CQC-WFF Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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

;

( ( (PR . n) `2 = 0 & (PR . n) `2 = 1 implies ( ex f being FinSequence of CQC-WFF Al st

( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*> ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 2 implies ( ex f being FinSequence of CQC-WFF Al 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 Al 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 Al 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 Al 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 Al 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 Al ex p being Element of CQC-WFF Al 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 Al 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 Al 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 Al st

( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al 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 Al st

( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al 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 Al st

( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al st

( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i being Nat ex f, g being FinSequence of CQC-WFF Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al 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 Al 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 Al 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 Al ex p being Element of CQC-WFF Al 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 Al 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 Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al 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 Al ex p being Element of CQC-WFF Al 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 Al 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 Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p being Element of CQC-WFF Al 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 Al 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 Al ex p being Element of CQC-WFF Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 ) ) ) ) ;

:: deftheorem Def7 defines is_a_correct_step CALCUL_1:def 7 :

for Al being QC-alphabet

for PR being FinSequence of [:(set_of_CQC-WFF-seq Al),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 Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> ) ) & ( (PR . n) `2 = 2 implies ( PR,n is_a_correct_step iff ex i being Nat ex f, g being FinSequence of CQC-WFF Al 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 Al 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 Al ex p being Element of CQC-WFF Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 ) ) ) );

for Al being QC-alphabet

for PR being FinSequence of [:(set_of_CQC-WFF-seq Al),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 Al 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 Al st (PR . n) `1 = f ^ <*(VERUM Al)*> ) ) & ( (PR . n) `2 = 2 implies ( PR,n is_a_correct_step iff ex i being Nat ex f, g being FinSequence of CQC-WFF Al 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 Al 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 Al ex p being Element of CQC-WFF Al 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 Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p, q being Element of CQC-WFF Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al 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 Al be QC-alphabet ;

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

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

attr PR is a_proof means :: CALCUL_1:def 8

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

PR,n is_a_correct_step ) );

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

PR,n is_a_correct_step ) );

:: deftheorem defines a_proof CALCUL_1:def 8 :

for Al being QC-alphabet

for PR being FinSequence of [:(set_of_CQC-WFF-seq Al),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 ) ) );

for Al being QC-alphabet

for PR being FinSequence of [:(set_of_CQC-WFF-seq Al),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 Al be QC-alphabet ;

let f be FinSequence of CQC-WFF Al;

end;
let f be FinSequence of CQC-WFF Al;

pred |- f means :: CALCUL_1:def 9

ex PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] st

( PR is a_proof & f = (PR . (len PR)) `1 );

ex PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] st

( PR is a_proof & f = (PR . (len PR)) `1 );

:: deftheorem defines |- CALCUL_1:def 9 :

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al holds

( |- f iff ex PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] st

( PR is a_proof & f = (PR . (len PR)) `1 ) );

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al holds

( |- f iff ex PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] st

( PR is a_proof & f = (PR . (len PR)) `1 ) );

definition

let Al be QC-alphabet ;

let p be Element of CQC-WFF Al;

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

end;
let p be Element of CQC-WFF Al;

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

pred p is_formal_provable_from X means :: CALCUL_1:def 10

ex f being FinSequence of CQC-WFF Al st

( rng (Ant f) c= X & Suc f = p & |- f );

ex f being FinSequence of CQC-WFF Al st

( rng (Ant f) c= X & Suc f = p & |- f );

:: deftheorem defines is_formal_provable_from CALCUL_1:def 10 :

for Al being QC-alphabet

for p being Element of CQC-WFF Al

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

( p is_formal_provable_from X iff ex f being FinSequence of CQC-WFF Al st

( rng (Ant f) c= X & Suc f = p & |- f ) );

for Al being QC-alphabet

for p being Element of CQC-WFF Al

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

( p is_formal_provable_from X iff ex f being FinSequence of CQC-WFF Al st

( rng (Ant f) c= X & Suc f = p & |- f ) );

definition

let Al be QC-alphabet ;

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

let A be non empty set ;

let J be interpretation of Al,A;

let v be Element of Valuations_in (Al,A);

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

let A be non empty set ;

let J be interpretation of Al,A;

let v be Element of Valuations_in (Al,A);

:: deftheorem defines |= CALCUL_1:def 11 :

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) holds

( J,v |= X iff for p being Element of CQC-WFF Al st p in X holds

J,v |= p );

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) holds

( J,v |= X iff for p being Element of CQC-WFF Al st p in X holds

J,v |= p );

definition

let Al be QC-alphabet ;

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

let p be Element of CQC-WFF Al;

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

let p be Element of CQC-WFF Al;

pred X |= p means :: CALCUL_1:def 12

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= X holds

J,v |= p;

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= X holds

J,v |= p;

:: deftheorem defines |= CALCUL_1:def 12 :

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al holds

( X |= p iff for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= X holds

J,v |= p );

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al holds

( X |= p iff for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= X holds

J,v |= p );

:: deftheorem defines |= CALCUL_1:def 13 :

for Al being QC-alphabet

for p being Element of CQC-WFF Al holds

( |= p iff {} (CQC-WFF Al) |= p );

for Al being QC-alphabet

for p being Element of CQC-WFF Al holds

( |= p iff {} (CQC-WFF Al) |= p );

definition

let Al be QC-alphabet ;

let f be FinSequence of CQC-WFF Al;

let A be non empty set ;

let J be interpretation of Al,A;

let v be Element of Valuations_in (Al,A);

end;
let f be FinSequence of CQC-WFF Al;

let A be non empty set ;

let J be interpretation of Al,A;

let v be Element of Valuations_in (Al,A);

:: deftheorem defines |= CALCUL_1:def 14 :

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) holds

( J,v |= f iff J,v |= rng f );

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) holds

( J,v |= f iff J,v |= rng f );

definition

let Al be QC-alphabet ;

let f be FinSequence of CQC-WFF Al;

let p be Element of CQC-WFF Al;

end;
let f be FinSequence of CQC-WFF Al;

let p be Element of CQC-WFF Al;

pred f |= p means :: CALCUL_1:def 15

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= f holds

J,v |= p;

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= f holds

J,v |= p;

:: deftheorem defines |= CALCUL_1:def 15 :

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al

for p being Element of CQC-WFF Al holds

( f |= p iff for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= f holds

J,v |= p );

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al

for p being Element of CQC-WFF Al holds

( f |= p iff for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= f holds

J,v |= p );

theorem Th15: :: CALCUL_1:15

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al st Suc f is_tail_of Ant f holds

Ant f |= Suc f

for f being FinSequence of CQC-WFF Al st Suc f is_tail_of Ant f holds

Ant f |= Suc f

proof end;

theorem Th16: :: CALCUL_1:16

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al st Ant f is_Subsequence_of Ant g & Suc f = Suc g & Ant f |= Suc f holds

Ant g |= Suc g

for f, g being FinSequence of CQC-WFF Al 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

for Al being QC-alphabet

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A)

for f being FinSequence of CQC-WFF Al st len f > 0 holds

( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A)

for f being FinSequence of CQC-WFF Al st len f > 0 holds

( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

proof end;

theorem Th18: :: CALCUL_1:18

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al 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

for f, g being FinSequence of CQC-WFF Al 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

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for f, g being FinSequence of CQC-WFF Al 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

for p being Element of CQC-WFF Al

for f, g being FinSequence of CQC-WFF Al 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

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al st Ant f = Ant g & Ant f |= Suc f & Ant g |= Suc g holds

Ant f |= (Suc f) '&' (Suc g)

for f, g being FinSequence of CQC-WFF Al 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

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st Ant f |= p '&' q holds

Ant f |= p

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st Ant f |= p '&' q holds

Ant f |= p

proof end;

theorem Th22: :: CALCUL_1:22

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st Ant f |= p '&' q holds

Ant f |= q

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st Ant f |= p '&' q holds

Ant f |= q

proof end;

theorem Th23: :: CALCUL_1:23

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A)

for Sub being CQC_Substitution of Al holds

( J,v |= [p,Sub] iff J,v |= p )

for p being Element of CQC-WFF Al

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A)

for Sub being CQC_Substitution of Al holds

( J,v |= [p,Sub] iff J,v |= p )

proof end;

theorem Th24: :: CALCUL_1:24

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) holds

( J,v |= p . (x,y) iff ex a being Element of A st

( v . y = a & J,v . (x | a) |= p ) )

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,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

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al st Suc f = All (x,p) & Ant f |= Suc f holds

for y being bound_QC-variable of Al holds Ant f |= p . (x,y)

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al st Suc f = All (x,p) & Ant f |= Suc f holds

for y being bound_QC-variable of Al holds Ant f |= p . (x,y)

proof end;

theorem Th26: :: CALCUL_1:26

for Al being QC-alphabet

for x being bound_QC-variable of Al

for A being non empty set

for v being Element of Valuations_in (Al,A)

for a being Element of A

for X being set st X c= bound_QC-variables Al & not x in X holds

(v . (x | a)) | X = v | X

for x being bound_QC-variable of Al

for A being non empty set

for v being Element of Valuations_in (Al,A)

for a being Element of A

for X being set st X c= bound_QC-variables Al & not x in X holds

(v . (x | a)) | X = v | X

proof end;

theorem Th27: :: CALCUL_1:27

for Al being QC-alphabet

for A being non empty set

for J being interpretation of Al,A

for f being FinSequence of CQC-WFF Al

for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in f) = w | (still_not-bound_in f) & J,v |= f holds

J,w |= f

for A being non empty set

for J being interpretation of Al,A

for f being FinSequence of CQC-WFF Al

for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in f) = w | (still_not-bound_in f) & J,v |= f holds

J,w |= f

proof end;

theorem Th28: :: CALCUL_1:28

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al

for A being non empty set

for v being Element of Valuations_in (Al,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)

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al

for A being non empty set

for v being Element of Valuations_in (Al,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

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al 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)

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al 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

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al holds Ant (f ^ <*(VERUM Al)*>) |= Suc (f ^ <*(VERUM Al)*>)

for f being FinSequence of CQC-WFF Al holds Ant (f ^ <*(VERUM Al)*>) |= Suc (f ^ <*(VERUM Al)*>)

proof end;

theorem Th31: :: CALCUL_1:31

for Al being QC-alphabet

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

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

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

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

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

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

proof end;

Lm3: for Al being QC-alphabet

for n being Nat

for PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] st 1 <= n & n <= len PR holds

(PR . n) `1 is FinSequence of CQC-WFF Al

proof end;

:: Theorem on the Correctness (Ebb et al, Chapter IV, Theorem 6.2)

theorem :: CALCUL_1:32

for Al being QC-alphabet

for p being Element of CQC-WFF Al

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

X |= p

for p being Element of CQC-WFF Al

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

X |= p

proof end;

theorem Th34: :: CALCUL_1:34

for Al being QC-alphabet

for PR, PR1 being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]

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

( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step )

for PR, PR1 being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]

for n being Nat 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

for Al being QC-alphabet

for n being Nat

for PR, PR1 being FinSequence of [:(set_of_CQC-WFF-seq Al),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

for n being Nat

for PR, PR1 being FinSequence of [:(set_of_CQC-WFF-seq Al),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

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al st Ant f is_Subsequence_of Ant g & Suc f = Suc g & |- f holds

|- g

for f, g being FinSequence of CQC-WFF Al st Ant f is_Subsequence_of Ant g & Suc f = Suc g & |- f holds

|- g

proof end;

theorem Th37: :: CALCUL_1:37

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al 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)*>

for f, g being FinSequence of CQC-WFF Al 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

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for f, g being FinSequence of CQC-WFF Al 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*>

for p being Element of CQC-WFF Al

for f, g being FinSequence of CQC-WFF Al 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

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al st Ant f = Ant g & |- f & |- g holds

|- (Ant f) ^ <*((Suc f) '&' (Suc g))*>

for f, g being FinSequence of CQC-WFF Al st Ant f = Ant g & |- f & |- g holds

|- (Ant f) ^ <*((Suc f) '&' (Suc g))*>

proof end;

theorem Th40: :: CALCUL_1:40

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st p '&' q = Suc f & |- f holds

|- (Ant f) ^ <*p*>

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st p '&' q = Suc f & |- f holds

|- (Ant f) ^ <*p*>

proof end;

theorem Th41: :: CALCUL_1:41

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st p '&' q = Suc f & |- f holds

|- (Ant f) ^ <*q*>

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st p '&' q = Suc f & |- f holds

|- (Ant f) ^ <*q*>

proof end;

theorem Th42: :: CALCUL_1:42

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al st Suc f = All (x,p) & |- f holds

|- (Ant f) ^ <*(p . (x,y))*>

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al st Suc f = All (x,p) & |- f holds

|- (Ant f) ^ <*(p . (x,y))*>

proof end;

theorem Th43: :: CALCUL_1:43

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al 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))*>

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al 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

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f & |- (Ant f) ^ <*('not' (Suc f))*> holds

|- (Ant f) ^ <*p*>

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f & |- (Ant f) ^ <*('not' (Suc f))*> holds

|- (Ant f) ^ <*p*>

proof end;

theorem Th45: :: CALCUL_1:45

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st 1 <= len f & |- f & |- f ^ <*p*> holds

|- (Ant f) ^ <*p*>

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st 1 <= len f & |- f & |- f ^ <*p*> holds

|- (Ant f) ^ <*p*>

proof end;

theorem Th46: :: CALCUL_1:46

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*q*> holds

|- (f ^ <*('not' q)*>) ^ <*('not' p)*>

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*q*> holds

|- (f ^ <*('not' q)*>) ^ <*('not' p)*>

proof end;

theorem :: CALCUL_1:47

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- (f ^ <*('not' p)*>) ^ <*('not' q)*> holds

|- (f ^ <*q*>) ^ <*p*>

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- (f ^ <*('not' p)*>) ^ <*('not' q)*> holds

|- (f ^ <*q*>) ^ <*p*>

proof end;

theorem Th48: :: CALCUL_1:48

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- (f ^ <*('not' p)*>) ^ <*q*> holds

|- (f ^ <*('not' q)*>) ^ <*p*>

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- (f ^ <*('not' p)*>) ^ <*q*> holds

|- (f ^ <*('not' q)*>) ^ <*p*>

proof end;

theorem Th49: :: CALCUL_1:49

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*('not' q)*> holds

|- (f ^ <*q*>) ^ <*('not' p)*>

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*('not' q)*> holds

|- (f ^ <*q*>) ^ <*('not' p)*>

proof end;

::$CT

theorem :: CALCUL_1:51

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds

|- f ^ <*(p 'or' q)*>

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds

|- f ^ <*(p 'or' q)*>

proof end;

theorem :: CALCUL_1:52

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*q*> holds

|- f ^ <*(p 'or' q)*>

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*q*> holds

|- f ^ <*(p 'or' q)*>

proof end;

theorem Th52: :: CALCUL_1:53

for Al being QC-alphabet

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

for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*r*> & |- (f ^ <*q*>) ^ <*r*> holds

|- (f ^ <*(p 'or' q)*>) ^ <*r*>

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

for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*r*> & |- (f ^ <*q*>) ^ <*r*> holds

|- (f ^ <*(p 'or' q)*>) ^ <*r*>

proof end;

theorem Th53: :: CALCUL_1:54

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds

|- f ^ <*('not' ('not' p))*>

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds

|- f ^ <*('not' ('not' p))*>

proof end;

theorem Th54: :: CALCUL_1:55

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*('not' ('not' p))*> holds

|- f ^ <*p*>

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*('not' ('not' p))*> holds

|- f ^ <*p*>

proof end;

theorem :: CALCUL_1:56

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*(p => q)*> & |- f ^ <*p*> holds

|- f ^ <*q*>

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*(p => q)*> & |- f ^ <*p*> holds

|- f ^ <*q*>

proof end;

theorem Th56: :: CALCUL_1:57

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al holds ('not' p) . (x,y) = 'not' (p . (x,y))

for p being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al holds ('not' p) . (x,y) = 'not' (p . (x,y))

proof end;

theorem :: CALCUL_1:58

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al st ex y being bound_QC-variable of Al st |- f ^ <*(p . (x,y))*> holds

|- f ^ <*(Ex (x,p))*>

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al st ex y being bound_QC-variable of Al st |- f ^ <*(p . (x,y))*> holds

|- f ^ <*(Ex (x,p))*>

proof end;

theorem Th58: :: CALCUL_1:59

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al holds still_not-bound_in (f ^ g) = (still_not-bound_in f) \/ (still_not-bound_in g)

for f, g being FinSequence of CQC-WFF Al holds still_not-bound_in (f ^ g) = (still_not-bound_in f) \/ (still_not-bound_in g)

proof end;

theorem Th59: :: CALCUL_1:60

for Al being QC-alphabet

for p being Element of CQC-WFF Al holds still_not-bound_in <*p*> = still_not-bound_in p

for p being Element of CQC-WFF Al holds still_not-bound_in <*p*> = still_not-bound_in p

proof end;

theorem :: CALCUL_1:61

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al st |- (f ^ <*(p . (x,y))*>) ^ <*q*> & not y in still_not-bound_in ((f ^ <*(Ex (x,p))*>) ^ <*q*>) holds

|- (f ^ <*(Ex (x,p))*>) ^ <*q*>

for p, q being Element of CQC-WFF Al

for x, y being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al 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 Th61: :: CALCUL_1:62

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al holds still_not-bound_in f = union { (still_not-bound_in p) where p is Element of CQC-WFF Al : ex i being Nat st

( i in dom f & p = f . i ) }

for f being FinSequence of CQC-WFF Al holds still_not-bound_in f = union { (still_not-bound_in p) where p is Element of CQC-WFF Al : ex i being Nat st

( i in dom f & p = f . i ) }

proof end;

theorem Th63: :: CALCUL_1:64

for Al being QC-alphabet holds

( card (bound_QC-variables Al) = card (QC-symbols Al) & not bound_QC-variables Al is finite )

( card (bound_QC-variables Al) = card (QC-symbols Al) & not bound_QC-variables Al is finite )

proof end;

theorem Th64: :: CALCUL_1:65

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al holds

not for x being bound_QC-variable of Al holds x in still_not-bound_in f

for f being FinSequence of CQC-WFF Al holds

not for x being bound_QC-variable of Al holds x in still_not-bound_in f

proof end;

theorem Th65: :: CALCUL_1:66

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*(All (x,p))*> holds

|- f ^ <*(All (x,('not' ('not' p))))*>

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*(All (x,p))*> holds

|- f ^ <*(All (x,('not' ('not' p))))*>

proof end;

theorem Th66: :: CALCUL_1:67

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*(All (x,('not' ('not' p))))*> holds

|- f ^ <*(All (x,p))*>

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*(All (x,('not' ('not' p))))*> holds

|- f ^ <*(All (x,p))*>

proof end;

theorem :: CALCUL_1:68

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al holds

( |- f ^ <*(All (x,p))*> iff |- f ^ <*('not' (Ex (x,('not' p))))*> )

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for f being FinSequence of CQC-WFF Al holds

( |- f ^ <*(All (x,p))*> iff |- f ^ <*('not' (Ex (x,('not' p))))*> )

proof end;

definition

let f be FinSequence;

let p be set ;

compatibility

( p is_tail_of f iff ex i being Nat st

( i in dom f & f . i = p ) ) by Lm1, Lm2;

end;
let p be set ;

compatibility

( p is_tail_of f iff ex i being Nat st

( i in dom f & f . i = p ) ) by Lm1, Lm2;

:: deftheorem defines is_tail_of CALCUL_1:def 16 :

for f being FinSequence

for p being set holds

( p is_tail_of f iff ex i being Nat st

( i in dom f & f . i = p ) );

for f being FinSequence

for p being set holds

( p is_tail_of f iff ex i being Nat st

( i in dom f & f . i = p ) );