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
( CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),(LifeSpan ((P +* I),(s +* (Initialize I))))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((P +* I),(s +* (Initialize I))) holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),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_on s,P & I is_halting_on s,P holds
( CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),(LifeSpan ((P +* I),(s +* (Initialize I))))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((P +* I),(s +* (Initialize I))) holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) <> halt SCM+FSA ) )
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),(LifeSpan ((P +* I),(s +* (Initialize I))))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((P +* I),(s +* (Initialize I))) holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) <> halt SCM+FSA ) ) )
A2: 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);
A3: I c= P +* I by FUNCT_4:26;
assume that
A4: I is_closed_on s,P and
A5: I is_halting_on s,P ; :: thesis: ( CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),(LifeSpan ((P +* I),(s +* (Initialize I))))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((P +* I),(s +* (Initialize I))) holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) <> halt SCM+FSA ) )
set k = LifeSpan ((P +* I),(s +* (Initialize I)));
A6: IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) in dom I by A4, SCMFSA7B:def 7, A2;
A7: dom (loop I) = dom I by FUNCT_4:105;
A8: P +* I halts_on s +* (Initialize I) by A5, SCMFSA7B:def 8, A2;
then A9: CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I))))))) = halt SCM+FSA by EXTPRO_1:def 14;
A10: (P +* I) /. (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I))))))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I))))))) by PBOOLE:158;
A11: CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I))))))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I))))))) by A10
.= I . (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I))))))) by A3, GRFUNC_1:8, A6
.= I . (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I))))))) ;
A12: rng I c= the Instructions of SCM+FSA by RELAT_1:def 19;
A13: (P +* (loop I)) /. (IC (Comput ((P +* (loop I)),(s +* (Initialize (loop I))),(LifeSpan ((P +* I),(s +* (Initialize I))))))) = (P +* (loop I)) . (IC (Comput ((P +* (loop I)),(s +* (Initialize (loop I))),(LifeSpan ((P +* I),(s +* (Initialize I))))))) by PBOOLE:158;
thus A14: CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),(LifeSpan ((P +* I),(s +* (Initialize I))))))) = (P +* (loop I)) . (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I))))))) by A4, A5, Th109, A13, COMPOS_1:24
.= (P +* (loop I)) . (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))))
.= (loop I) . (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I))))))) by FUNCT_4:14, A6, A7
.= (loop I) . (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))))
.= (((id the Instructions of SCM+FSA) +* ((halt SCM+FSA),(goto 0))) * I) . (IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I))))))) by A12, FUNCT_7:118
.= ((id the Instructions of SCM+FSA) +* ((halt SCM+FSA),(goto 0))) . (halt SCM+FSA) by A9, A6, A11, FUNCT_1:23
.= goto 0 by A1, FUNCT_7:33 ; :: thesis: for m being Element of NAT st m <= LifeSpan ((P +* I),(s +* (Initialize I))) holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) <> halt SCM+FSA
let m be Element of NAT ; :: thesis: ( m <= LifeSpan ((P +* I),(s +* (Initialize I))) implies CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) <> halt SCM+FSA )
assume A15: m <= LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis: CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) <> halt SCM+FSA

per cases ( m < LifeSpan ((P +* I),(s +* (Initialize I))) or m = LifeSpan ((P +* I),(s +* (Initialize I))) ) by A15, XXREAL_0:1;

suppose A16: m < LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis: CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) <> halt SCM+FSA

then CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) <> halt SCM+FSA by A8, EXTPRO_1:def 14;
hence CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) <> halt SCM+FSA by A4, A5, A16, Th110; :: thesis: verum

end;

suppose m = LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis: CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) <> halt SCM+FSA

hence CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) <> halt SCM+FSA by A14; :: thesis: verum

end;

end;