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 & I is_halting_onInit s & IC (Computation (s +* (Initialized (while>0 a,I))),(1 + (LifeSpan (s +* (Initialized I))))) = (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) + 4 holds
CurInstr (Computation (s +* (Initialized (while>0 a,I))),(1 + (LifeSpan (s +* (Initialized I))))) = goto (insloc ((card I) + 4))
let I be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA st I is_closed_onInit s & I is_halting_onInit s & IC (Computation (s +* (Initialized (while>0 a,I))),(1 + (LifeSpan (s +* (Initialized I))))) = (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) + 4 holds
CurInstr (Computation (s +* (Initialized (while>0 a,I))),(1 + (LifeSpan (s +* (Initialized I))))) = goto (insloc ((card I) + 4))
let s be State of SCM+FSA ; :: thesis: ( I is_closed_onInit s & I is_halting_onInit s & IC (Computation (s +* (Initialized (while>0 a,I))),(1 + (LifeSpan (s +* (Initialized I))))) = (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) + 4 implies CurInstr (Computation (s +* (Initialized (while>0 a,I))),(1 + (LifeSpan (s +* (Initialized I))))) = goto (insloc ((card I) + 4)) )
set s0 = Initialize s;
set sw = s +* (Initialized (while>0 a,I));
set sI = s +* (Initialized I);
set s0I = (Initialize s) +* (I +* (Start-At (insloc 0 )));
set s0w = (Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )));
assume A1: I is_closed_onInit s ; :: thesis: ( not I is_halting_onInit s or not IC (Computation (s +* (Initialized (while>0 a,I))),(1 + (LifeSpan (s +* (Initialized I))))) = (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) + 4 or CurInstr (Computation (s +* (Initialized (while>0 a,I))),(1 + (LifeSpan (s +* (Initialized I))))) = goto (insloc ((card I) + 4)) )
assume A2: I is_halting_onInit s ; :: thesis: ( not IC (Computation (s +* (Initialized (while>0 a,I))),(1 + (LifeSpan (s +* (Initialized I))))) = (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) + 4 or CurInstr (Computation (s +* (Initialized (while>0 a,I))),(1 + (LifeSpan (s +* (Initialized I))))) = goto (insloc ((card I) + 4)) )
assume A3: IC (Computation (s +* (Initialized (while>0 a,I))),(1 + (LifeSpan (s +* (Initialized I))))) = (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) + 4 ; :: thesis: CurInstr (Computation (s +* (Initialized (while>0 a,I))),(1 + (LifeSpan (s +* (Initialized I))))) = goto (insloc ((card I) + 4))
A4: I is_closed_on Initialize s by A1, SCM_HALT:40;
A5: I is_halting_on Initialize s by A2, SCM_HALT:41;
A6: s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
s +* (Initialized (while>0 a,I)) = (Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
hence CurInstr (Computation (s +* (Initialized (while>0 a,I))),(1 + (LifeSpan (s +* (Initialized I))))) = goto (insloc ((card I) + 4)) by A3, A4, A5, A6, SCMFSA_9:45; :: thesis: verum