let s be State of SCM ; :: thesis: for iloc being Instruction-Location of SCM
for a being Data-Location holds s . a = (s +* (Start-At iloc)) . a
let iloc be Instruction-Location of SCM ; :: thesis: for a being Data-Location holds s . a = (s +* (Start-At iloc)) . a
let a be Data-Location ; :: thesis: s . a = (s +* (Start-At iloc)) . a
A1: dom (Start-At iloc) = {(IC SCM )} by FUNCOP_1:19;
a in the carrier of SCM ;
then a in dom s by AMI_1:79;
then A2: a in (dom s) \/ (dom (Start-At iloc)) by XBOOLE_0:def 3;
a <> IC SCM by Th20;
then not a in {(IC SCM )} by TARSKI:def 1;
hence s . a = (s +* (Start-At iloc)) . a by A1, A2, FUNCT_4:def 1; :: thesis: verum