pith. machine review for the scientific record. sign in
theorem proved term proof

modal_T_weak

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)

 350theorem modal_T_weak (p : ConfigProp) (c : Config) :
 351    (□p) c → p (Actualize c) := by

proof body

Term-mode proof.

 352  intro h
 353  apply h
 354  exact identity_always_possible c
 355
 356/-! ## Counterfactuals -/
 357
 358/-- A **counterfactual** is an alternative possible future that wasn't actualized.
 359
 360    y is counterfactual from c if:
 361    1. y ∈ P(c) (y was possible)
 362    2. y ≠ Actualize(c) (y wasn't chosen)
 363    3. J(y) > J(Actualize c) (y costs more, which is why it wasn't chosen) -/

depends on (16)

Lean names referenced from this declaration's body.