let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
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 = Start-At (0,SCM+FSA);
assume A1: I is_closed_onInit s,P ; :: thesis:
YY: Initialize (Initialized s) = (s +* (Initialize ((intloc 0) .--> 1))) +* (Start-At (0,SCM+FSA)) by SCMFSA6A:def 4
.= s +* ((Initialize ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:99 ;

let k be Element of NAT ; :: thesis:
thus IC (Comput ((P +* I),(Initialize (Initialized s)),k)) in dom I by A1, YY, SCM_HALT:def 4; :: thesis:

end;

then A3: I is_closed_on Initialized s,P by SCMFSA7B:def 7;
assume I is_halting_onInit s,P ; :: thesis:
then A4: P +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by SCM_HALT:def 5;
s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by SCMFSA8A:13;
then A5: I is_halting_on Initialized s,P by A4, SCMFSA7B:def 8;
assume s . a > 0 ; :: thesis:
then A6: (Initialized s) . a > 0 by SCMFSA6C:3;

hereby :: thesis:

let k be Element of NAT ; :: thesis:
A7: s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by SCMFSA8A:13;
assume k <= (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3 ; :: thesis:
hence IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),k)) in dom (while>0 (a,I)) by A7, A3, A5, A6, SCMFSA_9:47; :: thesis:

end;