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:
set Is = Initialize s;
assume s . a <= 0 ; :: thesis:
then A1: (Initialize s) . a <= 0 by SCMFSA6C:3;
set A = NAT ;
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 s3 = Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2;
set s4 = Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3;
set s5 = Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4;
set i = a >0_goto (insloc 4);
A2: 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 A3: 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 A4: 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 ;
A5: ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (insloc 0 ) = ((while>0 a,I) +* (Start-At (insloc 0 ))) . (insloc 0 ) by A2, A3, FUNCT_4:14
.= (while>0 a,I) . (insloc 0 ) by A2, SCMFSA6B:7
.= a >0_goto (insloc 4) by SCMFSA_9:11 ;
then A6: CurInstr ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) = a >0_goto (insloc 4) by A4;
A7: 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 A4, A5 ;
( not a in dom ((while>0 a,I) +* (Start-At (insloc 0 ))) & a in dom (Initialize s) ) by SCMFSA6B:12, SCMFSA_2:66;
then ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . a = (Initialize s) . a by FUNCT_4:12;
then A8: IC (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) = Next (insloc 0 ) by A1, A4, A7, SCMFSA_2:97
.= insloc (0 + 1) ;
A9: insloc 1 in dom (while>0 a,I) by SCMFSA_9:10;
A10: (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) . (insloc 1) = ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (insloc 1) by AMI_1:54
.= ((while>0 a,I) +* (Start-At (insloc 0 ))) . (insloc 1) by A3, A9, FUNCT_4:14
.= (while>0 a,I) . (insloc 1) by A9, SCMFSA6B:7
.= goto (insloc 2) by SCMFSA_9:11 ;
A11: Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + 1) = Following (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) by AMI_1:14
.= Exec (goto (insloc 2)),(Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) by A8, A10 ;
A12: insloc 2 in dom (while>0 a,I) by SCMFSA_9:37;
A13: IC (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) = insloc 2 by A11, SCMFSA_2:95;
A14: (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) . (insloc 2) = ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (insloc 2) by AMI_1:54
.= ((while>0 a,I) +* (Start-At (insloc 0 ))) . (insloc 2) by A3, A12, FUNCT_4:14
.= (while>0 a,I) . (insloc 2) by A12, SCMFSA6B:7
.= goto (insloc 3) by SCMFSA_9:41 ;
A15: Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(2 + 1) = Following (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) by AMI_1:14
.= Exec (goto (insloc 3)),(Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) by A11, A14, SCMFSA_2:95 ;
A16: insloc 3 in dom (while>0 a,I) by SCMFSA_9:37;
set loc5 = insloc ((card I) + 5);
A17: (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) . (insloc 3) = ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (insloc 3) by AMI_1:54
.= ((while>0 a,I) +* (Start-At (insloc 0 ))) . (insloc 3) by A3, A16, FUNCT_4:14
.= (while>0 a,I) . (insloc 3) by A16, SCMFSA6B:7
.= goto (insloc ((card I) + 5)) by SCMFSA_9:40 ;
then A18: CurInstr (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) = goto (insloc ((card I) + 5)) by A15, SCMFSA_2:95;
A19: Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(3 + 1) = Following (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) by AMI_1:14
.= Exec (goto (insloc ((card I) + 5))),(Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) by A15, A17, SCMFSA_2:95 ;
A20: insloc ((card I) + 5) in dom (while>0 a,I) by SCMFSA_9:38;
(Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4) . (insloc ((card I) + 5)) = ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (insloc ((card I) + 5)) by AMI_1:54
.= ((while>0 a,I) +* (Start-At (insloc 0 ))) . (insloc ((card I) + 5)) by A3, A20, FUNCT_4:14
.= (while>0 a,I) . (insloc ((card I) + 5)) by A20, SCMFSA6B:7
.= halt SCM+FSA by SCMFSA_9:39 ;
then A21: CurInstr (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4) = halt SCM+FSA by A19, SCMFSA_2:95;
then A22: (Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) is halting by AMI_1:def 20;
A23: (Initialize s) +* (Initialized (while>0 a,I)) = (Initialize (Initialize s)) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) by SCMFSA8A:13
.= (Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) by SCMFSA8C:15 ;

now

let k be Element of NAT ; :: thesis:
assume A24: CurInstr (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),k) = halt SCM+FSA ; :: thesis:
CurInstr (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),0 ) = a >0_goto (insloc 4) by A6, AMI_1:13;
then A25: k <> 0 by A24, SCMFSA_9:8;
A26: k <> 1 by A8, A10, A24, SCMFSA_9:9;
A27: k <> 2 by A13, A14, A24, SCMFSA_9:9;
goto (insloc ((card I) + 5)) <> halt SCM+FSA by SCMFSA_9:9;
then 3 < k by A18, A24, A25, A26, A27, NAT_1:28;
hence 3 + 1 <= k by INT_1:20; :: thesis:

end;

then A28: LifeSpan ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) = 4 by A21, A22, AMI_1:def 46;
( (Initialize s) . (intloc 0 ) = 1 & IC (Initialize s) = insloc 0 ) by SCMFSA6C:3;
then A29: (Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) = (Initialize s) +* (while>0 a,I) by A23, Th6;

A30: now

let a be Int-Location ; :: thesis:
thus (Initialize s) . a = ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . a by A29, AMI_1:120, SCMFSA6A:30
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) . a by A7, SCMFSA_2:97
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) . a by A11, SCMFSA_2:95
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) . a by A15, SCMFSA_2:95
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4) . a by A19, SCMFSA_2:95 ; :: thesis:

end;

A31: now

let f be FinSeq-Location ; :: thesis:
thus (Initialize s) . f = ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . f by A29, AMI_1:120, SCMFSA6A:31
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) . f by A7, SCMFSA_2:97
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) . f by A11, SCMFSA_2:95
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) . f by A15, SCMFSA_2:95
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4) . f by A19, SCMFSA_2:95 ; :: thesis:

end;

thus DataPart (IExec (while>0 a,I),s) = DataPart (IExec (while>0 a,I),(Initialize s)) by SCMFSA8C:17
.= DataPart ((Result ((Initialize s) +* (Initialized (while>0 a,I)))) +* ((Initialize s) | NAT )) by SCMFSA6B:def 1
.= DataPart (Result ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 ))))) by A23, SCMFSA8C:35
.= DataPart (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4) by A22, A28, AMI_1:122
.= DataPart (Initialize s) by A30, A31, SCMFSA6A:38 ; :: thesis: