let s be State of ; for I being Program of
for a being read-write Int-Location st I is_closed_onInit s & I is_halting_onInit s & s . a > 0 holds
( IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0 & DataPart (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) )
let I be Program of ; for a being read-write Int-Location st I is_closed_onInit s & I is_halting_onInit s & s . a > 0 holds
( IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0 & DataPart (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = DataPart (Computation (s +* (Initialized I)),(LifeSpan (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 (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0 & DataPart (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) ) )
set D = Int-Locations \/ FinSeq-Locations ;
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 )));
defpred S1[ 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) ) );
set loc4 = insloc ((card I) + 4);
set s3 = Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1);
A1:
insloc ((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 (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0 & DataPart (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) ) )
then A3:
I is_closed_on Initialize s
by SCMFSA7B:def 7;
assume
I is_halting_onInit s
; ( not s . a > 0 or ( IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0 & DataPart (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) ) )
then X:
ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I)
by SCM_HALT:def 5;
s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 )))
by SCMFSA8A:13;
then
ProgramPart ((Initialize s) +* (I +* (Start-At (insloc 0 )))) halts_on (Initialize s) +* (I +* (Start-At (insloc 0 )))
by SCMFSA8A:13, X;
then A4:
I is_halting_on Initialize s
by 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 ((Initialize s) +* (I +* (Start-At (insloc 0 ))))
;
( 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)) )then
k < LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 ))))
by A7, 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 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 (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;
A9:
insloc 0 in dom (while>0 a,I)
by SCMFSA_9:10;
then A10: ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (insloc 0 ) =
((while>0 a,I) +* (Start-At (insloc 0 ))) . (insloc 0 )
by A8, FUNCT_4:14
.=
(while>0 a,I) . (insloc 0 )
by A9, SCMFSA6B:7
.=
a >0_goto (insloc 4)
by SCMFSA_9:11
;
IC SCM+FSA in dom ((while>0 a,I) +* (Start-At (insloc 0 )))
by SF_MASTR:65;
then A11: 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
;
A12: 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 A11, A10
;
then A13:
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 SCMFSA_2:97;
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
by A12, SCMFSA_2:97;
then A14: 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 A13, SCMFSA6A:38
.=
DataPart (Initialize s)
by SCMFSA8A:11
.=
DataPart ((Initialize s) +* (I +* (Start-At (insloc 0 ))))
by SCMFSA8A:11
;
set s4 = Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1) + 1);
set s2 = Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 ))))));
A15:
(((LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 ))))) + 1) + 1) + 1 = (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 ))))) + (2 + 1)
;
not a in dom ((while>0 a,I) +* (Start-At (insloc 0 )))
by SCMFSA6B:12;
then A16:
((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . a = (Initialize s) . a
by FUNCT_4:12;
assume
s . a > 0
; ( IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0 & DataPart (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) )
then A17:
(Initialize s) . a > 0
by SCMFSA6C:3;
A18:
S1[ 0 ]
proof
assume
0 <= LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 ))))
;
( 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 ) )
A19:
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 A19, 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 A17, A12, A16, A14, AMI_1:13, 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 ((Initialize s) +* (I +* (Start-At (insloc 0 ))))]
;
A21: Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1) =
Following (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))))
by AMI_1:14
.=
Exec (goto (insloc ((card I) + 4))),(Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))))
by A3, A4, A20, SCMFSA_9:45
;
then A22:
for f being FinSeq-Location holds (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1)) . f = (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 ))))))) . f
by SCMFSA_2:95;
A23: (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1)) . (insloc ((card I) + 4)) =
((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (insloc ((card I) + 4))
by AMI_1:54
.=
((while>0 a,I) +* (Start-At (insloc 0 ))) . (insloc ((card I) + 4))
by A8, A1, FUNCT_4:14
.=
(while>0 a,I) . (insloc ((card I) + 4))
by A1, SCMFSA6B:7
.=
goto (insloc 0 )
by SCMFSA_9:46
;
A24: Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1) + 1) =
Following (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1))
by AMI_1:14
.=
Exec (goto (insloc 0 )),(Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1))
by A21, A23, SCMFSA_2:95
;
then A25:
for f being FinSeq-Location holds (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1) + 1)) . f = (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1)) . f
by SCMFSA_2:95;
for c being Int-Location holds (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1)) . c = (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 ))))))) . c
by A21, SCMFSA_2:95;
then A26:
DataPart (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1)) = DataPart (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))))
by A22, SCMFSA6A:38;
A27: Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3) =
Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (Initialized I))) + 3)
by SCMFSA8A:13
.=
Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1) + 1)
by A15, SCMFSA8A:13
;
hence
IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0
by A24, SCMFSA_2:95; DataPart (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))
for c being Int-Location holds (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1) + 1)) . c = (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1)) . c
by A24, SCMFSA_2:95;
then
DataPart (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(((1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) + 1) + 1)) = DataPart (Computation ((Initialize s) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))))
by A26, A25, SCMFSA6A:38;
hence DataPart (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) =
DataPart (Computation (s +* (Initialized I)),(LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 ))))))
by A20, A27, SCMFSA8A:13
.=
DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))
by SCMFSA8A:13
;
verum