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))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))) = (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) + 3 holds
CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0
set J3 = (Goto 0) ";" (Stop SCM+FSA);
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))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))) = (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) + 3 holds
CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = 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))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))) = (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) + 3 holds
CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0
let s be State of SCM+FSA; :: thesis: ( I is_halting_on s,P & IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))) = (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) + 3 implies CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = 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),(Initialize s));
set sK1 = Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))));
set sK2 = Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))));
set I1 = I ';' (goto 0);
set i = a =0_goto 3;
reconsider n = IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) as Element of NAT ;
set Mi = (a =0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1));
set J2 = (I ';' (goto 0)) ";" (Stop SCM+FSA);
A2: I c= P +* I by FUNCT_4:25;
IC (Initialize s) = 0 by MEMSTR_0:def 11;
then IC (Initialize s) in dom I by AFINSQ_1:65;
then A3: n in dom I by AMISTD_1:21, A2;
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))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))) = (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) + 3 or CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0 )
then A5: P +* I halts_on Initialize s by SCMFSA7B:def 7;
A6: (P +* I) /. (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by PBOOLE:143;
A7: (P +* (while=0 (a,I))) /. (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = (P +* (while=0 (a,I))) . (IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) by PBOOLE:143;
assume A8: IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))) = (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) + 3 ; :: thesis: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0
CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = I . n by A3, A1, GRFUNC_1:2, A6;
then A9: I . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = halt SCM+FSA by A5, EXTPRO_1:def 15;
IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = LastLoc I by A3, A9, COMPOS_1:def 15
.= (card I) - 1 by AFINSQ_1:91 ;
then A10: (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) + 3 = (card I) + 2 ;
card (while=0 (a,I)) = (card I) + 5 by SCMFSA_X:3;
then A11: n + 3 in dom (while=0 (a,I)) by A4, AFINSQ_1:66;
A12: n + 3 in dom (if=0 (a,(I ';' (goto 0)))) by A11, FUNCT_7:30;
(P +* (while=0 (a,I))) . (n + 3) = (while=0 (a,I)) . (n + 3) by FUNCT_4:13, A11
.= (while=0 (a,I)) . ((card I) + 2) by A10
.= goto 0 by FUNCT_7:31, A10, A12 ;
hence CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0 by A8, A7; :: thesis: verum