let Al be QC-alphabet ; :: thesis: for s being QC-formula of Al

for x, y being bound_QC-variable of Al

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

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

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

( f is_a_proof_wrt X & Effect f = G ) }

let s be QC-formula of Al; :: thesis: for x, y being bound_QC-variable of Al

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

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

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

( f is_a_proof_wrt X & Effect f = G ) }

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

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

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

( f is_a_proof_wrt X & Effect f = G ) }

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

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

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

assume that

A1: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al ) and

A2: not x in still_not-bound_in s and

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

( f is_a_proof_wrt X & Effect f = F ) } ; :: thesis: s . y in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = G ) }

ex t being Element of CQC-WFF Al st

( t = s . x & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = t ) ) by A3;

then consider f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that

A4: f is_a_proof_wrt X and

A5: Effect f = s . x ;

reconsider qq = [(s . y),9] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by A1, Th17, ZFMISC_1:87;

set h = f ^ <*qq*>;

A6: len (f ^ <*qq*>) = (len f) + (len <*qq*>) by FINSEQ_1:22

.= (len f) + 1 by FINSEQ_1:39 ;

for n being Nat st 1 <= n & n <= len (f ^ <*qq*>) holds

f ^ <*qq*>,n is_a_correct_step_wrt X

Effect (f ^ <*qq*>) = ((f ^ <*qq*>) . ((len f) + 1)) `1 by A6, Def6

.= qq `1 by FINSEQ_1:42

.= s . y ;

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

( f is_a_proof_wrt X & Effect f = G ) } by A14; :: thesis: verum

for x, y being bound_QC-variable of Al

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

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

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

( f is_a_proof_wrt X & Effect f = G ) }

let s be QC-formula of Al; :: thesis: for x, y being bound_QC-variable of Al

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

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

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

( f is_a_proof_wrt X & Effect f = G ) }

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

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

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

( f is_a_proof_wrt X & Effect f = G ) }

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

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

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

assume that

A1: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al ) and

A2: not x in still_not-bound_in s and

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

( f is_a_proof_wrt X & Effect f = F ) } ; :: thesis: s . y in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = G ) }

ex t being Element of CQC-WFF Al st

( t = s . x & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = t ) ) by A3;

then consider f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that

A4: f is_a_proof_wrt X and

A5: Effect f = s . x ;

reconsider qq = [(s . y),9] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by A1, Th17, ZFMISC_1:87;

set h = f ^ <*qq*>;

A6: len (f ^ <*qq*>) = (len f) + (len <*qq*>) by FINSEQ_1:22

.= (len f) + 1 by FINSEQ_1:39 ;

for n being Nat st 1 <= n & n <= len (f ^ <*qq*>) holds

f ^ <*qq*>,n is_a_correct_step_wrt X

proof

then A14:
f ^ <*qq*> is_a_proof_wrt X
;
let n be Nat; :: thesis: ( 1 <= n & n <= len (f ^ <*qq*>) implies f ^ <*qq*>,n is_a_correct_step_wrt X )

assume that

A7: 1 <= n and

A8: n <= len (f ^ <*qq*>) ; :: thesis: f ^ <*qq*>,n is_a_correct_step_wrt X

end;assume that

A7: 1 <= n and

A8: n <= len (f ^ <*qq*>) ; :: thesis: f ^ <*qq*>,n is_a_correct_step_wrt X

now :: thesis: f ^ <*qq*>,n is_a_correct_step_wrt Xend;

hence
f ^ <*qq*>,n is_a_correct_step_wrt X
; :: thesis: verumper cases
( n <= len f or n = len (f ^ <*qq*>) )
by A6, A8, NAT_1:8;

end;

suppose A9:
n <= len f
; :: thesis: f ^ <*qq*>,n is_a_correct_step_wrt X

then
f,n is_a_correct_step_wrt X
by A4, A7;

hence f ^ <*qq*>,n is_a_correct_step_wrt X by A7, A9, Th23; :: thesis: verum

end;hence f ^ <*qq*>,n is_a_correct_step_wrt X by A7, A9, Th23; :: thesis: verum

suppose A10:
n = len (f ^ <*qq*>)
; :: thesis: f ^ <*qq*>,n is_a_correct_step_wrt X

then
(f ^ <*qq*>) . n = qq
by A6, FINSEQ_1:42;

then A11: ( ((f ^ <*qq*>) . n) `2 = 9 & ((f ^ <*qq*>) . n) `1 = s . y ) ;

len f <> 0 by A4;

then len f in Seg (len f) by FINSEQ_1:3;

then len f in dom f by FINSEQ_1:def 3;

then A12: ((f ^ <*qq*>) . (len f)) `1 = (f . (len f)) `1 by FINSEQ_1:def 7

.= s . x by A5, A4, Def6 ;

A13: 1 <= len f by A4, Th21;

len f < n by A6, A10, NAT_1:13;

hence f ^ <*qq*>,n is_a_correct_step_wrt X by A1, A2, A11, A12, A13, Def4; :: thesis: verum

end;then A11: ( ((f ^ <*qq*>) . n) `2 = 9 & ((f ^ <*qq*>) . n) `1 = s . y ) ;

len f <> 0 by A4;

then len f in Seg (len f) by FINSEQ_1:3;

then len f in dom f by FINSEQ_1:def 3;

then A12: ((f ^ <*qq*>) . (len f)) `1 = (f . (len f)) `1 by FINSEQ_1:def 7

.= s . x by A5, A4, Def6 ;

A13: 1 <= len f by A4, Th21;

len f < n by A6, A10, NAT_1:13;

hence f ^ <*qq*>,n is_a_correct_step_wrt X by A1, A2, A11, A12, A13, Def4; :: thesis: verum

Effect (f ^ <*qq*>) = ((f ^ <*qq*>) . ((len f) + 1)) `1 by A6, Def6

.= qq `1 by FINSEQ_1:42

.= s . y ;

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

( f is_a_proof_wrt X & Effect f = G ) } by A14; :: thesis: verum