let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for I being Program of SCM+FSA st s . (intloc 0) = 1 & s . a <= 0 holds
DataPart (IExec ((while>0 (a,I)),s)) = DataPart s
let a be read-write Int-Location ; :: thesis: for I being Program of SCM+FSA st s . (intloc 0) = 1 & s . a <= 0 holds
DataPart (IExec ((while>0 (a,I)),s)) = DataPart s
let I be Program of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 & s . a <= 0 implies DataPart (IExec ((while>0 (a,I)),s)) = DataPart s )
set Ins = NAT ;
assume that
A1: s . (intloc 0) = 1 and
A2: s . a <= 0 ; :: thesis: DataPart (IExec ((while>0 (a,I)),s)) = DataPart s
set WH = while>0 (a,I);
set Is = Initialized s;
set Ids = s +* (Initialized (while>0 (a,I)));
A3: s +* (Initialized (while>0 (a,I))) = (Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by SCMFSA8A:13;
then A4: (while>0 (a,I)) +* (Start-At (0,SCM+FSA)) c= s +* (Initialized (while>0 (a,I))) by FUNCT_4:26;
(Initialized s) . a = s . a by SCMFSA6C:3;
then while>0 (a,I) is_halting_on Initialized s by A2, SCMFSA_9:43;
then A5: ProgramPart (s +* (Initialized (while>0 (a,I)))) halts_on s +* (Initialized (while>0 (a,I))) by A3, SCMFSA7B:def 8;
DataPart (Initialized s) = DataPart (s +* (Initialized (while>0 (a,I)))) by SCMFSA8B:5;
then A6: (s +* (Initialized (while>0 (a,I)))) . a = (Initialized s) . a by SCMFSA6A:38
.= s . a by SCMFSA6C:3 ;
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A7: dom (ProgramPart s) misses Int-Locations \/ FinSeq-Locations by COMPOS_1:34;
thus DataPart (IExec ((while>0 (a,I)),s)) = DataPart ((Result ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))))) +* (s | NAT)) by SCMFSA6B:def 1
.= DataPart (Result ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))))) by A7, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),(LifeSpan ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))))))) by A5, EXTPRO_1:23
.= DataPart (s +* (Initialized (while>0 (a,I)))) by A2, A6, A4, Th35
.= DataPart (Initialized s) by SCMFSA8B:5
.= DataPart s by A1, SCMFSA8C:27 ; :: thesis: verum