let s be State of SCMPDS ; :: thesis: for I, J being Program of SCMPDS
for l being Instruction-Location of SCMPDS holds s +* (I +* (Start-At l)),s +* (J +* (Start-At l)) equal_outside NAT
let I, J be Program of SCMPDS ; :: thesis: for l being Instruction-Location of SCMPDS holds s +* (I +* (Start-At l)),s +* (J +* (Start-At l)) equal_outside NAT
let l be Instruction-Location of SCMPDS ; :: thesis: s +* (I +* (Start-At l)),s +* (J +* (Start-At l)) equal_outside NAT
A1: IC (s +* (J +* (Start-At l))) = IC ((s +* J) +* (Start-At l)) by FUNCT_4:15
.= l by AMI_1:111
.= IC ((s +* I) +* (Start-At l)) by AMI_1:111
.= IC (s +* (I +* (Start-At l))) by FUNCT_4:15 ;

now

let a be Int_position ; :: thesis: (s +* (J +* (Start-At l))) . a = (s +* (I +* (Start-At l))) . a
A2: ( a in dom s & not a in dom (I +* (Start-At l)) & not a in dom (J +* (Start-At l)) ) by SCMPDS_2:49, SCMPDS_4:61;
hence (s +* (J +* (Start-At l))) . a = s . a by FUNCT_4:12
.= (s +* (I +* (Start-At l))) . a by A2, FUNCT_4:12 ;
:: thesis: verum

end;

hence s +* (I +* (Start-At l)),s +* (J +* (Start-At l)) equal_outside NAT by A1, SCMPDS_4:11; :: thesis: verum