90 Nonempty (PeelingData inputs aRef φ H) 91 92/-- Forced-implication reachability (abstract): there is a directed arborescence 93 of locally-determining constraints from OUTPUT to every input. 94 95 **Definition**: We define ForcedArborescence as equivalent to PeelingWitness. 96 The peeling order (v₁, v₂, ..., vₙ) with determining constraints (K₁, K₂, ..., Kₙ) 97 implicitly defines an arborescence where each variable's parent is determined 98 by the constraint that determines it. 99 100 **Graph interpretation**: The arborescence edges are: 101 - v → K_i for each variable v mentioned in K_i's "known" portion 102 - K_i → v_i for the variable determined by K_i 103 104 This forms a directed tree rooted at OUTPUT reaching all input variables. -/
used by (6)
From the project-wide theorem graph. These declarations reference this one in their body.