set D = Int-Locations \/ FinSeq-Locations ;
let a be Int-Location ; :: thesis:
let I be Program of SCM+FSA ; :: thesis:
let s be State of SCM+FSA ; :: thesis:
let k be Element of NAT ; :: thesis:
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 )));
set sK1 = Computation (s +* (Initialized (while>0 a,I))),(1 + k);
set sK2 = Computation (s +* (Initialized I)),k;
set l3 = IC (Computation (s +* (Initialized I)),k);
assume A1: I is_closed_onInit s ; :: thesis:
assume A2: I is_halting_onInit s ; :: thesis:
assume A3: k < LifeSpan (s +* (Initialized I)) ; :: thesis:
assume A4: IC (Computation (s +* (Initialized (while>0 a,I))),(1 + k)) = (IC (Computation (s +* (Initialized I)),k)) + 4 ; :: thesis:
assume A5: DataPart (Computation (s +* (Initialized (while>0 a,I))),(1 + k)) = DataPart (Computation (s +* (Initialized I)),k) ; :: thesis:
A6: I is_closed_on Initialize s by A1, SCM_HALT:40;
A7: I is_halting_on Initialize s by A2, SCM_HALT:41;
A8: s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
A9: s +* (Initialized (while>0 a,I)) = (Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
hence IC (Computation (s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = (IC (Computation (s +* (Initialized I)),(k + 1))) + 4 by A3, A4, A5, A6, A7, A8, SCMFSA_9:44; :: thesis:
thus DataPart (Computation (s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = DataPart (Computation (s +* (Initialized I)),(k + 1)) by A3, A4, A5, A6, A7, A8, A9, SCMFSA_9:44; :: thesis: