let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for s being State of S
for iloc, a being Instruction-Location of S holds s . a = (s +* (Start-At iloc)) . a
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for s being State of S
for iloc, a being Instruction-Location of S holds s . a = (s +* (Start-At iloc)) . a
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N; :: thesis: for s being State of S
for iloc, a being Instruction-Location of S holds s . a = (s +* (Start-At iloc)) . a
let s be State of S; :: thesis: for iloc, a being Instruction-Location of S holds s . a = (s +* (Start-At iloc)) . a
let iloc, a be Instruction-Location of S; :: thesis: s . a = (s +* (Start-At iloc)) . a
A1: dom (Start-At iloc) = {(IC S)} by FUNCOP_1:19;
a in the carrier of S ;
then a in dom s by Th79;
then A2: a in (dom s) \/ (dom (Start-At iloc)) by XBOOLE_0:def 3;
a <> IC S by Th48;
then not a in {(IC S)} by TARSKI:def 1;
hence s . a = (s +* (Start-At iloc)) . a by A1, A2, FUNCT_4:def 1; :: thesis: verum