145def RSTrue {C : Type*} 146 (bridge : CostBridge C) (B : C → C) (c₀ c_star : C) (P : C → Bool) : Prop :=
proof body
Definition body.
147 RSExists_cfg bridge c_star ∧ P c_star = true ∧ Stabilizes B P c₀ c_star 148 149/-! ## RS-Decidability and Boolean Laws -/ 150 151/-- A predicate is **RS-decidable** at `(c_star, B, c₀)` when the background 152 conditions for Boolean reasoning hold: existence and stabilization. -/
used by (14)
From the project-wide theorem graph. These declarations reference this one in their body.