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
( CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) <> halt SCM+FSA ) )
A1: dom (id the Instructions of SCM+FSA) = the Instructions of SCM+FSA by RELAT_1:71;
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
( CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) <> halt SCM+FSA ) )
let I be Program of SCM+FSA; :: thesis: ( I is_closed_onInit s,p & I is_halting_onInit s,p implies ( CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) <> halt SCM+FSA ) ) )
set s1 = s +* (Initialize ((intloc 0) .--> 1));
set p1 = p +* I;
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: ( CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) <> halt SCM+FSA ) )
set k = LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))));
A5: rng I c= the Instructions of SCM+FSA by RELAT_1:def 19;
A6: IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) in dom I by A3, Def4;
A7: dom (loop I) = dom I by FUNCT_4:105;
A8: CurInstr ((p +* I),(Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) = (p +* I) . (IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) by PBOOLE:158
.= I . (IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) by A6, FUNCT_4:14 ;
A9: p +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by A4, Def5;
then A10: CurInstr ((p +* I),(Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) = halt SCM+FSA by EXTPRO_1:def 14;
NPP (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = NPP (Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) by A3, A4, Th68;
then IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = IC (Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) by COMPOS_1:230;
hence A11: CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) = (p +* (loop I)) . (IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) by PBOOLE:158
.= (loop I) . (IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) by A2, A6, A7, GRFUNC_1:8
.= (((id the Instructions of SCM+FSA) +* ((halt SCM+FSA),(goto 0))) * I) . (IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) by A5, FUNCT_7:118
.= ((id the Instructions of SCM+FSA) +* ((halt SCM+FSA),(goto 0))) . (halt SCM+FSA) by A10, A6, A8, FUNCT_1:23
.= goto 0 by A1, FUNCT_7:33 ;
:: thesis: for m being Element of NAT st m <= LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) <> halt SCM+FSA
let m be Element of NAT ; :: thesis: ( m <= LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) <> halt SCM+FSA )
assume A12: m <= LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; :: thesis: CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) <> halt SCM+FSA

per cases ( m < LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) or m = LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ) by A12, XXREAL_0:1;

suppose A13: m < LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; :: thesis: CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) <> halt SCM+FSA

then CurInstr ((p +* I),(Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),m))) <> halt SCM+FSA by A9, EXTPRO_1:def 14;
hence CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) <> halt SCM+FSA by A3, A4, A13, Th69; :: thesis: verum

end;

suppose m = LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; :: thesis: CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) <> halt SCM+FSA

hence CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m))) <> halt SCM+FSA by A11; :: thesis: verum

end;

end;