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 = Initialize s;
set IA = I +* (Start-At 0 ,SCM+FSA );
assume A1: I is_closed_onInit s ; :: thesis:

let k be Element of NAT ; :: thesis:
X: s +* (Initialized I) = (Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )) by SCMFSA8A:13;
IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k) in dom I by A1, SCM_HALT:def 4;
hence IC (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),k) in dom I by X; :: thesis:

end;

then A2: I is_closed_on Initialize s by SCMFSA7B:def 7;
assume I is_halting_onInit s ; :: thesis:
then X: ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) by SCM_HALT:def 5;
s +* (Initialized I) = (Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )) by SCMFSA8A:13;
then ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))) halts_on (Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )) by X;
then A3: I is_halting_on Initialize s by SCMFSA7B:def 8;
assume s . a > 0 ; :: thesis:
then A4: (Initialize s) . a > 0 by SCMFSA6C:3;

hereby :: thesis:

let k be Element of NAT ; :: thesis:
X: s +* (Initialized (while>0 a,I)) = (Initialize s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) by SCMFSA8A:13;
assume k <= (LifeSpan (s +* (Initialized I))) + 3 ; :: thesis:
then k <= (LifeSpan ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 by SCMFSA8A:13;
then IC (Comput (ProgramPart ((Initialize s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k) in dom (while>0 a,I) by A2, A3, A4, SCMFSA_9:47;
hence IC (Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),k) in dom (while>0 a,I) by X; :: thesis:

end;