let P be Instruction-Sequence of SCM+FSA; :: thesis: for a being Int-Location
for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_onInit s,P & 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)))))) + 4 holds
CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto ((card I) + 4)
let a be Int-Location ; :: thesis: for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_onInit s,P & 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)))))) + 4 holds
CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto ((card I) + 4)
let I be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st I is_closed_onInit s,P & 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)))))) + 4 holds
CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto ((card I) + 4)
let s be State of SCM+FSA; :: thesis: ( I is_closed_onInit s,P & 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)))))) + 4 implies CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto ((card I) + 4) )
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_closed_onInit s,P ; :: thesis: ( not I is_halting_onInit s,P or 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)))))) + 4 or CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto ((card I) + 4) )
then A3: I is_closed_on Initialized s,P by SCM_HALT:30;
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)))))) + 4 or CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto ((card I) + 4) )
then A4: 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)))))) + 4 ; :: thesis: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto ((card I) + 4)
hence CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto ((card I) + 4) by A3, A4, A1, SCMFSA_9:40; :: thesis: verum