pith. machine review for the scientific record. sign in
def definition def or abbrev

Contingent

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 101def Contingent (p : ConfigProp) (c : Config) : Prop :=

proof body

Definition body.

 102  p (Actualize c) ∧ Degenerate c ∧
 103  ∃ y ∈ Possibility c, J y.value = J (Actualize c).value ∧ ¬p y
 104
 105/-- **DETERMINED**: A property that could not have been otherwise.
 106
 107    p is determined at c if all cost-minimal successors satisfy p. -/

depends on (21)

Lean names referenced from this declaration's body.