let k, loc be Element of NAT ; :: thesis: for a being Data-Location holds IncAddr (a >0_goto loc),k = a >0_goto (loc + k)
let a be Data-Location ; :: thesis: IncAddr (a >0_goto loc),k = a >0_goto (loc + k)
A: InsCode (IncAddr (a >0_goto loc),k) = InsCode (a >0_goto loc) by AMISTD_2:def 14
.= 8 by RECDEF_2:def 1
.= InsCode (a >0_goto (loc + k)) by RECDEF_2:def 1 ;
B: AddressPart (IncAddr (a >0_goto loc),k) = AddressPart (a >0_goto loc) by AMISTD_2:def 14
.= <*a*> by RECDEF_2:def 3
.= AddressPart (a >0_goto (loc + k)) by RECDEF_2:def 3 ;
X1: JumpPart (IncAddr (a >0_goto loc),k) = k + (JumpPart (a >0_goto loc)) by AMISTD_2:def 14;
JumpPart (IncAddr (a >0_goto loc),k) = JumpPart (a >0_goto (loc + k))

proof

thus K: dom (JumpPart (IncAddr (a >0_goto loc),k)) = dom (JumpPart (a >0_goto (loc + k))) by A, AMISTD_2:def 4; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in proj1 (JumpPart (IncAddr (a >0_goto loc),k)) or (JumpPart (IncAddr (a >0_goto loc),k)) . b₁ = (JumpPart (a >0_goto (loc + k))) . b₁ )
A1: JumpPart (a >0_goto loc) = <*loc*> by RECDEF_2:def 2;
A2: JumpPart (a >0_goto (loc + k)) = <*(loc + k)*> by RECDEF_2:def 2;
let x be set ; :: thesis: ( not x in proj1 (JumpPart (IncAddr (a >0_goto loc),k)) or (JumpPart (IncAddr (a >0_goto loc),k)) . x = (JumpPart (a >0_goto (loc + k))) . x )
assume Z: x in dom (JumpPart (IncAddr (a >0_goto loc),k)) ; :: thesis: (JumpPart (IncAddr (a >0_goto loc),k)) . x = (JumpPart (a >0_goto (loc + k))) . x
dom <*(loc + k)*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then C: x = 1 by Z, K, A2, TARSKI:def 1;
thus (JumpPart (IncAddr (a >0_goto loc),k)) . x = k + ((JumpPart (a >0_goto loc)) . x) by X1, Z, VALUED_1:def 2
.= loc + k by A1, C, FINSEQ_1:57
.= (JumpPart (a >0_goto (loc + k))) . x by A2, C, FINSEQ_1:57 ; :: thesis: verum

end;

hence IncAddr (a >0_goto loc),k = a >0_goto (loc + k) by A, B, COMPOS_1:7; :: thesis: verum