set D = Int-Locations \/ FinSeq-Locations ;
let s be State of SCM+FSA ; :: thesis:
let I be Program of SCM+FSA ; :: thesis:
let a be read-write Int-Location ; :: thesis:
assume A1: I is_closed_onInit s ; :: thesis:
assume A2: I is_halting_onInit s ; :: thesis:
assume A3: s . a > 0 ; :: thesis:
set s0 = Initialize s;
set IA = I +* (Start-At (insloc 0 ));
set s1 = (Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )));
set s2 = Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1;
set i = a >0_goto (insloc 4);
set sI = (Initialize s) +* (I +* (Start-At (insloc 0 )));

now

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

end;

then A4: I is_closed_on Initialize s by SCMFSA7B:def 7;
s +* (Initialized I) is halting by A2, SCM_HALT:def 5;
then (Initialize s) +* (I +* (Start-At (insloc 0 ))) is halting by SCMFSA8A:13;
then A5: I is_halting_on Initialize s by SCMFSA7B:def 8;
A6: (Initialize s) . a > 0 by A3, SCMFSA6C:3;
A7: insloc 0 in dom (while>0 a,I) by SCMFSA_9:10;
while>0 a,I c= (while>0 a,I) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A8: dom (while>0 a,I) c= dom ((while>0 a,I) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
IC SCM+FSA in dom ((while>0 a,I) +* (Start-At (insloc 0 ))) by SF_MASTR:65;
then A9: IC ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) = ((while>0 a,I) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by FUNCT_4:14
.= insloc 0 by SF_MASTR:66 ;
A10: ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (insloc 0 ) = ((while>0 a,I) +* (Start-At (insloc 0 ))) . (insloc 0 ) by A7, A8, FUNCT_4:14
.= (while>0 a,I) . (insloc 0 ) by A7, SCMFSA6B:7
.= a >0_goto (insloc 4) by SCMFSA_9:11 ;
A11: Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(0 + 1) = Following (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),0 ) by AMI_1:14
.= Following ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) by AMI_1:13
.= Exec (a >0_goto (insloc 4)),((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) by A9, A10 ;
( not a in dom ((while>0 a,I) +* (Start-At (insloc 0 ))) & a in dom (Initialize s) ) by SCMFSA6B:12, SCMFSA_2:66;
then A12: ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . a = (Initialize s) . a by FUNCT_4:12;
( ( for c being Int-Location holds (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) . c = ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . c ) & ( for f being FinSeq-Location holds (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) . f = ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . f ) ) by A11, SCMFSA_2:97;
then A13: DataPart (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) = DataPart ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) by SCMFSA6A:38
.= DataPart (Initialize s) by SCMFSA8A:11
.= DataPart ((Initialize s) +* (I +* (Start-At (insloc 0 )))) by SCMFSA8A:11 ;
defpred S₁[ Nat] means ( $1 <= LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))) implies ( IC (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + $1)) = (IC (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),$1)) + 4 & DataPart (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + $1)) = DataPart (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),$1) ) );
A14: S₁[ 0 ]

proof

assume 0 <= LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))) ; :: thesis:
A15: IC SCM+FSA in dom (I +* (Start-At (insloc 0 ))) by SF_MASTR:65;
IC (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),0 ) = ((Initialize s) +* (I +* (Start-At (insloc 0 )))) . (IC SCM+FSA ) by AMI_1:13
.= (I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A15, FUNCT_4:14
.= insloc 0 by SF_MASTR:66 ;
hence ( IC (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + 0 )) = (IC (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),0 )) + 4 & DataPart (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + 0 )) = DataPart (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),0 ) ) by A6, A11, A12, A13, AMI_1:13, SCMFSA_2:97; :: thesis:

end;

A16: now

let k be Element of NAT ; :: thesis:
assume A17: S₁[k] ; :: thesis:

now

assume A18: k + 1 <= LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))) ; :: thesis:
k + 0 < k + 1 by XREAL_1:8;
then k < LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))) by A18, XXREAL_0:2;
hence ( IC (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + k) + 1)) = (IC (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(k + 1))) + 4 & DataPart (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + k) + 1)) = DataPart (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(k + 1)) ) by A4, A5, A17, SCMFSA_9:44; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;