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