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_onInit s,P & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s)))))) = (IC (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) + 3 holds

CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto 0

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_onInit s,P & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s)))))) = (IC (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) + 3 holds

CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto 0

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

CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto 0

let s be State of SCM+FSA; :: thesis: ( I is_halting_onInit s,P & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s)))))) = (IC (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) + 3 implies CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto 0 )

set s0 = Initialized s;

set sw = Initialized s;

set Pw = P +* (while>0 (a,I));

set PI = P +* I;

set s0I = Initialize (Initialized s);

A1: Initialized s = Initialize (Initialized s) by MEMSTR_0:44;

assume I is_halting_onInit s,P ; :: thesis: ( not IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s)))))) = (IC (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) + 3 or CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto 0 )

then A2: I is_halting_on Initialized s,P by SCM_HALT:31;

assume IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s)))))) = (IC (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) + 3 ; :: thesis: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto 0

hence CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto 0 by A2, A1, SCMFSA_9:40; :: thesis: verum

for I being really-closed MacroInstruction of SCM+FSA

for s being State of SCM+FSA st I is_halting_onInit s,P & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s)))))) = (IC (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) + 3 holds

CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto 0

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_onInit s,P & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s)))))) = (IC (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) + 3 holds

CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto 0

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

CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto 0

let s be State of SCM+FSA; :: thesis: ( I is_halting_onInit s,P & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s)))))) = (IC (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) + 3 implies CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto 0 )

set s0 = Initialized s;

set sw = Initialized s;

set Pw = P +* (while>0 (a,I));

set PI = P +* I;

set s0I = Initialize (Initialized s);

A1: Initialized s = Initialize (Initialized s) by MEMSTR_0:44;

assume I is_halting_onInit s,P ; :: thesis: ( not IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s)))))) = (IC (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) + 3 or CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto 0 )

then A2: I is_halting_on Initialized s,P by SCM_HALT:31;

assume IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s)))))) = (IC (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) + 3 ; :: thesis: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto 0

hence CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto 0 by A2, A1, SCMFSA_9:40; :: thesis: verum