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

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

end;

then A2: I is_closed_on Initialized 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) = (Initialized s) +* (I +* (Start-At (0,SCM+FSA))) by SCMFSA8A:13;
then A3: I is_halting_on Initialized s by X, SCMFSA7B:def 8;
assume s . a > 0 ; :: thesis:
then A4: (Initialized s) . a > 0 by SCMFSA6C:3;

hereby :: thesis:

let k be Element of NAT ; :: thesis:
X: s +* (Initialized (while>0 (a,I))) = (Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by SCMFSA8A:13;
XX: s +* (Initialized I) = (Initialized s) +* (I +* (Start-At (0,SCM+FSA))) by SCMFSA8A:13;
assume k <= (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3 ; :: thesis:
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, A2, A3, A4, XX, SCMFSA_9:47; :: thesis:

end;