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