theorem LO.Modal.Kripke.valid_on_FiniteTransitiveTreeClass_of_valid_on_TransitiveIrreflexiveFrameClass {φ : Formula ℕ} (h : FrameClass.finite_trans_irrefl ⊧ φ) (F : Frame) (r : F.World) [F.IsFiniteTree r] : F ⊧ φ

theorem LO.Modal.Kripke.satisfies_at_root_on_FiniteTransitiveTree {φ : Formula ℕ} (h : ∀ (F : Frame) (r : F.World) [inst : Finite F.World] [inst : F.IsTree r], F ⊧ φ) (M : Model) (r : M.World) [M.IsFiniteTree r] : Formula.Kripke.Satisfies M r φ

theorem LO.Modal.Kripke.valid_on_TransitiveIrreflexiveFrameClass_of_satisfies_at_root_on_FiniteTransitiveTree {φ : Formula ℕ} : (∀ (M : Model) (r : M.World) [inst : M.IsFiniteTree r], Formula.Kripke.Satisfies M r φ) → FrameClass.finite_trans_irrefl ⊧ φ

theorem LO.Modal.Hilbert.GL.Kripke.iff_provable_satisfies_FiniteTransitiveTree {φ : Formula ℕ} : Hilbert.GL ⊢! φ ↔ ∀ (M : Kripke.Model) (r : M.World) [inst : M.IsFiniteTree r], Formula.Kripke.Satisfies M r φ

theorem LO.Modal.Hilbert.GL.Kripke.iff_unprovable_exists_unsatisfies_FiniteTransitiveTree {φ : Formula ℕ} : Hilbert.GL ⊬ φ ↔ ∃ (M : Kripke.Model) (r : M.World), M.IsFiniteTree r ∧ ¬Formula.Kripke.Satisfies M r φ