ch:very-dependent-functions: very-dependent functions

At $0$ , the restriction is empty and the range PER is equality on naturals. At $1$ , the restriction contains only $f (0)$ ; after choosing a natural $n_{0}$ , the range is the finite PER on values below $n_{0} + 1$ . At $2$ , the restriction contains $f (0)$ and $f (1)$ ; after values $n_{0}, n_{1}$ have been validated, the range is the finite PER below $n_{0} + n_{1} + 1$ . Each definition uses only PERs at strict predecessors, so induction on $0 < 1 < 2$ constructs them in that order.

With $1 < 0$ , label $1$ has no predecessor. Its original range reads $f (0)$ , but $0 ≮ 1$ , so the predecessor-function context contains no such application and formation fails. An accepted reversed family is $B [f, 1] = N$ and $B [f, 0] = Fin (f (1) + 1)$ : the only dependency at $0$ now reads its strict predecessor $1$ .

Place $eq : R \to R \to Bool$ in $M (R)$ . Opening independently packed $o_{1}, o_{2} : Object (M)$ gives $R_{1}, s_{1}, m_{1}$ and $R_{2}, s_{2}, m_{2}$ . The receiver method $m_{1} . eq$ expects two $R_{1}$ values. The application $m_{1} . eq s_{1} s_{2}$ is ill typed because $s_{2} : R_{2}$ ; it would require $R_{1} \equiv R_{2}$ , which existential unpacking does not provide.

Take ordered labels $R < get < set < law$ and the VDF whose ranges are respectively $U_{i}$ , $R \to Z$ , $R \to Z \to R$ , and the equation $\forall r, i . get (set (r, i)) = i$ . The predecessor sets read by the ranges are $\emptyset$ , ${R}$ , ${R}$ , and ${R, get, set}$ . If $law$ is placed before $set$ , its range still mentions $set$ , which is no longer a strict predecessor; the fourth premise of VDF-F fails at that label.

Append $color : Color$ and $recolor : R \to Color \to R$ after the Point fields. Restricting an extended record to the old labels preserves every old predecessor restriction, so proposition 95.7 gives the Point view. A wrapper applies old $set$ to the position component and copies the color branch; its proof fields are recomputed from the old law and reflexivity of the copied color. If a new field is inserted before $law$ and the law’s range is defined over all predecessors, that range changes. The old law proof then has the old type, so merely copying it is a counterexample to the wrapper calculation.