let k, loc be 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:7;
A2:
a =0_goto (loc + k) = [7,<*(loc + k)*>,<*a*>]
by SCMFSA10:7;
A3: InsCode (IncAddr ((a =0_goto loc),k)) =
InsCode (a =0_goto loc)
by COMPOS_0:def 9
.=
7
by A1
.=
InsCode (a =0_goto (loc + k))
by A2
;
A4: AddressPart (IncAddr ((a =0_goto loc),k)) =
AddressPart (a =0_goto loc)
by COMPOS_0:def 9
.=
<*a*>
by A1
.=
AddressPart (a =0_goto (loc + k))
by A2
;
A5:
JumpPart (IncAddr ((a =0_goto loc),k)) = k + (JumpPart (a =0_goto loc))
by COMPOS_0:def 9;
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_0:def 5;
FUNCT_1:def 11 for b1 being object 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;
A8:
JumpPart (a =0_goto (loc + k)) = <*(loc + k)*>
by A2;
let x be
object ;
( 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:2, FINSEQ_1:38;
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:40
.=
(JumpPart (a =0_goto (loc + k))) . x
by A8, A10, FINSEQ_1:40
;
verum
end;
hence
IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k)
by A3, A4, COMPOS_0:1; verum