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

proof

let x be set ; :: thesis: ( x in dom (JumpPart (SCM-goto i1)) implies (JumpPart (IncAddr (SCM-goto i1),k)) . x = (JumpPart (SCM-goto (i1 + k))) . x )
assume A4: x in dom (JumpPart (SCM-goto i1)) ; :: thesis: (JumpPart (IncAddr (SCM-goto i1),k)) . x = (JumpPart (SCM-goto (i1 + k))) . x
then x in dom <*i1*> by RECDEF_2:def 2;
then A5: x = 1 by FINSEQ_1:111;
then (product" (JumpParts (InsCode (SCM-goto i1)))) . x = NAT by Th35;
set f = (JumpPart (SCM-goto i1)) . x;
A7: (JumpPart (IncAddr (SCM-goto i1),k)) . x = k + ((JumpPart (SCM-goto i1)) . x) by A4, A1, X1, VALUED_1:def 2;
(JumpPart (SCM-goto i1)) . x = <*i1*> . x by RECDEF_2:def 2
.= i1 by A5, FINSEQ_1:def 8 ;
hence (JumpPart (IncAddr (SCM-goto i1),k)) . x = <*(i1 + k)*> . x by A5, A7, FINSEQ_1:def 8
.= (JumpPart (SCM-goto (i1 + k))) . x by RECDEF_2:def 2 ;
:: thesis: verum

end;

AA: AddressPart (IncAddr (SCM-goto i1),k) = AddressPart (SCM-goto i1) by AMISTD_2:def 14
.= {} by RECDEF_2:def 3
.= AddressPart (SCM-goto (i1 + k)) by RECDEF_2:def 3 ;
BB: InsCode (IncAddr (SCM-goto i1),k) = InsCode (SCM-goto i1) by AMISTD_2:def 14
.= 6 by RECDEF_2:def 1
.= InsCode (SCM-goto (i1 + k)) by RECDEF_2:def 1 ;
JumpPart (IncAddr (SCM-goto i1),k) = JumpPart (SCM-goto (i1 + k)) by A1, A2, A3, FUNCT_1:9;
hence IncAddr (SCM-goto i1),k = SCM-goto (i1 + k) by AA, BB, COMPOS_1:7; :: thesis: verum