set A = NAT ;
let s be State of SCM+FSA ; for I being Program of SCM+FSA
for a being read-write Int-Location st s . a <= 0 holds
DataPart (IExec (while>0 a,I),s) = DataPart (Initialized s)
let I be Program of SCM+FSA ; for a being read-write Int-Location st s . a <= 0 holds
DataPart (IExec (while>0 a,I),s) = DataPart (Initialized s)
let a be read-write Int-Location ; ( s . a <= 0 implies DataPart (IExec (while>0 a,I),s) = DataPart (Initialized s) )
set D = Int-Locations \/ FinSeq-Locations ;
set Is = Initialized s;
set s1 = (Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ));
set s2 = Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),1;
set s3 = Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),2;
set s4 = Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3;
set s5 = Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),4;
set i = a >0_goto 4;
A1:
1 in dom (while>0 a,I)
by SCMFSA_9:10;
while>0 a,I c= (while>0 a,I) +* (Start-At 0 ,SCM+FSA )
by SCMFSA8A:9;
then A2:
dom (while>0 a,I) c= dom ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))
by GRFUNC_1:8;
A3: (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),1) . 1 =
((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) . 1
by AMI_1:54
.=
((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) . 1
by A2, A1, FUNCT_4:14
.=
(while>0 a,I) . 1
by A1, SCMFSA6B:7
.=
goto 2
by SCMFSA_9:11
;
IC SCM+FSA in dom ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))
by SF_MASTR:65;
then A4: IC ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) =
((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) . (IC SCM+FSA )
by FUNCT_4:14
.=
0
by SF_MASTR:66
;
Y:
(ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))) /. (IC ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))) = ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) . (IC ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))))
by COMPOS_1:38;
A5:
0 in dom (while>0 a,I)
by SCMFSA_9:10;
then A6: ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) . 0 =
((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) . 0
by A2, FUNCT_4:14
.=
(while>0 a,I) . 0
by A5, SCMFSA6B:7
.=
a >0_goto 4
by SCMFSA_9:11
;
then A7:
CurInstr (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = a >0_goto 4
by A4, Y;
A8: Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(0 + 1) =
Following (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),0 )
by AMI_1:14
.=
Following (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))
by AMI_1:13
.=
Exec (a >0_goto 4),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))
by A4, A6, Y
;
set loc5 = (card I) + 5;
A9:
2 in dom (while>0 a,I)
by SCMFSA_9:37;
A10: (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),2) . 2 =
((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) . 2
by AMI_1:54
.=
((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) . 2
by A2, A9, FUNCT_4:14
.=
(while>0 a,I) . 2
by A9, SCMFSA6B:7
.=
goto 3
by SCMFSA_9:41
;
A11:
IC (Initialized s) = 0
by SCMFSA6C:3;
A12:
(card I) + 5 in dom (while>0 a,I)
by SCMFSA_9:38;
not a in dom ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))
by SCMFSA6B:12;
then A13:
((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) . a = (Initialized s) . a
by FUNCT_4:12;
A14:
3 in dom (while>0 a,I)
by SCMFSA_9:37;
assume
s . a <= 0
; DataPart (IExec (while>0 a,I),s) = DataPart (Initialized s)
then
(Initialized s) . a <= 0
by SCMFSA6C:3;
then A15: IC (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),1) =
succ 0
by A4, A8, A13, SCMFSA_2:97
.=
0 + 1
;
Y:
(ProgramPart (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),1)) /. (IC (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),1)) = (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),1) . (IC (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),1))
by COMPOS_1:38;
T:
ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),1)
by AMI_1:123;
A16: Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + 1) =
Following (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),1)
by AMI_1:14
.=
Exec (goto 2),(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),1)
by A15, A3, Y, T
;
then A17:
IC (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),2) = 2
by SCMFSA_2:95;
Y:
(ProgramPart (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),2)) /. (IC (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),2)) = (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),2) . (IC (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),2))
by COMPOS_1:38;
T:
ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),2)
by AMI_1:123;
A18: Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(2 + 1) =
Following (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),2)
by AMI_1:14
.=
Exec (goto 3),(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),2)
by A16, A10, Y, T, SCMFSA_2:95
;
A19: (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3) . 3 =
((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) . 3
by AMI_1:54
.=
((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) . 3
by A2, A14, FUNCT_4:14
.=
(while>0 a,I) . 3
by A14, SCMFSA6B:7
.=
goto ((card I) + 5)
by SCMFSA_9:40
;
Y:
(ProgramPart (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3)) /. (IC (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3)) = (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3) . (IC (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3))
by COMPOS_1:38;
T:
ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3)
by AMI_1:123;
A20: Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(3 + 1) =
Following (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3)
by AMI_1:14
.=
Exec (goto ((card I) + 5)),(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3)
by A18, A19, Y, T, SCMFSA_2:95
;
Y:
(ProgramPart (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),4)) /. (IC (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),4)) = (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),4) . (IC (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),4))
by COMPOS_1:38;
TX:
ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),4)
by AMI_1:123;
(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),4) . ((card I) + 5) =
((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) . ((card I) + 5)
by AMI_1:54
.=
((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) . ((card I) + 5)
by A2, A12, FUNCT_4:14
.=
(while>0 a,I) . ((card I) + 5)
by A12, SCMFSA6B:7
.=
halt SCM+FSA
by SCMFSA_9:39
;
then A21:
CurInstr (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),4) = halt SCM+FSA
by A20, Y, TX, SCMFSA_2:95;
then A22:
ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) halts_on (Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))
by AMI_1:146;
Y:
(ProgramPart (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3)) /. (IC (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3)) = (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3) . (IC (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3))
by COMPOS_1:38;
A23:
CurInstr (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3) = goto ((card I) + 5)
by A18, A19, Y, T, SCMFSA_2:95;
now let k be
Element of
NAT ;
( CurInstr (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k) = halt SCM+FSA implies 3 + 1 <= k )A24:
goto ((card I) + 5) <> halt SCM+FSA
by SCMFSA_9:9;
u:
Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),
((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),
0 = (Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))
by AMI_1:13;
Y:
(ProgramPart (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k)) /. (IC (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k)) = (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k) . (IC (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k))
by COMPOS_1:38;
TX:
ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k)
by AMI_1:123;
assume A25:
CurInstr (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),
(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k) = halt SCM+FSA
;
3 + 1 <= kthen A26:
k <> 2
by A17, A10, Y, TX, SCMFSA_9:9;
CurInstr (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),
(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),0 ) = a >0_goto 4
by A7, u;
then A27:
k <> 0
by A25, SCMFSA_9:8;
xx:
k <> 1
by A15, A3, A25, Y, TX, SCMFSA_9:9;
3
<> k
by A23, A25, A24;
then
3
< k
by A27, A26, xx, NAT_1:28;
hence
3
+ 1
<= k
by INT_1:20;
verum end;
then A28:
LifeSpan (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) = 4
by A21, A22, AMI_1:def 46;
A29: (Initialized s) +* (Initialized (while>0 a,I)) =
(Initialized (Initialized s)) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))
by SCMFSA8A:13
.=
(Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))
by SCMFSA8C:15
;
(Initialized s) . (intloc 0 ) = 1
by SCMFSA6C:3;
then A30:
(Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) = (Initialized s) +* (while>0 a,I)
by A29, A11, Th6;
A31:
now let a be
Int-Location ;
(Initialized s) . a = (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),4) . athus (Initialized s) . a =
((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) . a
by A30, FUNCT_7:132, SCMFSA10:92
.=
(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),1) . a
by A8, SCMFSA_2:97
.=
(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),2) . a
by A16, SCMFSA_2:95
.=
(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3) . a
by A18, SCMFSA_2:95
.=
(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),4) . a
by A20, SCMFSA_2:95
;
verum end;
A32:
now let f be
FinSeq-Location ;
(Initialized s) . f = (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),4) . fthus (Initialized s) . f =
((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) . f
by A30, FUNCT_7:132, SCMFSA10:93
.=
(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),1) . f
by A8, SCMFSA_2:97
.=
(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),2) . f
by A16, SCMFSA_2:95
.=
(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),3) . f
by A18, SCMFSA_2:95
.=
(Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),4) . f
by A20, SCMFSA_2:95
;
verum end;
thus DataPart (IExec (while>0 a,I),s) =
DataPart (IExec (while>0 a,I),(Initialized s))
by SCMFSA8C:17
.=
DataPart ((Result (ProgramPart ((Initialized s) +* (Initialized (while>0 a,I)))),((Initialized s) +* (Initialized (while>0 a,I)))) +* ((Initialized s) | NAT ))
by SCMFSA6B:def 1
.=
DataPart (Result (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))))
by A29, SCMFSA8C:35
.=
DataPart (Comput (ProgramPart ((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),4)
by A22, A28, AMI_1:122
.=
DataPart (Initialized s)
by A31, A32, SCMFSA6A:38
; verum