let R be Ring; :: thesis: for a being Data-Location of R
for i1, k being Nat holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
let a be Data-Location of R; :: thesis: for i1, k being Nat holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
let i1, k be Nat; :: thesis: IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
A1: JumpPart (IncAddr ((a =0_goto i1),k)) = k + (JumpPart (a =0_goto i1)) by COMPOS_0:def 9;
then A2: dom (JumpPart (IncAddr ((a =0_goto i1),k))) = dom (JumpPart (a =0_goto i1)) by VALUED_1:def 2;
A3: dom (JumpPart (a =0_goto (i1 + k))) = dom <*(i1 + k)*>
.= Seg 1 by FINSEQ_1:38
.= dom <*i1*> by FINSEQ_1:38
.= dom (JumpPart (a =0_goto i1)) ;
A4: for x being object st x in dom (JumpPart (a =0_goto i1)) holds
(JumpPart (IncAddr ((a =0_goto i1),k))) . x = (JumpPart (a =0_goto (i1 + k))) . x

proof

let x be object ; :: thesis: ( x in dom (JumpPart (a =0_goto i1)) implies (JumpPart (IncAddr ((a =0_goto i1),k))) . x = (JumpPart (a =0_goto (i1 + k))) . x )
assume A5: x in dom (JumpPart (a =0_goto i1)) ; :: thesis: (JumpPart (IncAddr ((a =0_goto i1),k))) . x = (JumpPart (a =0_goto (i1 + k))) . x
then x in dom <*i1*> ;
then A6: x = 1 by FINSEQ_1:90;
reconsider f = (JumpPart (a =0_goto i1)) . x as Element of NAT by ORDINAL1:def 12;
A7: (JumpPart (IncAddr ((a =0_goto i1),k))) . x = k + f by A5, A1, A2, VALUED_1:def 2;
f = <*i1*> . x
.= i1 by A6, FINSEQ_1:40 ;
hence (JumpPart (IncAddr ((a =0_goto i1),k))) . x = <*(i1 + k)*> . x by A6, A7, FINSEQ_1:40
.= (JumpPart (a =0_goto (i1 + k))) . x ;
:: thesis: verum

end;

A8: InsCode (IncAddr ((a =0_goto i1),k)) = InsCode (a =0_goto i1) by COMPOS_0:def 9
.= 7
.= InsCode (a =0_goto (i1 + k)) ;
A9: AddressPart (IncAddr ((a =0_goto i1),k)) = AddressPart (a =0_goto i1) by COMPOS_0:def 9
.= <*a*>
.= AddressPart (a =0_goto (i1 + k)) ;
JumpPart (IncAddr ((a =0_goto i1),k)) = JumpPart (a =0_goto (i1 + k)) by A2, A3, A4, FUNCT_1:2;
hence IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k) by A8, A9, COMPOS_0:1; :: thesis: verum