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