let R be good Ring; :: thesis: for i1 being Element of NAT
for k being natural number holds IncAddr ((goto (i1,R)),k) = goto ((i1 + k),R)
let i1 be Element of NAT ; :: thesis: for k being natural number holds IncAddr ((goto (i1,R)),k) = goto ((i1 + k),R)
let k be natural number ; :: thesis: IncAddr ((goto (i1,R)),k) = goto ((i1 + k),R)
A1: JumpPart (IncAddr ((goto (i1,R)),k)) = k + (JumpPart (goto (i1,R))) by COMPOS_1:def 17;
then A2: dom (JumpPart (IncAddr ((goto (i1,R)),k))) = dom (JumpPart (goto (i1,R))) by VALUED_1:def 2;
A3: dom (JumpPart (goto ((i1 + k),R))) = dom <*(i1 + k)*> by RECDEF_2:def 2
.= Seg 1 by FINSEQ_1:def 8
.= dom <*i1*> by FINSEQ_1:def 8
.= dom (JumpPart (goto (i1,R))) by RECDEF_2:def 2 ;
A4: for x being set st x in dom (JumpPart (goto (i1,R))) holds
(JumpPart (IncAddr ((goto (i1,R)),k))) . x = (JumpPart (goto ((i1 + k),R))) . x

proof

let x be set ; :: thesis: ( x in dom (JumpPart (goto (i1,R))) implies (JumpPart (IncAddr ((goto (i1,R)),k))) . x = (JumpPart (goto ((i1 + k),R))) . x )
assume A5: x in dom (JumpPart (goto (i1,R))) ; :: thesis: (JumpPart (IncAddr ((goto (i1,R)),k))) . x = (JumpPart (goto ((i1 + k),R))) . x
then x in dom <*i1*> by RECDEF_2:def 2;
then A6: x = 1 by Lm1;
reconsider f = (JumpPart (goto (i1,R))) . x as Element of NAT by ORDINAL1:def 12;
A7: (JumpPart (IncAddr ((goto (i1,R)),k))) . x = k + f by A5, A1, A2, VALUED_1:def 2;
f = <*i1*> . x by RECDEF_2:def 2
.= i1 by A6, FINSEQ_1:def 8 ;
hence (JumpPart (IncAddr ((goto (i1,R)),k))) . x = <*(i1 + k)*> . x by A6, A7, FINSEQ_1:def 8
.= (JumpPart (goto ((i1 + k),R))) . x by RECDEF_2:def 2 ;
:: thesis: verum

end;

A8: InsCode (IncAddr ((goto (i1,R)),k)) = InsCode (goto (i1,R)) by COMPOS_1:def 17
.= 6 by RECDEF_2:def 1
.= InsCode (goto ((i1 + k),R)) by RECDEF_2:def 1 ;
A9: AddressPart (IncAddr ((goto (i1,R)),k)) = AddressPart (goto (i1,R)) by COMPOS_1:def 17
.= {} by RECDEF_2:def 3
.= AddressPart (goto ((i1 + k),R)) by RECDEF_2:def 3 ;
JumpPart (IncAddr ((goto (i1,R)),k)) = JumpPart (goto ((i1 + k),R)) by A2, A3, A4, FUNCT_1:2;
hence IncAddr ((goto (i1,R)),k) = goto ((i1 + k),R) by A8, A9, COMPOS_1:1; :: thesis: verum