let s be State of SCM+FSA; :: thesis:
let I be Program of SCM+FSA; :: thesis:
let a be read-write Int-Location ; :: thesis:
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 ; :: thesis:
then A3: I is_closed_on Initialized s by SCM_HALT:40;
assume I is_halting_onInit s ; :: thesis:
then A4: I is_halting_on Initialized s by SCM_HALT:41;
assume s . a > 0 ; :: thesis:
then A5: (Initialized s) . a > 0 by SCMFSA6C:3;
hence IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = 0 by A3, A4, A1, A2, SCMFSA_9:47; :: thesis:
thus for k being Element of NAT st k <= (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3 holds
IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),k)) in dom (while>0 (a,I)) by A3, A4, A5, A1, A2, SCMFSA_9:47; :: thesis: