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
.=
8
by SCMFSA_2:25
.=
InsCode (a >0_goto (i1 + k))
by SCMFSA_2:25
;
A2:
a >0_goto i1 = [8,<*i1*>,<*a*>]
by Th8;
A3:
a >0_goto (i1 + k) = [8,<*(i1 + k)*>,<*a*>]
by Th8;
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 Th16;
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 Th16, 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 Th16
;
verum
end;
dom (JumpPart (a >0_goto (i1 + k))) =
dom <*(i1 + k)*>
by Th16
.=
Seg 1
by FINSEQ_1:38
.=
dom <*i1*>
by FINSEQ_1:38
.=
dom (JumpPart (a >0_goto i1))
by Th16
;
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