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