let x be set ; :: thesis: for s being State of SCMPDS
for l being Instruction-Location of SCMPDS
for I being Program of SCMPDS st x in dom I holds
I . x = (s +* (I +* (Start-At l))) . x
let s be State of SCMPDS ; :: thesis: for l being Instruction-Location of SCMPDS
for I being Program of SCMPDS st x in dom I holds
I . x = (s +* (I +* (Start-At l))) . x
let l be Instruction-Location of SCMPDS ; :: thesis: for I being Program of SCMPDS st x in dom I holds
I . x = (s +* (I +* (Start-At l))) . x
let I be Program of SCMPDS ; :: thesis: ( x in dom I implies I . x = (s +* (I +* (Start-At l))) . x )
assume A1: x in dom I ; :: thesis: I . x = (s +* (I +* (Start-At l))) . x
dom I c= NAT by RELAT_1:def 18;
then reconsider y = x as Instruction-Location of SCMPDS by A1, AMI_1:def 4;
A2: not y in dom (Start-At l) by AMI_1:137;
x in dom (I +* (Start-At l)) by A1, FUNCT_4:13;
hence (s +* (I +* (Start-At l))) . x = (I +* (Start-At l)) . x by FUNCT_4:14
.= I . x by A2, FUNCT_4:12 ;
:: thesis: verum