let P be Instruction-Sequence of SCM+FSA; :: thesis: for a being Int-Location
for I being really-closed MacroInstruction of SCM+FSA
for s being State of SCM+FSA st I is_halting_on s,P & IC (Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),()))))) = (IC (Comput ((P +* I),(),(LifeSpan ((P +* I),()))))) + 3 holds
CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),())))))) = goto 0

set J3 = () ";" ();
set J = Stop SCM+FSA;
let a be Int-Location; :: thesis: for I being really-closed MacroInstruction of SCM+FSA
for s being State of SCM+FSA st I is_halting_on s,P & IC (Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),()))))) = (IC (Comput ((P +* I),(),(LifeSpan ((P +* I),()))))) + 3 holds
CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),())))))) = goto 0

let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: for s being State of SCM+FSA st I is_halting_on s,P & IC (Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),()))))) = (IC (Comput ((P +* I),(),(LifeSpan ((P +* I),()))))) + 3 holds
CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),())))))) = goto 0

let s be State of SCM+FSA; :: thesis: ( I is_halting_on s,P & IC (Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),()))))) = (IC (Comput ((P +* I),(),(LifeSpan ((P +* I),()))))) + 3 implies CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),())))))) = goto 0 )
set s1 = Initialize s;
set P1 = P +* (while>0 (a,I));
set sI = Initialize s;
set PI = P +* I;
A1: I c= P +* I by FUNCT_4:25;
set life = LifeSpan ((P +* I),());
set sK1 = Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),()))));
set sK2 = Comput ((P +* I),(),(LifeSpan ((P +* I),())));
set I1 = I ';' ();
set i = a >0_goto 3;
reconsider n = IC (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) as Element of NAT ;
set Mi = (a >0_goto 3) ";" (Goto ((card (I ';' ())) + 1));
set J2 = (I ';' ()) ";" ();
A2: I c= P +* I by FUNCT_4:25;
IC () = 0 by MEMSTR_0:def 11;
then IC () in dom I by AFINSQ_1:65;
then A3: n in dom I by ;
then n < card I by AFINSQ_1:66;
then A4: n + 3 < (card I) + 5 by XREAL_1:8;
assume I is_halting_on s,P ; :: thesis: ( not IC (Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),()))))) = (IC (Comput ((P +* I),(),(LifeSpan ((P +* I),()))))) + 3 or CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),())))))) = goto 0 )
then A5: P +* I halts_on Initialize s by SCMFSA7B:def 7;
A6: (P +* I) /. (IC (Comput ((P +* I),(),(LifeSpan ((P +* I),()))))) = (P +* I) . (IC (Comput ((P +* I),(),(LifeSpan ((P +* I),()))))) by PBOOLE:143;
A7: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),())))))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),())))))) by PBOOLE:143;
assume A8: IC (Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),()))))) = (IC (Comput ((P +* I),(),(LifeSpan ((P +* I),()))))) + 3 ; :: thesis: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),())))))) = goto 0
CurInstr ((P +* I),(Comput ((P +* I),(),(LifeSpan ((P +* I),()))))) = I . n by ;
then A9: I . (IC (Comput ((P +* I),(),(LifeSpan ((P +* I),()))))) = halt SCM+FSA by ;
IC (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) = LastLoc I by
.= (card I) - 1 by AFINSQ_1:91 ;
then A10: (IC (Comput ((P +* I),(),(LifeSpan ((P +* I),()))))) + 3 = (card I) + 2 ;
card (while>0 (a,I)) = (card I) + 5 by SCMFSA_X:4;
then A11: n + 3 in dom (while>0 (a,I)) by ;
A12: n + 3 in dom (if>0 (a,(I ';' ()))) by ;
(P +* (while>0 (a,I))) . (n + 3) = (while>0 (a,I)) . (n + 3) by
.= (while>0 (a,I)) . ((card I) + 2) by A10
.= goto 0 by ;
hence CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),())))))) = goto 0 by A8, A7; :: thesis: verum