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 )
assume that
A1: s . (intloc 0 ) = 1 and
A2: s . a <> 0 ; :: thesis: DataPart (IExec (while=0 a,I),s) = DataPart s
set Is = Initialize s;
set WH = while=0 a,I;
set Ins = NAT ;
set Ids = s +* (Initialized (while=0 a,I));
DataPart (Initialize s) = DataPart (s +* (Initialized (while=0 a,I))) by SCMFSA8B:5;
then A3: (s +* (Initialized (while=0 a,I))) . a = (Initialize s) . a by SCMFSA6A:38
.= s . a by SCMFSA6C:3 ;
A4: s +* (Initialized (while=0 a,I)) = (Initialize s) +* ((while=0 a,I) +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
then A5: (while=0 a,I) +* (Start-At (insloc 0 )) c= s +* (Initialized (while=0 a,I)) by FUNCT_4:26;
(Initialize s) . a = s . a by SCMFSA6C:3;
then while=0 a,I is_halting_on Initialize s by A2, SCMFSA_9:18;
then A6: s +* (Initialized (while=0 a,I)) is halting by A4, SCMFSA7B:def 8;
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A7: dom (s | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA8A:3;
thus DataPart (IExec (while=0 a,I),s) = DataPart ((Result (s +* (Initialized (while=0 a,I)))) +* (s | NAT )) by SCMFSA6B:def 1
.= DataPart (Result (s +* (Initialized (while=0 a,I)))) by A7, FUNCT_4:94, SCMFSA_2:127
.= DataPart (Computation (s +* (Initialized (while=0 a,I))),(LifeSpan (s +* (Initialized (while=0 a,I))))) by A6, AMI_1:122
.= DataPart (s +* (Initialized (while=0 a,I))) by A2, A3, A5, Th22
.= DataPart (Initialize s) by SCMFSA8B:5
.= DataPart s by A1, SCMFSA8C:27 ; :: thesis: verum