Function term_depth 

pub fn term_depth(t: &Term) -> usize

The nesting depth of a Term, counted in EDGES: a leaf is 0.

This is the DOOR’s measure — type_checker::depth_exceeds(t, n) is exactly term_depth(t) > n — and it is one less than TermStore::depth, which counts a leaf as one rung. The unit tests at the bottom of this file pin both relations, so the three measures cannot drift apart silently.