SSL AOT_PossibleWorlds.thy   Interaktion und
PortierbarkeitIsabelle

(*<*)
theory AOT_PossibleWorlds
  imports AOT_PLM AOT_BasicLogicalObjects AOT_RestrictedVariables
begin
(*>*)

section‹Possible Worlds›

AOT_define Situation :: ‹τ → φ› (‹Situation'(_')›)
  situations: ‹Situation(x) ≡_df A!x & ∀F (x[F] → Propositional([F]))›

AOT_theorem "T-sit": ‹TruthValue(x) → Situation(x)›
proof(rule "→I")
  AOT_assume ‹TruthValue(x)›
  AOT_hence ‹∃p TruthValueOf(x,p)›
    using "T-value"[THEN "≡_dfE"] by blast
  then AOT_obtain p where ‹TruthValueOf(x,p)› using "∃E"[rotated] by blast
  AOT_hence θ: ‹A!x & ∀F (x[F] ≡ ∃q((q ≡ p) & F = [λy q]))›
    using "tv-p"[THEN "≡_dfE"] by blast
  AOT_show ‹Situation(x)›
  proof(rule situations[THEN "≡_dfI"]; safe intro!: "&I" GEN "→I" θ[THEN "&E"(1)])
    fix F
    AOT_assume ‹x[F]›
    AOT_hence ‹∃q((q ≡ p) & F = [λy q])›
      using θ[THEN "&E"(2), THEN "∀E"(2)[where β=F], THEN "≡E"(1)] by argo
    then AOT_obtain q where ‹(q ≡ p) & F = [λy q]› using "∃E"[rotated] by blast
    AOT_hence ‹∃p F = [λy p]› using "&E"(2) "∃I"(2) by metis
    AOT_thus ‹Propositional([F])›
      by (metis "≡_dfI" "prop-prop1")
  qed
qed

AOT_theorem "possit-sit:1": ‹Situation(x) ≡ ◻Situation(x)›
proof(rule "≡I"; rule "→I")
  AOT_assume ‹Situation(x)›
  AOT_hence 0: ‹A!x & ∀F (x[F] → Propositional([F]))›
    using situations[THEN "≡_dfE"] by blast
  AOT_have 1: ‹◻(A!x & ∀F (x[F] → Propositional([F])))›
  proof(rule "KBasic:3"[THEN "≡E"(2)]; rule "&I")
    AOT_show ‹◻A!x› using 0[THEN "&E"(1)] by (metis "oa-facts:2"[THEN "→E"])
  next
    AOT_have ‹∀F (x[F] → Propositional([F])) → ◻∀F (x[F] → Propositional([F]))›
      by (AOT_subst ‹Propositional([F])› ‹∃p (F = [λy p])› for: F :: ‹<\<kappa>>›)
         (auto simp: "prop-prop1" "≡Df" "enc-prop-nec:2")
    AOT_thus ‹◻∀F (x[F] → Propositional([F]))›
      using 0[THEN "&E"(2)] "→E" by blast
  qed
  AOT_show ‹◻Situation(x)›
    by (AOT_subst ‹Situation(x)› ‹A!x & ∀F (x[F] → Propositional([F]))›)
       (auto simp: 1 "≡Df" situations)
next
  AOT_show ‹Situation(x)› if ‹◻Situation(x)›
    using "qml:2"[axiom_inst, THEN "→E", OF that].
qed

AOT_theorem "possit-sit:2": ‹♢Situation(x) ≡ Situation(x)›
  using "possit-sit:1"
  by (metis "RE♢" "S5Basic:2" "≡E"(1) "≡E"(5) "Commutativity of ≡")

AOT_theorem "possit-sit:3": ‹♢Situation(x) ≡ ◻Situation(x)›
  using "possit-sit:1" "possit-sit:2" by (meson "≡E"(5))

AOT_theorem "possit-sit:4": ‹\ASituation(x) ≡ Situation(x)›
  by (meson "Act-Basic:5" "Act-Sub:2" "RA[2]" "≡E"(1) "≡E"(6) "possit-sit:2")

AOT_theorem "possit-sit:5": ‹Situation(∘p)›
proof (safe intro!: situations[THEN "≡_dfI"] "&I" GEN "→I" "prop-prop1"[THEN "≡_dfI"])
  AOT_have ‹∃F ∘p[F]›
    using "tv-id:2"[THEN "prop-enc"[THEN "≡_dfE"], THEN "&E"(2)]
          "existential:1" "prop-prop2:2" by blast
  AOT_thus ‹A!∘p›
    by (safe intro!: "encoders-are-abstract"[unvarify x, THEN "→E"]
                     "t=t-proper:2"[THEN "→E", OF "ext-p-tv:3"])
next
  fix F
  AOT_assume ‹∘p[F]›
  AOT_hence ‹\ιx(A!x & ∀F (x[F] ≡ ∃q ((q ≡ p) & F = [λy q])))[F]›
    using "tv-id:1" "rule=E" by fast
  AOT_hence ‹\A∃q ((q ≡ p) & F = [λy q])›
    using "≡E"(1) "desc-nec-encode:1" by fast
  AOT_hence ‹∃q \A((q ≡ p) & F = [λy q])›
    by (metis "Act-Basic:10" "≡E"(1))
  then AOT_obtain q where ‹\A((q ≡ p) & F = [λy q])› using "∃E"[rotated] by blast
  AOT_hence ‹\AF = [λy q]› by (metis "Act-Basic:2" "con-dis-i-e:2:b" "intro-elim:3:a")
  AOT_hence ‹F = [λy q]›
    using "id-act:1"[unvarify β, THEN "≡E"(2)] by (metis "prop-prop2:2")
  AOT_thus ‹∃p F = [λy p]›
    using "∃I" by fast
qed

AOT_theorem "possit-sit:6": ‹Situation(⊤)›
proof -
  AOT_have true_def: ‹\⊨_\◻ ⊤ = \ιx (A!x & ∀F (x[F] ≡ ∃p(p & F = [λy p])))›
    by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
  AOT_hence true_den: ‹\⊨_\◻ ⊤↓›
    using "t=t-proper:1" "vdash-properties:6" by blast
  AOT_have ‹\ATruthValue(⊤)›
    using "actual-desc:2"[unvarify x, OF true_den, THEN "→E", OF true_def]
    using "TV-lem2:1"[unvarify x, OF true_den, THEN "RA[2]",
                      THEN "act-cond"[THEN "→E"], THEN "→E"]
    by blast
  AOT_hence ‹\ASituation(⊤)›
    using "T-sit"[unvarify x, OF true_den, THEN "RA[2]",
                  THEN "act-cond"[THEN "→E"], THEN "→E"] by blast
  AOT_thus ‹Situation(⊤)›
    using "possit-sit:4"[unvarify x, OF true_den, THEN "≡E"(1)] by blast
qed

AOT_theorem "possit-sit:7": ‹Situation(⊥)›
proof -
  AOT_have true_def: ‹\⊨_\◻ ⊥ = \ιx (A!x & ∀F (x[F] ≡ ∃p(¬p & F = [λy p])))›
    by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:2")
  AOT_hence true_den: ‹\⊨_\◻ ⊥↓›
    using "t=t-proper:1" "vdash-properties:6" by blast
  AOT_have ‹\ATruthValue(⊥)›
    using "actual-desc:2"[unvarify x, OF true_den, THEN "→E", OF true_def]
    using "TV-lem2:2"[unvarify x, OF true_den, THEN "RA[2]",
                      THEN "act-cond"[THEN "→E"], THEN "→E"]
    by blast
  AOT_hence ‹\ASituation(⊥)›
    using "T-sit"[unvarify x, OF true_den, THEN "RA[2]",
                  THEN "act-cond"[THEN "→E"], THEN "→E"] by blast
  AOT_thus ‹Situation(⊥)›
    using "possit-sit:4"[unvarify x, OF true_den, THEN "≡E"(1)] by blast
qed

AOT_register_rigid_restricted_type
  Situation: ‹Situation(κ)›
proof
  AOT_modally_strict {
    fix p
    AOT_obtain x where ‹TruthValueOf(x,p)›
      by (metis "instantiation" "p-has-!tv:1")
    AOT_hence ‹∃p TruthValueOf(x,p)› by (rule "∃I")
    AOT_hence ‹TruthValue(x)› by (metis "≡_dfI" "T-value")
    AOT_hence ‹Situation(x)› using "T-sit"[THEN "→E"] by blast
    AOT_thus ‹∃x Situation(x)› by (rule "∃I")
  }
next
  AOT_modally_strict {
    AOT_show ‹Situation(κ) → κ↓› for κ
    proof (rule "→I")
      AOT_assume ‹Situation(κ)›
      AOT_hence ‹A!κ› by (metis "≡_dfE" "&E"(1) situations)
      AOT_thus ‹κ↓› by (metis "russell-axiom[exe,1].ψ_denotes_asm")
    qed
  }
next
  AOT_modally_strict {
    AOT_show ‹∀α(Situation(α) → ◻Situation(α))›
      using "possit-sit:1"[THEN "conventions:3"[THEN "≡_dfE"],
                           THEN "&E"(1)] GEN by fast
  }
qed

AOT_register_variable_names
  Situation: s

AOT_define TruthInSituation :: ‹τ → φ → φ› (‹(_ ⊨/ _)› [100, 40] 100)
  "true-in-s": ‹s ⊨ p ≡_df s\Σp›

notepad
begin
  (* Verify precedence. *)
  fix x p q
  have ‹«x ⊨ p → q¬ = «(x ⊨ p) → q¬›
    by simp
  have ‹«x ⊨ p & q¬ = «(x ⊨ p) & q¬›
    by simp
  have ‹«x ⊨ ¬p¬ = «x ⊨ (¬p)¬›
    by simp
  have ‹«x ⊨ ◻p¬ = «x ⊨ (◻p)¬›
    by simp
  have ‹«x ⊨ \Ap¬ = «x ⊨ (\Ap)¬›
    by simp
  have ‹«◻x ⊨ p¬ = «◻(x ⊨ p)¬›
    by simp
  have ‹«¬x ⊨ p¬ = «¬(x ⊨ p)¬›
    by simp
end


AOT_theorem lem1: ‹Situation(x) → (x ⊨ p ≡ x[λy p])›
proof (rule "→I"; rule "≡I"; rule "→I")
  AOT_assume ‹Situation(x)›
  AOT_assume ‹x ⊨ p›
  AOT_hence ‹x\Σp›
    using "true-in-s"[THEN "≡_dfE"] "&E" by blast
  AOT_thus ‹x[λy p]› using "prop-enc"[THEN "≡_dfE"] "&E" by blast
next
  AOT_assume 1: ‹Situation(x)›
  AOT_assume ‹x[λy p]›
  AOT_hence ‹x\Σp›
    using "prop-enc"[THEN "≡_dfI", OF "&I", OF "cqt:2"(1)] by blast
  AOT_thus ‹x ⊨ p›
    using "true-in-s"[THEN "≡_dfI"] 1 "&I" by blast
qed

AOT_theorem "lem2:1": ‹s ⊨ p ≡ ◻s ⊨ p›
proof -
  AOT_have sit: ‹Situation(s)›
    by (simp add: Situation.ψ)
  AOT_have ‹s ⊨ p ≡ s[λy p]›
    using lem1[THEN "→E", OF sit] by blast
  also AOT_have ‹… ≡ ◻s[λy p]›
    by (rule "en-eq:2[1]"[unvarify F]) "cqt:2[lambda]"
  also AOT_have ‹… ≡ ◻s ⊨ p›
    using lem1[THEN RM, THEN "→E", OF "possit-sit:1"[THEN "≡E"(1), OF sit]]
    by (metis "KBasic:6" "≡E"(2) "Commutativity of ≡" "→E")
  finally show ?thesis.
qed

AOT_theorem "lem2:2": ‹♢s ⊨ p ≡ s ⊨ p›
proof -
  AOT_have ‹◻(s ⊨ p → ◻s ⊨ p)›
    using "possit-sit:1"[THEN "≡E"(1), OF Situation.ψ]
          "lem2:1"[THEN "conventions:3"[THEN "≡_dfE", THEN "&E"(1)]]
          RM[OF "→I", THEN "→E"] by blast
  thus ?thesis by (metis "B♢" "S5Basic:13" "T♢" "≡I" "≡E"(1) "→E")
qed

AOT_theorem "lem2:3": ‹♢s ⊨ p ≡ ◻s ⊨ p›
  using "lem2:1" "lem2:2" by (metis "≡E"(5))

AOT_theorem "lem2:4": ‹\A(s ⊨ p) ≡ s ⊨ p›
proof -
  AOT_have ‹◻(s ⊨ p → ◻s ⊨ p)›
    using "possit-sit:1"[THEN "≡E"(1), OF Situation.ψ]
      "lem2:1"[THEN "conventions:3"[THEN "≡_dfE", THEN "&E"(1)]]
      RM[OF "→I", THEN "→E"] by blast
  thus ?thesis
    using "sc-eq-fur:2"[THEN "→E"] by blast
qed

AOT_theorem "lem2:5": ‹¬s ⊨ p ≡ ◻¬s ⊨ p›
  by (metis "KBasic2:1" "contraposition:1[2]" "→I" "≡I" "≡E"(3) "≡E"(4) "lem2:2")

AOT_theorem "sit-identity": ‹s = s' ≡ ∀p(s ⊨ p ≡ s' ⊨ p)›
proof(rule "≡I"; rule "→I")
  AOT_assume ‹s = s'›
  moreover AOT_have ‹∀p(s ⊨ p ≡ s ⊨ p)›
    by (simp add: "oth-class-taut:3:a" "universal-cor")
  ultimately AOT_show ‹∀p(s ⊨ p ≡ s' ⊨ p)›
    using "rule=E" by fast
next
  AOT_assume a: ‹∀p (s ⊨ p ≡ s' ⊨ p)›
  AOT_show ‹s = s'›
  proof(safe intro!: "ab-obey:1"[THEN "→E", THEN "→E"] "&I" GEN "≡I" "→I")
    AOT_show ‹A!s› using Situation.ψ "≡_dfE" "&E"(1) situations by blast
  next
    AOT_show ‹A!s'› using Situation.ψ "≡_dfE" "&E"(1) situations by blast
  next
    fix F
    AOT_assume 0: ‹s[F]›
    AOT_hence ‹∃p (F = [λy p])›
      using Situation.ψ[THEN situations[THEN "≡_dfE"], THEN "&E"(2),
                        THEN "∀E"(2)[where β=F], THEN "→E"]
            "prop-prop1"[THEN "≡_dfE"] by blast
    then AOT_obtain p where F_def: ‹F = [λy p]›
      using "∃E" by metis
    AOT_hence ‹s[λy p]›
      using 0 "rule=E" by blast
    AOT_hence ‹s ⊨ p›
      using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)] by blast
    AOT_hence ‹s' ⊨ p›
      using a[THEN "∀E"(2)[where β=p], THEN "≡E"(1)] by blast
    AOT_hence ‹s'[λy p]›
      using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(1)] by blast
    AOT_thus ‹s'[F]›
      using F_def[symmetric] "rule=E" by blast
  next
    fix F
    AOT_assume 0: ‹s'[F]›
    AOT_hence ‹∃p (F = [λy p])›
      using Situation.ψ[THEN situations[THEN "≡_dfE"], THEN "&E"(2),
                        THEN "∀E"(2)[where β=F], THEN "→E"]
            "prop-prop1"[THEN "≡_dfE"] by blast
    then AOT_obtain p where F_def: ‹F = [λy p]›
      using "∃E" by metis
    AOT_hence ‹s'[λy p]›
      using 0 "rule=E" by blast
    AOT_hence ‹s' ⊨ p›
      using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)] by blast
    AOT_hence ‹s ⊨ p›
      using a[THEN "∀E"(2)[where β=p], THEN "≡E"(2)] by blast
    AOT_hence ‹s[λy p]›
      using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(1)] by blast
    AOT_thus ‹s[F]›
      using F_def[symmetric] "rule=E" by blast
  qed
qed

AOT_define PartOfSituation :: ‹τ → τ → φ› (infixl ‹⊴› 80)
  "sit-part-whole": ‹s ⊴ s' ≡_df ∀p (s ⊨ p → s' ⊨ p)›

AOT_theorem "part:1": ‹s ⊴ s›
  by (rule "sit-part-whole"[THEN "≡_dfI"])
     (safe intro!: "&I" Situation.ψ GEN "→I")

AOT_theorem "part:2": ‹s ⊴ s' & s ≠ s' → ¬(s' ⊴ s)›
proof(rule "→I"; frule "&E"(1); drule "&E"(2); rule "raa-cor:2")
  AOT_assume 0: ‹s ⊴ s'›
  AOT_hence a: ‹s ⊨ p → s' ⊨ p› for p
    using "∀E"(2) "sit-part-whole"[THEN "≡_dfE"] "&E" by blast
  AOT_assume ‹s' ⊴ s›
  AOT_hence b: ‹s' ⊨ p → s ⊨ p› for p
    using "∀E"(2) "sit-part-whole"[THEN "≡_dfE"] "&E" by blast
  AOT_have ‹∀p (s ⊨ p ≡ s' ⊨ p)›
    using a b by (simp add: "≡I" "universal-cor")
  AOT_hence 1: ‹s = s'›
    using "sit-identity"[THEN "≡E"(2)] by metis
  AOT_assume ‹s ≠ s'›
  AOT_hence ‹¬(s = s')›
    by (metis "≡_dfE" "=-infix")
  AOT_thus ‹s = s' & ¬(s = s')›
    using 1 "&I" by blast
qed

AOT_theorem "part:3": ‹s ⊴ s' & s' ⊴ s'' → s ⊴ s''›
proof(rule "→I"; frule "&E"(1); drule "&E"(2);
      safe intro!: "&I" GEN "→I" "sit-part-whole"[THEN "≡_dfI"] Situation.ψ)
  fix p
  AOT_assume ‹s ⊨ p›
  moreover AOT_assume ‹s ⊴ s'›
  ultimately AOT_have ‹s' ⊨ p›
    using "sit-part-whole"[THEN "≡_dfE", THEN "&E"(2),
                           THEN "∀E"(2)[where β=p], THEN "→E"] by blast
  moreover AOT_assume ‹s' ⊴ s''›
  ultimately AOT_show ‹s'' ⊨ p›
    using "sit-part-whole"[THEN "≡_dfE", THEN "&E"(2),
                           THEN "∀E"(2)[where β=p], THEN "→E"] by blast
qed

AOT_theorem "sit-identity2:1": ‹s = s' ≡ s ⊴ s' & s' ⊴ s›
proof (safe intro!: "≡I" "&I" "→I")
  AOT_show ‹s ⊴ s'› if ‹s = s'›
    using "rule=E" "part:1" that by blast
next
  AOT_show ‹s' ⊴ s› if ‹s = s'›
    using "rule=E" "part:1" that[symmetric] by blast
next
  AOT_assume ‹s ⊴ s' & s' ⊴ s›
  AOT_thus ‹s = s'› using "part:2"[THEN "→E", OF "&I"]
    by (metis "≡_dfI" "&E"(1) "&E"(2) "=-infix" "raa-cor:3")
qed

AOT_theorem "sit-identity2:2": ‹s = s' ≡ ∀s'' (s'' ⊴ s ≡ s'' ⊴ s')›
proof(safe intro!: "≡I" "→I" Situation.GEN "sit-identity"[THEN "≡E"(2)]
                   GEN[where 'a=o])
  AOT_show ‹s'' ⊴ s'› if ‹s'' ⊴ s› and ‹s = s'› for s''
    using "rule=E" that by blast
next
  AOT_show ‹s'' ⊴ s› if ‹s'' ⊴ s'› and ‹s = s'› for s''
    using "rule=E" id_sym that by blast
next
  AOT_show ‹s' ⊨ p› if ‹s ⊨ p› and ‹∀s'' (s'' ⊴ s ≡ s'' ⊴ s')› for p
    using "sit-part-whole"[THEN "≡_dfE", THEN "&E"(2),
              OF that(2)[THEN "Situation.∀E", THEN "≡E"(1), OF "part:1"],
              THEN "∀E"(2), THEN "→E", OF that(1)].
next
  AOT_show ‹s ⊨ p› if ‹s' ⊨ p› and ‹∀s'' (s'' ⊴ s ≡ s'' ⊴ s')› for p
    using "sit-part-whole"[THEN "≡_dfE", THEN "&E"(2),
          OF that(2)[THEN "Situation.∀E", THEN "≡E"(2), OF "part:1"],
          THEN "∀E"(2), THEN "→E", OF that(1)].
qed

AOT_define Persistent :: ‹φ → φ› (‹Persistent'(_')›)
  persistent: ‹Persistent(p) ≡_df ∀s (s ⊨ p → ∀s' (s ⊴ s' → s' ⊨ p))›

AOT_theorem "pers-prop": ‹∀p Persistent(p)›
  by (safe intro!: GEN[where 'a=o] Situation.GEN persistent[THEN "≡_dfI"] "→I")
     (simp add: "sit-part-whole"[THEN "≡_dfE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"])

AOT_define NullSituation :: ‹τ → φ› (‹NullSituation'(_')›)
  "df-null-trivial:1": ‹NullSituation(s) ≡_df ¬∃p s ⊨ p›

AOT_define TrivialSituation :: ‹τ → φ› (‹TrivialSituation'(_')›)
  "df-null-trivial:2": ‹TrivialSituation(s) ≡_df ∀p s ⊨ p›

AOT_theorem "thm-null-trivial:1": ‹∃!x NullSituation(x)›
proof (AOT_subst ‹NullSituation(x)› ‹A!x & ∀F (x[F] ≡ F ≠ F)› for: x)
  AOT_modally_strict {
    AOT_show ‹NullSituation(x) ≡ A!x & ∀F (x[F] ≡ F ≠ F)› for x
    proof (safe intro!: "≡I" "→I" "df-null-trivial:1"[THEN "≡_dfI"]
                dest!: "df-null-trivial:1"[THEN "≡_dfE"])
      AOT_assume 0: ‹Situation(x) & ¬∃p x ⊨ p›
      AOT_have 1: ‹A!x›
        using 0[THEN "&E"(1), THEN situations[THEN "≡_dfE"], THEN "&E"(1)].
      AOT_have 2: ‹x[F] → ∃p F = [λy p]› for F
        using 0[THEN "&E"(1), THEN situations[THEN "≡_dfE"],
                THEN "&E"(2), THEN "∀E"(2)]
        by (metis "≡_dfE" "→I" "prop-prop1" "→E")
      AOT_show ‹A!x & ∀F (x[F] ≡ F ≠ F)›
      proof (safe intro!: "&I" 1 GEN "≡I" "→I")
        fix F
        AOT_assume ‹x[F]›
        moreover AOT_obtain p where ‹F = [λy p]›
          using calculation 2[THEN "→E"] "∃E"[rotated] by blast
        ultimately AOT_have ‹x[λy p]›
          by (metis "rule=E")
        AOT_hence ‹x ⊨ p›
          using lem1[THEN "→E", OF 0[THEN "&E"(1)], THEN "≡E"(2)] by blast
        AOT_hence ‹∃p (x ⊨ p)›
          by (rule "∃I")
        AOT_thus ‹F ≠ F›
          using 0[THEN "&E"(2)] "raa-cor:1" "&I" by blast
      next
        fix F :: ‹<\<kappa>> AOT_var›
        AOT_assume ‹F ≠ F›
        AOT_hence ‹¬(F = F)› by (metis "≡_dfE" "=-infix")
        moreover AOT_have ‹F = F›
          by (simp add: "id-eq:1")
        ultimately AOT_show ‹x[F]› using "&I" "raa-cor:1" by blast
      qed
    next
      AOT_assume 0: ‹A!x & ∀F (x[F] ≡ F ≠ F)›
      AOT_hence ‹x[F] ≡ F ≠ F› for F
        using "∀E" "&E" by blast
      AOT_hence 1: ‹¬x[F]› for F
        using "≡_dfE" "id-eq:1" "=-infix" "reductio-aa:1" "≡E"(1) by blast
      AOT_show ‹Situation(x) & ¬∃p x ⊨ p›
      proof (safe intro!: "&I" situations[THEN "≡_dfI"] 0[THEN "&E"(1)] GEN "→I")
        AOT_show ‹Propositional([F])› if ‹x[F]› for F
          using that 1 "&I" "raa-cor:1" by fast
      next
        AOT_show ‹¬∃p x ⊨ p›
        proof(rule "raa-cor:2")
          AOT_assume ‹∃p x ⊨ p›
          then AOT_obtain p where ‹x ⊨ p› using "∃E"[rotated] by blast
          AOT_hence ‹x[λy p]›
            using "≡_dfE" "&E"(1) "≡E"(1) lem1 "modus-tollens:1"
                  "raa-cor:3" "true-in-s" by fast
          moreover AOT_have ‹¬x[λy p]›
            by (rule 1[unvarify F]) "cqt:2[lambda]"
          ultimately AOT_show ‹p & ¬p› for p using "&I" "raa-cor:1" by blast
        qed
      qed
    qed
  }
next
  AOT_show ‹∃!x ([A!]x & ∀F (x[F] ≡ F ≠ F))›
    by (simp add: "A-objects!")
qed


AOT_theorem "thm-null-trivial:2": ‹∃!x TrivialSituation(x)›
proof (AOT_subst ‹TrivialSituation(x)› ‹A!x & ∀F (x[F] ≡ ∃p F = [λy p])› for: x)
  AOT_modally_strict {
    AOT_show ‹TrivialSituation(x) ≡ A!x & ∀F (x[F] ≡ ∃p F = [λy p])› for x
    proof (safe intro!: "≡I" "→I" "df-null-trivial:2"[THEN "≡_dfI"]
                 dest!: "df-null-trivial:2"[THEN "≡_dfE"])
      AOT_assume 0: ‹Situation(x) & ∀p x ⊨ p›
      AOT_have 1: ‹A!x›
        using 0[THEN "&E"(1), THEN situations[THEN "≡_dfE"], THEN "&E"(1)].
      AOT_have 2: ‹x[F] → ∃p F = [λy p]› for F
        using 0[THEN "&E"(1), THEN situations[THEN "≡_dfE"],
                THEN "&E"(2), THEN "∀E"(2)]
        by (metis "≡_dfE" "deduction-theorem" "prop-prop1" "→E")
      AOT_show ‹A!x & ∀F (x[F] ≡ ∃p F = [λy p])›
      proof (safe intro!: "&I" 1 GEN "≡I" "→I" 2)
        fix F
        AOT_assume ‹∃p F = [λy p]›
        then AOT_obtain p where ‹F = [λy p]›
          using "∃E"[rotated] by blast
        moreover AOT_have ‹x ⊨ p›
          using 0[THEN "&E"(2)] "∀E" by blast
        ultimately AOT_show ‹x[F]›
          by (metis 0 "rule=E" "&E"(1) id_sym "≡E"(2) lem1
                    "Commutativity of ≡" "→E")
      qed
    next
      AOT_assume 0: ‹A!x & ∀F (x[F] ≡ ∃p F = [λy p])›
      AOT_hence 1: ‹x[F] ≡ ∃p F = [λy p]› for F
        using "∀E" "&E" by blast
      AOT_have 2: ‹Situation(x)›
      proof (safe intro!: "&I" situations[THEN "≡_dfI"] 0[THEN "&E"(1)] GEN "→I")
        AOT_show ‹Propositional([F])› if ‹x[F]› for F
          using 1[THEN "≡E"(1), OF that]
          by (metis "≡_dfI" "prop-prop1")
      qed
      AOT_show ‹Situation(x) & ∀p (x ⊨ p)›
      proof (safe intro!: "&I" 2 0[THEN "&E"(1)] GEN "→I")
        AOT_have ‹x[λy p] ≡ ∃q [λy p] = [λy q]› for p
          by (rule 1[unvarify F, where τ="«[λy p]¬"]) "cqt:2[lambda]"
        moreover AOT_have ‹∃q [λy p] = [λy q]› for p
          by (rule "∃I"(2)[where β=p])
             (simp add: "rule=I:1" "prop-prop2:2")
        ultimately AOT_have ‹x[λy p]› for p by (metis "≡E"(2))
        AOT_thus ‹x ⊨ p› for p
          by (metis "2" "≡E"(2) lem1 "→E")
      qed
    qed
  }
next
  AOT_show ‹∃!x ([A!]x & ∀F (x[F] ≡ ∃p F = [λy p]))›
    by (simp add: "A-objects!")
qed

AOT_theorem "thm-null-trivial:3": ‹\ιx NullSituation(x)↓›
  by (meson "A-Exists:2" "RA[2]" "≡E"(2) "thm-null-trivial:1")

AOT_theorem "thm-null-trivial:4": ‹\ιx TrivialSituation(x)↓›
  using "A-Exists:2" "RA[2]" "≡E"(2) "thm-null-trivial:2" by blast

AOT_define TheNullSituation :: ‹κ_s› (‹s_\∅›)
  "df-the-null-sit:1": ‹s_\∅ =_df \ιx NullSituation(x)›

AOT_define TheTrivialSituation :: ‹κ_s› (‹s_V›)
  "df-the-null-sit:2": ‹s_V =_df \ιx TrivialSituation(x)›

AOT_theorem "null-triv-sc:1": ‹NullSituation(x) → ◻NullSituation(x)›
proof(safe intro!: "→I" dest!: "df-null-trivial:1"[THEN "≡_dfE"];
      frule "&E"(1); drule "&E"(2))
  AOT_assume 1: ‹¬∃p (x ⊨ p)›
  AOT_assume 0: ‹Situation(x)›
  AOT_hence ‹◻Situation(x)› by (metis "≡E"(1) "possit-sit:1")
  moreover AOT_have ‹◻¬∃p (x ⊨ p)›
  proof(rule "raa-cor:1")
    AOT_assume ‹¬◻¬∃p (x ⊨ p)›
    AOT_hence ‹♢∃p (x ⊨ p)›
      by (metis "≡_dfI" "conventions:5")
    AOT_hence ‹∃p ♢(x ⊨ p)› by (metis "BF♢" "→E")
    then AOT_obtain p where ‹♢(x ⊨ p)› using "∃E"[rotated] by blast
    AOT_hence ‹x ⊨ p›
      by (metis "≡E"(1) "lem2:2"[unconstrain s, THEN "→E", OF 0])
    AOT_hence ‹∃p x ⊨ p› using "∃I" by fast
    AOT_thus ‹∃p x ⊨ p & ¬∃p x ⊨ p› using 1 "&I" by blast
  qed
  ultimately AOT_have 2: ‹◻(Situation(x) & ¬∃p x ⊨ p)›
    by (metis "KBasic:3" "&I" "≡E"(2))
  AOT_show ‹◻NullSituation(x)›
    by (AOT_subst ‹NullSituation(x)› ‹Situation(x) & ¬∃p x ⊨ p›)
       (auto simp: "df-null-trivial:1" "≡Df" 2)
qed


AOT_theorem "null-triv-sc:2": ‹TrivialSituation(x) → ◻TrivialSituation(x)›
proof(safe intro!: "→I" dest!: "df-null-trivial:2"[THEN "≡_dfE"];
      frule "&E"(1); drule "&E"(2))
  AOT_assume 0: ‹Situation(x)›
  AOT_hence 1: ‹◻Situation(x)› by (metis "≡E"(1) "possit-sit:1")
  AOT_assume ‹∀p x ⊨ p›
  AOT_hence ‹x ⊨ p› for p
    using "∀E" by blast
  AOT_hence ‹◻x ⊨ p› for p
    using  0 "≡E"(1) "lem2:1"[unconstrain s, THEN "→E"] by blast
  AOT_hence ‹∀p ◻x ⊨ p›
    by (rule GEN)
  AOT_hence ‹◻∀p x ⊨ p›
    by (rule BF[THEN "→E"])
  AOT_hence 2: ‹◻(Situation(x) & ∀p x ⊨ p)›
    using 1 by (metis "KBasic:3" "&I" "≡E"(2))
  AOT_show ‹◻TrivialSituation(x)›
    by (AOT_subst ‹TrivialSituation(x)› ‹Situation(x) & ∀p x ⊨ p›)
       (auto simp: "df-null-trivial:2" "≡Df" 2)
qed

AOT_theorem "null-triv-sc:3": ‹NullSituation(s_\∅)›
  by (safe intro!: "df-the-null-sit:1"[THEN "=_dfI"(2)] "thm-null-trivial:3"
       "rule=I:1"[OF "thm-null-trivial:3"]
       "!box-desc:2"[THEN "→E", THEN "→E", rotated, OF "thm-null-trivial:1",
                     OF "∀I", OF "null-triv-sc:1", THEN "∀E"(1), THEN "→E"])

AOT_theorem "null-triv-sc:4": ‹TrivialSituation(s_V)›
  by (safe intro!: "df-the-null-sit:2"[THEN "=_dfI"(2)] "thm-null-trivial:4"
       "rule=I:1"[OF "thm-null-trivial:4"]
       "!box-desc:2"[THEN "→E", THEN "→E", rotated, OF "thm-null-trivial:2",
                     OF "∀I", OF "null-triv-sc:2", THEN "∀E"(1), THEN "→E"])

AOT_theorem "null-triv-facts:1": ‹NullSituation(x) ≡ Null(x)›
proof (safe intro!: "≡I" "→I" "df-null-uni:1"[THEN "≡_dfI"]
                    "df-null-trivial:1"[THEN "≡_dfI"]
            dest!: "df-null-uni:1"[THEN "≡_dfE"] "df-null-trivial:1"[THEN "≡_dfE"])
  AOT_assume 0: ‹Situation(x) & ¬∃p x ⊨ p›
  AOT_have 1: ‹x[F] → ∃p F = [λy p]› for F
    using 0[THEN "&E"(1), THEN situations[THEN "≡_dfE"], THEN "&E"(2), THEN "∀E"(2)]
    by (metis "≡_dfE" "deduction-theorem" "prop-prop1" "→E")
  AOT_show ‹A!x & ¬∃F x[F]›
  proof (safe intro!: "&I" 0[THEN "&E"(1), THEN situations[THEN "≡_dfE"],
                             THEN "&E"(1)];
         rule "raa-cor:2")
    AOT_assume ‹∃F x[F]›
    then AOT_obtain F where F_prop: ‹x[F]›
      using "∃E"[rotated] by blast
    AOT_hence ‹∃p F = [λy p]›
      using 1[THEN "→E"] by blast
    then AOT_obtain p where ‹F = [λy p]›
      using "∃E"[rotated] by blast
    AOT_hence ‹x[λy p]›
      by (metis "rule=E" F_prop)
    AOT_hence ‹x ⊨ p›
      using lem1[THEN "→E", OF 0[THEN "&E"(1)], THEN "≡E"(2)] by blast
    AOT_hence ‹∃p x ⊨ p›
      by (rule "∃I")
    AOT_thus ‹∃p x ⊨ p & ¬∃p x ⊨ p›
      using 0[THEN "&E"(2)] "&I" by blast
  qed
next
  AOT_assume 0: ‹A!x & ¬∃F x[F]›
  AOT_have ‹Situation(x)›
    apply (rule situations[THEN "≡_dfI", OF "&I", OF 0[THEN "&E"(1)]]; rule GEN)
    using 0[THEN "&E"(2)] by (metis "→I" "existential:2[const_var]" "raa-cor:3") 
  moreover AOT_have ‹¬∃p x ⊨ p›
  proof (rule "raa-cor:2")
    AOT_assume ‹∃p x ⊨ p›
    then AOT_obtain p where ‹x ⊨ p› by (metis "instantiation")
    AOT_hence ‹x[λy p]› by (metis "≡_dfE" "&E"(2) "prop-enc" "true-in-s")
    AOT_hence ‹∃F x[F]› by (rule "∃I") "cqt:2[lambda]"
    AOT_thus ‹∃F x[F] & ¬∃F x[F]› using 0[THEN "&E"(2)] "&I"</span> by blast
  qed
  ultimately AOT_show ‹Situation(x) & ¬∃p x ⊨ p› using "&I"span> by blast
qed

AOT_theorem "null-triv-facts:2": ‹s_\∅ = a_\∅›
  apply (rule "=_dfI"(2)[OF "df-the-null-sit:1"])
   apply (fact "thm-null-trivial:3")
  apply (rule "=_dfI"(2)[OF "df-null-uni-terms:1"])
   apply (fact "null-uni-uniq:3")
  apply (rule "equiv-desc-eq:3"[THEN "→E"])
  apply (rule "&I")
   apply (fact "thm-null-trivial:3")
  by (rule RN; rule GEN; rule "null-triv-facts:1")

AOT_theorem "null-triv-facts:3": ‹s_V ≠ a_V›
proof(rule "=-infix"[THEN "≡_dfI"])
  AOT_have ‹Universal(a_V)›
    by (simp add: "null-uni-facts:4")
  AOT_hence 0: ‹a_V[A!]›
    using "df-null-uni:2"[THEN "≡_dfE"] "&E" "∀E"(1)
    by (metis "cqt:5:a" "vdash-properties:10" "vdash-properties:1[2]")
  moreover AOT_have 1: ‹¬s_V[A!]›
  proof(rule "raa-cor:2")
    AOT_have ‹Situation(s_V)›
      using "≡_dfE" "&E"(1) "df-null-trivial:2" "null-triv-sc:4" by blast
    AOT_hence ‹∀F (s_V[F] → Propositional([F]))›
      by (metis "≡_dfE" "&E"(2) situations)
    moreover AOT_assume ‹s_V[A!]›
    ultimately AOT_have ‹Propositional(A!)›
      using "∀E"(1)[rotated, OF "oa-exist:2"] "→E" by blast
    AOT_thus ‹Propositional(A!) & ¬Propositional(A!)›
      using "prop-in-f:4:d" "&I" by blast
  qed
  AOT_show ‹¬(s_V = a_V)›
  proof (rule "raa-cor:2")
    AOT_assume ‹s_V = a_V›
    AOT_hence ‹s_V[A!]› using 0 "rule=E" id_sym by fast
    AOT_thus ‹s_V[A!] & ¬s_V[A!]› using 1 "&I" by blast
  qed
qed

definition ConditionOnPropositionalProperties :: ‹(<\<kappa>> → o) → bool› where
  "cond-prop": ‹ConditionOnPropositionalProperties ≡ λ φ . ∀ v .
 [v ⊨ ∀F (φ{F} → Propositional([F]))]›

syntax ConditionOnPropositionalProperties :: ‹id_position → AOT_prop›
  (‹CONDITION'_ON'_PROPOSITIONAL'_PROPERTIES'(_')›)

AOT_theorem "cond-prop[E]":
  assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
  shows ‹∀F (φ{F} → Propositional([F]))›
  using assms[unfolded "cond-prop"] by auto

AOT_theorem "cond-prop[I]":
  assumes ‹\⊨_\◻ ∀F (φ{F} → Propositional([F]))›
  shows ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
  using assms "cond-prop" by metis

AOT_theorem "pre-comp-sit":
  assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
  shows ‹(Situation(x) & ∀F (x[F] ≡ φ{F})) ≡ (A!x & tyle='font-size: 18px;'>∀F (x[F] ≡ φ{F}))›
proof(rule "≡I"; rule "→I")
  AOT_assume ‹Situation(x) & ∀F (x[F] ≡ φ{F})›
  AOT_thus ‹A!x & ∀F (x[F] ≡ φ{F})›
    using "&E" situations[THEN "≡_dfE"] "&I" by blast
next
  AOT_assume 0: ‹A!x & ∀F (x[F] ≡ φ{F})›
  AOT_show ‹Situation(x) & ∀F (x[F] ≡ φ{F})›
  proof (safe intro!: situations[THEN "≡_dfI"] "&I")
    AOT_show ‹A!x› using 0[THEN "&E"(1)].
  next
    AOT_show ‹∀F (x[F] → Propositional([F]))›
    proof(rule GEN; rule "→I")
      fix F
      AOT_assume ‹x[F]›
      AOT_hence ‹φ{F}›
        using 0[THEN "&E"(2)] "∀E" "≡E" by blast
      AOT_thus ‹Propositional([F])›
        using "cond-prop[E]"[OF assms] "∀E" "→E" by blast
    qed
  next
    AOT_show ‹∀F (x[F] ≡ φ{F})› using 0 "&E" by blast
  qed
qed

AOT_theorem "comp-sit:1":
  assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
  shows ‹∃s ∀F(s[F] ≡ φ{F})›
  by (AOT_subst ‹Situation(x) & ∀F(x[F] ≡ φ{F})› ‹A!x & n style='font-size: 18px;'>∀F (x[F] ≡ φ{F})› for: x)
     (auto simp: "pre-comp-sit"[OF assms] "A-objects"[where φ=φ, axiom_inst])

AOT_theorem "comp-sit:2":
  assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
  shows ‹∃!s ∀F(s[F] ≡ φ{F})›
  by (AOT_subst ‹Situation(x) & ∀F(x[F] ≡ φ{F})› ‹A!x & n style='font-size: 18px;'>∀F (x[F] ≡ φ{F})› for: x)
     (auto simp: assms "pre-comp-sit"  "pre-comp-sit"[OF assms] "A-objects!")

AOT_theorem "can-sit-desc:1":
  assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
  shows ‹\ιs(∀F (s[F] ≡ φ{F}))↓›
  using "comp-sit:2"[OF assms] "A-Exists:2" "RA[2]" "≡E"(2) by blast

AOT_theorem "can-sit-desc:2":
  assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
  shows ‹\ιs(∀F (s[F] ≡ φ{F})) = \ιx(A!x & ∀F (x[F] ≡ φ{F}))›
  by (auto intro!: "equiv-desc-eq:2"[THEN "→E", OF "&I",
                                     OF "can-sit-desc:1"[OF assms]]
                   "RA[2]" GEN "pre-comp-sit"[OF assms])

AOT_theorem "strict-sit":
  assumes ‹RIGID_CONDITION(φ)›
      and ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
    shows ‹y = \ιs(∀F (s[F] ≡ φ{F})) → ∀F (y[F] ≡ φ{F})›
  using "rule=E"[rotated, OF "can-sit-desc:2"[OF assms(2), symmetric]]
        "box-phi-a:2"[OF assms(1)] "→E" "→I" "&E" by fast

(* TODO: exercise (479) sit-lit *)

AOT_define actual :: ‹τ → φ› (‹Actual'(_')›)
  ‹Actual(s) ≡_df ∀p (s ⊨ p → p)›

AOT_theorem "act-and-not-pos": ‹∃s (Actual(s) & ♢¬Actual(s))›
proof -
  AOT_obtain q₁ where q₁_prop: ‹q₁ & ♢¬q₁›
    by (metis "≡_dfE" "instantiation" "cont-tf:1" "cont-tf-thm:1")
  AOT_have ‹∃s (∀F (s[F] ≡ F = [λy q₁]))›
  proof (safe intro!: "comp-sit:1" "cond-prop[I]" GEN "→I")
    AOT_modally_strict {
      AOT_show ‹Propositional([F])› if ‹F = [λy q₁]› for F
        using "≡_dfI" "existential:2[const_var]" "prop-prop1" that by fastforce
    }
  qed
  then AOT_obtain s₁ where s_prop: ‹∀F (s₁[F] ≡ F = [λy q₁])›
    using "Situation.∃E"[rotated] by meson
  AOT_have ‹Actual(s₁)›
  proof(safe intro!: actual[THEN "≡_dfI"] "&I" GEN "→I" s_prop Situation.ψ)
    fix p
    AOT_assume ‹s₁ ⊨ p›
    AOT_hence ‹s₁[λy p]›
      by (metis "≡_dfE" "&E"(2) "prop-enc" "true-in-s")
    AOT_hence ‹[λy p] = [λy q₁]›
      by (rule s_prop[THEN "∀E"(1), THEN "≡E"(1), rotated]) "cqt:2[lambda]"
    AOT_hence ‹p = q₁› by (metis "≡E"(2) "p-identity-thm2:3")
    AOT_thus ‹p› using q₁_prop[THEN "&E"(1)] "rule=E" id_sym by fast
  qed
  moreover AOT_have ‹♢¬Actual(s₁)›
  proof(rule "raa-cor:1"; drule "KBasic:12"[THEN "≡E"(2)])
    AOT_assume ‹◻Actual(s₁)›
    AOT_hence ‹◻(Situation(s₁) & ∀p (s₁ ⊨ p → p))›
      using actual[THEN "≡Df", THEN "conventions:3"[THEN "≡_dfE"],
                   THEN "&E"(1), THEN RM, THEN "→E"] by blast
    AOT_hence ‹◻∀p (s₁ ⊨ p → p)›
      by (metis "RM:1" "Conjunction Simplification"(2) "→E")
    AOT_hence ‹∀p ◻(s₁ ⊨ p → p)›
      by (metis "CBF" "vdash-properties:10")
    AOT_hence ‹◻(s₁ ⊨ q₁ → q₁)›
      using "∀E" by blast
    AOT_hence ‹◻s₁ ⊨ q₁ → ◻q₁›
      by (metis "→E" "qml:1" "vdash-properties:1[2]")
    moreover AOT_have ‹s₁ ⊨ q₁›
      using s_prop[THEN "∀E"(1), THEN "≡E"(2),
                   THEN lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)]]
            "rule=I:1" "prop-prop2:2" by blast
    ultimately AOT_have ‹◻q₁›
      using "≡_dfE" "&E"(1) "≡E"(1) "lem2:1" "true-in-s" "→E" by fast
    AOT_thus ‹♢¬q₁ & ¬♢¬q₁›
      using "KBasic:12"[THEN "≡E"(1)] q₁_prop[THEN "&E"(2)] "&I" by blast
  qed
  ultimately AOT_have ‹(Actual(s₁) & ♢¬Actual(s₁))›
    using s_prop "&I" by blast
  thus ?thesis
    by (rule "Situation.∃I")
qed

AOT_theorem "actual-s:1": ‹∃s Actual(s)›
proof -
  AOT_obtain s where ‹(Actual(s) & ♢¬Actual(s))›
    using "act-and-not-pos" "Situation.∃E"[rotated] by meson
  AOT_hence ‹Actual(s)› using "&E" "&I" by metis
  thus ?thesis by (rule "Situation.∃I")
qed

AOT_theorem "actual-s:2": ‹∃s ¬Actual(s)›
proof(rule "∃I"(1)[where τ=‹«s_V¬›]; (rule "&I")?)
  AOT_show ‹Situation(s_V)›
    using "≡_dfE" "&E"(1) "df-null-trivial:2" "null-triv-sc:4" by blast
next
  AOT_show ‹¬Actual(s_V)›
  proof(rule "raa-cor:2")
    AOT_assume 0: ‹Actual(s_V)›
    AOT_obtain p₁ where notp₁: ‹¬p₁›
      by (metis "∃E" "∃I"(1) "log-prop-prop:2" "non-contradiction")
    AOT_have ‹s_V ⊨ p₁›
      using "null-triv-sc:4"[THEN "≡_dfE"[OF "df-null-trivial:2"], THEN "&E"(2)]
            "∀E" by blast
    AOT_hence ‹p₁›
      using 0[THEN actual[THEN "≡_dfE"], THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
      by blast
    AOT_thus ‹p & ¬p› for p using notp₁ by (metis "raa-cor:3")
  qed
next
  AOT_show ‹s_V↓›
    using "df-the-null-sit:2" "rule-id-df:2:b[zero]" "thm-null-trivial:4" by blast
qed

AOT_theorem "actual-s:3": ‹∃p∀s(Actual(s) → ¬s ⊨ p)›
proof -
  AOT_obtain p₁ where notp₁: ‹¬p₁›
    by (metis "∃E" "∃I"(1) "log-prop-prop:2" "non-contradiction")
  AOT_have ‹∀s (Actual(s) → ¬(s ⊨ p₁))›
  proof (rule Situation.GEN; rule "→I"; rule "raa-cor:2")
    fix s
    AOT_assume ‹Actual(s)›
    moreover AOT_assume ‹s ⊨ p₁›
    ultimately AOT_have ‹p₁›
      using actual[THEN "≡_dfE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] by blast
    AOT_thus ‹p₁ & ¬p₁›
      using notp₁ "&I" by simp
  qed
  thus ?thesis by (rule "∃I")
qed

AOT_theorem comp:
  ‹∃s (s' ⊴ s & s'' ⊴ s & ∀s''' (s' ⊴ s''' & s'' ⊴ s''' → s ⊴ s'''))›
proof -
  have cond_prop: ‹ConditionOnPropositionalProperties (λ Π . «s'[Π] ∨ s''[Π]¬)›
  proof(safe intro!: "cond-prop[I]" GEN "oth-class-taut:8:c"[THEN "→E", THEN "→E"];
        rule "→I")
    AOT_modally_strict {
      fix F
      AOT_have ‹Situation(s')›
        by (simp add: Situation.restricted_var_condition)
      AOT_hence ‹s'[F] → Propositional([F])›
        using "situations"[THEN "≡_dfE", THEN "&E"(2), THEN "∀E"(2)] by blast
      moreover AOT_assume ‹s'[F]›
      ultimately AOT_show ‹Propositional([F])›
        using "→E" by blast
    }
  next
    AOT_modally_strict {
      fix F
      AOT_have ‹Situation(s'')›
        by (simp add: Situation.restricted_var_condition)
      AOT_hence ‹s''[F] → Propositional([F])›
        using "situations"[THEN "≡_dfE", THEN "&E"(2), THEN "∀E"(2)] by blast
      moreover AOT_assume ‹s''[F]›
      ultimately AOT_show ‹Propositional([F])›
        using "→E" by blast
    }
  qed
  AOT_obtain s₃ where θ: ‹∀F (s₃[F] ≡ s'[F] ∨ s''[F])›
    using "comp-sit:1"[OF cond_prop] "Situation.∃E"[rotated] by meson
  AOT_have ‹s' ⊴ s₃ & s'' ⊴ s₃ & ∀s''' (s' ⊴ s''' & s'' ⊴ s''' → s₃ ⊴ s''')›
  proof(safe intro!: "&I" "≡_dfI"[OF "true-in-s"] "≡_dfI"[OF "prop-enc"]
                     "Situation.GEN" "GEN"[where 'a=o] "→I"
                     "sit-part-whole"[THEN "≡_dfI"]
                     Situation.ψ "cqt:2[const_var]"[axiom_inst])
    fix p
    AOT_assume ‹s' ⊨ p›
    AOT_hence ‹s'[λx p]›
      by (metis "&E"(2) "prop-enc" "≡_dfE" "true-in-s")
    AOT_thus ‹s₃[λx p]›
      using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(2), OF "∨I"(1)] by blast
  next
    fix p
    AOT_assume ‹s'' ⊨ p›
    AOT_hence ‹s''[λx p]›
      by (metis "&E"(2) "prop-enc" "≡_dfE" "true-in-s")
    AOT_thus ‹s₃[λx p]›
      using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(2), OF "∨I"(2)] by blast
  next
    fix s p
    AOT_assume 0: ‹s' ⊴ s & s'' ⊴ s›
    AOT_assume ‹s₃ ⊨ p›
    AOT_hence ‹s₃[λx p]›
      by (metis "&E"(2) "prop-enc" "≡_dfE" "true-in-s")
    AOT_hence ‹s'[λx p] ∨ s''[λx p]›
      using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(1)] by blast
    moreover {
      AOT_assume ‹s'[λx p]›
      AOT_hence ‹s' ⊨ p›
        by (safe intro!: "prop-enc"[THEN "≡_dfI"] "true-in-s"[THEN "≡_dfI"] "&I"
                         Situation.ψ "cqt:2[const_var]"[axiom_inst])
      moreover AOT_have ‹s' ⊨ p → s ⊨ p›
        using "sit-part-whole"[THEN "≡_dfE", THEN "&E"(2)] 0[THEN "&E"(1)]
              "∀E"(2) by blast
      ultimately AOT_have ‹s ⊨ p›
        using "→E" by blast
      AOT_hence ‹s[λx p]›
        using "true-in-s"[THEN "≡_dfE"] "prop-enc"[THEN "≡_dfE"] "&E" by blast
    }
    moreover {
      AOT_assume ‹s''[λx p]›
      AOT_hence ‹s'' ⊨ p›
        by (safe intro!: "prop-enc"[THEN "≡_dfI"] "true-in-s"[THEN "≡_dfI"] "&I"
                         Situation.ψ "cqt:2[const_var]"[axiom_inst])
      moreover AOT_have ‹s'' ⊨ p → s ⊨ p›
        using "sit-part-whole"[THEN "≡_dfE", THEN "&E"(2)] 0[THEN "&E"(2)]
              "∀E"(2) by blast
      ultimately AOT_have ‹s ⊨ p›
        using "→E" by blast
      AOT_hence ‹s[λx p]›
        using "true-in-s"[THEN "≡_dfE"] "prop-enc"[THEN "≡_dfE"] "&E" by blast
    }
    ultimately AOT_show ‹s[λx p]›
      by (metis "∨E"(1) "→I")
  qed
  thus ?thesis
    using "Situation.∃I" by fast
qed

AOT_theorem "act-sit:1": ‹Actual(s) → (s ⊨ p → [λy p]s)›
proof (safe intro!: "→I")
  AOT_assume ‹Actual(s)›
  AOT_hence p if ‹s ⊨ p›
    using actual[THEN "≡_dfE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] that by blast
  moreover AOT_assume ‹s ⊨ p›
  ultimately AOT_have p by blast
  AOT_thus ‹[λy p]s›
    by (safe intro!: "β←C"(1) "cqt:2")
qed

AOT_theorem "act-sit:2":
  ‹(Actual(s') & Actual(s'')) → ∃x (Actual(x) & s' ⊴ x & s'' ⊴ x)›
proof(rule "→I"; frule "&E"(1); drule "&E"(2))
  AOT_assume act_s': ‹Actual(s')›
  AOT_assume act_s'': ‹Actual(s'')›
  have "cond-prop": ‹ConditionOnPropositionalProperties
 (λ Π . «∃p (Π = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))¬)›
  proof (safe intro!: "cond-prop[I]"  "∀I" "→I" "prop-prop1"[THEN "≡_dfI"])
    AOT_modally_strict {
      fix β
      AOT_assume ‹∃p (β = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))›
      then AOT_obtain p where ‹β = [λy p]› using "∃E"[rotated] "&E" by blast
      AOT_thus ‹∃p β = [λy p]› by (rule "∃I")
    }
  qed
  have rigid: ‹rigid_condition (λ Π . «∃p (Π = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))¬)›
  proof(safe intro!: "strict-can:1[I]" "→I" GEN)
    AOT_modally_strict {
      fix F
      AOT_assume ‹∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))›
      then AOT_obtain p₁ where p₁_prop: ‹F = [λy p₁] & (s' ⊨ p₁ ∨ s'' ⊨ p₁)›
        using "∃E"[rotated] by blast
      AOT_hence ‹◻(F = [λy p₁])›
        using "&E"(1) "id-nec:2" "vdash-properties:10" by blast
      moreover AOT_have ‹◻(s' ⊨ p₁ ∨ s'' ⊨ p₁)›
      proof(rule "∨E"; (rule "→I"; rule "KBasic:15"[THEN "→E"])?)
        AOT_show ‹s' ⊨ p₁ ∨ s'' ⊨ p₁› using p₁_prop "&E" by blast
      next
        AOT_show ‹◻s' ⊨ p₁ ∨ ◻s'' ⊨ p₁› if ‹s' ⊨ p₁›
          apply (rule "∨I"(1))
          using "≡_dfE" "&E"(1) "≡E"(1) "lem2:1" that "true-in-s" by blast
      next
        AOT_show ‹◻s' ⊨ p₁ ∨ ◻s'' ⊨ p₁› if ‹s'' ⊨ p₁›
          apply (rule "∨I"(2))
          using "≡_dfE" "&E"(1) "≡E"(1) "lem2:1" that "true-in-s" by blast
      qed
      ultimately AOT_have ‹◻(F = [λy p₁] & (s' ⊨ p₁ ∨ s'' ⊨ p₁))›
        by (metis "KBasic:3" "&I" "≡E"(2))
      AOT_hence ‹∃p ◻(F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))› by (rule "∃I")
      AOT_thus ‹◻∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))›
        using Buridan[THEN "→E"] by fast
    }
  qed

  AOT_have desc_den: ‹\ιs(∀F (s[F] ≡ ∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))))↓›
    by (rule "can-sit-desc:1"[OF "cond-prop"])
  AOT_obtain x₀
    where x₀_prop1: ‹x₀ = \ιs(∀F (s[F] ≡ ∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))))›
    by (metis (no_types, lifting) "∃E" "rule=I:1" desc_den "∃I"(1) id_sym)
  AOT_hence x₀_sit: ‹Situation(x₀)›
    using "actual-desc:3"[THEN "→E"] "Act-Basic:2" "&E"(1) "≡E"(1)
          "possit-sit:4" by blast

  AOT_have 1: ‹∀F (x₀[F] ≡ ∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p)))›
    using "strict-sit"[OF rigid, OF "cond-prop", THEN "→E", OF x₀_prop1].
  AOT_have 2: ‹(x₀ ⊨ p) ≡ (s' ⊨ p ∨ s'' ⊨ p)› for p
  proof (rule "≡I"; rule "→I")
    AOT_assume ‹x₀ ⊨ p›
    AOT_hence ‹x₀[λy p]› using lem1[THEN "→E", OF x₀_sit, THEN "≡E"(1)] by blast
    then AOT_obtain q where ‹[λy p] = [λy q] & (s' ⊨ q ∨ s'' ⊨ q)›
      using 1[THEN "∀E"(1)[where τ="«[λy p]¬"], OF "prop-prop2:2", THEN "≡E"(1)]
            "∃E"[rotated] by blast
    AOT_thus ‹s' ⊨ p ∨ s'' ⊨ p›
      by (metis "rule=E" "&E"(1) "&E"(2) "∨I"(1) "∨I"(2)
                "∨E"(1) "deduction-theorem" id_sym "≡E"(2) "p-identity-thm2:3")
  next
    AOT_assume ‹s' ⊨ p ∨ s'' ⊨ p›
    AOT_hence ‹[λy p] = [λy p] & (s' ⊨ p ∨ s'' ⊨ p)›
      by (metis "rule=I:1" "&I" "prop-prop2:2") 
    AOT_hence ‹∃q ([λy p] = [λy q] & (s' ⊨ q ∨ s'' ⊨ q))›
      by (rule "∃I")
    AOT_hence ‹x₀[λy p]›
      using 1[THEN "∀E"(1), OF "prop-prop2:2", THEN "≡E"(2)] by blast
    AOT_thus ‹x₀ ⊨ p›
      by (metis "≡_dfI" "&I" "ex:1:a" "prop-enc" "rule-ui:2[const_var]"
                x₀_sit "true-in-s")
  qed

  AOT_have ‹Actual(x₀) & s' ⊴ x₀ & s'' ⊴ x₀›
  proof(safe intro!: "→I" "&I" "∃I"(1) actual[THEN "≡_dfI"] x₀_sit GEN
                     "sit-part-whole"[THEN "≡_dfI"])
    fix p
    AOT_assume ‹x₀ ⊨ p›
    AOT_hence ‹s' ⊨ p ∨ s'' ⊨ p›
      using 2 "≡E"(1) by metis
    AOT_thus ‹p›
      using act_s' act_s''
            actual[THEN "≡_dfE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
      by (metis "∨E"(3) "reductio-aa:1")
  next
    AOT_show ‹x₀ ⊨ p› if ‹s' ⊨ p› for p
      using 2[THEN "≡E"(2), OF "∨I"(1), OF that].
  next
    AOT_show ‹x₀ ⊨ p› if ‹s'' ⊨ p› for p
      using 2[THEN "≡E"(2), OF "∨I"(2), OF that].
  next
    AOT_show ‹Situation(s')›
      using act_s'[THEN actual[THEN "≡_dfE"]] "&E" by blast
  next
    AOT_show ‹Situation(s'')›
      using act_s''[THEN actual[THEN "≡_dfE"]] "&E" by blast
  qed
  AOT_thus ‹∃x (Actual(x) & s' ⊴ x & s'' ⊴ x)›
    by (rule "∃I")
qed

AOT_define Consistent :: ‹τ → φ› (‹Consistent'(_')›)
  cons: ‹Consistent(s) ≡_df ¬∃p (s ⊨ p & s ⊨ ¬p)›

AOT_theorem "sit-cons": ‹Actual(s) → Consistent(s)›
proof(safe intro!: "→I" cons[THEN "≡_dfI"] "&I" Situation.ψ
            dest!: actual[THEN "≡_dfE"]; frule "&E"(1); drule "&E"(2))
  AOT_assume 0: ‹∀p (s ⊨ p → p)›
  AOT_show ‹¬∃p (s ⊨ p & s ⊨ ¬p)›
  proof (rule "raa-cor:2")
    AOT_assume ‹∃p (s ⊨ p & s ⊨ ¬p)›
    then AOT_obtain p where ‹s ⊨ p & s ⊨ ¬p›
      using "∃E"[rotated] by blast
    AOT_hence ‹p & ¬p›
      using 0[THEN "∀E"(1)[where τ=‹«¬p¬›, THEN "→E"], OF "log-prop-prop:2"]
            0[THEN "∀E"(2)[where β=p], THEN "→E"] "&E" "&I" by blast
    AOT_thus ‹p & ¬p› for p by (metis "raa-cor:1") 
  qed
qed

AOT_theorem "cons-rigid:1": ‹¬Consistent(s) ≡ ◻¬Consistent(s)›
proof (rule "≡I"; rule "→I")
  AOT_assume ‹¬Consistent(s)›
  AOT_hence ‹∃p (s ⊨ p & s ⊨ ¬p)›
    using cons[THEN "≡_dfI", OF "&I", OF Situation.ψ]
    by (metis "raa-cor:3")
  then AOT_obtain p where p_prop: ‹s ⊨ p & s ⊨ ¬p›
    using "∃E"[rotated] by blast
  AOT_hence ‹◻s ⊨ p›
    using "&E"(1) "≡E"(1) "lem2:1" by blast
  moreover AOT_have ‹◻s ⊨ ¬p›
    using p_prop "T♢" "&E" "≡E"(1)
      "modus-tollens:1" "raa-cor:3" "lem2:3"[unvarify p]
      "log-prop-prop:2" by metis
  ultimately AOT_have ‹◻(s ⊨ p & s ⊨ ¬p)›
    by (metis "KBasic:3" "&I" "≡E"(2))
  AOT_hence ‹∃p ◻(s ⊨ p & s ⊨ ¬p)›
    by (rule "∃I")
  AOT_hence ‹◻∃p(s ⊨ p & s ⊨ ¬p)›
    by (metis Buridan "vdash-properties:10") 
  AOT_thus ‹◻¬Consistent(s)›
    apply (rule "qml:1"[axiom_inst, THEN "→E", THEN "→E", rotated])
    apply (rule RN)
    using "≡_dfE" "&E"(2) cons "deduction-theorem" "raa-cor:3" by blast
next
  AOT_assume ‹◻¬Consistent(s)›
  AOT_thus ‹¬Consistent(s)› using "qml:2"[axiom_inst, THEN "→E"] by auto
qed

AOT_theorem "cons-rigid:2": ‹♢Consistent(x) ≡ Consistent(x)›
proof(rule "≡I"; rule "→I")
  AOT_assume 0: ‹♢Consistent(x)›
  AOT_have ‹♢(Situation(x) & ¬∃p (x ⊨ p & x ⊨ ¬p))›
    apply (AOT_subst ‹Situation(x) & ¬∃p (x ⊨ p & x ='font-size: 18px;'>⊨ ¬p)› ‹Consistent(x)›)
     using cons "≡E"(2) "Commutativity of ≡" "≡Df" apply blast
    by (simp add: 0)
  AOT_hence ‹♢Situation(x)› and 1: ‹♢¬∃p (x ⊨ p & x ⊨ ¬p)›
    using "RM♢" "Conjunction Simplification"(1) "Conjunction Simplification"(2)
          "modus-tollens:1" "raa-cor:3" by blast+
  AOT_hence 2: ‹Situation(x)› by (metis "≡E"(1) "possit-sit:2")
  AOT_have 3: ‹¬◻∃p (x ⊨ p & x ⊨ ¬p)›
    using 2 using 1 "KBasic:11" "≡E"(2) by blast
  AOT_show ‹Consistent(x)›
  proof (rule "raa-cor:1")
    AOT_assume ‹¬Consistent(x)›
    AOT_hence ‹∃p (x ⊨ p & x ⊨ ¬p)›
      using 0 "≡_dfE" "conventions:5" 2 "cons-rigid:1"[unconstrain s, THEN "→E"]
            "modus-tollens:1" "raa-cor:3" "≡E"(4) by meson
    then AOT_obtain p where ‹x ⊨ p› and 4: ‹x ⊨ ¬p›
      using "∃E"[rotated] "&E" by blast
    AOT_hence ‹◻x ⊨ p›
      by (metis "2" "≡E"(1) "lem2:1"[unconstrain s, THEN "→E"])
    moreover AOT_have ‹◻x ⊨ ¬p›
      using 4 "lem2:1"[unconstrain s, unvarify p, THEN "→E"]
      by (metis 2 "≡E"(1) "log-prop-prop:2")
    ultimately AOT_have ‹◻(x ⊨ p & x ⊨ ¬p)›
      by (metis "KBasic:3" "&I" "≡E"(3) "raa-cor:3")
    AOT_hence ‹∃p ◻(x ⊨ p & x ⊨ ¬p)›
      by (metis "existential:1" "log-prop-prop:2")
    AOT_hence ‹◻∃p (x ⊨ p & x ⊨ ¬p)›
      by (metis Buridan "vdash-properties:10")
    AOT_thus ‹p & ¬p› for p
      using 3 "&I"  by (metis "raa-cor:3")
  qed
next
  AOT_show ‹♢Consistent(x)› if ‹Consistent(x)›
    using "T♢" that "vdash-properties:10" by blast
qed

AOT_define possible :: ‹τ → φ› (‹Possible'(_')›)
  pos: ‹Possible(s) ≡_df ♢Actual(s)›

AOT_theorem "sit-pos:1": ‹Actual(s) → Possible(s)›
  apply(rule "→I"; rule pos[THEN "≡_dfI"]; rule "&I")
  apply (meson "≡_dfE" actual "&E"(1))
  using "T♢" "vdash-properties:10" by blast

AOT_theorem "sit-pos:2": ‹∃p ((s ⊨ p) & ¬♢p) → ¬Possible(s)›
proof(rule "→I")
  AOT_assume ‹∃p ((s ⊨ p) & ¬♢p)›
  then AOT_obtain p where a: ‹(s ⊨ p) & ¬♢p›
    using "∃E"[rotated] by blast
  AOT_hence ‹◻(s ⊨ p)›
    using "&E" by (metis "T♢" "≡E"(1) "lem2:3" "vdash-properties:10")
  moreover AOT_have ‹◻¬p›
    using a[THEN "&E"(2)] by (metis "KBasic2:1" "≡E"(2))
  ultimately AOT_have ‹◻(s ⊨ p & ¬p)›
    by (metis "KBasic:3" "&I" "≡E"(3) "raa-cor:3")
  AOT_hence ‹∃p ◻(s ⊨ p & ¬p)›
    by (rule "∃I")
  AOT_hence 1: ‹◻∃q (s ⊨ q & ¬q)›
    by (metis Buridan "vdash-properties:10")
  AOT_have ‹◻¬∀q (s ⊨ q → q)›
    apply (AOT_subst ‹s ⊨ q → q› ‹¬(s ⊨ q & ¬q)› for: q)
     apply (simp add: "oth-class-taut:1:a")
    apply (AOT_subst ‹¬∀q ¬(s ⊨ q & ¬q)› ‹∃q (s ⊨ q & tyle='font-size: 18px;'>¬q)›)
    by (auto simp: "conventions:4" "df-rules-formulas[3]" "df-rules-formulas[4]" "≡I" 1)
  AOT_hence 0: ‹¬♢∀q (s ⊨ q → q)›
    by (metis "≡_dfE" "conventions:5" "raa-cor:3")
  AOT_show ‹¬Possible(s)›
    apply (AOT_subst ‹Possible(s)› ‹Situation(s) & ♢Actual(s)›)
     apply (simp add: pos "≡Df")
    apply (AOT_subst ‹Actual(s)› ‹Situation(s) & ∀q (s ⊨ q → q)›)
     using actual "≡Df" apply presburger
    by (metis "0" "KBasic2:3" "&E"(2) "raa-cor:3" "vdash-properties:10")
qed

AOT_theorem "pos-cons-sit:1": ‹Possible(s) → Consistent(s)›
  by (auto simp: "sit-cons"[THEN "RM♢", THEN "→E",
                            THEN "cons-rigid:2"[THEN "≡E"(1)]]
           intro!: "→I" dest!: pos[THEN "≡_dfE"] "&E"(2))

AOT_theorem "pos-cons-sit:2": ‹∃s (Consistent(s) & ¬Possible(s))›
proof -
  AOT_obtain q₁ where ‹q₁ & ♢¬q₁›
    using "≡_dfE" "instantiation" "cont-tf:1" "cont-tf-thm:1" by blast
  have "cond-prop": ‹ConditionOnPropositionalProperties
 (λ Π . «Π = [λy q₁ & ¬q₁]¬)›
    by (auto intro!: "cond-prop[I]" GEN "→I" "prop-prop1"[THEN "≡_dfI"]
                     "∃I"(1)[where τ=‹«q₁ & ¬q₁¬›, rotated, OF "log-prop-prop:2"])
  have rigid: ‹rigid_condition (λ Π . «Π = [λy q₁ & ¬q₁]¬)›
    by (auto intro!: "strict-can:1[I]" GEN "→I" simp: "id-nec:2"[THEN "→E"])

  AOT_obtain x where x_prop: ‹x = \ιs (∀F (s[F] ≡ F = [λy q₁ & ¬q₁]))›
    using "ex:1:b"[THEN "∀E"(1), OF "can-sit-desc:1", OF "cond-prop"]
          "∃E"[rotated] by blast    
  AOT_hence 0: ‹\A(Situation(x) & ∀F (x[F] ≡ F = [λy q₁ & pan style='font-size: 18px;'>¬q₁]))›
    using "→E" "actual-desc:2" by blast
  AOT_hence ‹\A(Situation(x))› by (metis "Act-Basic:2" "&E"(1) "≡E"(1))
  AOT_hence s_sit: ‹Situation(x)› by (metis "≡E"(1) "possit-sit:4")
  AOT_have s_enc_prop: ‹∀F (x[F] ≡ F = [λy q₁ & ¬q₁])›
    using "strict-sit"[OF rigid, OF "cond-prop", THEN "→E", OF x_prop].
  AOT_hence ‹x[λy q₁ & ¬q₁]›
    using "∀E"(1)[rotated, OF "prop-prop2:2"]
          "rule=I:1"[OF "prop-prop2:2"] "≡E" by blast
  AOT_hence ‹x ⊨ (q₁ & ¬q₁)›
    using lem1[THEN "→E", OF s_sit, unvarify p, THEN "≡E"(2), OF "log-prop-prop:2"]
    by blast
  AOT_hence ‹◻(x ⊨ (q₁ & ¬q₁))›
    using "lem2:1"[unconstrain s, THEN "→E", OF s_sit, unvarify p,
                   OF "log-prop-prop:2", THEN "≡E"(1)] by blast
  moreover AOT_have ‹◻(x ⊨ (q₁ & ¬q₁) → ¬Actual(x))›
  proof(rule RN; rule "→I"; rule "raa-cor:2")
    AOT_modally_strict {
      AOT_assume ‹Actual(x)›
      AOT_hence ‹∀p (x ⊨ p → p)›
        using actual[THEN "≡_dfE", THEN "&E"(2)] by blast
      moreover AOT_assume ‹x ⊨ (q₁ & ¬q₁)›
      ultimately AOT_show ‹q₁ & ¬q₁›
        using "∀E"(1)[rotated, OF "log-prop-prop:2"] "→E" by metis
    }
  qed
  ultimately AOT_have nec_not_actual_s: ‹◻¬Actual(x)›
    using "qml:1"[axiom_inst, THEN "→E", THEN "→E"] by blast
  AOT_have 1: ‹¬∃p (x ⊨ p & x ⊨ ¬p)›
  proof (rule "raa-cor:2")
    AOT_assume ‹∃p (x ⊨ p & x ⊨ ¬p)›
    then AOT_obtain p where ‹x ⊨ p & x ⊨ ¬p›
      using "∃E"[rotated] by blast
    AOT_hence ‹x[λy p] & x[λy ¬p]›
      using lem1[unvarify p, THEN "→E", OF "log-prop-prop:2",
                 OF s_sit, THEN "≡E"(1)] "&I" "&E" by metis
    AOT_hence ‹[λy p] = [λy q₁ & ¬q₁]› and ‹[λy ¬p] = [λy q₁ & pan style='font-size: 18px;'>¬q₁]›
      by (auto intro!: "prop-prop2:2" s_enc_prop[THEN "∀E"(1), THEN "≡E"(1)]
               elim: "&E")
    AOT_hence i: ‹[λy p] = [λy ¬p]› by (metis "rule=E" id_sym)
    {
      AOT_assume 0: ‹p›
      AOT_have ‹[λy p]x› for x
        by (auto intro!: "β←C"(1) "cqt:2" 0)
      AOT_hence ‹[λy ¬p]x› for x using i "rule=E" by fast
      AOT_hence ‹¬p›
        using "β→C"(1) by auto
    }
    moreover {
      AOT_assume 0: ‹¬p›
      AOT_have ‹[λy ¬p]x› for x
        by (auto intro!: "β←C"(1) "cqt:2" 0)
      AOT_hence ‹[λy p]x› for x using i[symmetric] "rule=E" by fast
      AOT_hence ‹p›
        using "β→C"(1) by auto
    }
    ultimately AOT_show ‹p & ¬p› for p by (metis "raa-cor:1" "raa-cor:3")
  qed
  AOT_have 2: ‹¬Possible(x)›
  proof(rule "raa-cor:2")
    AOT_assume ‹Possible(x)›
    AOT_hence ‹♢Actual(x)›
      by (metis "≡_dfE" "&E"(2) pos)
    moreover AOT_have ‹¬♢Actual(x)› using nec_not_actual_s
      using "≡_dfE" "conventions:5" "reductio-aa:2" by blast
    ultimately AOT_show ‹♢Actual(x) & ¬♢Actual(x)› by (rule "&I")
  qed
  show ?thesis
    by(rule "∃I"(2)[where β=x]; safe intro!: "&I" 2 s_sit cons[THEN "≡_dfI"] 1)
qed

AOT_theorem "sit-classical:1": ‹∀p (s ⊨ p ≡ p) → ∀q(s ⊨ ¬q ≡ ¬s ⊨ q)›
proof(rule "→I"; rule GEN)
  fix q
  AOT_assume ‹∀p (s ⊨ p ≡ p)›
  AOT_hence ‹s ⊨ q ≡ q› and ‹s ⊨ ¬q ≡ ¬q›
    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
  AOT_thus ‹s ⊨ ¬q ≡ ¬s ⊨ q›
    by (metis "deduction-theorem" "≡I" "≡E"(1) "≡E"(2) "≡E"(4))
qed

AOT_theorem "sit-classical:2":
  ‹∀p (s ⊨ p ≡ p) → ∀q∀r((s ⊨ (q → r)) ≡ (s ⊨ q → s ⊨ r))›
proof(rule "→I"; rule GEN; rule GEN)
  fix q r
  AOT_assume ‹∀p (s ⊨ p ≡ p)›
  AOT_hence θ: ‹s ⊨ q ≡ q› and ξ: ‹s ⊨ r ≡ r› and ζ: ‹(s ⊨ (q → r)) ≡ (q → r)›
    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
  AOT_show ‹(s ⊨ (q → r)) ≡ (s ⊨ q → s ⊨ r)›
  proof (safe intro!: "≡I" "→I")
    AOT_assume ‹s ⊨ (q → r)›
    moreover AOT_assume ‹s ⊨ q›
    ultimately AOT_show ‹s ⊨ r›
      using θ ξ ζ by (metis "≡E"(1) "≡E"(2) "vdash-properties:10")
  next
    AOT_assume ‹s ⊨ q → s ⊨ r›
    AOT_thus ‹s ⊨ (q → r)›
      using θ ξ ζ by (metis "deduction-theorem" "≡E"(1) "≡E"(2) "→E") 
  qed
qed

AOT_theorem "sit-classical:3":
  ‹∀p (s ⊨ p ≡ p) → ((s ⊨ ∀α φ{α}) ≡ ∀α s ⊨ φ{α})›
proof (rule "→I")
  AOT_assume ‹∀p (s ⊨ p ≡ p)›
  AOT_hence θ: ‹s ⊨ φ{α} ≡ φ{α}› and ξ: ‹s ⊨ ∀α φ{α} ≡ ∀α φ{α}› for α
    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
  AOT_show ‹s ⊨ ∀α φ{α} ≡ ∀α s ⊨ φ{α}›
  proof (safe intro!: "≡I" "→I" GEN)
    fix α
    AOT_assume ‹s ⊨ ∀α φ{α}›
    AOT_hence ‹φ{α}› using ξ "∀E"(2) "≡E"(1) by blast
    AOT_thus ‹s ⊨ φ{α}› using θ "≡E"(2) by blast
  next
    AOT_assume ‹∀α s ⊨ φ{α}›
    AOT_hence ‹s ⊨ φ{α}› for α using "∀E"(2) by blast
    AOT_hence ‹φ{α}› for α using θ "≡E"(1) by blast
    AOT_hence ‹∀α φ{α}› by (rule GEN)
    AOT_thus ‹s ⊨ ∀α φ{α}› using ξ "≡E"(2) by blast
  qed
qed

AOT_theorem "sit-classical:4": ‹∀p (s ⊨ p ≡ p) → ∀q (s ⊨ ◻q → ◻s ⊨ q)›
proof(rule "→I"; rule GEN; rule "→I")
  fix q
  AOT_assume ‹∀p (s ⊨ p ≡ p)›
  AOT_hence θ: ‹s ⊨ q ≡ q› and ξ: ‹s ⊨ ◻q ≡ ◻q›
    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
  AOT_assume ‹s ⊨ ◻q›
  AOT_hence ‹◻q› using ξ "≡E"(1) by blast
  AOT_hence ‹q› using "qml:2"[axiom_inst, THEN "→E"] by blast
  AOT_hence ‹s ⊨ q› using θ "≡E"(2) by blast
  AOT_thus ‹◻s ⊨ q› using "≡_dfE" "&E"(1) "≡E"(1) "lem2:1" "true-in-s" by blast
qed

AOT_theorem "sit-classical:5":
  ‹∀p (s ⊨ p ≡ p) → ∃q(◻(s ⊨ q) & ¬(s ⊨ ◻ q))›
proof (rule "→I")
  AOT_obtain r where A: ‹r› and ‹♢¬r›
    by (metis "&E"(1) "&E"(2) "≡_dfE" "instantiation" "cont-tf:1" "cont-tf-thm:1")
  AOT_hence B: ‹¬◻r›
    using "KBasic:11" "≡E"(2) by blast
  moreover AOT_assume asm: ‹∀ p (s ⊨ p ≡ p)›
  AOT_hence ‹s ⊨ r›
    using "∀E"(2) A "≡E"(2) by blast
  AOT_hence 1: ‹◻s ⊨ r›
    using "≡_dfE" "&E"(1) "≡E"(1) "lem2:1" "true-in-s" by blast
  AOT_have ‹s ⊨ ¬◻r›
    using asm[THEN "∀E"(1)[rotated, OF "log-prop-prop:2"], THEN "≡E"(2)] B by blast
  AOT_hence ‹¬s ⊨ ◻r›
    using "sit-classical:1"[THEN "→E", OF asm,
              THEN "∀E"(1)[rotated, OF "log-prop-prop:2"], THEN "≡E"(1)] by blast
  AOT_hence ‹◻s ⊨ r & ¬s ⊨ ◻r›
    using 1 "&I" by blast
  AOT_thus ‹∃r (◻s ⊨ r & ¬s ⊨ ◻r)›
    by (rule "∃I")
qed

AOT_theorem "sit-classical:6":
  ‹∃s ∀p (s ⊨ p ≡ p)›
proof -
  have "cond-prop": ‹ConditionOnPropositionalProperties
 (λ Π . «∃q (q & Π = [λy q])¬)›
  proof (safe intro!: "cond-prop[I]" GEN "→I")
    fix F
    AOT_modally_strict {
      AOT_assume ‹∃q (q & F = [λy q])›
      then AOT_obtain q where ‹q & F = [λy q]›
        using "∃E"[rotated] by blast
      AOT_hence ‹F = [λy q]›
        using "&E" by blast
      AOT_hence ‹∃q F = [λy q]›
        by (rule "∃I")
      AOT_thus ‹Propositional([F])›
        by (metis "≡_dfI" "prop-prop1")
    }
  qed
  AOT_have ‹∃s ∀F (s[F] ≡ ∃q (q & F = [λy q]))›
    using "comp-sit:1"[OF "cond-prop"].
  then AOT_obtain s₀ where s₀_prop: ‹∀F (s₀[F] ≡ ∃q (q & F = [λy q]))›
    using "Situation.∃E"[rotated] by meson
  AOT_have ‹∀p (s₀ ⊨ p ≡ p)›
  proof(safe intro!: GEN "≡I" "→I")
    fix p
    AOT_assume ‹s₀ ⊨ p›
    AOT_hence ‹s₀[λy p]›
      using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(1)] by blast
    AOT_hence ‹∃q (q & [λy p] = [λy q])›
      using s₀_prop[THEN "∀E"(1)[rotated, OF "prop-prop2:2"], THEN "≡E"(1)] by blast
    then AOT_obtain q₁ where q₁_prop: ‹q₁ & [λy p] = [λy q₁]›
      using "∃E"[rotated] by blast
    AOT_hence ‹p = q₁›
      by (metis "&E"(2) "≡E"(2) "p-identity-thm2:3")
    AOT_thus ‹p›
      using q₁_prop[THEN "&E"(1)] "rule=E" id_sym by fast
  next
    fix p
    AOT_assume ‹p›
    moreover AOT_have ‹[λy p] = [λy p]›
      by (simp add: "rule=I:1"[OF "prop-prop2:2"])
    ultimately AOT_have ‹p & [λy p] = [λy p]›
      using "&I" by blast
    AOT_hence ‹∃q (q & [λy p] = [λy q])›
      by (rule "∃I")
    AOT_hence ‹s₀[λy p]›
      using s₀_prop[THEN "∀E"(1)[rotated, OF "prop-prop2:2"], THEN "≡E"(2)] by blast
    AOT_thus ‹s₀ ⊨ p›
      using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)] by blast
  qed
  AOT_hence ‹∀p (s₀ ⊨ p ≡ p)›
    using "&I" by blast
  AOT_thus ‹∃s ∀p (s ⊨ p ≡ p)›
    by (rule "Situation.∃I")
qed

AOT_define PossibleWorld :: ‹τ → φ› (‹PossibleWorld'(_')›)
  "world:1": ‹PossibleWorld(x) ≡_df Situation(x) & ♢∀p(x ⊨ p ≡ p)›

AOT_theorem "world:2": ‹∃x PossibleWorld(x)›
proof -
  AOT_obtain s where s_prop: ‹∀p (s ⊨ p ≡ p)›
    using "sit-classical:6" "Situation.∃E"[rotated] by meson
  AOT_have ‹∀p (s ⊨ p ≡ p)›
  proof(safe intro!: GEN "≡I" "→I")
    fix p
    AOT_assume ‹s ⊨ p›
    AOT_thus ‹p›
      using s_prop[THEN "∀E"(2), THEN "≡E"(1)] by blast
  next
    fix p
    AOT_assume ‹p›
    AOT_thus ‹s ⊨ p›
      using s_prop[THEN "∀E"(2), THEN "≡E"(2)] by blast
  qed
  AOT_hence ‹♢∀p (s ⊨ p ≡ p)›
    by (metis "T♢"[THEN "→E"])
  AOT_hence ‹♢∀p (s ⊨ p ≡ p)›
    using s_prop "&I" by blast
  AOT_hence ‹PossibleWorld(s)›
    using "world:1"[THEN "≡_dfI"] Situation.ψ "&I" by blast
  AOT_thus ‹∃x PossibleWorld(x)›
    by (rule "∃I")
qed

AOT_theorem "world:3": ‹PossibleWorld(κ) → κ↓›
proof (rule "→I")
  AOT_assume ‹PossibleWorld(κ)›
  AOT_hence ‹Situation(κ)›
    using "world:1"[THEN "≡_dfE"] "&E" by blast
  AOT_hence ‹A!κ›
    by (metis "≡_dfE" "&E"(1) situations)
  AOT_thus ‹κ↓›
    by (metis "russell-axiom[exe,1].ψ_denotes_asm")
qed

AOT_theorem "rigid-pw:1": ‹PossibleWorld(x) ≡ ◻PossibleWorld(x)›
proof(safe intro!: "≡I" "→I")
  AOT_assume ‹PossibleWorld(x)›
  AOT_hence ‹Situation(x) & ♢∀p(x ⊨ p ≡ p)›
    using "world:1"[THEN "≡_dfE"] by blast
  AOT_hence ‹◻Situation(x) & ◻♢∀p(x ⊨ p ≡ p)›
    by (metis "S5Basic:1" "&I" "&E"(1) "&E"(2) "≡E"(1) "possit-sit:1")
  AOT_hence 0: ‹◻(Situation(x) & ♢∀p(x ⊨ p ≡ p))›
    by (metis "KBasic:3" "≡E"(2))
  AOT_show ‹◻PossibleWorld(x)›
    by (AOT_subst ‹PossibleWorld(x)› ‹Situation(x) & ♢∀p(x ⊨ p ≡ p)›)
       (auto simp: "≡Df" "world:1" 0)
next
  AOT_show ‹PossibleWorld(x)› if ‹◻PossibleWorld(x)›
    using that "qml:2"[axiom_inst, THEN "→E"] by blast
qed

AOT_theorem "rigid-pw:2": ‹♢PossibleWorld(x) ≡ PossibleWorld(x)›
  using "rigid-pw:1"
  by (meson "RE♢" "S5Basic:2" "≡E"(2) "≡E"(6) "Commutativity of ≡")

AOT_theorem "rigid-pw:3": ‹♢PossibleWorld(x) ≡ ◻PossibleWorld(x)›
  using "rigid-pw:1" "rigid-pw:2" by (meson "≡E"(5))

AOT_theorem "rigid-pw:4": ‹\APossibleWorld(x) ≡ PossibleWorld(x)›
  by (metis "Act-Sub:3" "→I" "≡I" "≡E"(6) "nec-imp-act" "rigid-pw:1" "rigid-pw:2")

AOT_register_rigid_restricted_type
  PossibleWorld: ‹PossibleWorld(κ)›
proof
  AOT_modally_strict {
    AOT_show ‹∃x PossibleWorld(x)› using "world:2".
  }
next
  AOT_modally_strict {
    AOT_show ‹PossibleWorld(κ) → κ↓› for κ using "world:3".
  }
next
  AOT_modally_strict {
    AOT_show ‹∀α(PossibleWorld(α) → ◻PossibleWorld(α))›
      by (meson GEN "→I" "≡E"(1) "rigid-pw:1")
  }
qed
AOT_register_variable_names
  PossibleWorld: w

AOT_theorem "world-pos": ‹Possible(w)›
proof (safe intro!: "≡_dfE"[OF "world:1", OF PossibleWorld.ψ, THEN "&E"(1)]
                    pos[THEN "≡_dfI"] "&I" )
  AOT_have ‹♢∀p (w ⊨ p ≡ p)›
    using "world:1"[THEN "≡_dfE", OF PossibleWorld.ψ, THEN "&E"(2)].
  AOT_hence ‹♢∀p (w ⊨ p → p)›
  proof (rule "RM♢"[THEN "→E", rotated]; safe intro!: "→I" GEN)
    AOT_modally_strict {
      fix p
      AOT_assume ‹∀p (w ⊨ p ≡ p)›
      AOT_hence ‹w ⊨ p ≡ p› using "∀E"(2) by blast
      moreover AOT_assume ‹w ⊨ p›
      ultimately AOT_show p using "≡E"(1) by blast
    }
  qed
  AOT_hence 0: ‹♢(Situation(w) & ∀p (w ⊨ p → p))›
    using "world:1"[THEN "≡_dfE", OF PossibleWorld.ψ, THEN "&E"(1),
                    THEN "possit-sit:1"[THEN "≡E"(1)]]
    by (metis "KBasic:16" "&I" "vdash-properties:10")
  AOT_show ‹♢Actual(w)›
    by (AOT_subst ‹Actual(w)› ‹Situation(w) & ∀p (w ⊨ p → p)›)
       (auto simp: actual "≡Df" 0)
qed

AOT_theorem "world-cons:1": ‹Consistent(w)›
  using "world-pos"
  using "pos-cons-sit:1"[unconstrain s, THEN "→E", THEN "→E"]
  by (meson "≡_dfE" "&E"(1) pos)

AOT_theorem "world-cons:2": ‹¬TrivialSituation(w)›
proof(rule "raa-cor:2")
  AOT_assume ‹TrivialSituation(w)›
  AOT_hence ‹Situation(w) & ∀p w ⊨ p›
    using "df-null-trivial:2"[THEN "≡_dfE"] by blast
  AOT_hence 0: ‹◻w ⊨ (∃p (p & ¬p))›
    using "&E"
    by (metis "Buridan♢" "T♢" "&E"(2) "≡E"(1) "lem2:3"[unconstrain s, THEN "→E"]
              "log-prop-prop:2" "rule-ui:1" "universal-cor" "→E")
  AOT_have ‹♢∀p (w ⊨ p ≡ p)›
    using PossibleWorld.ψ "world:1"[THEN "≡_dfE", THEN "&E"(2)] by metis
  AOT_hence ‹∀p ♢(w ⊨ p ≡ p)›
    using "Buridan♢"[THEN "→E"] by blast
  AOT_hence ‹♢(w ⊨ (∃p (p & ¬p)) ≡ (∃p (p & ¬p)))›
    by (metis "log-prop-prop:2" "rule-ui:1")
  AOT_hence ‹♢(w ⊨ (∃p (p & ¬p)) → (∃p (p & ¬p)))›
    using "RM♢"[THEN "→E"] "→I" "≡E"(1) by meson
  AOT_hence ‹♢(∃p (p & ¬p))› using 0
    by (metis "KBasic2:4" "≡E"(1) "→E")
  moreover AOT_have ‹¬♢(∃p (p & ¬p))›
    by (metis "instantiation" "KBasic2:1" RN "≡E"(1) "raa-cor:2")
  ultimately AOT_show ‹♢(∃p (p & ¬p)) & ¬♢(∃p (p & ¬p))›
    using "&I" by blast
qed

AOT_theorem "rigid-truth-at:1": ‹w ⊨ p ≡ ◻w ⊨ p›
  using "lem2:1"[unconstrain s, THEN "→E",
                 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡_dfE"], THEN "&E"(1)]].

AOT_theorem "rigid-truth-at:2": ‹♢w ⊨ p ≡ w ⊨ p›
  using "lem2:2"[unconstrain s, THEN "→E",
                 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡_dfE"], THEN "&E"(1)]].

AOT_theorem "rigid-truth-at:3": ‹♢w ⊨ p ≡ ◻w ⊨ p›
  using "lem2:3"[unconstrain s, THEN "→E",
                 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡_dfE"], THEN "&E"(1)]].

AOT_theorem "rigid-truth-at:4": ‹\Aw ⊨ p ≡ w ⊨ p›
  using "lem2:4"[unconstrain s, THEN "→E",
                 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡_dfE"], THEN "&E"(1)]].

AOT_theorem "rigid-truth-at:5": ‹¬w ⊨ p ≡ ◻¬w ⊨ p›
  using "lem2:5"[unconstrain s, THEN "→E",
                 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡_dfE"], THEN "&E"(1)]].

AOT_define Maximal :: ‹τ → φ› (‹Maximal'(_')›)
  max: ‹Maximal(s) ≡_df ∀p (s ⊨ p ∨ s ⊨ ¬p)›

AOT_theorem "world-max": ‹Maximal(w)›
proof(safe intro!: PossibleWorld.ψ[THEN "≡_dfE"[OF "world:1"], THEN "&E"(1)]
                   GEN "≡_dfI"[OF max] "&I" )
  fix q
  AOT_have ‹♢(w ⊨ q ∨ w ⊨ ¬q)›
  proof(rule "RM♢"[THEN "→E"]; (rule "→I")?)
    AOT_modally_strict {
      AOT_assume ‹∀p (w ⊨ p ≡ p)›
      AOT_hence ‹w ⊨ q ≡ q› and ‹w ⊨ ¬q ≡ ¬q›
        using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
      AOT_thus ‹w ⊨ q ∨ w ⊨ ¬q›
        by (metis "∨I"(1) "∨I"(2) "≡E"(3) "reductio-aa:1")
    }
  next
    AOT_show ‹♢∀p (w ⊨ p ≡ p)›
      using PossibleWorld.ψ[THEN "≡_dfE"[OF "world:1"], THEN "&E"(2)].
  qed
  AOT_hence ‹♢w ⊨ q ∨ ♢w ⊨ ¬q›
    using "KBasic2:2"[THEN "≡E"(1)] by blast
  AOT_thus ‹w ⊨ q ∨ w ⊨ ¬q›
    using "lem2:2"[unconstrain s, THEN "→E", unvarify p,
                   OF PossibleWorld.ψ[THEN "≡_dfE"[OF "world:1"], THEN "&E"(1)],
                   THEN "≡E"(1), OF "log-prop-prop:2"]
    by (metis "∨I"(1) "∨I"(2) "∨E"(3) "raa-cor:2")
qed

AOT_theorem "world=maxpos:1": ‹Maximal(x) → ◻Maximal(x)›
proof (AOT_subst ‹Maximal(x)› ‹Situation(x) & ∀p (x ⊨ p ∨ x ⊨ ¬p)›;
       safe intro!: max "≡Df" "→I"; frule "&E"(1); drule "&E"(2))
  AOT_assume sit_x: ‹Situation(x)›
  AOT_hence nec_sit_x: ‹◻Situation(x)›
    by (metis "≡E"(1) "possit-sit:1")
  AOT_assume ‹∀p (x ⊨ p ∨ x ⊨ ¬p)›
  AOT_hence ‹x ⊨ p ∨ x ⊨ ¬p› for p
    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast
  AOT_hence ‹◻x ⊨ p ∨ ◻x ⊨ ¬p› for p
    using "lem2:1"[unconstrain s, THEN "→E", OF sit_x, unvarify p,
                   OF "log-prop-prop:2", THEN "≡E"(1)]
    by (metis "∨I"(1) "∨I"(2) "∨E"(2) "raa-cor:1")
  AOT_hence ‹◻(x ⊨ p ∨ x ⊨ ¬p)› for p
    by (metis "KBasic:15" "→E")
  AOT_hence ‹∀p ◻(x ⊨ p ∨ x ⊨ ¬p)›
    by (rule GEN)
  AOT_hence ‹◻∀p (x ⊨ p ∨ x ⊨ ¬p)›
    by (rule BF[THEN "→E"])
  AOT_thus ‹◻(Situation(x) & ∀p (x ⊨ p ∨ x ⊨ ¬p))›
    using nec_sit_x by (metis "KBasic:3" "&I" "≡E"(2))
qed

AOT_theorem "world=maxpos:2": ‹PossibleWorld(x) ≡ Maximal(x) & Possible(x)›
proof(safe intro!: "≡I" "→I" "&I" "world-pos"[unconstrain w, THEN "→E"]
                   "world-max"[unconstrain w, THEN "→E"];
      frule "&E"(2); drule "&E"(1))
  AOT_assume pos_x: ‹Possible(x)›
  AOT_have ‹♢(Situation(x) & ∀p(x ⊨ p → p))›
    apply (AOT_subst (reverse) ‹Situation(x) & ∀p(x ⊨ p → p)› ‹Actual(x)›)
     using actual "≡Df" apply presburger
    using "≡_dfE" "&E"(2) pos pos_x by blast
  AOT_hence 0: ‹♢∀p(x ⊨ p → p)›
    by (metis "KBasic2:3" "&E"(2) "vdash-properties:6")
  AOT_assume max_x: ‹Maximal(x)›
  AOT_hence sit_x: ‹Situation(x)› by (metis "≡_dfE" max_x "&E"(1) max)
  AOT_have ‹◻Maximal(x)› using "world=maxpos:1"[THEN "→E", OF max_x] by simp
  moreover AOT_have ‹◻Maximal(x) → ◻(∀p(x ⊨ p → p) → ∀p (x ⊨ p ≡ p))›
  proof(safe intro!: "→I" RM GEN)
    AOT_modally_strict {
      fix p
      AOT_assume 0: ‹Maximal(x)›
      AOT_assume 1: ‹∀p (x ⊨ p → p)›
      AOT_show ‹x ⊨ p ≡ p›
      proof(safe intro!: "≡I" "→I" 1[THEN "∀E"(2), THEN "→E"]; rule "raa-cor:1")
        AOT_assume ‹¬x ⊨ p›
        AOT_hence ‹x ⊨ ¬p›
          using 0[THEN "≡_dfE"[OF max], THEN "&E"(2), THEN "∀E"(2)]
                1 by (metis "∨E"(2))
        AOT_hence ‹¬p›
          using 1[THEN "∀E"(1), OF "log-prop-prop:2", THEN "→E"] by blast
        moreover AOT_assume p
        ultimately AOT_show ‹p & ¬p› using "&I" by blast
      qed
    }
  qed
  ultimately AOT_have ‹◻(∀p(x ⊨ p → p) → ∀p (x ⊨ p ≡ p))›
    using "→E" by blast
  AOT_hence ‹♢∀p(x ⊨ p → p) → ♢∀p(x ⊨ p ≡ p)›
    by (metis "KBasic:13"[THEN "→E"])
  AOT_hence ‹♢∀p(x ⊨ p ≡ p)›
    using 0 "→E" by blast
  AOT_thus ‹PossibleWorld(x)›
    using "≡_dfI"[OF "world:1", OF "&I", OF sit_x] by blast
qed

AOT_define NecImpl :: ‹φ → φ → φ› (infixl ‹→› 26)
  "nec-impl-p:1": ‹p → q ≡_df ◻(p → q)›
AOT_define NecEquiv :: ‹φ → φ → φ› (infixl ‹⇔› 21)
  "nec-impl-p:2": ‹p ⇔ q ≡_df (p → q) & (q → p)›

AOT_theorem "nec-equiv-nec-im": ‹p ⇔ q ≡ ◻(p ≡ q)›
proof(safe intro!: "≡I" "→I")
  AOT_assume ‹p ⇔ q›
  AOT_hence ‹(p → q)› and ‹(q → p)›
    using "nec-impl-p:2"[THEN "≡_dfE"] "&E" by blast+
  AOT_hence ‹◻(p → q)› and ‹◻(q → p)›
    using "nec-impl-p:1"[THEN "≡_dfE"] by blast+
  AOT_thus ‹◻(p ≡ q)› by (metis "KBasic:4" "&I" "≡E"(2))
next
  AOT_assume ‹◻(p ≡ q)›
  AOT_hence ‹◻(p → q)› and ‹◻(q → p)›
    using "KBasic:4" "&E" "≡E"(1) by blast+
  AOT_hence ‹(p → q)› and ‹(q → p)›
    using "nec-impl-p:1"[THEN "≡_dfI"] by blast+
  AOT_thus ‹p ⇔ q›
    using "nec-impl-p:2"[THEN "≡_dfI"] "&I" by blast
qed

(* TODO: PLM: discuss these; still not in PLM *)
AOT_theorem world_closed_lem_1_a:
  ‹(s ⊨ (φ & ψ)) → (∀p (s ⊨ p ≡ p) → (s ⊨ φ & s ⊨ ψ))›
proof(safe intro!: "→I")
  AOT_assume ‹∀ p (s ⊨ p ≡ p)›
  AOT_hence ‹s ⊨ (φ & ψ) ≡ (φ & ψ)› and ‹s ⊨ φ ≡ φ› and ‹s ⊨ ψ ≡ ψ›
    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
  moreover AOT_assume ‹s ⊨ (φ & ψ)›
  ultimately AOT_show ‹s ⊨ φ & s ⊨ ψ›
    by (metis "&I" "&E"(1) "&E"(2) "≡E"(1) "≡E"(2))
qed

AOT_theorem world_closed_lem_1_b:
  ‹(s ⊨ φ & (φ → q)) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
proof(safe intro!: "→I")
  AOT_assume ‹∀ p (s ⊨ p ≡ p)›
  AOT_hence ‹s ⊨ φ ≡ φ› for φ
    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast
  moreover AOT_assume ‹s ⊨ φ & (φ → q)›
  ultimately AOT_show ‹s ⊨ q›
    by (metis "&E"(1) "&E"(2) "≡E"(1) "≡E"(2) "→E")
qed

AOT_theorem world_closed_lem_1_c:
  ‹(s ⊨ φ & s ⊨ (φ → ψ)) → (∀p (s ⊨ p ≡ p) → s ⊨ ψ)›
proof(safe intro!: "→I")
  AOT_assume ‹∀ p (s ⊨ p ≡ p)›
  AOT_hence ‹s ⊨ φ ≡ φ› for φ
    using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast
  moreover AOT_assume ‹s ⊨ φ & s ⊨ (φ → ψ)›
  ultimately AOT_show ‹s ⊨ ψ›
    by (metis "&E"(1) "&E"(2) "≡E"(1) "≡E"(2) "→E")
qed

AOT_theorem "world-closed-lem:1[0]":
  ‹q → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
  by (meson "→I" "≡E"(2) "log-prop-prop:2" "rule-ui:1")

AOT_theorem "world-closed-lem:1[1]":
  ‹s ⊨ p₁ & (p₁ → q) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
  using world_closed_lem_1_b.

AOT_theorem "world-closed-lem:1[2]":
  ‹s ⊨ p₁ & s ⊨ p₂ & ((p₁ & p₂) → q) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
  using world_closed_lem_1_b world_closed_lem_1_a
  by (metis (full_types) "&I" "&E" "→I" "→E")

AOT_theorem "world-closed-lem:1[3]":
  ‹s ⊨ p₁ & s ⊨ p₂ & s ⊨ p₃ & ((pb>1 & p₂ & p₃) → q) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
  using world_closed_lem_1_b world_closed_lem_1_a
  by (metis (full_types) "&I" "&E" "→I" "→E")

AOT_theorem "world-closed-lem:1[4]":
  ‹s ⊨ p₁ & s ⊨ p₂ & s ⊨ p₃ & s an style='font-size: 18px;'>⊨ p₄ & ((p₁ & p₂ & p₃ & p₄) → q) →
 (∀p (s ⊨ p ≡ p) → s ⊨ q)›
  using world_closed_lem_1_b world_closed_lem_1_a
  by (metis (full_types) "&I" "&E" "→I" "→E")

AOT_theorem "coherent:1": ‹w ⊨ ¬p ≡ ¬w ⊨ p›
proof(safe intro!: "≡I" "→I")
  AOT_assume 1: ‹w ⊨ ¬p›
  AOT_show ‹¬w ⊨ p›
  proof(rule "raa-cor:2")
    AOT_assume ‹w ⊨ p›
    AOT_hence ‹w ⊨ p & w ⊨ ¬p› using 1 "&I" by blast
    AOT_hence ‹∃q (w ⊨ q & w ⊨ ¬q)› by (rule "∃I")
    moreover AOT_have ‹¬∃q (w ⊨ q & w ⊨ ¬q)›
      using "world-cons:1"[THEN "≡_dfE"[OF cons], THEN "&E"(2)].
    ultimately AOT_show ‹∃q (w ⊨ q & w ⊨ ¬q) & ¬∃q (w ⊨ q & w ⊨ ¬q)›
      using "&I" by blast
  qed
next
  AOT_assume ‹¬w ⊨ p›
  AOT_thus ‹w ⊨ ¬p›
    using "world-max"[THEN "≡_dfE"[OF max], THEN "&E"(2)]
    by (metis "∨E"(2) "log-prop-prop:2" "rule-ui:1")
qed

AOT_theorem "coherent:2": ‹w ⊨ p ≡ ¬w ⊨ ¬p›
  by (metis "coherent:1" "deduction-theorem" "≡I" "≡E"(1) "≡E"(2) "raa-cor:3")

AOT_theorem "act-world:1": ‹∃w ∀p (w ⊨ p ≡ p)›
proof -
  AOT_obtain s where s_prop: ‹∀p (s ⊨ p ≡ p)›
    using "sit-classical:6" "Situation.∃E"[rotated] by meson
  AOT_hence ‹♢∀p (s ⊨ p ≡ p)›
    by (metis "T♢" "vdash-properties:10")
  AOT_hence ‹PossibleWorld(s)›
    using "world:1"[THEN "≡_dfI"] Situation.ψ "&I" by blast
  AOT_hence ‹PossibleWorld(s) & ∀p (s ⊨ p ≡ p)›
    using "&I" s_prop by blast
  thus ?thesis by (rule "∃I")
qed

AOT_theorem "act-world:2": ‹∃!w Actual(w)›
proof -
  AOT_obtain w where w_prop: ‹∀p (w ⊨ p ≡ p)›
    using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
  AOT_have sit_s: ‹Situation(w)›
    using PossibleWorld.ψ "world:1"[THEN "≡_dfE", THEN "&E"(1)] by blast
  show ?thesis
  proof (safe intro!: "uniqueness:1"[THEN "≡_dfI"] "∃I"(2) "&I" GEN "→I"
                      PossibleWorld.ψ actual[THEN "≡_dfI"] sit_s
                      "sit-identity"[unconstrain s, unconstrain s', THEN "→E",
                                     THEN "→E", THEN "≡E"(2)] "≡I"
                      w_prop[THEN "∀E"(2), THEN "≡E"(1)])
    AOT_show ‹PossibleWorld(w)› using PossibleWorld.ψ.
  next
    AOT_show ‹Situation(w)›
      by (simp add: sit_s)
  next
    fix y p
    AOT_assume w_asm: ‹PossibleWorld(y) & Actual(y)›
    AOT_assume ‹w ⊨ p›
    AOT_hence p: ‹p›
      using w_prop[THEN "∀E"(2), THEN "≡E"(1)] by blast
    AOT_show ‹y ⊨ p›
    proof(rule "raa-cor:1")
      AOT_assume ‹¬y ⊨ p›
      AOT_hence ‹y ⊨ ¬p›
        by (metis "coherent:1"[unconstrain w, THEN "→E"] "&E"(1) "≡E"(2) w_asm)
      AOT_hence ‹¬p›
        using w_asm[THEN "&E"(2), THEN actual[THEN "≡_dfE"], THEN "&E"(2),
                    THEN "∀E"(1), rotated, OF "log-prop-prop:2"]
              "→E" by blast
      AOT_thus ‹p & ¬p› using p "&I" by blast
    qed
  next
    AOT_show ‹w ⊨ p› if ‹y ⊨ p› and ‹PossibleWorld(y) & Actual(y)› for p y
      using that(2)[THEN "&E"(2), THEN actual[THEN "≡_dfE"], THEN "&E"(2),
                    THEN "∀E"(2), THEN "→E", OF that(1)]
            w_prop[THEN "∀E"(2), THEN "≡E"(2)] by blast
  next
    AOT_show ‹Situation(y)› if ‹PossibleWorld(y) & Actual(y)› for y
      using that[THEN "&E"(1)] "world:1"[THEN "≡_dfE", THEN "&E"(1)] by blast
  next
    AOT_show ‹Situation(w)›
      using sit_s by blast
  qed(simp)
qed

AOT_theorem "pre-walpha": ‹\ιw Actual(w)↓›
  using "A-Exists:2" "RA[2]" "act-world:2" "≡E"(2) by blast

AOT_define TheActualWorld :: ‹κ_s› (‹w_\α›)
  "w-alpha": ‹w_\α =_df \ιw Actual(w)›

(* TODO: not in PLM *)
AOT_theorem true_in_truth_act_true: ‹⊤ ⊨ p ≡ \Ap›
proof(safe intro!: "≡I" "→I")
  AOT_have true_def: ‹\⊨_\◻ ⊤ = \ιx (A!x & ∀F (x[F] ≡ ∃p(p & F = [λy p])))›
    by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
  AOT_hence true_den: ‹\⊨_\◻ ⊤↓›
    using "t=t-proper:1" "vdash-properties:6" by blast
  {
    AOT_assume ‹⊤ ⊨ p›
    AOT_hence ‹⊤[λy p]›
      by (metis "≡_dfE" "con-dis-i-e:2:b" "prop-enc" "true-in-s")
    AOT_hence ‹\ιx(A!x & ∀F (x[F] ≡ ∃q (q & F = [λy q])))[λy p]›
      using "rule=E" true_def true_den by fast
    AOT_hence ‹\A∃q (q & [λy p] = [λy q])›
      using "≡E"(1) "desc-nec-encode:1"[unvarify F] "prop-prop2:2" by fast
    AOT_hence ‹∃q \A(q & [λy p] = [λy q])›
      by (metis "Act-Basic:10" "≡E"(1))
    then AOT_obtain q where ‹\A(q & [λy p] = [λy q])›
      using "∃E"[rotated] by blast
    AOT_hence actq: ‹\Aq› and ‹\A[λy p] = [λy q]›
      using "Act-Basic:2" "intro-elim:3:a" "&E" by blast+
    AOT_hence ‹[λy p] = [λy q]›
      using "id-act:1"[unvarify α β, THEN "≡E"(2)] "prop-prop2:2" by blast
    AOT_hence ‹p = q›
      by (metis "intro-elim:3:b" "p-identity-thm2:3")
    AOT_thus ‹\Ap›
      using actq "rule=E" id_sym by blast
  }
  {
    AOT_assume ‹\Ap›
    AOT_hence ‹\A(p & [λy p] = [λy p])›
      by (auto intro!: "Act-Basic:2"[THEN "≡E"(2)] "&I"
               intro: "RA[2]" "=I"(1)[OF "prop-prop2:2"])
    AOT_hence ‹∃q \A(q & [λy p] = [λy q])›
      using "∃I" by fast
    AOT_hence ‹\A∃q (q & [λy p] = [λy q])›
      by (metis "Act-Basic:10" "≡E"(2))
    AOT_hence ‹\ιx(A!x & ∀F (x[F] ≡ ∃q (q & F = [λy q])))[λy p]›
      using "≡E"(2) "desc-nec-encode:1"[unvarify F] "prop-prop2:2" by fast
    AOT_hence ‹⊤[λy p]›
      using "rule=E" true_def true_den id_sym by fast
    AOT_thus ‹⊤ ⊨ p›
      by (safe intro!: "true-in-s"[THEN "≡_dfI"] "&I" "possit-sit:6"
                       "prop-enc"[THEN "≡_dfI"] true_den)
  }
qed

AOT_theorem "T-world": ‹⊤ = w_\α›
proof -
  AOT_have true_den: ‹\⊨_\◻ ⊤↓›
    using "Situation.res-var:3" "possit-sit:6" "→E" by blast
  AOT_have ‹\A∀p (⊤ ⊨ p → p)›
  proof (safe intro!: "logic-actual-nec:3"[axiom_inst, THEN "≡E"(2)] GEN
                      "logic-actual-nec:2"[axiom_inst, THEN "≡E"(2)] "→I")
    fix p
    AOT_assume ‹\A⊤ ⊨ p›
    AOT_hence ‹⊤ ⊨ p›
      using "lem2:4"[unconstrain s, unvarify β, OF true_den,
                     THEN "→E", OF "possit-sit:6"] "≡E"(1) by blast
    AOT_thus ‹\Ap› using true_in_truth_act_true "≡E"(1) by blast
  qed
  moreover AOT_have ‹\A(Situation(κ) & ∀p (κ ⊨ p → p)) → \AActual(κ)› for κ
    using actual[THEN "≡Df", THEN "conventions:3"[THEN "≡_dfE", THEN "&E"(2)],
                 THEN "RA[2]", THEN "act-cond"[THEN "→E"]].
  ultimately AOT_have act_act_true: ‹\AActual(⊤)›
    using "possit-sit:4"[unvarify x, OF true_den, THEN "≡E"(2), OF "possit-sit:6"]
          "Act-Basic:2"[THEN "≡E"(2), OF "&I"] "→E" by blast
  AOT_hence ‹♢Actual(⊤)› by (metis "Act-Sub:3" "vdash-properties:10")
  AOT_hence ‹Possible(⊤)›
    by (safe intro!: pos[THEN "≡_dfI"] "&I" "possit-sit:6")
  moreover AOT_have ‹Maximal(⊤)›
  proof (safe intro!: max[THEN "≡_dfI"] "&I" "possit-sit:6" GEN)
    fix p
    AOT_have ‹\Ap ∨ \A¬p›
      by (simp add: "Act-Basic:1")
    moreover AOT_have ‹⊤ ⊨ p› if ‹\Ap›
        using that true_in_truth_act_true[THEN "≡E"(2)] by blast
    moreover AOT_have ‹⊤ ⊨ ¬p› if ‹\A¬p›
      using that true_in_truth_act_true[unvarify p, THEN "≡E"(2)]
            "log-prop-prop:2" by blast
    ultimately AOT_show ‹⊤ ⊨ p ∨ ⊤ ⊨ ¬p›
      using "∨I"(3) "→I" by blast
  qed
  ultimately AOT_have ‹PossibleWorld(⊤)›
    by (safe intro!: "world=maxpos:2"[unvarify x, OF true_den, THEN "≡E"(2)] "&I")
  AOT_hence ‹\APossibleWorld(⊤)›
    using "rigid-pw:4"[unvarify x, OF true_den, THEN "≡E"(2)] by blast
  AOT_hence 1: ‹\A(PossibleWorld(⊤) & Actual(⊤))›
    using act_act_true "Act-Basic:2" "df-simplify:2" "intro-elim:3:b" by blast
  AOT_have ‹w_\α = \ιw(Actual(w))›
    using "rule-id-df:1[zero]"[OF "w-alpha", OF "pre-walpha"] by simp
  moreover AOT_have w_act_den: ‹w_\α↓›
    using calculation "t=t-proper:1" "→E" by blast
  ultimately AOT_have ‹∀z (\A(PossibleWorld(z) & Actual(z)) → z = w_\α)›
    using "nec-hintikka-scheme"[unvarify x] "≡E"(1) "&E" by blast
  AOT_thus ‹⊤ = w_\α›
    using "∀E"(1)[rotated, OF true_den] 1 "→E" by blast
qed

AOT_act_theorem "truth-at-alpha:1": ‹p ≡ w_\α = \ιx (ExtensionOf(x, p))›
  by (metis "rule=E" "T-world" "deduction-theorem" "ext-p-tv:3" id_sym "≡I"
            "≡E"(1) "≡E"(2) "q-True:1")

AOT_act_theorem "truth-at-alpha:2": ‹p ≡ w_\α ⊨ p›
proof -
  AOT_have ‹PossibleWorld(w_\α)›
    using "&E"(1) "pre-walpha" "rule-id-df:2:b[zero]" "→E"
          "w-alpha" "y-in:3" by blast
  AOT_hence sit_w_alpha: ‹Situation(w_\α)›
    by (metis "≡_dfE" "&E"(1) "world:1")
  AOT_have w_alpha_den: ‹w_\α↓›
    using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
  AOT_have ‹p ≡ ⊤\Σp›
    using "q-True:3" by force
  moreover AOT_have ‹⊤ = w_\α›
    using "T-world" by auto
  ultimately AOT_have ‹p ≡ w_\α\Σp›
    using "rule=E" by fast
  moreover AOT_have ‹w_\α \Σ p ≡ w_\α ⊨ p›
    using lem1[unvarify x, OF w_alpha_den, THEN "→E", OF sit_w_alpha]
    using "≡S"(1) "≡E"(1) "Commutativity of ≡" "≡Df" sit_w_alpha "true-in-s" by blast
  ultimately AOT_show ‹p ≡ w_\α ⊨ p›
    by (metis "≡E"(5))
qed

AOT_theorem "alpha-world:1": ‹PossibleWorld(w_\α)›
proof -
  AOT_have 0: ‹w_\α = \ιw Actual(w)›
    using "pre-walpha" "rule-id-df:1[zero]" "w-alpha" by blast
  AOT_hence walpha_den: ‹w_\α↓›
    by (metis "t=t-proper:1" "vdash-properties:6")
  AOT_have ‹\A(PossibleWorld(w_\α) & Actual(w_\α))›
    by (rule "actual-desc:2"[unvarify x, OF walpha_den, THEN "→E"]) (fact 0)
  AOT_hence ‹\APossibleWorld(w_\α)›
    by (metis "Act-Basic:2" "&E"(1) "≡E"(1))
  AOT_thus ‹PossibleWorld(w_\α)›
    using "rigid-pw:4"[unvarify x, OF walpha_den, THEN "≡E"(1)]
    by blast
qed

AOT_theorem "alpha-world:2": ‹Maximal(w_\α)›
proof -
  AOT_have ‹w_\α↓›
    using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
  then AOT_obtain x where x_def: ‹x = w_\α›
    by (metis "instantiation" "rule=I:1" "existential:1" id_sym)
  AOT_hence ‹PossibleWorld(x)› using "alpha-world:1" "rule=E" id_sym by fast
  AOT_hence ‹Maximal(x)› by (metis "world-max"[unconstrain w, THEN "→E"]) 
  AOT_thus ‹Maximal(w_\α)› using x_def "rule=E" by blast
qed

AOT_theorem "t-at-alpha-strict": ‹w_\α ⊨ p ≡ \Ap›
proof -
  AOT_have 0: ‹w_\α = \ιw Actual(w)›
    using "pre-walpha" "rule-id-df:1[zero]" "w-alpha" by blast
  AOT_hence walpha_den: ‹w_\α↓›
    by (metis "t=t-proper:1" "vdash-properties:6")
  AOT_have 1: ‹\A(PossibleWorld(w_\α) & Actual(w_\α))›
    by (rule "actual-desc:2"[unvarify x, OF walpha_den, THEN "→E"]) (fact 0)
  AOT_have walpha_sit: ‹Situation(w_\α)›
    by (meson "≡_dfE" "alpha-world:2" "&E"(1) max)
  {
    fix p
    AOT_have 2: ‹Situation(x) → (\Ax ⊨ p ≡ x ⊨ p)› for x
      using "lem2:4"[unconstrain s] by blast
    AOT_assume ‹w_\α ⊨ p›
    AOT_hence θ: ‹\Aw_\α ⊨ p›
      using 2[unvarify x, OF walpha_den, THEN "→E", OF walpha_sit, THEN "≡E"(2)]
      by argo
    AOT_have 3: ‹\AActual(w_\α)›
      using "1" "Act-Basic:2" "&E"(2) "≡E"(1) by blast
    AOT_have ‹\A(Situation(w_\α) & ∀q(w_\α ⊨ q → q))›
      apply (AOT_subst (reverse) ‹Situation(w_\α) & ∀q(w_\α ⊨ q → q)› ‹Actual(w_\α)›)
       using actual "≡Df" apply blast
      by (fact 3)
    AOT_hence ‹\A∀q(w_\α ⊨ q → q)› by (metis "Act-Basic:2" "&E"(2) "≡E"(1))
    AOT_hence ‹∀q \A(w_\α ⊨ q → q)›
      using "logic-actual-nec:3"[axiom_inst, THEN "≡E"(1)] by blast
    AOT_hence ‹\A(w_\α ⊨ p → p)› using "∀E"(2) by blast
    AOT_hence ‹\A(w_\α ⊨ p) → \Ap› by (metis "act-cond" "vdash-properties:10")
    AOT_hence ‹\Ap› using θ "→E" by blast
  }
  AOT_hence 2: ‹w_\α ⊨ p → \Ap› for p by (rule "→I")
  AOT_have walpha_sit: ‹Situation(w_\α)›
    using "≡_dfE" "alpha-world:2" "&E"(1) max by blast
  show ?thesis
  proof(safe intro!: "≡I" "→I" 2)
    AOT_assume actp: ‹\Ap›
    AOT_show ‹w_\α ⊨ p›
    proof(rule "raa-cor:1")
      AOT_assume ‹¬w_\α ⊨ p›
      AOT_hence ‹w_\α ⊨ ¬p›
        using "alpha-world:2"[THEN max[THEN "≡_dfE"], THEN "&E"(2),
                              THEN "∀E"(1), OF "log-prop-prop:2"]
        by (metis "∨E"(2))
      AOT_hence ‹\A¬p›
        using 2[unvarify p, OF "log-prop-prop:2", THEN "→E"] by blast
      AOT_hence ‹¬\Ap› by (metis "¬¬I" "Act-Sub:1" "≡E"(4))
      AOT_thus ‹\Ap & ¬\Ap› using actp "&I" by blast
    qed
  qed
qed

AOT_act_theorem "not-act": ‹w ≠ w_\α → ¬Actual(w)›
proof (rule "→I"; rule "raa-cor:2")
  AOT_assume ‹w ≠ w_\α›
  AOT_hence 0: ‹¬(w = w_\α)› by (metis "≡_dfE" "=-infix")
  AOT_have walpha_den: ‹w_\α↓›
    using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
  AOT_have walpha_sit: ‹Situation(w_\α)›
    using "≡_dfE" "alpha-world:2" "&E"(1) max by blast
  AOT_assume act_w: ‹Actual(w)›
  AOT_hence w_sit: ‹Situation(w)› by (metis "≡_dfE" actual "&E"(1))
  AOT_have sid: ‹Situation(x') → (w = x' ≡ ∀p (w ⊨ p ≡ x' ⊨ p))› for x'
    using "sit-identity"[unconstrain s', unconstrain s, THEN "→E", OF w_sit]
    by blast
  AOT_have ‹w = w_\α›
  proof(safe intro!: GEN sid[unvarify x', OF walpha_den, THEN "→E",
                             OF walpha_sit, THEN "≡E"(2)] "≡I" "→I")
    fix p
    AOT_assume ‹w ⊨ p›
    AOT_hence ‹p›
      using actual[THEN "≡_dfE", OF act_w, THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
      by blast
    AOT_hence ‹\Ap›
      by (metis "RA[1]")
    AOT_thus ‹w_\α ⊨ p›
      using "t-at-alpha-strict"[THEN "≡E"(2)] by blast
  next
    fix p
    AOT_assume ‹w_\α ⊨ p›
    AOT_hence ‹\Ap›
      using "t-at-alpha-strict"[THEN "≡E"(1)] by blast
    AOT_hence p: ‹p›
      using "logic-actual"[act_axiom_inst, THEN "→E"] by blast
    AOT_show ‹w ⊨ p›
    proof(rule "raa-cor:1")
      AOT_assume ‹¬w ⊨ p›
      AOT_hence ‹w ⊨ ¬p›
        by (metis "coherent:1" "≡E"(2))
      AOT_hence ‹¬p›
        using actual[THEN "≡_dfE", OF act_w, THEN "&E"(2), THEN "∀E"(1),
                     OF "log-prop-prop:2", THEN "→E"] by blast
      AOT_thus ‹p & ¬p› using p "&I" by blast
    qed
  qed
  AOT_thus ‹w = w_\α & ¬(w = w_\α)› using 0 "&I" by blast
qed

AOT_act_theorem "w-alpha-part": ‹Actual(s) ≡ s ⊴ w_\α›
proof(safe intro!: "≡I" "→I" "sit-part-whole"[THEN "≡_dfI"] "&I" GEN
           dest!:  "sit-part-whole"[THEN "≡_dfE"])
  AOT_show ‹Situation(s)› if ‹Actual(s)›
    using "≡_dfE" actual "&E"(1) that by blast
next
  AOT_show ‹Situation(w_\α)›
    using "≡_dfE" "alpha-world:2" "&E"(1) max by blast
next
  fix p
  AOT_assume ‹Actual(s)›
  moreover AOT_assume ‹s ⊨ p›
  ultimately AOT_have ‹p›
    using actual[THEN "≡_dfE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] by blast
  AOT_thus ‹w_\α ⊨ p›
     by (metis "≡E"(1) "truth-at-alpha:2")
next
  AOT_assume 0: ‹Situation(s) & Situation(w_\α) & ∀p (s ⊨ p → w_\α ⊨ p)›
  AOT_hence ‹s ⊨ p → w_\α ⊨ p› for p
    using "&E" "∀E"(2) by blast
  AOT_hence ‹s ⊨ p → p› for p
    by (metis "→I" "≡E"(2) "truth-at-alpha:2" "→E")
  AOT_hence ‹∀p (s ⊨ p → p)› by (rule GEN)
  AOT_thus ‹Actual(s)›
    using actual[THEN "≡_dfI", OF "&I", OF 0[THEN "&E"(1), THEN "&E"(1)]] by blast
qed

AOT_act_theorem "act-world2:1": ‹w_\α ⊨ p ≡ [λy p]w_\α›
  apply (AOT_subst ‹[λy p]w_\α› p)
   apply (rule "beta-C-meta"[THEN "→E", OF "prop-prop2:2", unvarify ν₁ν_n])
  using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" apply blast
  using "≡E"(2) "Commutativity of ≡" "truth-at-alpha:2" by blast

AOT_act_theorem "act-world2:2": ‹p ≡ w_\α ⊨ [λy p]w_\α›
proof -
  AOT_have ‹p ≡ [λy p]w_\α›
    apply (rule "beta-C-meta"[THEN "→E", OF "prop-prop2:2",
                              unvarify ν₁ν_n, symmetric])
    using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
  also AOT_have ‹… ≡ w_\α ⊨ [λy p]w_\α›
    by (meson "log-prop-prop:2" "rule-ui:1" "truth-at-alpha:2" "universal-cor")
  finally show ?thesis.
qed

AOT_theorem "fund-lem:1": ‹♢p → ♢∃w (w ⊨ p)›
proof (rule "RM♢"; rule "→I"; rule "raa-cor:1")
  AOT_modally_strict {
    AOT_obtain w where w_prop: ‹∀q (w ⊨ q ≡ q)›
      using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
    AOT_assume p: ‹p›
    AOT_assume 0: ‹¬∃w (w ⊨ p)›
    AOT_have ‹∀w ¬(w ⊨ p)›
      apply (AOT_subst ‹PossibleWorld(x) → ¬x ⊨ p›
                       ‹¬(PossibleWorld(x) & x ⊨ p)› for: x)
      apply (metis "&I" "&E"(1) "&E"(2) "→I" "≡I" "modus-tollens:2")
      using "0" "cqt-further:4" "vdash-properties:10" by blast
    AOT_hence ‹¬(w ⊨ p)›
      using PossibleWorld.ψ "rule-ui:3" "→E" by blast
    AOT_hence ‹¬p›
      using w_prop[THEN "∀E"(2), THEN "≡E"(2)] 
      by (metis "raa-cor:3")
    AOT_thus ‹p & ¬p›
      using p "&I" by blast
  }
qed

AOT_theorem "fund-lem:2": ‹♢∃w (w ⊨ p) → ∃w (w ⊨ p)›
proof (rule "→I")
  AOT_assume ‹♢∃w (w ⊨ p)›
  AOT_hence ‹∃w ♢(w ⊨ p)›
    using "PossibleWorld.res-var-bound-reas[BF♢]"[THEN "→E"] by auto
  then AOT_obtain w where ‹♢(w ⊨ p)›
    using "PossibleWorld.∃E"[rotated] by meson
  moreover AOT_have ‹Situation(w)›
    by (metis "≡_dfE" "&E"(1) pos "world-pos")
  ultimately AOT_have ‹w ⊨ p›
    using "lem2:2"[unconstrain s, THEN "→E"]  "≡E" by blast
  AOT_thus ‹∃w w ⊨ p›
    by (rule "PossibleWorld.∃I")
qed

AOT_theorem "fund-lem:3": ‹p → ∀s(∀q (s ⊨ q ≡ q) → s ⊨ p)›
proof(safe intro!: "→I" Situation.GEN)
  fix s
  AOT_assume ‹p›
  moreover AOT_assume ‹∀q (s ⊨ q ≡ q)›
  ultimately AOT_show ‹s ⊨ p›
    using "∀E"(2) "≡E"(2) by blast
qed

AOT_theorem "fund-lem:4": ‹◻p → ◻∀s(∀q (s ⊨ q ≡ q) → s ⊨ p)›
  using "fund-lem:3" by (rule RM)

AOT_theorem "fund-lem:5": ‹◻∀s φ{s} → ∀s ◻φ{s}›
proof(safe intro!: "→I" Situation.GEN)
  fix s
  AOT_assume ‹◻∀s φ{s}›
  AOT_hence ‹∀s ◻φ{s}›
    using "Situation.res-var-bound-reas[CBF]"[THEN "→E"] by blast
  AOT_thus ‹◻φ{s}›
    using "Situation.∀E" by fast
qed

text‹Note: not explicit in PLM.›
AOT_theorem "fund-lem:5[world]": ‹◻∀w φ{w} → ∀w ◻φ{w}›
proof(safe intro!: "→I" PossibleWorld.GEN)
  fix w
  AOT_assume ‹◻∀w φ{w}›
  AOT_hence ‹∀w ◻φ{w}›
    using "PossibleWorld.res-var-bound-reas[CBF]"[THEN "→E"] by blast
  AOT_thus ‹◻φ{w}›
    using "PossibleWorld.∀E" by fast
qed

AOT_theorem "fund-lem:6": ‹∀w w ⊨ p → ◻∀w w ⊨ p›
proof(rule "→I")
  AOT_assume ‹∀w (w ⊨ p)›
  AOT_hence 1: ‹PossibleWorld(w) → (w ⊨ p)› for w
    using "∀E"(2) by blast
  AOT_show ‹◻∀w w ⊨ p›
  proof(rule "raa-cor:1")
    AOT_assume ‹¬◻∀w w ⊨ p›
    AOT_hence ‹♢¬∀w w ⊨ p›
      by (metis "KBasic:11" "≡E"(1))
    AOT_hence ‹♢∃x (¬(PossibleWorld(x) → x ⊨ p))›
      apply (rule "RM♢"[THEN "→E", rotated])
      by (simp add: "cqt-further:2")
    AOT_hence ‹∃x ♢(¬(PossibleWorld(x) → x ⊨ p))›
      by (metis "BF♢" "vdash-properties:10")
    then AOT_obtain x where x_prop: ‹♢¬(PossibleWorld(x) → x ⊨ p)›
      using "∃E"[rotated] by blast
    AOT_have ‹♢(PossibleWorld(x) & ¬x ⊨ p)›
      apply (AOT_subst ‹PossibleWorld(x) & ¬x ⊨ p›
                       ‹¬(PossibleWorld(x) → x ⊨ p)›)
       apply (meson "≡E"(6) "oth-class-taut:1:b" "oth-class-taut:3:a")
      by(fact x_prop)
    AOT_hence 2: ‹♢PossibleWorld(x) & ♢¬x ⊨ p›
      by (metis "KBasic2:3" "vdash-properties:10")
    AOT_hence ‹PossibleWorld(x)›
      using "&E"(1) "≡E"(1) "rigid-pw:2" by blast
    AOT_hence ‹◻(x ⊨ p)›
      using 2[THEN "&E"(2)]  1[unconstrain w, THEN "→E"] "→E"
            "rigid-truth-at:1"[unconstrain w, THEN "→E"]
      by (metis "≡E"(1))
    moreover AOT_have ‹¬◻(x ⊨ p)›
      using 2[THEN "&E"(2)] by (metis "¬¬I" "KBasic:12" "≡E"(4))
    ultimately AOT_show ‹p & ¬p› for p
      by (metis "raa-cor:3")
  qed
qed

AOT_theorem "fund-lem:7": ‹◻∀w(w ⊨ p) → ◻p›
proof(rule RM; rule "→I")
  AOT_modally_strict {
    AOT_obtain w where w_prop: ‹∀p (w ⊨ p ≡ p)›
      using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
    AOT_assume ‹∀w (w ⊨ p)›
    AOT_hence ‹w ⊨ p›
      using "PossibleWorld.∀E" by fast
    AOT_thus ‹p›
      using w_prop[THEN "∀E"(2), THEN "≡E"(1)] by blast
  }
qed

AOT_theorem "fund:1": ‹♢p ≡ ∃w w ⊨ p›
proof (rule "≡I"; rule "→I")
  AOT_assume ‹♢p›
  AOT_thus ‹∃w w ⊨ p›
    by (metis "fund-lem:1" "fund-lem:2" "→E")
next
  AOT_assume ‹∃w w ⊨ p›
  then AOT_obtain w where w_prop: ‹w ⊨ p›
    using "PossibleWorld.∃E"[rotated] by meson
  AOT_hence ‹♢∀p (w ⊨ p ≡ p)›
    using "world:1"[THEN "≡_dfE", THEN "&E"(2)] PossibleWorld.ψ "&E" by blast
  AOT_hence ‹∀p ♢(w ⊨ p ≡ p)›
    by (metis "Buridan♢" "→E")
  AOT_hence 1: ‹♢(w ⊨ p ≡ p)›
    by (metis "log-prop-prop:2" "rule-ui:1")
  AOT_have ‹♢((w ⊨ p → p) & (p → w ⊨ p))›
    apply (AOT_subst ‹(w ⊨ p → p) & (p → w ⊨ p)› ‹w ⊨ p ≡ p›)
     apply (meson "conventions:3" "≡E"(6) "oth-class-taut:3:a" "≡Df")
    by (fact 1)
  AOT_hence ‹♢(w ⊨ p → p)›
    by (metis "RM♢" "Conjunction Simplification"(1) "→E")
  moreover AOT_have ‹◻(w ⊨ p)›
    using w_prop by (metis "≡E"(1) "rigid-truth-at:1")
  ultimately AOT_show ‹♢p›
    by (metis "KBasic2:4" "≡E"(1) "→E")
qed

AOT_theorem "fund:2": ‹◻p ≡ ∀w (w ⊨ p)›
proof -
  AOT_have 0: ‹∀w (w ⊨ ¬p ≡ ¬w ⊨ p)›
    apply (rule PossibleWorld.GEN)
    using "coherent:1" by blast
  AOT_have ‹♢¬p ≡ ∃w (w ⊨ ¬p)›
    using "fund:1"[unvarify p, OF "log-prop-prop:2"] by blast
  also AOT_have ‹… ≡ ∃w ¬(w ⊨ p)›
  proof(safe intro!: "≡I" "→I")
    AOT_assume ‹∃w w ⊨ ¬p›
    then AOT_obtain w where w_prop: ‹w ⊨ ¬p›
      using "PossibleWorld.∃E"[rotated] by meson
    AOT_hence ‹¬w ⊨ p›
      using 0[THEN "PossibleWorld.∀E", THEN "≡E"(1)] "&E" by blast
    AOT_thus ‹∃w ¬w ⊨ p›
      by (rule "PossibleWorld.∃I")
  next
    AOT_assume ‹∃w ¬w ⊨ p›
    then AOT_obtain w where w_prop: ‹¬w ⊨ p›
      using "PossibleWorld.∃E"[rotated] by meson
    AOT_hence ‹w ⊨ ¬p›
      using 0[THEN "∀E"(2), THEN "→E", THEN "≡E"(1)] "&E"
      by (metis "coherent:1" "≡E"(2))
    AOT_thus ‹∃w w ⊨ ¬p›
      by (rule "PossibleWorld.∃I")
  qed
  finally AOT_have ‹¬♢¬p ≡ ¬∃w ¬w ⊨ p›
    by (meson "≡E"(1) "oth-class-taut:4:b")
  AOT_hence ‹◻p ≡ ¬∃w ¬w ⊨ p›
    by (metis "KBasic:12" "≡E"(5))
  also AOT_have ‹… ≡ ∀w w ⊨ p›
  proof(safe intro!: "≡I" "→I")
    AOT_assume ‹¬∃w ¬w ⊨ p›
    AOT_hence 0: ‹∀x (¬(PossibleWorld(x) & ¬x ⊨ p))›
      by (metis "cqt-further:4" "→E")
    AOT_show ‹∀w w ⊨ p›
      apply (AOT_subst ‹PossibleWorld(x) → x ⊨ p›
                       ‹¬(PossibleWorld(x) & ¬x ⊨ p)› for: x)
       using "oth-class-taut:1:a" apply presburger
      by (fact 0)
  next
    AOT_assume 0: ‹∀w w ⊨ p›
    AOT_have ‹∀x (¬(PossibleWorld(x) & ¬x ⊨ p))›
      by (AOT_subst (reverse) ‹¬(PossibleWorld(x) & ¬x ⊨ p)›
                              ‹PossibleWorld(x) → x ⊨ p› for: x)
         (auto simp: "oth-class-taut:1:a" 0)
    AOT_thus ‹¬∃w ¬w ⊨ p›
      by (metis "∃E" "raa-cor:3" "rule-ui:3")
  qed
  finally AOT_show ‹◻p ≡ ∀w w ⊨ p›.
qed

AOT_theorem "fund:3": ‹¬♢p ≡ ¬∃w w ⊨ p›
  by (metis (full_types) "contraposition:1[1]" "→I" "fund:1" "≡I" "≡E"(1,2))

AOT_theorem "fund:4": ‹¬◻p ≡ ∃w ¬w ⊨p›
  apply (AOT_subst ‹∃w ¬w ⊨ p› ‹¬ ∀w w ⊨ p›)
   apply (AOT_subst ‹PossibleWorld(x) → x ⊨ p›
                    ‹¬(PossibleWorld(x) & ¬x ⊨ p)› for: x)
  by (auto simp add: "oth-class-taut:1:a" "conventions:4" "≡Df" RN
                     "fund:2" "rule-sub-lem:1:a")

AOT_theorem "nec-dia-w:1": ‹◻p ≡ ∃w w ⊨ ◻p›
proof -
  AOT_have ‹◻p ≡ ♢◻p›
    using "S5Basic:2" by blast
  also AOT_have ‹... ≡ ∃w w ⊨ ◻p›
    using "fund:1"[unvarify p, OF "log-prop-prop:2"] by blast
  finally show ?thesis.
qed

AOT_theorem "nec-dia-w:2": ‹◻p ≡ ∀w w ⊨ ◻p›
proof -
  AOT_have ‹◻p ≡ ◻◻p›
    using 4 "qml:2"[axiom_inst] "≡I" by blast
  also AOT_have ‹... ≡ ∀w w ⊨ ◻p›
    using "fund:2"[unvarify p, OF "log-prop-prop:2"] by blast
  finally show ?thesis.
qed

AOT_theorem "nec-dia-w:3": ‹♢p ≡ ∃w w ⊨ ♢p›
proof -
  AOT_have ‹♢p ≡ ♢♢p›
    by (simp add: "4♢" "T♢" "≡I")
  also AOT_have ‹... ≡ ∃w w ⊨ ♢p›
    using "fund:1"[unvarify p, OF "log-prop-prop:2"] by blast
  finally show ?thesis.
qed

AOT_theorem "nec-dia-w:4": ‹♢p ≡ ∀w w ⊨ ♢p›
proof -
  AOT_have ‹♢p ≡ ◻♢p›
    by (simp add: "S5Basic:1")
  also AOT_have ‹... ≡ ∀w w ⊨ ♢p›
    using "fund:2"[unvarify p, OF "log-prop-prop:2"] by blast
  finally show ?thesis.
qed

AOT_theorem "conj-dist-w:1": ‹w ⊨ (p & q) ≡ ((w ⊨ p) & (w style='font-size: 18px;'>⊨ q))›
proof(safe intro!: "≡I" "→I")
  AOT_assume ‹w ⊨ (p & q)›
  AOT_hence 0: ‹◻w ⊨ (p & q)›
    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by blast
  AOT_modally_strict {
    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ & ψ)) → (w ⊨ φ & w ⊨ ψ))› for w φ ψ
    proof(safe intro!: "→I")
      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
      AOT_hence ‹w ⊨ (φ & ψ) ≡ (φ & ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
        using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
      moreover AOT_assume ‹w ⊨ (φ & ψ)›
      ultimately AOT_show ‹w ⊨ φ & w ⊨ ψ›
        by (metis "&I" "&E"(1) "&E"(2) "≡E"(1) "≡E"(2))
    qed
  }
  AOT_hence ‹♢∀p (w ⊨ p ≡ p) → ♢(w ⊨ (φ & ψ) → w ⊨ φ & w ⊨ ψ)› for w φ ψ
    by (rule "RM♢")
  moreover AOT_have pos: ‹♢∀p (w ⊨ p ≡ p)›
    using "world:1"[THEN "≡_dfE", OF PossibleWorld.ψ] "&E" by blast
  ultimately AOT_have ‹♢(w ⊨ (p & q) → w ⊨ p & w ⊨ q)› using "→E" by blast
  AOT_hence ‹♢(w ⊨ p) & ♢(w ⊨ q)›
    by (metis 0 "KBasic2:3" "KBasic2:4" "≡E"(1) "vdash-properties:10")
  AOT_thus ‹w ⊨ p & w ⊨ q›
    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
          "&E" "&I" by meson
next
  AOT_assume ‹w ⊨ p & w ⊨ q›
  AOT_hence ‹◻w ⊨ p & ◻w ⊨ q›
    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
          "&E" "&I" by blast
  AOT_hence 0: ‹◻(w ⊨ p & w ⊨ q)›
    by (metis "KBasic:3" "≡E"(2))
  AOT_modally_strict {
    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ φ & w ⊨ ψ) → (w ⊨ (φ & ψ)))› for w φ ψ
    proof(safe intro!: "→I")
      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
      AOT_hence ‹w ⊨ (φ & ψ) ≡ (φ & ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
        using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
      moreover AOT_assume ‹w ⊨ φ & w ⊨ ψ›
      ultimately AOT_show ‹w ⊨ (φ & ψ)›
        by (metis "&I" "&E"(1) "&E"(2) "≡E"(1) "≡E"(2))
    qed
  }
  AOT_hence ‹♢∀p (w ⊨ p ≡ p) → ♢((w ⊨ φ & w ⊨ ψ) → w ⊨ (φ & ψ))› for w φ ψ
    by (rule "RM♢")
  moreover AOT_have pos: ‹♢∀p (w ⊨ p ≡ p)›
    using "world:1"[THEN "≡_dfE", OF PossibleWorld.ψ] "&E" by blast
  ultimately AOT_have ‹♢((w ⊨ p & w ⊨ q) → w ⊨ (p & q))›
    using "→E" by blast
  AOT_hence ‹♢(w ⊨ (p & q))›
    by (metis 0 "KBasic2:4" "≡E"(1) "vdash-properties:10")
  AOT_thus ‹w ⊨ (p & q)›
    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by blast
qed

AOT_theorem "conj-dist-w:2": ‹w ⊨ (p → q) ≡ ((w ⊨ p) → (w ⊨ q))›
proof(safe intro!: "≡I" "→I")
  AOT_assume ‹w ⊨ (p → q)›
  AOT_hence 0: ‹◻w ⊨ (p → q)›
    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by blast
  AOT_assume ‹w ⊨ p›
  AOT_hence 1: ‹◻w ⊨ p›
    by (metis "T♢" "≡E"(1) "rigid-truth-at:3" "→E")
  AOT_modally_strict {
    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ → ψ)) → (w ⊨ φ → w ⊨ ψ))› for w φ ψ
    proof(safe intro!: "→I")
      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
      AOT_hence ‹w ⊨ (φ → ψ) ≡ (φ → ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
        using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
      moreover AOT_assume ‹w ⊨ (φ → ψ)›
      moreover AOT_assume ‹w ⊨ φ›
      ultimately AOT_show ‹w ⊨ ψ›
        by (metis "≡E"(1) "≡E"(2) "→E")
    qed
  }
  AOT_hence ‹♢∀p (w ⊨ p ≡ p) → ♢(w ⊨ (φ → ψ) → (w ⊨ φ → w ⊨ ψ))› for w φ ψ
    by (rule "RM♢")
  moreover AOT_have pos: ‹♢∀p (w ⊨ p ≡ p)›
    using "world:1"[THEN "≡_dfE", OF PossibleWorld.ψ] "&E" by blast
  ultimately AOT_have ‹♢(w ⊨ (p → q) → (w ⊨ p → w ⊨ q))›
    using "→E" by blast
  AOT_hence ‹♢(w ⊨ p → w ⊨ q)›
    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
  AOT_hence ‹♢w ⊨ q›
    by (metis 1 "KBasic2:4" "≡E"(1) "→E")
  AOT_thus ‹w ⊨ q›
    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
          "&E" "&I" by meson
next
  AOT_assume ‹w ⊨ p → w ⊨ q›
  AOT_hence ‹¬(w ⊨ p) ∨ w ⊨ q›
    by (metis "∨I"(1) "∨I"(2) "reductio-aa:1" "→E")
  AOT_hence ‹w ⊨ ¬p ∨ w ⊨ q›
    by (metis "coherent:1" "∨I"(1) "∨I"(2) "∨E"(2) "≡E"(2) "reductio-aa:1")
  AOT_hence 0: ‹◻(w ⊨ ¬p ∨ w ⊨ q)›
    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by (metis "KBasic:15" "∨I"(1) "∨I"(2) "∨E"(2) "reductio-aa:1" "→E")
  AOT_modally_strict {
    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ ¬φ ∨ w ⊨ ψ) → (w ⊨ (φ → ψ)))› for w φ ψ
    proof(safe intro!: "→I")
      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
      moreover AOT_assume ‹w ⊨ ¬φ ∨ w ⊨ ψ›
      ultimately AOT_show ‹w ⊨ (φ → ψ)›
        by (metis "∨E"(2) "→I" "≡E"(1) "≡E"(2) "log-prop-prop:2"
                  "reductio-aa:1" "rule-ui:1")
    qed
  }
  AOT_hence ‹♢∀p (w ⊨ p ≡ p) → ♢((w ⊨ ¬φ ∨ w ⊨ ψ) → w ⊨ (φ → ψ))› for w φ ψ
    by (rule "RM♢")
  moreover AOT_have pos: ‹♢∀p (w ⊨ p ≡ p)›
    using "world:1"[THEN "≡_dfE", OF PossibleWorld.ψ] "&E" by blast
  ultimately AOT_have ‹♢((w ⊨ ¬p ∨ w ⊨ q) → w ⊨ (p → q))›
    using "→E" by blast
  AOT_hence ‹♢(w ⊨ (p → q))›
    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
  AOT_thus ‹w ⊨ (p → q)›
    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by blast
qed

AOT_theorem "conj-dist-w:3": ‹w ⊨ (p ∨ q) ≡ ((w ⊨ p) ∨ (w ⊨ q))›
proof(safe intro!: "≡I" "→I")
  AOT_assume ‹w ⊨ (p ∨ q)›
  AOT_hence 0: ‹◻w ⊨ (p ∨ q)›
    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by blast
  AOT_modally_strict {
    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ ∨ ψ)) → (w ⊨ φ ∨ w ⊨ ψ))› for w φ ψ
    proof(safe intro!: "→I")
      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
      AOT_hence ‹w ⊨ (φ ∨ ψ) ≡ (φ ∨ ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
        using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
      moreover AOT_assume ‹w ⊨ (φ ∨ ψ)›
      ultimately AOT_show ‹w ⊨ φ ∨ w ⊨ ψ›
        by (metis "∨I"(1) "∨I"(2) "∨E"(3) "≡E"(1) "≡E"(2) "reductio-aa:1")
    qed
  }
  AOT_hence ‹♢∀p (w ⊨ p ≡ p) → ♢(w ⊨ (φ ∨ ψ) → (w ⊨ φ ∨ w ⊨ ψ))› for w φ ψ
    by (rule "RM♢")
  moreover AOT_have pos: ‹♢∀p (w ⊨ p ≡ p)›
    using "world:1"[THEN "≡_dfE", OF PossibleWorld.ψ] "&E" by blast
  ultimately AOT_have ‹♢(w ⊨ (p ∨ q) → (w ⊨ p ∨ w ⊨ q))› using "→E" by blast
  AOT_hence ‹♢(w ⊨ p ∨ w ⊨ q)›
    by (metis 0 "KBasic2:4" "≡E"(1) "vdash-properties:10")
  AOT_hence ‹♢w ⊨ p ∨ ♢w ⊨ q›
    using "KBasic2:2"[THEN "≡E"(1)] by blast
  AOT_thus ‹w ⊨ p ∨ w ⊨ q›
    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by (metis "∨I"(1) "∨I"(2) "∨E"(2) "reductio-aa:1")
next
  AOT_assume ‹w ⊨ p ∨ w ⊨ q›
  AOT_hence 0: ‹◻(w ⊨ p ∨ w ⊨ q)›
    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by (metis "KBasic:15" "∨I"(1) "∨I"(2) "∨E"(2) "reductio-aa:1" "→E")
  AOT_modally_strict {
    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ φ ∨ w ⊨ ψ) → (w ⊨ (φ ∨ ψ)))› for w φ ψ
    proof(safe intro!: "→I")
      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
      moreover AOT_assume ‹w ⊨ φ ∨ w ⊨ ψ›
      ultimately AOT_show ‹w ⊨ (φ ∨ ψ)›
        by (metis "∨I"(1) "∨I"(2) "∨E"(2) "≡E"(1) "≡E"(2)
                  "log-prop-prop:2" "reductio-aa:1" "rule-ui:1")
    qed
  }
  AOT_hence ‹♢∀p (w ⊨ p ≡ p) → ♢((w ⊨ φ ∨ w ⊨ ψ) → w ⊨ (φ ∨ ψ))› for w φ ψ
    by (rule "RM♢")
  moreover AOT_have pos: ‹♢∀p (w ⊨ p ≡ p)›
    using "world:1"[THEN "≡_dfE", OF PossibleWorld.ψ] "&E" by blast
  ultimately AOT_have ‹♢((w ⊨ p ∨ w ⊨ q) → w ⊨ (p ∨ q))›
    using "→E" by blast
  AOT_hence ‹♢(w ⊨ (p ∨ q))›
    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
  AOT_thus ‹w ⊨ (p ∨ q)›
    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by blast
qed

AOT_theorem "conj-dist-w:4": ‹w ⊨ (p ≡ q) ≡ ((w ⊨ p) ≡ (w ⊨ q))›
proof(rule "≡I"; rule "→I")
  AOT_assume ‹w ⊨ (p ≡ q)›
  AOT_hence 0: ‹◻w ⊨ (p ≡ q)›
    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by blast
  AOT_modally_strict {
    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ ≡ ψ)) → (w ⊨ φ ≡ w ⊨ ψ))› for w φ ψ
    proof(safe intro!: "→I")
      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
      AOT_hence ‹w ⊨ (φ ≡ ψ) ≡ (φ ≡ ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
        using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
      moreover AOT_assume ‹w ⊨ (φ ≡ ψ)›
      ultimately AOT_show ‹w ⊨ φ ≡ w ⊨ ψ›
        by (metis "≡E"(2) "≡E"(5) "Commutativity of ≡")
    qed
  }
  AOT_hence ‹♢∀p (w ⊨ p ≡ p) → ♢(w ⊨ (φ ≡ ψ) → (w ⊨ φ ≡ w ⊨ ψ))› for w φ ψ
    by (rule "RM♢")
  moreover AOT_have pos: ‹♢∀p (w ⊨ p ≡ p)›
    using "world:1"[THEN "≡_dfE", OF PossibleWorld.ψ] "&E" by blast
  ultimately AOT_have ‹♢(w ⊨ (p ≡ q) → (w ⊨ p ≡ w ⊨ q))›
    using "→E" by blast
  AOT_hence 1: ‹♢(w ⊨ p ≡ w ⊨ q)›
    by (metis 0 "KBasic2:4" "≡E"(1) "vdash-properties:10")
  AOT_have ‹♢((w ⊨ p → w ⊨ q) & (w ⊨ q → w ⊨ p))›
    apply (AOT_subst ‹(w ⊨ p → w ⊨ q) & (w ⊨ q → w ⊨ p)› ‹w ⊨ p ≡ w ⊨ q›)
     apply (meson "≡_dfE" "conventions:3" "→I" "df-rules-formulas[4]" "≡I")
    by (fact 1)
  AOT_hence 2: ‹♢(w ⊨ p → w ⊨ q) & ♢(w ⊨ q → w ⊨ p)›
    by (metis "KBasic2:3" "vdash-properties:10")
  AOT_have ‹♢(¬w ⊨ p ∨ w ⊨ q)› and ‹♢(¬w ⊨ q ∨ w ⊨ p)›
     apply (AOT_subst (reverse) ‹¬w ⊨ p ∨ w ⊨ q› ‹w ⊨ p → w ⊨ q›)
      apply (simp add: "oth-class-taut:1:c")
     apply (fact 2[THEN "&E"(1)])
    apply (AOT_subst (reverse) ‹¬w ⊨ q ∨ w ⊨ p› ‹w ⊨ q → w ⊨ p›)
     apply (simp add: "oth-class-taut:1:c")
    by (fact 2[THEN "&E"(2)])
  AOT_hence ‹♢(¬w ⊨ p) ∨ ♢w ⊨ q› and ‹♢¬w ⊨ q ∨ ♢w ⊨ p›
    using "KBasic2:2" "≡E"(1) by blast+
  AOT_hence ‹¬◻w ⊨ p ∨ ♢w ⊨ q› and ‹¬◻w ⊨ q ∨ ♢w ⊨ p›
    by (metis "KBasic:11" "∨I"(1) "∨I"(2) "∨E"(2) "≡E"(2) "raa-cor:1")+
  AOT_thus ‹w ⊨ p ≡ w ⊨ q›
    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by (metis "¬¬I" "T♢" "∨E"(2) "→I" "≡I" "≡E"(1) "rigid-truth-at:3")
next
  AOT_have ‹◻PossibleWorld(w)›
    using "≡E"(1) "rigid-pw:1" PossibleWorld.ψ by blast
  moreover {
    fix p
    AOT_modally_strict {
      AOT_have ‹PossibleWorld(w) → (w ⊨ p → ◻w ⊨ p)›
        using "rigid-truth-at:1" "→I"
        by (metis "≡E"(1))
    }
    AOT_hence ‹◻PossibleWorld(w) → ◻(w ⊨ p → ◻w ⊨ p)›
      by (rule RM)
  }
  ultimately AOT_have 1: ‹◻(w ⊨ p → ◻w ⊨ p)› for p
    by (metis "→E")
  AOT_assume ‹w ⊨ p ≡ w ⊨ q›
  AOT_hence 0: ‹◻(w ⊨ p ≡ w ⊨ q)›
    using "sc-eq-box-box:5"[THEN "→E", THEN "qml:2"[axiom_inst, THEN "→E"],
                            THEN "→E", OF "&I"]
          by (metis "1")
  AOT_modally_strict {
    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ φ ≡ w ⊨ ψ) → (w ⊨ (φ ≡ ψ)))› for w φ ψ
    proof(safe intro!: "→I")
      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
      moreover AOT_assume ‹w ⊨ φ ≡ w ⊨ ψ›
      ultimately AOT_show ‹w ⊨ (φ ≡ ψ)›
        by (metis "≡E"(2) "≡E"(6) "log-prop-prop:2" "rule-ui:1")
    qed
  }
  AOT_hence ‹♢∀p (w ⊨ p ≡ p) → ♢((w ⊨ φ ≡ w ⊨ ψ) → w ⊨ (φ ≡ ψ))› for w φ ψ
    by (rule "RM♢")
  moreover AOT_have pos: ‹♢∀p (w ⊨ p ≡ p)›
    using "world:1"[THEN "≡_dfE", OF PossibleWorld.ψ] "&E" by blast
  ultimately AOT_have ‹♢((w ⊨ p ≡ w ⊨ q) → w ⊨ (p ≡ q))›
    using "→E" by blast
  AOT_hence ‹♢(w ⊨ (p ≡ q))›
    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
  AOT_thus ‹w ⊨ (p ≡ q)›
    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by blast
qed

AOT_theorem "conj-dist-w:5": ‹w ⊨ (∀α φ{α}) ≡ (∀ α (w ⊨ φ{α}))›
proof(safe intro!: "≡I" "→I" GEN)
  AOT_assume ‹w ⊨ (∀α φ{α})›
  AOT_hence 0: ‹◻w ⊨ (∀α φ{α})›
    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by blast
  AOT_modally_strict {
    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (∀α φ{α})) → (∀α w ⊨ φ{α}))› for w
    proof(safe intro!: "→I" GEN)
      AOT_assume ‹∀p (w ⊨ p ≡ p)›
      moreover AOT_assume ‹w ⊨ (∀α φ{α})›
      ultimately AOT_show ‹w ⊨ φ{α}› for α
        by (metis "≡E"(1) "≡E"(2) "log-prop-prop:2" "rule-ui:1" "rule-ui:3")
    qed
  }
  AOT_hence ‹♢∀p (w ⊨ p ≡ p) → ♢(w ⊨ (∀α φ{α}) → (∀α w ⊨ φ{α}))› for w
    by (rule "RM♢")
  moreover AOT_have pos: ‹♢∀p (w ⊨ p ≡ p)›
    using "world:1"[THEN "≡_dfE", OF PossibleWorld.ψ] "&E" by blast
  ultimately AOT_have ‹♢(w ⊨ (∀α φ{α}) → (∀α w ⊨ φ{α}))› using "→E" by blast
  AOT_hence ‹♢(∀α w ⊨ φ{α})›
    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
  AOT_hence ‹∀α ♢w ⊨ φ{α}›
    by (metis "Buridan♢" "→E")
  AOT_thus ‹w ⊨ φ{α}› for α
    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
          "∀E"(2) by blast
next
  AOT_assume ‹∀α w ⊨ φ{α}›
  AOT_hence ‹w ⊨ φ{α}› for α using "∀E"(2) by blast
  AOT_hence ‹◻w ⊨ φ{α}› for α
    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
          "&E" "&I" by blast
  AOT_hence ‹∀α ◻w ⊨ φ{α}› by (rule GEN)
  AOT_hence 0: ‹◻∀α w ⊨ φ{α}› by (rule BF[THEN "→E"])
  AOT_modally_strict {
    AOT_have ‹∀p (w ⊨ p ≡ p) → ((∀α w ⊨ φ{α}) → (w ⊨ (∀α φ{α})))› for w
    proof(safe intro!: "→I")
      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
      moreover AOT_assume ‹∀α w ⊨ φ{α}›
      ultimately AOT_show ‹w ⊨ (∀α φ{α})›
        by (metis "≡E"(1) "≡E"(2) "log-prop-prop:2" "rule-ui:1"
                  "rule-ui:3" "universal-cor")
    qed
  }
  AOT_hence ‹♢∀p (w ⊨ p ≡ p) → ♢((∀α w ⊨ φ{α}) → w ⊨ (∀α φ{α}))› for w
    by (rule "RM♢")
  moreover AOT_have pos: ‹♢∀p (w ⊨ p ≡ p)›
    using "world:1"[THEN "≡_dfE", OF PossibleWorld.ψ] "&E" by blast
  ultimately AOT_have ‹♢((∀α w ⊨ φ{α}) → w ⊨ (∀α φ{α}))›
    using "→E" by blast
  AOT_hence ‹♢(w ⊨ (∀α φ{α}))›
    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
  AOT_thus ‹w ⊨ (∀α φ{α})›
    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by blast
qed

AOT_theorem "conj-dist-w:6": ‹w ⊨ (∃α φ{α}) ≡ (∃ α (w ⊨ φ{α}))›
proof(safe intro!: "≡I" "→I" GEN)
  AOT_assume ‹w ⊨ (∃α φ{α})›
  AOT_hence 0: ‹◻w ⊨ (∃α φ{α})›
    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by blast
  AOT_modally_strict {
    AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (∃α φ{α})) → (∃α w ⊨ φ{α}))› for w
    proof(safe intro!: "→I" GEN)
      AOT_assume ‹∀p (w ⊨ p ≡ p)›
      moreover AOT_assume ‹w ⊨ (∃α φ{α})›
      ultimately AOT_show ‹∃ α (w ⊨ φ{α})›
        by (metis "∃E" "∃I"(2) "≡E"(1,2) "log-prop-prop:2" "rule-ui:1") 
    qed
  }
  AOT_hence ‹♢∀p (w ⊨ p ≡ p) → ♢(w ⊨ (∃α φ{α}) → (∃α w ⊨ φ{α}))› for w
    by (rule "RM♢")
  moreover AOT_have pos: ‹♢∀p (w ⊨ p ≡ p)›
    using "world:1"[THEN "≡_dfE", OF PossibleWorld.ψ] "&E" by blast
  ultimately AOT_have ‹♢(w ⊨ (∃α φ{α}) → (∃α w ⊨ φ{α}))› using "→E" by blast
  AOT_hence ‹♢(∃α w ⊨ φ{α})›
    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
  AOT_hence ‹∃α ♢w ⊨ φ{α}›
    by (metis "BF♢" "→E")
  then AOT_obtain α where ‹♢w ⊨ φ{α}›
    using "∃E"[rotated] by blast
  AOT_hence ‹w ⊨ φ{α}›
    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"] by blast
  AOT_thus ‹∃ α w ⊨ φ{α}› by (rule "∃I")
next
  AOT_assume ‹∃α w ⊨ φ{α}›
  then AOT_obtain α where ‹w ⊨ φ{α}› using "∃E"[rotated] by blast
  AOT_hence ‹◻w ⊨ φ{α}›
    using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
          "&E" "&I" by blast
  AOT_hence ‹∃α ◻w ⊨ φ{α}›
    by (rule "∃I")
  AOT_hence 0: ‹◻∃α w ⊨ φ{α}›
    by (metis Buridan "→E")
  AOT_modally_strict {
    AOT_have ‹∀p (w ⊨ p ≡ p) → ((∃α w ⊨ φ{α}) → (w ⊨ (∃α φ{α})))› for w
    proof(safe intro!: "→I")
      AOT_assume ‹∀ p (w ⊨ p ≡ p)›
      moreover AOT_assume ‹∃α w ⊨ φ{α}›
      then AOT_obtain α where ‹w ⊨ φ{α}›
        using "∃E"[rotated] by blast
      ultimately AOT_show ‹w ⊨ (∃α φ{α})›
        by (metis "∃I"(2) "≡E"(1,2) "log-prop-prop:2" "rule-ui:1")
    qed
  }
  AOT_hence ‹♢∀p (w ⊨ p ≡ p) → ♢((∃α w ⊨ φ{α}) → w ⊨ (∃α φ{α}))› for w
    by (rule "RM♢")
  moreover AOT_have pos: ‹♢∀p (w ⊨ p ≡ p)›
    using "world:1"[THEN "≡_dfE", OF PossibleWorld.ψ] "&E" by blast
  ultimately AOT_have ‹♢((∃α w ⊨ φ{α}) → w ⊨ (∃α φ{α}))›
    using "→E" by blast
  AOT_hence ‹♢(w ⊨ (∃α φ{α}))›
    by (metis 0 "KBasic2:4" "≡E"(1) "→E")
  AOT_thus ‹w ⊨ (∃α φ{α})›
    using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
    by blast
qed

AOT_theorem "conj-dist-w:7": ‹(w ⊨ ◻p) → ◻w ⊨ p›
proof(rule "→I")
  AOT_assume ‹w ⊨ ◻p›
  AOT_hence ‹∃w w ⊨ ◻p› by (rule "PossibleWorld.∃I")
  AOT_hence ‹♢◻p› using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(2)]
    by blast
  AOT_hence ‹◻p›
    by (metis "5♢" "→E")
  AOT_hence 1: ‹◻◻p›
    by (metis "S5Basic:6" "≡E"(1))
  AOT_have ‹◻∀w w ⊨ p›
    by (AOT_subst (reverse) ‹∀w w ⊨ p› ‹◻p›)
       (auto simp add: "fund:2" 1)
  AOT_hence ‹∀w ◻w ⊨ p›
    using "fund-lem:5[world]"[THEN "→E"] by simp
  AOT_thus ‹◻w ⊨ p›
    using "→E" "PossibleWorld.∀E" by fast
qed

AOT_theorem "conj-dist-w:8": ‹∃w∃p((◻w ⊨ p) & ¬w ⊨ ◻p)›
proof -
  AOT_obtain r where A: r and ‹♢¬r›
    by (metis "&E"(1) "&E"(2) "≡_dfE" "∃E" "cont-tf:1" "cont-tf-thm:1")
  AOT_hence B: ‹¬◻r›
    by (metis "KBasic:11" "≡E"(2))
  AOT_have ‹♢r›
    using A "T♢"[THEN "→E"] by simp
  AOT_hence ‹∃w w ⊨ r›
    using "fund:1"[THEN "≡E"(1)] by blast
  then AOT_obtain w where w: ‹w ⊨ r›
    using "PossibleWorld.∃E"[rotated] by meson
  AOT_hence ‹◻w ⊨ r›
    by (metis "T♢" "≡E"(1) "rigid-truth-at:3" "vdash-properties:10")
  moreover AOT_have ‹¬w ⊨ ◻r›
  proof(rule "raa-cor:2")
    AOT_assume ‹w ⊨ ◻r›
    AOT_hence ‹∃w w ⊨ ◻r›
      by (rule "PossibleWorld.∃I")
    AOT_hence ‹◻r›
      by (metis "≡E"(2) "nec-dia-w:1")
    AOT_thus ‹◻r & ¬◻r›
      using B "&I" by blast
  qed
  ultimately AOT_have ‹◻w ⊨ r & ¬w ⊨ ◻r›
    by (rule "&I")
  AOT_hence ‹∃p (◻w ⊨ p & ¬w ⊨ ◻p)›
    by (rule "∃I")
  thus ?thesis
    by (rule "PossibleWorld.∃I")
qed

AOT_theorem "conj-dist-w:9": ‹(♢w ⊨ p) → w ⊨ ♢p›
proof(rule "→I"; rule "raa-cor:1")
  AOT_assume ‹♢w ⊨ p›
  AOT_hence 0: ‹w ⊨ p›
    by (metis "≡E"(1) "rigid-truth-at:2")
  AOT_assume ‹¬w ⊨ ♢p›
  AOT_hence 1: ‹w ⊨ ¬♢p›
    using "coherent:1"[unvarify p, THEN "≡E"(2), OF "log-prop-prop:2"] by blast
  moreover AOT_have ‹w ⊨ (¬♢p → ¬p)›
    using "T♢"[THEN "contraposition:1[1]", THEN RN]
          "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1), THEN "∀E"(2),
                   THEN "→E", rotated, OF PossibleWorld.ψ]
          by blast
  ultimately AOT_have ‹w ⊨ ¬p›
    using "conj-dist-w:2"[unvarify p q, OF "log-prop-prop:2", OF "log-prop-prop:2",
                          THEN "≡E"(1), THEN "→E"]
    by blast
  AOT_hence ‹w ⊨ p & w ⊨ ¬p› using 0 "&I" by blast
  AOT_thus ‹p & ¬p›
    by (metis "coherent:1" "Conjunction Simplification"(1,2) "≡E"(4)
              "modus-tollens:1" "raa-cor:3")
qed

AOT_theorem "conj-dist-w:10": ‹∃w∃p((w ⊨ ♢p) & ¬♢w ⊨ p)›
proof -
  AOT_obtain w where w: ‹∀p (w ⊨ p ≡ p)›
    using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
  AOT_obtain r where ‹¬r› and ‹♢r›
    using "cont-tf-thm:2" "cont-tf:2"[THEN "≡_dfE"] "&E" "∃E"[rotated] by metis
  AOT_hence ‹w ⊨ ¬r› and 0: ‹w ⊨ ♢r›
    using w[THEN "∀E"(1), OF "log-prop-prop:2", THEN "≡E"(2)] by blast+
  AOT_hence ‹¬w ⊨ r› using "coherent:1"[THEN "≡E"(1)] by blast
  AOT_hence ‹¬♢w ⊨ r› by (metis "≡E"(4) "rigid-truth-at:2")
  AOT_hence ‹w ⊨ ♢r & ¬♢w ⊨ r› using 0 "&I" by blast
  AOT_hence ‹∃p (w ⊨ ♢p & ¬♢w ⊨ p)› by (rule "∃I")
  thus ?thesis by (rule "PossibleWorld.∃I")
qed

AOT_theorem "two-worlds-exist:1": ‹∃p(ContingentlyTrue(p)) → ∃w (¬Actual(w))›
proof(rule "→I")
  AOT_assume ‹∃p ContingentlyTrue(p)›
  then AOT_obtain p where ‹ContingentlyTrue(p)›
    using "∃E"[rotated] by blast
  AOT_hence p: ‹p & ♢¬p›
    by (metis "≡_dfE" "cont-tf:1")
  AOT_hence ‹∃w w ⊨ ¬p›
    using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] "&E" by blast
  then AOT_obtain w where w: ‹w ⊨ ¬p›
    using "PossibleWorld.∃E"[rotated] by meson
  AOT_have ‹¬Actual(w)›
  proof(rule "raa-cor:2")
    AOT_assume ‹Actual(w)›
    AOT_hence ‹w ⊨ p›
      using p[THEN "&E"(1)] actual[THEN "≡_dfE", THEN "&E"(2)]
      by (metis "log-prop-prop:2" "raa-cor:3" "rule-ui:1" "→E" w)
    moreover AOT_have ‹¬(w ⊨ p)›
      by (metis "coherent:1" "≡E"(4) "reductio-aa:2" w) 
    ultimately AOT_show ‹w ⊨ p & ¬(w ⊨ p)›
      using "&I" by blast
  qed
  AOT_thus ‹∃w ¬Actual(w)›
    by (rule "PossibleWorld.∃I")
qed


AOT_theorem "two-worlds-exist:2": ‹∃p(ContingentlyFalse(p)) → ∃w (¬Actual(w))›
proof(rule "→I")
  AOT_assume ‹∃p ContingentlyFalse(p)›
  then AOT_obtain p where ‹ContingentlyFalse(p)›
    using "∃E"[rotated] by blast
  AOT_hence p: ‹¬p & ♢p›
    by (metis "≡_dfE" "cont-tf:2")
  AOT_hence ‹∃w w ⊨ p›
    using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] "&E" by blast
  then AOT_obtain w where w: ‹w ⊨ p›
    using "PossibleWorld.∃E"[rotated] by meson
  moreover AOT_have ‹¬Actual(w)›
  proof(rule "raa-cor:2")
    AOT_assume ‹Actual(w)›
    AOT_hence ‹w ⊨ ¬p›
      using p[THEN "&E"(1)] actual[THEN "≡_dfE", THEN "&E"(2)]
      by (metis "log-prop-prop:2" "raa-cor:3" "rule-ui:1" "→E" w)
    moreover AOT_have ‹¬(w ⊨ p)›
      using calculation by (metis "coherent:1" "≡E"(4) "reductio-aa:2") 
    AOT_thus ‹w ⊨ p & ¬(w ⊨ p)›
      using "&I" w by metis
  qed
  AOT_thus ‹∃w ¬Actual(w)›
    by (rule "PossibleWorld.∃I")
qed

AOT_theorem "two-worlds-exist:3": ‹∃w ¬Actual(w)›
  using "cont-tf-thm:1" "two-worlds-exist:1" "→E" by blast

AOT_theorem "two-worlds-exist:4": ‹∃w∃w'(w ≠ w')›
proof -
  AOT_obtain w where w: ‹Actual(w)›
    using "act-world:2"[THEN "uniqueness:1"[THEN "≡_dfE"],
                        THEN "cqt-further:5"[THEN "→E"]]
          "PossibleWorld.∃E"[rotated] "&E"
    by blast
  moreover AOT_obtain w' where w': ‹¬Actual(w')›
    using "two-worlds-exist:3" "PossibleWorld.∃E"[rotated] by meson
  AOT_have ‹¬(w = w')›
  proof(rule "raa-cor:2")
    AOT_assume ‹w = w'›
    AOT_thus ‹p & ¬p› for p
      using w w' "&E" by (metis "rule=E" "raa-cor:3")
  qed
  AOT_hence ‹w ≠ w'›
    by (metis "≡_dfI" "=-infix")
  AOT_hence ‹∃w' w ≠ w'›
    by (rule "PossibleWorld.∃I")
  thus ?thesis
    by (rule "PossibleWorld.∃I")
qed

(* TODO: more theorems *)

AOT_theorem "w-rel:1": ‹[λx φ{x}]↓ → [λx w ⊨ φ{x}]↓›
proof(rule "→I")
  AOT_assume ‹[λx φ{x}]↓›
  AOT_hence ‹◻[λx φ{x}]↓›
    by (metis "exist-nec" "→E")
  moreover AOT_have
    ‹◻[λx φ{x}]↓ → ◻∀x∀y(∀F([F]x ≡ [F]y) → ((w ⊨ φ{x}) ≡ ( w ⊨ φ{y})))›
  proof (rule RM; rule "→I"; rule GEN; rule GEN; rule "→I")
    AOT_modally_strict {
      fix x y
      AOT_assume ‹[λx φ{x}]↓›
      AOT_hence ‹∀x∀y (∀F ([F]x ≡ [F]y) → ◻(φ{x} ≡ φ{y}))›
        using "&E" "kirchner-thm-cor:1"[THEN "→E"] by blast
      AOT_hence ‹∀F ([F]x ≡ [F]y) → ◻(φ{x} ≡ φ{y})›
        using "∀E"(2) by blast
      moreover AOT_assume ‹∀F ([F]x ≡ [F]y)›
      ultimately AOT_have ‹◻(φ{x} ≡ φ{y})›
        using "→E" by blast
      AOT_hence ‹∀w (w ⊨ (φ{x} ≡ φ{y}))›
        using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
      AOT_hence ‹w ⊨ (φ{x} ≡ φ{y})›
        using "∀E"(2) using PossibleWorld.ψ "→E" by blast
      AOT_thus ‹(w ⊨ φ{x}) ≡ (w ⊨ φ{y})›
        using "conj-dist-w:4"[unvarify p q, OF "log-prop-prop:2",
                              OF "log-prop-prop:2", THEN "≡E"(1)] by blast
    }
  qed
  ultimately AOT_have ‹◻∀x∀y(∀F([F]x ≡ [F]y) → ((w ⊨ φ{x}) ≡ ( w ⊨ φ{y})))›
    using "→E" by blast
  AOT_thus ‹[λx w ⊨ φ{x}]↓›
    using "kirchner-thm:1"[THEN "≡E"(2)] by fast
qed

AOT_theorem "w-rel:2": ‹[λx₁...x_n φ{x₁...x_n}]↓ → [λx₁...x_n w ⊨ φ{x₁...x_n}]↓›
proof(rule "→I")
  AOT_assume ‹[λx₁...x_n φ{x₁...x_n}]↓›
  AOT_hence ‹◻[λx₁...x_n φ{x₁...x_n}]↓›
    by (metis "exist-nec" "→E")
  moreover AOT_have ‹◻[λx₁...x_n φ{x₁...x_n}]↓ → ◻∀x₁...∀x_n∀y₁...∀y_n(
 ∀F([F]x₁...x_n ≡ [F]y₁...y_n) → ((w ⊨ φ{x₁...x_n}) ≡ ( w ⊨ φ{y₁...y_n})))›
  proof (rule RM; rule "→I"; rule GEN; rule GEN; rule "→I")
    AOT_modally_strict {
      fix x₁x_n y₁y_n
      AOT_assume ‹[λx₁...x_n φ{x₁...x_n}]↓›
      AOT_hence ‹∀x₁...∀x_n∀y₁...∀y_n (
 ∀F ([F]x₁...x_n ≡ [F]y₁...y_n) → ◻(φ{x₁...x_n} ≡ φ{y₁...y_n}))›
        using "&E" "kirchner-thm-cor:2"[THEN "→E"] by blast
      AOT_hence ‹∀F ([F]x₁...x_n ≡ [F]y₁...y_n) → ◻(φ{x₁...x_n} ≡ φ{y₁...y_n})›
        using "∀E"(2) by blast
      moreover AOT_assume ‹∀F ([F]x₁...x_n ≡ [F]y₁...y_n)›
      ultimately AOT_have ‹◻(φ{x₁...x_n} ≡ φ{y₁...y_n})›
        using "→E" by blast
      AOT_hence ‹∀w (w ⊨ (φ{x₁...x_n} ≡ φ{y₁...y_n}))›
        using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
      AOT_hence ‹w ⊨ (φ{x₁...x_n} ≡ φ{y₁...y_n})›
        using "∀E"(2) using PossibleWorld.ψ "→E" by blast
      AOT_thus ‹(w ⊨ φ{x₁...x_n}) ≡ (w ⊨ φ{y₁...y_n})›
        using "conj-dist-w:4"[unvarify p q, OF "log-prop-prop:2",
                              OF "log-prop-prop:2", THEN "≡E"(1)] by blast
    }
  qed
  ultimately AOT_have ‹◻∀x₁...∀x_n∀y₁...∀y_n(
 ∀F([F]x₁...x_n ≡ [F]y₁...y_n) → ((w ⊨ φ{x₁...x_n}) ≡ ( w ⊨ φ{y₁...y_n})))›
    using "→E" by blast
  AOT_thus ‹[λx₁...x_n w ⊨ φ{x₁...x_n}]↓›
    using "kirchner-thm:2"[THEN "≡E"(2)] by fast
qed

AOT_theorem "w-rel:3": ‹[λx₁...x_n w ⊨ [F]x₁...x_n]↓›
  by (rule "w-rel:2"[THEN "→E"]) "cqt:2[lambda]"

AOT_define WorldIndexedRelation :: ‹Π → τ → Π› (‹__{_}›)
  "w-index": ‹[F]_w =_df [λx₁...x_n w ⊨ [F]x₁...x_n]›

AOT_define Rigid :: ‹τ → φ› (‹Rigid'(_')›)
  "df-rigid-rel:1":
‹Rigid(F) ≡_df F↓ & ◻∀x₁...∀x_n([F]x₁...x_n → ◻[F]x₁...x_n)›

AOT_define Rigidifies :: ‹τ → τ → φ› (‹Rigidifies'(_,_')›)
  "df-rigid-rel:2":
‹Rigidifies(F, G) ≡_df Rigid(F) & ∀x₁...∀x_n([F]x₁...x_n ≡ [G]x₁...x_n)›

AOT_theorem "rigid-der:1": ‹[[F]_w]x₁...x_n ≡ w ⊨ [F]x₁...x_n›
  apply (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]_\<kappa>¬" and
                                        σ="λ(Π, κ). «[λx₁...x_n κ ⊨ [Π]x₁...x_n]¬",
                                  simplified, OF "w-index"])
   apply (fact "w-rel:3")
  apply (rule "beta-C-meta"[THEN "→E"])
  by (fact "w-rel:3")

AOT_theorem "rigid-der:2": ‹Rigid([G]_w)›
proof(safe intro!: "≡_dfI"[OF "df-rigid-rel:1"] "&I")
  AOT_show ‹[G]_w↓›
    by (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]_\<kappa>¬" and
                                       σ="λ(Π, κ). «[λx₁...x_n κ ⊨ [Π]x₁...x_n]¬",
                                 simplified, OF "w-index"])
       (fact "w-rel:3")+
next
  AOT_have ‹◻∀x₁...∀x_n ([[G]_w]x₁...x_n → ◻[[G]_w]x₁...x_n)›
  proof(rule RN; safe intro!: "→I" GEN)
    AOT_modally_strict {
      AOT_have assms: ‹PossibleWorld(w)› using PossibleWorld.ψ.
      AOT_hence nec_pw_w: ‹◻PossibleWorld(w)›
        using "≡E"(1) "rigid-pw:1" by blast
      fix x₁x_n
      AOT_assume ‹[[G]_w]x₁...x_n›
      AOT_hence ‹[λx₁...x_n w ⊨ [G]x₁...x_n]x₁...x_n›
        using "rule-id-df:2:a[2]"[where τ="λ (Π, κ). «[Π]_\<kappa>¬" and
                                        σ="λ(Π, κ). «[λx₁...x_n κ ⊨ [Π]x₁...x_n]¬",
                                        simplified, OF "w-index", OF "w-rel:3"]
        by fast
      AOT_hence ‹w ⊨ [G]x₁...x_n›
        by (metis "β→C"(1))
      AOT_hence ‹◻w ⊨ [G]x₁...x_n›
        using "rigid-truth-at:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)]
        by blast
      moreover AOT_have ‹◻w ⊨ [G]x₁...x_n → ◻[λx₁...x_n w ⊨ [G]x₁...x_n]x₁...x_n›
      proof (rule RM; rule "→I")
        AOT_modally_strict {
          AOT_assume ‹w ⊨ [G]x₁...x_n›
          AOT_thus ‹[λx₁...x_n w ⊨ [G]x₁...x_n]x₁...x_n›
            by (auto intro!: "β←C"(1) simp: "w-rel:3" "cqt:2")
        }
      qed
      ultimately AOT_have 1: ‹◻[λx₁...x_n w ⊨ [G]x₁...x_n]x₁...x_n›
        using "→E" by blast
      AOT_show ‹◻[[G]_w]x₁...x_n›
        by (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]_\<kappa>¬" and
                                           σ="λ(Π, κ). «[λx₁...x_n κ ⊨ [Π]x₁...x_n]¬",
                                     simplified, OF "w-index"])
           (auto simp: 1 "w-rel:3")
    }
  qed
  AOT_thus ‹◻∀x₁...∀x_n ([[G]_w]x₁...x_n → ◻[[G]_w]x₁...x_n)›
    using "→E" by blast
qed

AOT_theorem "rigid-der:3": ‹∃F Rigidifies(F, G)›
proof -
  AOT_obtain w where w: ‹∀p (w ⊨ p ≡ p)›
    using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
  show ?thesis
  proof (rule "∃I"(1)[where τ=‹«[G]_w¬›])
    AOT_show ‹Rigidifies([G]_w, [G])›
    proof(safe intro!: "≡_dfI"[OF "df-rigid-rel:2"] "&I" GEN)
      AOT_show ‹Rigid([G]_w)›
        using "rigid-der:2" by blast
    next
      fix x₁x_n
      AOT_have ‹[[G]_w]x₁...x_n ≡ [λx₁...x_n w ⊨ [G]x₁...x_n]x₁...x_n›
      proof(rule "≡I"; rule "→I")
        AOT_assume ‹[[G]_w]x₁...x_n›
        AOT_thus ‹[λx₁...x_n w ⊨ [G]x₁...x_n]x₁...x_n›
          by (rule "rule-id-df:2:a[2]"
                      [where τ="λ (Π, κ). «[Π]_\<kappa>¬" and
                             σ="λ(Π, κ). «[λx₁...x_n κ ⊨ [Π]x₁...x_n]¬",
                       simplified, OF "w-index", OF "w-rel:3"])
      next
        AOT_assume ‹[λx₁...x_n w ⊨ [G]x₁...x_n]x₁...x_n›
        AOT_thus ‹[[G]_w]x₁...x_n›
          by (rule "rule-id-df:2:b[2]"
                      [where τ="λ (Π, κ). «[Π]_\<kappa>¬" and
                             σ="λ(Π, κ). «[λx₁...x_n κ ⊨ [Π]x₁...x_n]¬",
                       simplified, OF "w-index", OF "w-rel:3"])
      qed
      also AOT_have ‹… ≡ w ⊨ [G]x₁...x_n›
        by (rule "beta-C-meta"[THEN "→E"])
           (fact "w-rel:3")
      also AOT_have ‹… ≡ [G]x₁...x_n›
        using w[THEN "∀E"(1), OF "log-prop-prop:2"] by blast
      finally AOT_show ‹[[G]_w]x₁...x_n ≡ [G]x₁...x_n›.
    qed
  next
    AOT_show ‹[G]_w↓›
      by (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]_\<kappa>¬"
                                     and σ="λ(Π, κ). «[λx₁...x_n κ ⊨ [Π]x₁...x_n]¬",
                                   simplified, OF "w-index"])
         (auto simp: "w-rel:3")
  qed
qed

AOT_theorem "rigid-rel-thms:1":
  ‹◻(∀x₁...∀x_n ([F]x₁...x_n → ◻[F]x₁...x_n)) ≡ ∀x₁...∀x_n(♢[F]x₁...x_n → ◻[F]x₁...x_n)›
proof(safe intro!: "≡I" "→I" GEN)
  fix x₁x_n
  AOT_assume ‹◻∀x₁...∀x_n ([F]x₁...x_n → ◻[F]x₁...x_n)›
  AOT_hence ‹∀x₁...∀x_n ◻([F]x₁...x_n → ◻[F]x₁...x_n)›
    by (metis "→E" GEN RM "cqt-orig:3")
  AOT_hence ‹◻([F]x₁...x_n → ◻[F]x₁...x_n)›
    using "∀E"(2) by blast
  AOT_hence ‹♢[F]x₁...x_n → ◻[F]x₁...x_n›
    by (metis "≡E"(1) "sc-eq-box-box:1")
  moreover AOT_assume ‹♢[F]x₁...x_n›
  ultimately AOT_show ‹◻[F]x₁...x_n›
    using "→E" by blast
next
  AOT_assume ‹∀x₁...∀x_n (♢[F]x₁...x_n → ◻[F]x₁...x_n)›
  AOT_hence ‹♢[F]x₁...x_n → ◻[F]x₁...x_n› for x₁x_n
    using "∀E"(2) by blast
  AOT_hence ‹◻([F]x₁...x_n → ◻[F]x₁...x_n)› for x₁x_n
    by (metis "≡E"(2) "sc-eq-box-box:1")
  AOT_hence 0: ‹∀x₁...∀x_n ◻([F]x₁...x_n → ◻[F]x₁...x_n)›
    by (rule GEN)
  AOT_thus ‹◻(∀x₁...∀x_n ([F]x₁...x_n → ◻[F]x₁...x_n))›
    using "BF" "vdash-properties:10" by blast
qed

AOT_theorem "rigid-rel-thms:2":
  ‹◻(∀x₁...∀x_n ([F]x₁...x_n → ◻[F]x₁...x_n)) ≡ ∀x₁...∀x_n(◻[F]x₁...x_n ∨ ◻¬[F]x₁...x_n)›
proof(safe intro!: "≡I" "→I")
  AOT_assume ‹◻(∀x₁...∀x_n ([F]x₁...x_n → ◻[F]x₁...x_n))›
  AOT_hence 0: ‹∀x₁...∀x_n ◻([F]x₁...x_n → ◻[F]x₁...x_n)›
    using CBF[THEN "→E"] by blast
  AOT_show ‹∀x₁...∀x_n(◻[F]x₁...x_n ∨ ◻¬[F]x₁...x_n)›
  proof(rule GEN)
    fix x₁x_n
    AOT_have 1: ‹◻([F]x₁...x_n → ◻[F]x₁...x_n)›
      using 0[THEN "∀E"(2)].
    AOT_hence 2: ‹♢[F]x₁...x_n → [F]x₁...x_n›
      using "B♢" "Hypothetical Syllogism" "K♢" "vdash-properties:10" by blast
    AOT_have ‹[F]x₁...x_n ∨ ¬[F]x₁...x_n›
      using "exc-mid".
    moreover {
      AOT_assume ‹[F]x₁...x_n›
      AOT_hence ‹◻[F]x₁...x_n›
        using 1[THEN "qml:2"[axiom_inst, THEN "→E"], THEN "→E"] by blast
    }
    moreover {
      AOT_assume 3: ‹¬[F]x₁...x_n›
      AOT_have ‹◻¬[F]x₁...x_n›
      proof(rule "raa-cor:1")
        AOT_assume ‹¬◻¬[F]x₁...x_n›
        AOT_hence ‹♢[F]x₁...x_n›
          by (AOT_subst_def "conventions:5")
        AOT_hence ‹[F]x₁...x_n› using 2[THEN "→E"] by blast
        AOT_thus ‹[F]x₁...x_n & ¬[F]x₁...x_n›
          using 3 "&I" by blast
      qed
    }
    ultimately AOT_show ‹◻[F]x₁...x_n ∨ ◻¬[F]x₁...x_n›
      by (metis "∨I"(1,2) "raa-cor:1")
  qed
next
  AOT_assume 0: ‹∀x₁...∀x_n(◻[F]x₁...x_n ∨ ◻¬[F]x₁...x_n)›
  {
    fix x₁x_n
    AOT_have ‹◻[F]x₁...x_n ∨ ◻¬[F]x₁...x_n› using 0[THEN "∀E"(2)] by blast
    moreover {
      AOT_assume ‹◻[F]x₁...x_n›
      AOT_hence ‹◻◻[F]x₁...x_n›
        using "S5Basic:6"[THEN "≡E"(1)] by blast
      AOT_hence ‹◻([F]x₁...x_n → ◻[F]x₁...x_n)›
        using "KBasic:1"[THEN "→E"] by blast
    }
    moreover {
      AOT_assume ‹◻¬[F]x₁...x_n›
      AOT_hence ‹◻([F]x₁...x_n → ◻[F]x₁...x_n)›
        using "KBasic:2"[THEN "→E"] by blast
    }
    ultimately AOT_have ‹◻([F]x₁...x_n → ◻[F]x₁...x_n)›
      using "con-dis-i-e:4:b" "raa-cor:1" by blast
  }
  AOT_hence ‹∀x₁...∀x_n ◻([F]x₁...x_n → ◻[F]x₁...x_n)›
    by (rule GEN)
  AOT_thus ‹◻(∀x₁...∀x_n ([F]x₁...x_n → ◻[F]x₁...x_n))›
    using BF[THEN "→E"] by fast
qed

AOT_theorem "rigid-rel-thms:3": ‹Rigid(F) ≡ ∀x₁...∀x_n (◻[F]x₁...x_n ∨ ◻¬[F]x₁...x_n)›
  by (AOT_subst_thm "df-rigid-rel:1"[THEN "≡Df", THEN "≡S"(1), OF "cqt:2"(1)];
      AOT_subst_thm "rigid-rel-thms:2")
     (simp add: "oth-class-taut:3:a")

(*<*)
end
(*>*)