def definition def or abbrev

`RSDecidable`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 153def RSDecidable {C : Type*}
 154    (bridge : CostBridge C) (B : C → C) (c₀ c_star : C) (P : C → Bool) : Prop :=

Definition body.

 155  RSExists_cfg bridge c_star ∧ Stabilizes B P c₀ c_star
 156
 157/-- One direction always holds: RSTrue(¬P) ⟹ ¬RSTrue(P). -/

From the project-wide theorem graph. These declarations reference this one in their body.

rs_true_neg_iff_neg_rs_true in IndisputableMonolith.Foundation.OntologyPredicates decl_use
rs_true_or_iff in IndisputableMonolith.Foundation.OntologyPredicates decl_use

Lean names referenced from this declaration's body.