let s be State of ; :: thesis: for I being Program of
for a being read-write Int-Location st I is_closed_onInit s & I is_halting_onInit s & s . a > 0 holds
( IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0 & ( for k being Element of NAT st k <= (LifeSpan (s +* (Initialized I))) + 3 holds
IC (Computation (s +* (Initialized (while>0 a,I))),k) in dom (while>0 a,I) ) )
let I be Program of ; :: thesis: for a being read-write Int-Location st I is_closed_onInit s & I is_halting_onInit s & s . a > 0 holds
( IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0 & ( for k being Element of NAT st k <= (LifeSpan (s +* (Initialized I))) + 3 holds
IC (Computation (s +* (Initialized (while>0 a,I))),k) in dom (while>0 a,I) ) )
let a be read-write Int-Location ; :: thesis: ( I is_closed_onInit s & I is_halting_onInit s & s . a > 0 implies ( IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0 & ( for k being Element of NAT st k <= (LifeSpan (s +* (Initialized I))) + 3 holds
IC (Computation (s +* (Initialized (while>0 a,I))),k) in dom (while>0 a,I) ) ) )
set s0 = Initialize s;
set sw = s +* (Initialized (while>0 a,I));
set sI = s +* (Initialized I);
set s0I = (Initialize s) +* (I +* (Start-At (insloc 0 )));
set s0w = (Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )));
A1: s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
A2: s +* (Initialized (while>0 a,I)) = (Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
assume I is_closed_onInit s ; :: thesis: ( not I is_halting_onInit s or not s . a > 0 or ( IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0 & ( for k being Element of NAT st k <= (LifeSpan (s +* (Initialized I))) + 3 holds
IC (Computation (s +* (Initialized (while>0 a,I))),k) in dom (while>0 a,I) ) ) )
then A3: I is_closed_on Initialize s by SCM_HALT:40;
assume I is_halting_onInit s ; :: thesis: ( not s . a > 0 or ( IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0 & ( for k being Element of NAT st k <= (LifeSpan (s +* (Initialized I))) + 3 holds
IC (Computation (s +* (Initialized (while>0 a,I))),k) in dom (while>0 a,I) ) ) )
then A4: I is_halting_on Initialize s by SCM_HALT:41;
assume s . a > 0 ; :: thesis: ( IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0 & ( for k being Element of NAT st k <= (LifeSpan (s +* (Initialized I))) + 3 holds
IC (Computation (s +* (Initialized (while>0 a,I))),k) in dom (while>0 a,I) ) )
then A5: (Initialize s) . a > 0 by SCMFSA6C:3;
hence IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0 by A3, A4, A1, A2, SCMFSA_9:47; :: thesis: for k being Element of NAT st k <= (LifeSpan (s +* (Initialized I))) + 3 holds
IC (Computation (s +* (Initialized (while>0 a,I))),k) in dom (while>0 a,I)
thus for k being Element of NAT st k <= (LifeSpan (s +* (Initialized I))) + 3 holds
IC (Computation (s +* (Initialized (while>0 a,I))),k) in dom (while>0 a,I) by A3, A4, A5, A1, A2, SCMFSA_9:47; :: thesis: verum