let k, loc be Element of NAT ; for a being Int-Location holds IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k)
let a be Int-Location ; IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k)
A1:
a =0_goto loc = [7,<*loc*>,<*a*>]
by SCMFSA10:15;
A2:
a =0_goto (loc + k) = [7,<*(loc + k)*>,<*a*>]
by SCMFSA10:15;
A3: InsCode (IncAddr ((a =0_goto loc),k)) =
InsCode (a =0_goto loc)
by COMPOS_1:def 38
.=
7
by A1, RECDEF_2:def 1
.=
InsCode (a =0_goto (loc + k))
by A2, RECDEF_2:def 1
;
A4: AddressPart (IncAddr ((a =0_goto loc),k)) =
AddressPart (a =0_goto loc)
by COMPOS_1:def 38
.=
<*a*>
by A1, RECDEF_2:def 3
.=
AddressPart (a =0_goto (loc + k))
by A2, RECDEF_2:def 3
;
A5:
JumpPart (IncAddr ((a =0_goto loc),k)) = k + (JumpPart (a =0_goto loc))
by COMPOS_1:def 38;
JumpPart (IncAddr ((a =0_goto loc),k)) = JumpPart (a =0_goto (loc + k))
proof
thus A6:
dom (JumpPart (IncAddr ((a =0_goto loc),k))) = dom (JumpPart (a =0_goto (loc + k)))
by A3, COMPOS_1:def 33;
FUNCT_1:def 17 for b1 being set holds
( not b1 in proj1 (JumpPart (IncAddr ((a =0_goto loc),k))) or (JumpPart (IncAddr ((a =0_goto loc),k))) . b1 = (JumpPart (a =0_goto (loc + k))) . b1 )
A7:
JumpPart (a =0_goto loc) = <*loc*>
by A1, RECDEF_2:def 2;
A8:
JumpPart (a =0_goto (loc + k)) = <*(loc + k)*>
by A2, RECDEF_2:def 2;
let x be
set ;
( 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 A9:
x in dom (JumpPart (IncAddr ((a =0_goto loc),k)))
;
(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 A10:
x = 1
by A9, A6, A8, TARSKI:def 1;
thus (JumpPart (IncAddr ((a =0_goto loc),k))) . x =
k + ((JumpPart (a =0_goto loc)) . x)
by A5, A9, VALUED_1:def 2
.=
loc + k
by A7, A10, FINSEQ_1:57
.=
(JumpPart (a =0_goto (loc + k))) . x
by A8, A10, FINSEQ_1:57
;
verum
end;
hence
IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k)
by A3, A4, COMPOS_1:7; verum