let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
let a be Int-Location ; :: thesis:
let I be Program of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
set s0 = Initialized s;
set sw = s +* (Initialized (while>0 (a,I)));
set Pw = P +* (while>0 (a,I));
set sI = s +* (Initialized I);
set PI = P +* I;
set s0I = (Initialized s) +* (Initialize I);
set s0w = (Initialized s) +* (Initialize (while>0 (a,I)));
A1: s +* (Initialized I) = (Initialized s) +* (Initialize I) by SCMFSA8A:13;
A2: s +* (Initialized (while>0 (a,I))) = (Initialized s) +* (Initialize (while>0 (a,I))) by SCMFSA8A:13;
assume I is_closed_onInit s,P ; :: thesis:
then A3: I is_closed_on Initialized s,P by SCM_HALT:40;
assume I is_halting_onInit s,P ; :: thesis:
then A4: I is_halting_on Initialized s,P by SCM_HALT:41;
assume IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),(1 + (LifeSpan ((P +* I),(s +* (Initialized I))))))) = (IC (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I))))))) + 4 ; :: thesis:
hence CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),(1 + (LifeSpan ((P +* I),(s +* (Initialized I)))))))) = goto ((card I) + 4) by A3, A4, A1, A2, SCMFSA_9:45; :: thesis: