let i be Instruction of S; COMPOS_2:def 5 ( i in rng (Reloc (I,k)) implies rng (JumpPart i) c= dom (Reloc (I,k)) )
assume
i in rng (Reloc (I,k))
; rng (JumpPart i) c= dom (Reloc (I,k))
then consider n being set such that
W1:
n in dom (Reloc (I,k))
and
W2:
(Reloc (I,k)) . n = i
by FUNCT_1:def 3;
dom (Reloc (I,k)) c= NAT
by RELAT_1:def 18;
then reconsider n = n as Nat by W1;
B:
dom (Reloc (I,k)) = dom (Shift (I,k))
by COMPOS_1:32;
then consider j being Nat such that
W3:
j in dom I
and
W4:
n = j + k
by W1, VALUED_1:39;
I . j = I /. j
by W3, PARTFUN1:def 6;
then reconsider i1 = I . j as Instruction of S ;
A:
IncAddr (i1,k) = i
by W2, W3, W4, COMPOS_1:35;
let x be set ; TARSKI:def 3 ( not x in rng (JumpPart i) or x in dom (Reloc (I,k)) )
assume C:
x in rng (JumpPart i)
; x in dom (Reloc (I,k))
then consider y being set such that
W5:
y in dom (JumpPart i)
and
W6:
(JumpPart i) . y = x
by FUNCT_1:def 3;
dom (JumpPart i) c= NAT
by RELAT_1:def 18;
then reconsider y = y as Nat by W5;
H:
JumpPart i = (JumpPart i1) + k
by A, COMPOS_0:def 9;
then E:
dom (JumpPart i) = dom (JumpPart i1)
by VALUED_1:def 2;
rng (JumpPart i) c= NAT
by RELAT_1:def 19;
then reconsider m = x as Nat by C;
reconsider n = (JumpPart i1) . y as Nat ;
D:
m = n + k
by W6, H, W5, VALUED_1:def 2;
G:
n in rng (JumpPart i1)
by W5, E, FUNCT_1:3;
i1 in rng I
by W3, FUNCT_1:3;
then
rng (JumpPart i1) c= dom I
by Def5;
hence
x in dom (Reloc (I,k))
by B, D, G, VALUED_1:24; verum