let p be Instruction-Sequence of SCM+FSA; :: thesis: for I being InitHalting keepInt0_1 Program of SCM+FSA

for s being State of SCM+FSA holds DataPart (Initialized (IExec (I,p,s))) = DataPart (IExec (I,p,s))

set IF = Data-Locations ;

let I be InitHalting keepInt0_1 Program of SCM+FSA; :: thesis: for s being State of SCM+FSA holds DataPart (Initialized (IExec (I,p,s))) = DataPart (IExec (I,p,s))

let s be State of SCM+FSA; :: thesis: DataPart (Initialized (IExec (I,p,s))) = DataPart (IExec (I,p,s))

set IE = IExec (I,p,s);

for s being State of SCM+FSA holds DataPart (Initialized (IExec (I,p,s))) = DataPart (IExec (I,p,s))

set IF = Data-Locations ;

let I be InitHalting keepInt0_1 Program of SCM+FSA; :: thesis: for s being State of SCM+FSA holds DataPart (Initialized (IExec (I,p,s))) = DataPart (IExec (I,p,s))

let s be State of SCM+FSA; :: thesis: DataPart (Initialized (IExec (I,p,s))) = DataPart (IExec (I,p,s))

set IE = IExec (I,p,s);

now :: thesis: ( dom (DataPart (Initialized (IExec (I,p,s)))) = (dom (IExec (I,p,s))) /\ (Data-Locations ) & ( for x being object st x in dom (DataPart (Initialized (IExec (I,p,s)))) holds

(DataPart (Initialized (IExec (I,p,s)))) . x = (IExec (I,p,s)) . x ) )

hence
DataPart (Initialized (IExec (I,p,s))) = DataPart (IExec (I,p,s))
by FUNCT_1:46; :: thesis: verum(DataPart (Initialized (IExec (I,p,s)))) . x = (IExec (I,p,s)) . x ) )

A1:
dom (Initialized (IExec (I,p,s))) = the carrier of SCM+FSA
by PARTFUN1:def 2;

A2: dom (Initialized (IExec (I,p,s))) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;

A3: dom (IExec (I,p,s)) = the carrier of SCM+FSA by PARTFUN1:def 2;

hence dom (DataPart (Initialized (IExec (I,p,s)))) = (dom (IExec (I,p,s))) /\ (Data-Locations ) by A1, RELAT_1:61; :: thesis: for x being object st x in dom (DataPart (Initialized (IExec (I,p,s)))) holds

(DataPart (Initialized (IExec (I,p,s)))) . b_{2} = (IExec (I,p,s)) . b_{2}

then A4: dom (DataPart (Initialized (IExec (I,p,s)))) = Data-Locations by A1, A3, A2, XBOOLE_1:21;

let x be object ; :: thesis: ( x in dom (DataPart (Initialized (IExec (I,p,s)))) implies (DataPart (Initialized (IExec (I,p,s)))) . b_{1} = (IExec (I,p,s)) . b_{1} )

assume A5: x in dom (DataPart (Initialized (IExec (I,p,s)))) ; :: thesis: (DataPart (Initialized (IExec (I,p,s)))) . b_{1} = (IExec (I,p,s)) . b_{1}

end;A2: dom (Initialized (IExec (I,p,s))) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;

A3: dom (IExec (I,p,s)) = the carrier of SCM+FSA by PARTFUN1:def 2;

hence dom (DataPart (Initialized (IExec (I,p,s)))) = (dom (IExec (I,p,s))) /\ (Data-Locations ) by A1, RELAT_1:61; :: thesis: for x being object st x in dom (DataPart (Initialized (IExec (I,p,s)))) holds

(DataPart (Initialized (IExec (I,p,s)))) . b

then A4: dom (DataPart (Initialized (IExec (I,p,s)))) = Data-Locations by A1, A3, A2, XBOOLE_1:21;

let x be object ; :: thesis: ( x in dom (DataPart (Initialized (IExec (I,p,s)))) implies (DataPart (Initialized (IExec (I,p,s)))) . b

assume A5: x in dom (DataPart (Initialized (IExec (I,p,s)))) ; :: thesis: (DataPart (Initialized (IExec (I,p,s)))) . b

per cases
( x in Int-Locations or x in FinSeq-Locations )
by A5, A4, SCMFSA_2:100, XBOOLE_0:def 3;

end;

suppose
x in Int-Locations
; :: thesis: (DataPart (Initialized (IExec (I,p,s)))) . b_{1} = (IExec (I,p,s)) . b_{1}

then reconsider x9 = x as Int-Location by AMI_2:def 16;

end;hereby :: thesis: verum
end;

per cases
( x9 is read-write or x9 is read-only )
;

end;

suppose A6:
x9 is read-write
; :: thesis: (DataPart (Initialized (IExec (I,p,s)))) . x = (IExec (I,p,s)) . x

thus (DataPart (Initialized (IExec (I,p,s)))) . x =
(Initialized (IExec (I,p,s))) . x
by A5, A4, FUNCT_1:49

.= (IExec (I,p,s)) . x by A6, SCMFSA_M:37 ; :: thesis: verum

end;.= (IExec (I,p,s)) . x by A6, SCMFSA_M:37 ; :: thesis: verum

suppose
x9 is read-only
; :: thesis: (DataPart (Initialized (IExec (I,p,s)))) . x = (IExec (I,p,s)) . x

then A7:
x9 = intloc 0
;

thus (DataPart (Initialized (IExec (I,p,s)))) . x = (Initialized (IExec (I,p,s))) . x9 by A5, A4, FUNCT_1:49

.= 1 by A7, SCMFSA_M:9

.= (IExec (I,p,s)) . x by A7, Th7 ; :: thesis: verum

end;thus (DataPart (Initialized (IExec (I,p,s)))) . x = (Initialized (IExec (I,p,s))) . x9 by A5, A4, FUNCT_1:49

.= 1 by A7, SCMFSA_M:9

.= (IExec (I,p,s)) . x by A7, Th7 ; :: thesis: verum

suppose
x in FinSeq-Locations
; :: thesis: (DataPart (Initialized (IExec (I,p,s)))) . b_{1} = (IExec (I,p,s)) . b_{1}

then reconsider x9 = x as FinSeq-Location by SCMFSA_2:def 5;

thus (DataPart (Initialized (IExec (I,p,s)))) . x = (Initialized (IExec (I,p,s))) . x9 by A5, A4, FUNCT_1:49

.= (IExec (I,p,s)) . x by SCMFSA_M:37 ; :: thesis: verum

end;thus (DataPart (Initialized (IExec (I,p,s)))) . x = (Initialized (IExec (I,p,s))) . x9 by A5, A4, FUNCT_1:49

.= (IExec (I,p,s)) . x by SCMFSA_M:37 ; :: thesis: verum