let s be QC-formula; for x, y being bound_QC-variable
for X being Subset of CQC-WFF st s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) } holds
s . y in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = G ) }
let x, y be bound_QC-variable; for X being Subset of CQC-WFF st s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) } holds
s . y in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = G ) }
let X be Subset of CQC-WFF ; ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) } implies s . y in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = G ) } )
assume that
A1:
( s . x in CQC-WFF & s . y in CQC-WFF )
and
A2:
not x in still_not-bound_in s
and
A3:
s . x in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) }
; s . y in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = G ) }
A4:
ex t being Element of CQC-WFF st
( t = s . x & ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = t ) )
by A3;
consider f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] such that
A5:
f is_a_proof_wrt X
and
A6:
Effect f = s . x
by A4;
A7:
f <> {}
by A5, Def5;
reconsider qq = [(s . y),9] as Element of [:CQC-WFF ,Proof_Step_Kinds :] by A1, Th43, ZFMISC_1:106;
set h = f ^ <*qq*>;
A8: len (f ^ <*qq*>) =
(len f) + (len <*qq*>)
by FINSEQ_1:35
.=
(len f) + 1
by FINSEQ_1:56
;
A9:
for n being Element of NAT st 1 <= n & n <= len (f ^ <*qq*>) holds
f ^ <*qq*>,n is_a_correct_step_wrt X
proof
let n be
Element of
NAT ;
( 1 <= n & n <= len (f ^ <*qq*>) implies f ^ <*qq*>,n is_a_correct_step_wrt X )
assume that A10:
1
<= n
and A11:
n <= len (f ^ <*qq*>)
;
f ^ <*qq*>,n is_a_correct_step_wrt X
A12:
now per cases
( n <= len f or n = len (f ^ <*qq*>) )
by A8, A11, NAT_1:8;
suppose A15:
n = len (f ^ <*qq*>)
;
f ^ <*qq*>,n is_a_correct_step_wrt XA16:
(f ^ <*qq*>) . n = qq
by A8, A15, FINSEQ_1:59;
A17:
(
((f ^ <*qq*>) . n) `2 = 9 &
((f ^ <*qq*>) . n) `1 = s . y )
by A16, MCART_1:7;
A18:
len f <> 0
by A5, Th58;
A19:
len f in Seg (len f)
by A18, FINSEQ_1:5;
A20:
len f in dom f
by A19, FINSEQ_1:def 3;
A21:
((f ^ <*qq*>) . (len f)) `1 =
(f . (len f)) `1
by A20, FINSEQ_1:def 7
.=
s . x
by A6, A7, Def6
;
A22:
1
<= len f
by A5, Th58;
A23:
len f < n
by A8, A15, NAT_1:13;
thus
f ^ <*qq*>,
n is_a_correct_step_wrt X
by A1, A2, A17, A21, A22, A23, Def4;
verum end;
thus
f ^ <*qq*>,
n is_a_correct_step_wrt X
by A12;
verum
end;
A24:
f ^ <*qq*> is_a_proof_wrt X
by A9, Def5;
A25: Effect (f ^ <*qq*>) =
((f ^ <*qq*>) . ((len f) + 1)) `1
by A8, Def6
.=
qq `1
by FINSEQ_1:59
.=
s . y
by MCART_1:7
;
thus
s . y in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = G ) }
by A24, A25; verum