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_onInit s,p & I is_halting_onInit s,p holds
for m being Element of NAT st m < LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
CurInstr ((p +* I),(Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m))) = CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m)))
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I is_closed_onInit s,p & I is_halting_onInit s,p holds
for m being Element of NAT st m < LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
CurInstr ((p +* I),(Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m))) = CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m)))
let I be Program of SCM+FSA; :: thesis: ( I is_closed_onInit s,p & I is_halting_onInit s,p implies for m being Element of NAT st m < LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
CurInstr ((p +* I),(Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m))) = CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) )
set s1 = s +* (Initialize ((intloc 0) .--> 1));
set p1 = p +* I;
A1: I c= p +* I by FUNCT_4:26;
set s2 = s +* (Initialize ((intloc 0) .--> 1));
set p2 = p +* (loop I);
A2: loop I c= p +* (loop I) by FUNCT_4:26;
assume that
A3: I is_closed_onInit s,p and
A4: I is_halting_onInit s,p ; :: thesis: for m being Element of NAT st m < LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
CurInstr ((p +* I),(Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m))) = CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m)))
let m be Element of NAT ; :: thesis: ( m < LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies CurInstr ((p +* I),(Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m))) = CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) )
A5: IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m)) in dom I by A3, Def4;
then A6: IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m)) in dom (loop I) by FUNCT_4:105;
A7: (p +* I) /. (IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m))) = (p +* I) . (IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m))) by PBOOLE:158;
A8: CurInstr ((p +* I),(Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m))) = I . (IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m))) by A5, A7, A1, GRFUNC_1:8;
assume A9: m < LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; :: thesis: CurInstr ((p +* I),(Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m))) = CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m)))
A10: (p +* (loop I)) /. (IC (Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) = (p +* (loop I)) . (IC (Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) by PBOOLE:158;
p +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by A4, Def5;
then I . (IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m))) <> halt SCM+FSA by A9, A8, EXTPRO_1:def 14;
then A11: I . (IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m))) = (loop I) . (IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m))) by FUNCT_4:111;
NPP (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m)) = NPP (Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m)) by A3, A4, A9, Th68;
then IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m)) = IC (Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m)) by COMPOS_1:230;
hence CurInstr ((p +* I),(Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m))) = CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) by A6, A8, A11, A10, A2, GRFUNC_1:8; :: thesis: verum