let i1 be Element of NAT ; :: thesis: for k being natural number
for a being Int-Location holds IncAddr (a =0_goto i1),k = a =0_goto (i1 + k)
let k be natural number ; :: thesis: for a being Int-Location holds IncAddr (a =0_goto i1),k = a =0_goto (i1 + k)
let a be Int-Location ; :: thesis: IncAddr (a =0_goto i1),k = a =0_goto (i1 + k)
A1: InsCode (IncAddr (a =0_goto i1),k) = InsCode (a =0_goto i1) by AMISTD_2:def 14
.= 7 by SCMFSA_2:48
.= InsCode (a =0_goto (i1 + k)) by SCMFSA_2:48 ;
X: a =0_goto i1 = [7,<*i1*>,<*a*>] by Th15;
Y: a =0_goto (i1 + k) = [7,<*(i1 + k)*>,<*a*>] by Th15;
B1: AddressPart (IncAddr (a =0_goto i1),k) = AddressPart (a =0_goto i1) by AMISTD_2:def 14
.= <*a*> by X, RECDEF_2:def 3
.= AddressPart (a =0_goto (i1 + k)) by Y, RECDEF_2:def 3 ;
X1: JumpPart (IncAddr (a =0_goto i1),k) = k + (JumpPart (a =0_goto i1)) by AMISTD_2:def 14;
then A2: dom (JumpPart (IncAddr (a =0_goto i1),k)) = dom (JumpPart (a =0_goto i1)) by VALUED_1:def 2;
A3: for x being set 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 set ; :: 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 A4: 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*> by Th24;
then A6: x = 1 by FINSEQ_1:111;
then (product" (JumpParts (InsCode (a =0_goto i1)))) . x = NAT by Th54;
set f = (JumpPart (a =0_goto i1)) . x;
A8: (JumpPart (IncAddr (a =0_goto i1),k)) . x = k + ((JumpPart (a =0_goto i1)) . x) by A2, X1, A4, VALUED_1:def 2;
(JumpPart (a =0_goto i1)) . x = <*i1*> . x by Th24
.= i1 by A6, FINSEQ_1:57 ;
hence (JumpPart (IncAddr (a =0_goto i1),k)) . x = <*(i1 + k)*> . x by A6, A8, FINSEQ_1:57
.= (JumpPart (a =0_goto (i1 + k))) . x by Th24 ;
:: thesis: verum

end;

dom (JumpPart (a =0_goto (i1 + k))) = dom <*(i1 + k)*> by Th24
.= Seg 1 by FINSEQ_1:55
.= dom <*i1*> by FINSEQ_1:55
.= dom (JumpPart (a =0_goto i1)) by Th24 ;
then JumpPart (IncAddr (a =0_goto i1),k) = JumpPart (a =0_goto (i1 + k)) by A2, A3, FUNCT_1:9;
hence IncAddr (a =0_goto i1),k = a =0_goto (i1 + k) by A1, B1, COMPOS_1:7; :: thesis: verum