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

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