let i1, k be Nat; for a being Int-Location holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
let a be Int-Location; 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_0:def 9
.=
7
by SCMFSA_2:24
.=
InsCode (a =0_goto (i1 + k))
by SCMFSA_2:24
;
A2:
a =0_goto i1 = [7,<*i1*>,<*a*>]
by Th7;
A3:
a =0_goto (i1 + k) = [7,<*(i1 + k)*>,<*a*>]
by Th7;
A4: AddressPart (IncAddr ((a =0_goto i1),k)) =
AddressPart (a =0_goto i1)
by COMPOS_0:def 9
.=
<*a*>
by A2
.=
AddressPart (a =0_goto (i1 + k))
by A3
;
A5:
JumpPart (IncAddr ((a =0_goto i1),k)) = k + (JumpPart (a =0_goto i1))
by COMPOS_0:def 9;
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 object 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
object ;
( 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))
;
(JumpPart (IncAddr ((a =0_goto i1),k))) . x = (JumpPart (a =0_goto (i1 + k))) . x
then
x in dom <*i1*>
by Th15;
then A9:
x = 1
by FINSEQ_1:90;
set f =
(JumpPart (a =0_goto i1)) . x;
A10:
(JumpPart (IncAddr ((a =0_goto i1),k))) . x = k + ((JumpPart (a =0_goto i1)) . x)
by A6, A5, A8, VALUED_1:def 2;
(JumpPart (a =0_goto i1)) . x =
<*i1*> . x
by Th15
.=
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 Th15
;
verum
end;
dom (JumpPart (a =0_goto (i1 + k))) =
dom <*(i1 + k)*>
by Th15
.=
Seg 1
by FINSEQ_1:38
.=
dom <*i1*>
by FINSEQ_1:38
.=
dom (JumpPart (a =0_goto i1))
by Th15
;
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_0:1; verum