set A = NAT ;
let s be State of ; :: thesis: for I being Program of
for a being read-write Int-Location st s . a <= 0 holds
DataPart (IExec (while>0 a,I),s) = DataPart (Initialize s)
let I be Program of ; :: thesis: for a being read-write Int-Location st s . a <= 0 holds
DataPart (IExec (while>0 a,I),s) = DataPart (Initialize s)
let a be read-write Int-Location ; :: thesis: ( s . a <= 0 implies DataPart (IExec (while>0 a,I),s) = DataPart (Initialize s) )
set D = Int-Locations \/ FinSeq-Locations ;
set Is = Initialize s;
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);
A1: insloc 1 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 A2: dom (while>0 a,I) c= dom ((while>0 a,I) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
A3: (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 A2, A1, FUNCT_4:14
.= (while>0 a,I) . (insloc 1) by A1, SCMFSA6B:7
.= goto (insloc 2) by SCMFSA_9:11 ;
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: insloc 0 in dom (while>0 a,I) by SCMFSA_9:10;
then A6: ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (insloc 0 ) = ((while>0 a,I) +* (Start-At (insloc 0 ))) . (insloc 0 ) by A2, FUNCT_4:14
.= (while>0 a,I) . (insloc 0 ) by A5, SCMFSA6B:7
.= a >0_goto (insloc 4) by SCMFSA_9:11 ;
then A7: CurInstr ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) = a >0_goto (insloc 4) by A4;
A8: 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, A6 ;
set loc5 = insloc ((card I) + 5);
A9: insloc 2 in dom (while>0 a,I) by SCMFSA_9:37;
A10: (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 A2, A9, FUNCT_4:14
.= (while>0 a,I) . (insloc 2) by A9, SCMFSA6B:7
.= goto (insloc 3) by SCMFSA_9:41 ;
A11: IC (Initialize s) = insloc 0 by SCMFSA6C:3;
A12: insloc ((card I) + 5) in dom (while>0 a,I) by SCMFSA_9:38;
not a in dom ((while>0 a,I) +* (Start-At (insloc 0 ))) by SCMFSA6B:12;
then A13: ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . a = (Initialize s) . a by FUNCT_4:12;
A14: insloc 3 in dom (while>0 a,I) by SCMFSA_9:37;
assume s . a <= 0 ; :: thesis: DataPart (IExec (while>0 a,I),s) = DataPart (Initialize s)
then (Initialize s) . a <= 0 by SCMFSA6C:3;
then A15: IC (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) = Next (insloc 0 ) by A4, A8, A13, SCMFSA_2:97
.= insloc (0 + 1) ;
A16: 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 A15, A3 ;
then A17: IC (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) = insloc 2 by SCMFSA_2:95;
A18: 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 A16, A10, SCMFSA_2:95 ;
A19: (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 A2, A14, FUNCT_4:14
.= (while>0 a,I) . (insloc 3) by A14, SCMFSA6B:7
.= goto (insloc ((card I) + 5)) by SCMFSA_9:40 ;
A20: 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 A18, A19, SCMFSA_2:95 ;
(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 A2, A12, FUNCT_4:14
.= (while>0 a,I) . (insloc ((card I) + 5)) by A12, 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 A20, SCMFSA_2:95;
then A22: ProgramPart ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) halts_on (Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) by AMI_1:146;
A23: CurInstr (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) = goto (insloc ((card I) + 5)) by A18, A19, SCMFSA_2:95;

now

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

end;

then A28: LifeSpan ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) = 4 by A21, A22, AMI_1:def 46;
A29: (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 ;
(Initialize s) . (intloc 0 ) = 1 by SCMFSA6C:3;
then A30: (Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) = (Initialize s) +* (while>0 a,I) by A29, A11, Th6;

A31: now

let a be Int-Location ; :: thesis: (Initialize s) . a = (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4) . a
thus (Initialize s) . a = ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . a by A30, AMI_1:120, SCMFSA6A:30
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) . a by A8, SCMFSA_2:97
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) . a by A16, SCMFSA_2:95
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) . a by A18, SCMFSA_2:95
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4) . a by A20, SCMFSA_2:95 ; :: thesis: verum

end;

A32: now

let f be FinSeq-Location ; :: thesis: (Initialize s) . f = (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4) . f
thus (Initialize s) . f = ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . f by A30, AMI_1:120, SCMFSA6A:31
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) . f by A8, SCMFSA_2:97
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) . f by A16, SCMFSA_2:95
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) . f by A18, SCMFSA_2:95
.= (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4) . f by A20, SCMFSA_2:95 ; :: thesis: verum

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 A29, 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 A31, A32, SCMFSA6A:38 ; :: thesis: verum