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 COMPOS_1:def 17
.= 8 by SCMFSA_2:25
.= InsCode (a >0_goto (i1 + k)) by SCMFSA_2:25 ;
A2: a >0_goto i1 = [8,<*i1*>,<*a*>] by Th16;
A3: a >0_goto (i1 + k) = [8,<*(i1 + k)*>,<*a*>] by Th16;
A4: AddressPart (IncAddr ((a >0_goto i1),k)) = AddressPart (a >0_goto i1) by COMPOS_1:def 17
.= <*a*> by A2, RECDEF_2:def 3
.= AddressPart (a >0_goto (i1 + k)) by A3, RECDEF_2:def 3 ;
A5: JumpPart (IncAddr ((a >0_goto i1),k)) = k + (JumpPart (a >0_goto i1)) by COMPOS_1:def 17;
then A6: dom (JumpPart (IncAddr ((a >0_goto i1),k))) = dom (JumpPart (a >0_goto i1)) by VALUED_1:def 2;
A7: 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 A8: 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 Th25;
then A9: x = 1 by FINSEQ_1:90;
set f = (JumpPart (a >0_goto i1)) . 1;
A10: (JumpPart (IncAddr ((a >0_goto i1),k))) . 1 = k + ((JumpPart (a >0_goto i1)) . 1) by A9, A6, A5, A8, VALUED_1:def 2;
(JumpPart (a >0_goto i1)) . 1 = <*i1*> . x by Th25, A9
.= i1 by A9, FINSEQ_1:40 ;
hence (JumpPart (IncAddr ((a >0_goto i1),k))) . x = <*(i1 + k)*> . x by A9, A10, FINSEQ_1:40
.= (JumpPart (a >0_goto (i1 + k))) . x by Th25 ;
:: thesis: verum

end;

dom (JumpPart (a >0_goto (i1 + k))) = dom <*(i1 + k)*> by Th25
.= Seg 1 by FINSEQ_1:38
.= dom <*i1*> by FINSEQ_1:38
.= dom (JumpPart (a >0_goto i1)) by Th25 ;
then JumpPart (IncAddr ((a >0_goto i1),k)) = JumpPart (a >0_goto (i1 + k)) by A6, A7, FUNCT_1:2;
hence IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k) by A1, A4, COMPOS_1:1; :: thesis: verum