let n be Element of NAT ; :: thesis: for loc being Instruction-Location of SCMPDS
for I being Program of SCMPDS st loc in dom I holds
(Shift (stop I),n) . (loc + n) = (Shift I,n) . (loc + n)
let loc be Instruction-Location of SCMPDS ; :: thesis: for I being Program of SCMPDS st loc in dom I holds
(Shift (stop I),n) . (loc + n) = (Shift I,n) . (loc + n)
let I be Program of SCMPDS ; :: thesis: ( loc in dom I implies (Shift (stop I),n) . (loc + n) = (Shift I,n) . (loc + n) )
assume A1: loc in dom I ; :: thesis: (Shift (stop I),n) . (loc + n) = (Shift I,n) . (loc + n)
A2: dom I c= dom (stop I) by SCMPDS_4:39;
reconsider l = loc as Element of NAT by ORDINAL1:def 13;
thus (Shift I,n) . (loc + n) = I . l by A1, VALUED_1:def 12
.= (stop I) . l by A1, SCMPDS_4:37
.= (Shift (stop I),n) . (loc + n) by A1, A2, VALUED_1:def 12 ; :: thesis: verum