let p be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for Ig being good really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) holds
DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s))
let s be State of SCM+FSA; for Ig being good really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) holds
DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s))
let Ig be good really-closed Program of SCM+FSA; ( ( Ig is parahalting or Ig is_halting_on Initialized s,p ) implies DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s)) )
set I = Ig;
set IE = IExec (Ig,p,s);
assume A1:
( Ig is parahalting or Ig is_halting_on Initialized s,p )
; DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s))
A2:
Ig is_halting_on Initialized s,p
by A1, SCMFSA7B:19;
now ( dom (DataPart (Initialized (IExec (Ig,p,s)))) = (dom (IExec (Ig,p,s))) /\ (Data-Locations ) & ( for x being object st x in dom (DataPart (Initialized (IExec (Ig,p,s)))) holds
(DataPart (Initialized (IExec (Ig,p,s)))) . x = (IExec (Ig,p,s)) . x ) )A3:
dom (Initialized (IExec (Ig,p,s))) = the
carrier of
SCM+FSA
by PARTFUN1:def 2;
A4:
dom (Initialized (IExec (Ig,p,s))) =
(Data-Locations ) \/ {(IC )}
by MEMSTR_0:13
.=
(Data-Locations ) \/ {(IC )}
;
A5:
dom (IExec (Ig,p,s)) = the
carrier of
SCM+FSA
by PARTFUN1:def 2;
hence
dom (DataPart (Initialized (IExec (Ig,p,s)))) = (dom (IExec (Ig,p,s))) /\ (Data-Locations )
by A3, RELAT_1:61;
for x being object st x in dom (DataPart (Initialized (IExec (Ig,p,s)))) holds
(DataPart (Initialized (IExec (Ig,p,s)))) . b2 = (IExec (Ig,p,s)) . b2then A6:
dom (DataPart (Initialized (IExec (Ig,p,s)))) = Data-Locations
by A3, A5, A4, XBOOLE_1:21;
let x be
object ;
( x in dom (DataPart (Initialized (IExec (Ig,p,s)))) implies (DataPart (Initialized (IExec (Ig,p,s)))) . b1 = (IExec (Ig,p,s)) . b1 )assume A7:
x in dom (DataPart (Initialized (IExec (Ig,p,s))))
;
(DataPart (Initialized (IExec (Ig,p,s)))) . b1 = (IExec (Ig,p,s)) . b1per cases
( x in Int-Locations or x in FinSeq-Locations )
by A7, A6, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
(DataPart (Initialized (IExec (Ig,p,s)))) . b1 = (IExec (Ig,p,s)) . b1then reconsider x9 =
x as
Int-Location by AMI_2:def 16;
hereby verum
per cases
( x9 is read-write or x9 is read-only )
;
suppose
x9 is
read-only
;
(DataPart (Initialized (IExec (Ig,p,s)))) . x = (IExec (Ig,p,s)) . xthen A9:
x9 = intloc 0
;
thus (DataPart (Initialized (IExec (Ig,p,s)))) . x =
(Initialized (IExec (Ig,p,s))) . x9
by A7, A6, FUNCT_1:49
.=
1
by A9, SCMFSA_M:9
.=
(IExec (Ig,p,s)) . x
by A2, A9, SCMFSA8C:67
;
verum end; end;
end; end; end; end;
hence
DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s))
by FUNCT_1:46; verum