Help me understand propagation rules

Help
1

The propagation of build inputs are explained in Nixpkgs 23.05 manual | Nix & NixOS. The section is a bit hard to understand, but I thought I had understood it. Then there comes an example in the explanation of propagatedNativeBuildInputs:

For example, if package Y has propagatedNativeBuildInputs = [X] , and package Z has buildInputs = [Y] , then package Z will be built as if it included package X in its nativeBuildInputs . If instead, package Z has nativeBuildInputs = [Y] , then Z will be built as if it included X in the depsBuildBuild of package Z , because of the sum of the two -1 host offsets.

This gives us two examples that I’m going to write down in the style of the Natural Deduction rules in the same section

1st Example

X is in propagatedNativeBuildInputs of Y with offset (-1,0)
Y is in buildInputs of Z with offset (0,1)

# Y
let mapOffset(h, t, i) = i + (if i <= 0 then h else t - 1)

dep(0, 1, Z, Y)
propagated-dep(-1, 0, Y, X)
0 + -1 in {-1, 0, 1}
0 + 0 in {-1, 0, 1}
# ->
propagated-dep(mapOffset(0, 1, -1),
               mapOffset(0, 1, 0),
               Z, X) = propagated-dep(-1, 0, Z, X)

This gives us that X is in nativeBuildInputs of Z as stated in the example.

2nd Example

X is in propagatedNativeBuildInputs of Y with offset (-1,0)
Y is in nativeBuildInputs of Z with offset (-1,0)

# Y
let mapOffset(h, t, i) = i + (if i <= 0 then h else t - 1)

dep(-1, 0, Z, Y)
propagated-dep(-1, 0, Y, X)
-1 + -1 in {-1, 0, 1} # This is no true!
-1 + 0 in {-1, 0, -1}
# ->
propagated-dep(mapOffset(-1, 0, -1),
               mapOffset(-1, 0, 0),
               Z, X) = propagated-dep(-2, -1, Z, X)

This calculation gives us a propagated offset tuple of (-2,1), but the calculation is not valid because one of the conditions is not fulfilled: The host offsets sum to -2.

Still, the example says that the result will be that X is in depsBuildBuild of Z which would
correspond to propagated-dep(-1,-1, Z, X). I do not understand how to get this from the inference rules.