let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
for m being Element of NAT st m < LifeSpan ((P +* I),(s +* (Initialize I))) holds
CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) = CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m)))
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
for m being Element of NAT st m < LifeSpan ((P +* I),(s +* (Initialize I))) holds
CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) = CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m)))
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies for m being Element of NAT st m < LifeSpan ((P +* I),(s +* (Initialize I))) holds
CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) = CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) )
A1: ProgramPart I = I by RELAT_1:209;
set s1 = s +* (Initialize I);
set P1 = P +* I;
set s2 = s +* (Initialize (loop I));
set P2 = P +* (loop I);
A2: I c= P +* I by FUNCT_4:26;
A3: loop I c= P +* (loop I) by FUNCT_4:26;
assume that
A4: I is_closed_on s,P and
A5: I is_halting_on s,P ; :: thesis: for m being Element of NAT st m < LifeSpan ((P +* I),(s +* (Initialize I))) holds
CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) = CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m)))
let m be Element of NAT ; :: thesis: ( m < LifeSpan ((P +* I),(s +* (Initialize I))) implies CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) = CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) )
A6: IC (Comput ((P +* I),(s +* (Initialize I)),m)) in dom I by A4, SCMFSA7B:def 7, A1;
then A7: IC (Comput ((P +* I),(s +* (Initialize I)),m)) in dom (loop I) by FUNCT_4:105;
A8: (P +* I) /. (IC (Comput ((P +* I),(s +* (Initialize I)),m))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by PBOOLE:158;
A9: CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) = I . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by A6, A8, GRFUNC_1:8, A2;
assume A10: m < LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis: CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) = CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m)))
A11: (P +* (loop I)) /. (IC (Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) = (P +* (loop I)) . (IC (Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) by PBOOLE:158;
P +* I halts_on s +* (Initialize I) by A5, SCMFSA7B:def 8, A1;
then I . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) <> halt SCM+FSA by A10, A9, EXTPRO_1:def 14;
then A12: I . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) = (loop I) . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by FUNCT_4:111;
thus CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by A8
.= I . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by GRFUNC_1:8, A2, A6
.= (loop I) . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by A12
.= (P +* (loop I)) . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by A7, GRFUNC_1:8, A3
.= CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) by A4, A5, A10, Th109, A11, COMPOS_1:24 ; :: thesis: verum