let R be good Ring; :: thesis: for i1 being Element of NAT
for k being natural number holds IncAddr (goto i1,R),k = goto (il. (SCM R),((locnum i1,(SCM R)) + k)),R
let i1 be Element of NAT ; :: thesis: for k being natural number holds IncAddr (goto i1,R),k = goto (il. (SCM R),((locnum i1,(SCM R)) + k)),R
let k be natural number ; :: thesis: IncAddr (goto i1,R),k = goto (il. (SCM R),((locnum i1,(SCM R)) + k)),R
A1: dom (AddressPart (IncAddr (goto i1,R),k)) = dom (AddressPart (goto i1,R)) by AMISTD_2:def 14;
A2: dom (AddressPart (goto (il. (SCM R),((locnum i1,(SCM R)) + k)),R)) = dom <*(il. (SCM R),((locnum i1,(SCM R)) + k))*> by MCART_1:def 2
.= Seg 1 by FINSEQ_1:def 8
.= dom <*i1*> by FINSEQ_1:def 8
.= dom (AddressPart (goto i1,R)) by MCART_1:def 2 ;
A3: for x being set st x in dom (AddressPart (goto i1,R)) holds
(AddressPart (IncAddr (goto i1,R),k)) . x = (AddressPart (goto (il. (SCM R),((locnum i1,(SCM R)) + k)),R)) . x

proof

let x be set ; :: thesis: ( x in dom (AddressPart (goto i1,R)) implies (AddressPart (IncAddr (goto i1,R),k)) . x = (AddressPart (goto (il. (SCM R),((locnum i1,(SCM R)) + k)),R)) . x )
assume A4: x in dom (AddressPart (goto i1,R)) ; :: thesis: (AddressPart (IncAddr (goto i1,R),k)) . x = (AddressPart (goto (il. (SCM R),((locnum i1,(SCM R)) + k)),R)) . x
then x in dom <*i1*> by MCART_1:def 2;
then A5: x = 1 by Lm1;
then (product" (AddressParts (InsCode (goto i1,R)))) . x = NAT by Th50;
then consider f being Element of NAT such that
A6: f = (AddressPart (goto i1,R)) . x and
A7: (AddressPart (IncAddr (goto i1,R),k)) . x = il. (SCM R),(k + (locnum f,(SCM R))) by A4, AMISTD_2:def 14;
f = <*i1*> . x by A6, MCART_1:def 2
.= i1 by A5, FINSEQ_1:def 8 ;
hence (AddressPart (IncAddr (goto i1,R),k)) . x = <*(il. (SCM R),((locnum i1,(SCM R)) + k))*> . x by A5, A7, FINSEQ_1:def 8
.= (AddressPart (goto (il. (SCM R),((locnum i1,(SCM R)) + k)),R)) . x by MCART_1:def 2 ;
:: thesis: verum

end;

InsCode (IncAddr (goto i1,R),k) = InsCode (goto i1,R) by AMISTD_2:def 14
.= 6 by MCART_1:def 1
.= InsCode (goto (il. (SCM R),((locnum i1,(SCM R)) + k)),R) by MCART_1:def 1 ;
hence IncAddr (goto i1,R),k = goto (il. (SCM R),((locnum i1,(SCM R)) + k)),R by A1, A2, A3, FUNCT_1:9, MCART_1:95; :: thesis: verum