let R be good Ring; :: thesis: for a being Data-Location of R
for i1 being Element of NAT
for k being natural number holds IncAddr (a =0_goto i1),k = a =0_goto (il. (SCM R),((locnum i1,(SCM R)) + k))
let a be Data-Location of R; :: thesis: for i1 being Element of NAT
for k being natural number holds IncAddr (a =0_goto i1),k = a =0_goto (il. (SCM R),((locnum i1,(SCM R)) + k))
let i1 be Element of NAT ; :: thesis: for k being natural number holds IncAddr (a =0_goto i1),k = a =0_goto (il. (SCM R),((locnum i1,(SCM R)) + k))
let k be natural number ; :: thesis: IncAddr (a =0_goto i1),k = a =0_goto (il. (SCM R),((locnum i1,(SCM R)) + k))
A1: dom (AddressPart (IncAddr (a =0_goto i1),k)) = dom (AddressPart (a =0_goto i1)) by AMISTD_2:def 14;
A2: dom (AddressPart (a =0_goto (il. (SCM R),((locnum i1,(SCM R)) + k)))) = dom <*(il. (SCM R),((locnum i1,(SCM R)) + k)),a*> by MCART_1:def 2
.= Seg 2 by FINSEQ_3:29
.= dom <*i1,a*> by FINSEQ_3:29
.= dom (AddressPart (a =0_goto i1)) by MCART_1:def 2 ;
A3: for x being set st x in dom (AddressPart (a =0_goto i1)) holds
(AddressPart (IncAddr (a =0_goto i1),k)) . x = (AddressPart (a =0_goto (il. (SCM R),((locnum i1,(SCM R)) + k)))) . x

proof

let x be set ; :: thesis: ( x in dom (AddressPart (a =0_goto i1)) implies (AddressPart (IncAddr (a =0_goto i1),k)) . x = (AddressPart (a =0_goto (il. (SCM R),((locnum i1,(SCM R)) + k)))) . x )
assume A4: x in dom (AddressPart (a =0_goto i1)) ; :: thesis: (AddressPart (IncAddr (a =0_goto i1),k)) . x = (AddressPart (a =0_goto (il. (SCM R),((locnum i1,(SCM R)) + k)))) . x
then A5: x in dom <*i1,a*> by MCART_1:def 2;

per cases ( x = 1 or x = 2 ) by A5, Lm2;

suppose A6: x = 1 ; :: thesis: (AddressPart (IncAddr (a =0_goto i1),k)) . x = (AddressPart (a =0_goto (il. (SCM R),((locnum i1,(SCM R)) + k)))) . x

then (product" (AddressParts (InsCode (a =0_goto i1)))) . x = NAT by Th51;
then consider f being Element of NAT such that
A7: f = (AddressPart (a =0_goto i1)) . x and
A8: (AddressPart (IncAddr (a =0_goto i1),k)) . x = il. (SCM R),(k + (locnum f,(SCM R))) by A4, AMISTD_2:def 14;
f = <*i1,a*> . x by A7, MCART_1:def 2
.= i1 by A6, FINSEQ_1:61 ;
hence (AddressPart (IncAddr (a =0_goto i1),k)) . x = <*(il. (SCM R),((locnum i1,(SCM R)) + k)),a*> . x by A6, A8, FINSEQ_1:61
.= (AddressPart (a =0_goto (il. (SCM R),((locnum i1,(SCM R)) + k)))) . x by MCART_1:def 2 ;
:: thesis: verum

end;

suppose A9: x = 2 ; :: thesis: (AddressPart (IncAddr (a =0_goto i1),k)) . x = (AddressPart (a =0_goto (il. (SCM R),((locnum i1,(SCM R)) + k)))) . x

then (product" (AddressParts (InsCode (a =0_goto i1)))) . x <> NAT by Th4, Th52;
hence (AddressPart (IncAddr (a =0_goto i1),k)) . x = (AddressPart (a =0_goto i1)) . x by A4, AMISTD_2:def 14
.= <*i1,a*> . x by MCART_1:def 2
.= a by A9, FINSEQ_1:61
.= <*(il. (SCM R),((locnum i1,(SCM R)) + k)),a*> . x by A9, FINSEQ_1:61
.= (AddressPart (a =0_goto (il. (SCM R),((locnum i1,(SCM R)) + k)))) . x by MCART_1:def 2 ;
:: thesis: verum

end;

end;

end;

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