# Help me understand propagation rules

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.