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

modal_K

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)

 341theorem modal_K (p q : ConfigProp) (c : Config) :
 342    (□(fun x => p x → q x)) c → (□p) c → (□q) c := by

proof body

Term-mode proof.

 343  intro hpq hp y hy
 344  exact hpq y hy (hp y hy)
 345
 346/-- Reflexivity: □p → p (T axiom) fails in general because c ∉ Possibility(c)
 347    (time must advance). But we have the weaker:
 348
 349    If p holds at all possible futures, and c evolves, then p holds after evolution. -/

depends on (11)

Lean names referenced from this declaration's body.