set D = Int-Locations \/ FinSeq-Locations ;
let s be State of SCM+FSA ; :: thesis: for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st s . a > 0 & while>0 a,I is InitHalting holds
DataPart (IExec (while>0 a,I),s) = DataPart (IExec (while>0 a,I),(IExec I,s))
let I be good InitHalting Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st s . a > 0 & while>0 a,I is InitHalting holds
DataPart (IExec (while>0 a,I),s) = DataPart (IExec (while>0 a,I),(IExec I,s))
let a be read-write Int-Location ; :: thesis: ( s . a > 0 & while>0 a,I is InitHalting implies DataPart (IExec (while>0 a,I),s) = DataPart (IExec (while>0 a,I),(IExec I,s)) )
assume A1:
( s . a > 0 & while>0 a,I is InitHalting )
; :: thesis: DataPart (IExec (while>0 a,I),s) = DataPart (IExec (while>0 a,I),(IExec I,s))
set ps = s | NAT ;
set sI = s +* (Initialized I);
set Iwhile = Initialized (while>0 a,I);
set sW = s +* (Initialized (while>0 a,I));
set s3 = (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I));
set m1 = LifeSpan (s +* (Initialized I));
set m3 = LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)));
set A = NAT ;
Initialized I c= s +* (Initialized I)
by FUNCT_4:26;
then A2:
s +* (Initialized I) is halting
by AMI_1:def 26;
A3:
Initialized (while>0 a,I) c= s +* (Initialized (while>0 a,I))
by FUNCT_4:26;
A4:
Initialized (while>0 a,I) is halting
by A1;
then A5:
s +* (Initialized (while>0 a,I)) is halting
by A3, AMI_1:def 26;
A6:
Initialized (while>0 a,I) c= (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))
by FUNCT_4:26;
then A7:
(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)) is halting
by A4, AMI_1:def 26;
A8: dom (s | NAT ) =
(dom s) /\ NAT
by RELAT_1:90
.=
(((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) /\ NAT
by SCMFSA6A:34
.=
NAT
by XBOOLE_1:21
;
(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)),((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (s | NAT )) +* (Initialized (while>0 a,I)) equal_outside dom (s | NAT )
by FUNCT_7:31, FUNCT_7:106;
then A9:
((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (s | NAT )) +* (Initialized (while>0 a,I)),(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)) equal_outside dom (s | NAT )
by FUNCT_7:28;
Result ((IExec I,s) +* (Initialized (while>0 a,I))), Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))) equal_outside NAT
proof
A10:
Initialized (while>0 a,I) c= (IExec I,s) +* (Initialized (while>0 a,I))
by FUNCT_4:26;
IExec I,
s =
(Result (s +* (Initialized I))) +* (s | NAT )
by SCMFSA6B:def 1
.=
(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (s | NAT )
by A2, AMI_1:122
;
hence
Result ((IExec I,s) +* (Initialized (while>0 a,I))),
Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))) equal_outside NAT
by A1, A6, A8, A9, A10, Th12;
:: thesis: verum
end;
then A11:
(Result ((IExec I,s) +* (Initialized (while>0 a,I)))) +* (s | NAT ) = (Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))) +* (s | NAT )
by A8, FUNCT_7:108;
set mW = LifeSpan (s +* (Initialized (while>0 a,I)));
A12:
LifeSpan (s +* (Initialized (while>0 a,I))) <= (((LifeSpan (s +* (Initialized I))) + 3) + (LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))))) + (LifeSpan (s +* (Initialized (while>0 a,I))))
by NAT_1:11;
A13: IExec (while>0 a,I),s =
(Result (s +* (Initialized (while>0 a,I)))) +* (s | NAT )
by SCMFSA6B:def 1
.=
(Computation (s +* (Initialized (while>0 a,I))),(LifeSpan (s +* (Initialized (while>0 a,I))))) +* (s | NAT )
by A5, AMI_1:122
.=
(Computation (s +* (Initialized (while>0 a,I))),(((LifeSpan (s +* (Initialized I))) + 3) + ((LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))) + (LifeSpan (s +* (Initialized (while>0 a,I))))))) +* (s | NAT )
by A5, A12, AMI_1:128
;
(IExec I,s) | NAT =
((Result (s +* (Initialized I))) +* (s | NAT )) | NAT
by SCMFSA6B:def 1
.=
s | NAT
by CARD_3:99
;
then A14: IExec (while>0 a,I),(IExec I,s) =
(Result ((IExec I,s) +* (Initialized (while>0 a,I)))) +* (s | NAT )
by SCMFSA6B:def 1
.=
(Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))))) +* (s | NAT )
by A7, A11, AMI_1:122
;
A15:
DataPart (Computation (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)),((LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))) + (LifeSpan (s +* (Initialized (while>0 a,I)))))) = DataPart (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))))
proof
set Cm3 =
Computation (s +* (Initialized (while>0 a,I))),
((LifeSpan (s +* (Initialized I))) + 3);
A16:
I is_closed_onInit s
by SCM_HALT:35;
A17:
I is_halting_onInit s
by SCM_HALT:36;
then A18:
IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0
by A1, A16, Th21;
then A19:
IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = IC ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))
by FUNCT_4:26, SCMFSA6B:34;
A20:
DataPart (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) =
DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))
by A1, A16, A17, Th21
.=
DataPart ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (while>0 a,I))
by SCMFSA8C:34
;
reconsider Wg =
while>0 a,
I as
good InitHalting Program of
SCM+FSA by A1;
Wg is
keepInt0_1
;
then A21:
(Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) . (intloc 0 ) = 1
by A3, SCM_HALT:def 3;
while>0 a,
I c= Initialized (while>0 a,I)
by SCMFSA6A:26;
then
while>0 a,
I c= s +* (Initialized (while>0 a,I))
by A3, XBOOLE_1:1;
then
while>0 a,
I c= Computation (s +* (Initialized (while>0 a,I))),
((LifeSpan (s +* (Initialized I))) + 3)
by AMI_1:81;
then
(Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) +* (while>0 a,I) = Computation (s +* (Initialized (while>0 a,I))),
((LifeSpan (s +* (Initialized I))) + 3)
by FUNCT_4:79;
then
(Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) +* (Initialized (while>0 a,I)) = Computation (s +* (Initialized (while>0 a,I))),
((LifeSpan (s +* (Initialized I))) + 3)
by A18, A21, Th6;
then A22:
Initialized (while>0 a,I) c= Computation (s +* (Initialized (while>0 a,I))),
((LifeSpan (s +* (Initialized I))) + 3)
by FUNCT_4:26;
A23:
now let f be
FinSeq-Location ;
:: thesis: ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))) . f = (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) . fA24:
not
f in dom (Initialized (while>0 a,I))
by SCMFSA6A:49;
A25:
not
f in dom (while>0 a,I)
by Th13;
thus ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))) . f =
(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) . f
by A24, FUNCT_4:12
.=
((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (while>0 a,I)) . f
by A25, FUNCT_4:12
.=
(Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) . f
by A20, SCMFSA6A:38
;
:: thesis: verum end;
now let b be
Int-Location ;
:: thesis: ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))) . b1 = (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) . b1per cases
( b <> intloc 0 or b = intloc 0 )
;
suppose
b <> intloc 0
;
:: thesis: ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))) . b1 = (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) . b1then A26:
not
b in dom (Initialized (while>0 a,I))
by SCMFSA6A:48;
A27:
not
b in dom (while>0 a,I)
by Th14;
thus ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))) . b =
(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) . b
by A26, FUNCT_4:12
.=
((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (while>0 a,I)) . b
by A27, FUNCT_4:12
.=
(Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) . b
by A20, SCMFSA6A:38
;
:: thesis: verum end; end;
then A28:
Computation (s +* (Initialized (while>0 a,I))),
((LifeSpan (s +* (Initialized I))) + 3),
(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)) equal_outside NAT
by A19, A23, SCMFSA6A:28;
then A29:
LifeSpan (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))
by A1, A6, A22, Th12;
A31:
Computation (s +* (Initialized (while>0 a,I))),
((LifeSpan (s +* (Initialized I))) + 3) is
halting
by A4, A22, AMI_1:def 26;
hence DataPart (Computation (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)),((LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))) + (LifeSpan (s +* (Initialized (while>0 a,I)))))) =
DataPart (Computation (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)),(LifeSpan (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3))))
by A29, AMI_1:128, NAT_1:11
.=
DataPart (Result (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)))
by A31, AMI_1:122
.=
DataPart (Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))))
by A1, A6, A22, A28, Th12, SCMFSA6A:39
.=
DataPart (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))))
by A7, AMI_1:122
;
:: thesis: verum
end;
thus
DataPart (IExec (while>0 a,I),s) = DataPart (IExec (while>0 a,I),(IExec I,s))
:: thesis: verumproof
A32:
dom (s | NAT ) misses Int-Locations \/ FinSeq-Locations
by A8, SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
hence DataPart (IExec (while>0 a,I),s) =
DataPart (Computation (s +* (Initialized (while>0 a,I))),(((LifeSpan (s +* (Initialized I))) + 3) + ((LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))) + (LifeSpan (s +* (Initialized (while>0 a,I)))))))
by A13, FUNCT_4:76, SCMFSA_2:127
.=
DataPart (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))))
by A15, AMI_1:51
.=
DataPart (IExec (while>0 a,I),(IExec I,s))
by A14, A32, FUNCT_4:76, SCMFSA_2:127
;
:: thesis: verum
end;