let s be State of SCM+FSA; for I being Program of SCM+FSA
for a being read-write Int-Location st I is_closed_onInit s & I is_halting_onInit s & s . a > 0 holds
( IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = 0 & DataPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) )
let I be Program of SCM+FSA; for a being read-write Int-Location st I is_closed_onInit s & I is_halting_onInit s & s . a > 0 holds
( IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = 0 & DataPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) )
let a be read-write Int-Location ; ( I is_closed_onInit s & I is_halting_onInit s & s . a > 0 implies ( IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = 0 & DataPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) ) )
set D = Int-Locations \/ FinSeq-Locations;
set s0 = Initialized s;
set IA = I +* (Start-At (0,SCM+FSA));
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 i = a >0_goto 4;
set sI = (Initialized s) +* (I +* (Start-At (0,SCM+FSA)));
defpred S1[ Nat] means ( $1 <= LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))) implies ( 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 + $1))) = (IC (Comput ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))),$1))) + 4 & 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)))),(1 + $1))) = DataPart (Comput ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))),$1)) ) );
set loc4 = (card I) + 4;
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)))),((1 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))) + 1));
A1:
(card I) + 4 in dom (while>0 (a,I))
by SCMFSA_9:38;
assume A2:
I is_closed_onInit s
; ( not I is_halting_onInit s or not s . a > 0 or ( IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = 0 & DataPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) ) )
now let k be
Element of
NAT ;
IC (Comput ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))),k)) in dom I
s +* (Initialized I) = (Initialized s) +* (I +* (Start-At (0,SCM+FSA)))
by SCMFSA8A:13;
hence
IC (Comput ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))),k)) in dom I
by A2, SCM_HALT:def 4;
verum end;
then A3:
I is_closed_on Initialized s
by SCMFSA7B:def 7;
assume
I is_halting_onInit s
; ( not s . a > 0 or ( IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = 0 & DataPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) ) )
then X:
ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I)
by SCM_HALT:def 5;
s +* (Initialized I) = (Initialized s) +* (I +* (Start-At (0,SCM+FSA)))
by SCMFSA8A:13;
then A4:
I is_halting_on Initialized s
by X, SCMFSA7B:def 8;
A5:
now let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )assume A6:
S1[
k]
;
S1[k + 1]now A7:
k + 0 < k + 1
by XREAL_1:8;
assume
k + 1
<= LifeSpan (
(ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),
((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))))
;
( 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 + k) + 1))) = (IC (Comput ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)))) + 4 & 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)))),((1 + k) + 1))) = DataPart (Comput ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) )then
k < LifeSpan (
(ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),
((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))))
by A7, XXREAL_0:2;
hence
(
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 + k) + 1))) = (IC (Comput ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)))) + 4 &
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)))),((1 + k) + 1))) = DataPart (Comput ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) )
by A3, A4, A6, SCMFSA_9:44;
verum end; hence
S1[
k + 1]
;
verum end;
while>0 (a,I) c= (while>0 (a,I)) +* (Start-At (0,SCM+FSA))
by SCMFSA8A:9;
then A8:
dom (while>0 (a,I)) c= dom ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))
by GRFUNC_1:8;
A9:
0 in dom (while>0 (a,I))
by SCMFSA_9:10;
then A10: ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . 0 =
((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . 0
by A8, FUNCT_4:14
.=
(while>0 (a,I)) . 0
by A9, COMPOS_1:145
.=
a >0_goto 4
by SCMFSA_9:11
;
IC SCM+FSA in dom ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))
by COMPOS_1:141;
then A11: IC ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) =
IC ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))
by FUNCT_4:14
.=
0
by COMPOS_1:142
;
A12: 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 EXTPRO_1:4
.=
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 EXTPRO_1:3
.=
Exec ((a >0_goto 4),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))))
by A11, A10, COMPOS_1:38
;
then A13:
for f being FinSeq-Location holds (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 = ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . f
by SCMFSA_2:97;
for c being Int-Location holds (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)) . c = ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . c
by A12, SCMFSA_2:97;
then A14: 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)))),1)) =
DataPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))
by A13, SCMFSA6A:38
.=
DataPart (Initialized s)
by SCMFSA8A:11
.=
DataPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))
by SCMFSA8A:11
;
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)))),(((1 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))) + 1) + 1));
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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))));
not a in dom ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))
by SCMFSA6B:12;
then A16:
((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . a = (Initialized s) . a
by FUNCT_4:12;
assume
s . a > 0
; ( IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = 0 & DataPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) )
then A17:
(Initialized s) . a > 0
by SCMFSA6C:3;
A18:
S1[ 0 ]
proof
assume
0 <= LifeSpan (
(ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),
((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))))
;
( 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 + 0))) = (IC (Comput ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))),0))) + 4 & 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)))),(1 + 0))) = DataPart (Comput ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))),0)) )
A19:
IC SCM+FSA in dom (I +* (Start-At (0,SCM+FSA)))
by COMPOS_1:141;
IC (Comput ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))),0)) =
((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))) . (IC SCM+FSA)
by EXTPRO_1:3
.=
IC (I +* (Start-At (0,SCM+FSA)))
by A19, FUNCT_4:14
.=
0
by COMPOS_1:142
;
hence
(
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 + 0))) = (IC (Comput ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))),0))) + 4 &
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)))),(1 + 0))) = DataPart (Comput ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))),0)) )
by A17, A12, A16, A14, EXTPRO_1:3, SCMFSA_2:97;
verum
end;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A18, A5);
then A20:
S1[ LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))))]
;
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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))))))))
by AMI_1:123;
A21: 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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))) + 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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))))))
by EXTPRO_1:4
.=
Exec ((goto ((card I) + 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)))),(1 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))))))
by A3, A4, A20, T, SCMFSA_9:45
;
then A22:
for f being FinSeq-Location holds (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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))) + 1))) . 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)))),(1 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))))) . f
by SCMFSA_2:95;
A23: (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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))) + 1))) . ((card I) + 4) =
((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . ((card I) + 4)
by AMI_1:54
.=
((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . ((card I) + 4)
by A8, A1, FUNCT_4:14
.=
(while>0 (a,I)) . ((card I) + 4)
by A1, COMPOS_1:145
.=
goto 0
by SCMFSA_9:46
;
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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))) + 1)))
by AMI_1:123;
A24: 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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))) + 1))))
by EXTPRO_1:4
.=
Exec ((goto 0),(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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))) + 1))))
by A21, A23, Y, T, SCMFSA_2:95
;
then A25:
for f being FinSeq-Location holds (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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))) + 1) + 1))) . 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)))),((1 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))) + 1))) . f
by SCMFSA_2:95;
for c being Int-Location holds (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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))) + 1))) . c = (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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))))) . c
by A21, SCMFSA_2:95;
then A26:
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)))),((1 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))) + 1))) = 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)))),(1 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA)))))))))
by A22, SCMFSA6A:38;
X:
s +* (Initialized (while>0 (a,I))) = (Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))
by SCMFSA8A:13;
XX:
(Initialized s) +* (I +* (Start-At (0,SCM+FSA))) = s +* (Initialized I)
by SCMFSA8A:13;
A27: Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 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)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))
by X
.=
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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))) + 1) + 1))
by XX
;
hence
IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = 0
by A24, SCMFSA_2:95; DataPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))
X:
s +* (Initialized I) = (Initialized s) +* (I +* (Start-At (0,SCM+FSA)))
by SCMFSA8A:13;
XX:
(Initialized s) +* (I +* (Start-At (0,SCM+FSA))) = s +* (Initialized I)
by SCMFSA8A:13;
for c being Int-Location holds (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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))) + 1) + 1))) . c = (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 + (LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))) + 1))) . c
by A24, SCMFSA_2:95;
hence DataPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) =
DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart ((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))),((Initialized s) +* (I +* (Start-At (0,SCM+FSA))))))))
by A20, A27, X, A26, A25, SCMFSA6A:38
.=
DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))
by XX
;
verum