Quellcode-Bibliothek AOT_PossibleWorlds.thy   Sprache: Isabelle

(*<*)
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 "\<rightarrow>I"; rule GEN)
  fix q
  AOT_assume \<open>\<forall>p (s \<Turnstile> p \<equiv> p)\<close>
  AOT_hence \<open>s \<Turnstile> q \<equiv> q\<close> and \<open>s \<Turnstile> \<not>q \<equiv> \<not>q\<close>
    using "\<forall>E"(1)[rotated, OF "log-prop-prop:2"] by blast+
  AOT_thus \<open>s \<Turnstile> \<not>q \<equiv> \<not>s \<Turnstile> q\<close>
    by (metis "deduction-theorem" "\<equiv>I" "\<equiv>E"(1) "\<equiv>E"(2) "\<equiv>E"(4))
qed

AOT_theorem "sit-classical:2":
  \<open>\<forall>p (s \<Turnstile> p \<equiv> p) \<rightarrow> \<forall>q\<forall>r((s \<Turnstile> (q \<rightarrow> r)) \<equiv> (s \<Turnstile> q \<rightarrow> s \<Turnstile> r))\<close>
proof(rule "\<rightarrow>I"; rule GEN; rule GEN)
  fix q r
  AOT_assume \<open>\<forall>p (s \<Turnstile> p \<equiv> p)\<close>
  AOT_hence \<theta>: \<open>s \<Turnstile> q \<equiv> q\<close> and \<xi>: \<open>s \<Turnstile> r \<equiv> r\<close> and \<zeta>: \<open>(s \<Turnstile> (q \<rightarrow> r)) \<equiv> (q \<rightarrow> r)\<close>
    using "\<forall>E"(1)[rotated, OF "log-prop-prop:2"] by blast+
  AOT_show \<open>(s \<Turnstile> (q \<rightarrow> r)) \<equiv> (s \<Turnstile> q \<rightarrow> s \<Turnstile> r)\<close>
  proof (safe intro!: "\<equiv>I" "\<rightarrow>I")
    AOT_assume \<open>s \<Turnstile> (q \<rightarrow> r)\<close>
    moreover AOT_assume \<open>s \<Turnstile> q\<close>
    ultimately AOT_show \<open>s \<Turnstile> r\<close>
      using \<theta> \<xi> \<zeta> by (metis "\<equiv>E"(1) "\<equiv>E"(2) "vdash-properties:10")
  next
    AOT_assume \<open>s \<Turnstile> q \<rightarrow> s \<Turnstile> r\<close>
    AOT_thus \<open>s \<Turnstile> (q \<rightarrow> r)\<close>
      using \<theta> \<xi> \<zeta> by (metis "deduction-theorem" "\<equiv>E"(1) "\<equiv>E"(2) "\<rightarrow>E") 
  qed
qed

AOT_theorem "sit-classical:3":
  \<open>\<forall>p (s \<Turnstile> p \<equiv> p) \<rightarrow> ((s \<Turnstile> \<forall>\<alpha> \<phi>{\<alpha>}) \<equiv> \<forall>\<alpha> s \<Turnstile> \<phi>{\<alpha>})\<close>
proof (rule "\<rightarrow>I")
  AOT_assume \<open>\<forall>p (s \<Turnstile> p \<equiv> p)\<close>
  AOT_hence \<theta>: \<open>s \<Turnstile> \<phi>{\<alpha>} \<equiv> \<phi>{\<alpha>}\<close> and \<xi>: \<open>s \<Turnstile> \<forall>\<alpha> \<phi>{\<alpha>} \<equiv> \<forall>\<alpha> \<phi>{\<alpha>}\<close> for \<alpha>
    using "\<forall>E"(1)[rotated, OF "log-prop-prop:2"] by blast+
  AOT_show \<open>s \<Turnstile> \<forall>\<alpha> \<phi>{\<alpha>} \<equiv> \<forall>\<alpha> s \<Turnstile> \<phi>{\<alpha>}\<close>
  proof (safe intro!: "\<equiv>I" "\<rightarrow>I" GEN)
    fix \<alpha>
    AOT_assume \<open>s \<Turnstile> \<forall>\<alpha> \<phi>{\<alpha>}\<close>
    AOT_hence \<open>\<phi>{\<alpha>}\<close> using \<xi> "\<forall>E"(2) "\<equiv>E"(1) by blast
    AOT_thus \<open>s \<Turnstile> \<phi>{\<alpha>}\<close> using \<theta> "\<equiv>E"(2) by blast
  next
    AOT_assume \<open>\<forall>\<alpha> s \<Turnstile> \<phi>{\<alpha>}\<close>
    AOT_hence \<open>s \<Turnstile> \<phi>{\<alpha>}\<close> for \<alpha> using "\<forall>E"(2) by blast
    AOT_hence \<open>\<phi>{\<alpha>}\<close> for \<alpha> using \<theta> "\<equiv>E"(1) by blast
    AOT_hence \<open>\<forall>\<alpha> \<phi>{\<alpha>}\<close> by (rule GEN)
    AOT_thus \<open>s \<Turnstile> \<forall>\<alpha> \<phi>{\<alpha>}\<close> using \<xi> "\<equiv>E"(2) by blast
  qed
qed

AOT_theorem "sit-classical:4": \<open>\<forall>p (s \<Turnstile> p \<equiv> p) \<rightarrow> \<forall>q (s \<Turnstile> \<box>q \<rightarrow> \<box>s \<Turnstile> q)\<close>
proof(rule "\<rightarrow>I"; rule GEN; rule "\<rightarrow>I")
  fix q
  AOT_assume \<open>\<forall>p (s \<Turnstile> p \<equiv> p)\<close>
  AOT_hence \<theta>: \<open>s \<Turnstile> q \<equiv> q\<close> and \<xi>: \<open>s \<Turnstile> \<box>q \<equiv> \<box>q\<close>
    using "\<forall>E"(1)[rotated, OF "log-prop-prop:2"] by blast+
  AOT_assume \<open>s \<Turnstile> \<box>q\<close>
  AOT_hence \<open>\<box>q\<close> using \<xi> "\<equiv>E"(1) by blast
  AOT_hence \<open>q\<close> using "qml:2"[axiom_inst, THEN "\<rightarrow>E"] by blast
  AOT_hence \<open>s \<Turnstile> q\<close> using \<theta> "\<equiv>E"(2) by blast
  AOT_thus \<open>\<box>s \<Turnstile> q\<close> using "\<equiv>\<^sub>d\<^sub>fE" "&E"(1) "\<equiv>E"(1) "lem2:1" "true-in-s" by blast
qed

AOT_theorem "sit-classical:5":
  \<open>\<forall>p (s \<Turnstile> p \<equiv> p) \<rightarrow> \<exists>q(\<box>(s \<Turnstile> q) & \<not>(s \<Turnstile> \<box> q))\<close>
proof (rule "\<rightarrow>I")
  AOT_obtain r where A: \<open>r\<close> and \<open>\<diamond>\<not>r\<close>
    by (metis "&E"(1) "&E"(2) "\<equiv>\<^sub>d\<^sub>fE" "instantiation" "cont-tf:1" "cont-tf-thm:1")
  AOT_hence B: \<open>\<not>\<box>r\<close>
    using "KBasic:11" "\<equiv>E"(2) by blast
  moreover AOT_assume asm: \<open>\<forall> p (s \<Turnstile> p \<equiv> p)\<close>
  AOT_hence \<open>s \<Turnstile> r\<close>
    using "\<forall>E"(2) A "\<equiv>E"(2) by blast
  AOT_hence 1: \<open>\<box>s \<Turnstile> r\<close>
    using "\<equiv>\<^sub>d\<^sub>fE" "&E"(1) "\<equiv>E"(1) "lem2:1" "true-in-s" by blast
  AOT_have \<open>s \<Turnstile> \<not>\<box>r\<close>
    using asm[THEN "\<forall>E"(1)[rotated, OF "log-prop-prop:2"], THEN "\<equiv>E"(2)] B by blast
  AOT_hence \<open>\<not>s \<Turnstile> \<box>r\<close>
    using "sit-classical:1"[THEN "\<rightarrow>E", OF asm,
              THEN "\<forall>E"(1)[rotated, OF "log-prop-prop:2"], THEN "\<equiv>E"(1)] by blast
  AOT_hence \<open>\<box>s \<Turnstile> r & \<not>s \<Turnstile> \<box>r\<close>
    using 1 "&I" by blast
  AOT_thus \<open>\<exists>r (\<box>s \<Turnstile> r & \<not>s \<Turnstile> \<box>r)\<close>
    by (rule "\<exists>I")
qed

AOT_theorem "sit-classical:6":
  \<open>\<exists>s \<forall>p (s \<Turnstile> p \<equiv> p)\<close>
proof -
  have "cond-prop": \<open>ConditionOnPropositionalProperties
                        (\<lambda> \<Pi> . \<guillemotleft>\<exists>q (q & \<Pi> = [\<lambda>y q])\<guillemotright>)\<close>
  proof (safe intro!: "cond-prop[I]" GEN "\<rightarrow>I")
    fix F
    AOT_modally_strict {
      AOT_assume \<open>\<exists>q (q & F = [\<lambda>y q])\<close>
      then AOT_obtain q where \<open>q & F = [\<lambda>y q]\<close>
        using "\<exists>E"[rotated] by blast
      AOT_hence \<open>F = [\<lambda>y q]\<close>
        using "&E" by blast
      AOT_hence \<open>\<exists>q F = [\<lambda>y q]\<close>
        by (rule "\<exists>I")
      AOT_thus \<open>Propositional([F])\<close>
        by (metis "\<equiv>\<^sub>d\<^sub>fI" "prop-prop1")
    }
  qed
  AOT_have \<open>\<exists>s \<forall>F (s[F] \<equiv> \<exists>q (q & F = [\<lambda>y q]))\<close>
    using "comp-sit:1"[OF "cond-prop"].
  then AOT_obtain s\<^sub>0 where s\<^sub>0_prop: \<open>\<forall>F (s\<^sub>0[F] \<equiv> \<exists>q (q &&nbsp;F = [\<lambda>y q]))\<close>
    using "Situation.\<exists>E"[rotated] by meson
  AOT_have \<open>\<forall>p (s\<^sub>0 \<Turnstile> p \<equiv> p)\<close>
  proof(safe intro!: GEN "\<equiv>I" "\<rightarrow>I")
    fix p
    AOT_assume \<open>s\<^sub>0 \<Turnstile> p\<close>
    AOT_hence \<open>s\<^sub>0[\<lambda>y p]\<close>
      using lem1[THEN "\<rightarrow>E", OF Situation.\<psi>, THEN "\<equiv>E"(1)] by blast
    AOT_hence \<open>\<exists>q (q & [\<lambda>y p] = [\<lambda>y q])\<close>
      using s\<^sub>0_prop[THEN "\<forall>E"(1)[rotated, OF "prop-prop2:2"], THEN "\<equiv>E"(1)] by blast
    then AOT_obtain q\<^sub>1 where q\<^sub>1_prop: \<open>q\<^sub>1 & [\<lambda>y p] = [\<lambda>y q\<^sub>1]\<close>
      using "\<exists>E"[rotated] by blast
    AOT_hence \<open>p = q\<^sub>1\<close>
      by (metis "&E"(2) "\<equiv>E"(2) "p-identity-thm2:3")
    AOT_thus \<open>p\<close>
      using q\<^sub>1_prop[THEN "&E"(1)] "rule=E" id_sym by fast
  next
    fix p
    AOT_assume \<open>p\<close>
    moreover AOT_have \<open>[\<lambda>y p] = [\<lambda>y p]\<close>
      by (simp add: "rule=I:1"[OF "prop-prop2:2"])
    ultimately AOT_have \<open>p & [\<lambda>y p] = [\<lambda>y p]\<close>
      using "&I" by blast
    AOT_hence \<open>\<exists>q (q & [\<lambda>y p] = [\<lambda>y q])\<close>
      by (rule "\<exists>I")
    AOT_hence \<open>s\<^sub>0[\<lambda>y p]\<close>
      using s\<^sub>0_prop[THEN "\<forall>E"(1)[rotated, OF "prop-prop2:2"], THEN "\<equiv>E"(2)] by blast
    AOT_thus \<open>s\<^sub>0 \<Turnstile> p\<close>
      using lem1[THEN "\<rightarrow>E", OF Situation.\<psi>, THEN "\<equiv>E"(2)] by blast
  qed
  AOT_hence \<open>\<forall>p (s\<^sub>0 \<Turnstile> p \<equiv> p)\<close>
    using "&I" by blast
  AOT_thus \<open>\<exists>s \<forall>p (s \<Turnstile> p \<equiv> p)\<close>
    by (rule "Situation.\<exists>I")
qed

AOT_define PossibleWorld :: \<open>\<tau> \<Rightarrow> \<phi>\<close> (\<open>PossibleWorld'(_')\<close>)
  "world:1": \<open>PossibleWorld(x) \<equiv>\<^sub>d\<^sub>f Situation(x) & \<diamond>\<forall>p(x \<Turnstile> p \<equiv> p)\<close>

AOT_theorem "world:2": \<open>\<exists>x PossibleWorld(x)\<close>
proof -
  AOT_obtain s where s_prop: \<open>\<forall>p (s \<Turnstile> p \<equiv> p)\<close>
    using "sit-classical:6" "Situation.\<exists>E"[rotated] by meson
  AOT_have \<open>\<forall>p (s \<Turnstile> p \<equiv> p)\<close>
  proof(safe intro!: GEN "\<equiv>I" "\<rightarrow>I")
    fix p
    AOT_assume \<open>s \<Turnstile> p\<close>
    AOT_thus \<open>p\<close>
      using s_prop[THEN "\<forall>E"(2), THEN "\<equiv>E"(1)] by blast
  next
    fix p
    AOT_assume \<open>p\<close>
    AOT_thus \<open>s \<Turnstile> p\<close>
      using s_prop[THEN "\<forall>E"(2), THEN "\<equiv>E"(2)] by blast
  qed
  AOT_hence \<open>\<diamond>\<forall>p (s \<Turnstile> p \<equiv> p)\<close>
    by (metis "T\<diamond>"[THEN "\<rightarrow>E"])
  AOT_hence \<open>\<diamond>\<forall>p (s \<Turnstile> p \<equiv> p)\<close>
    using s_prop "&I" by blast
  AOT_hence \<open>PossibleWorld(s)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fI"] Situation.\<psi> "&I" by blast
  AOT_thus \<open>\<exists>x PossibleWorld(x)\<close>
    by (rule "\<exists>I")
qed

AOT_theorem "world:3": \<open>PossibleWorld(\<kappa>) \<rightarrow> \<kappa>\<down>\<close>
proof (rule "\<rightarrow>I")
  AOT_assume \<open>PossibleWorld(\<kappa>)\<close>
  AOT_hence \<open>Situation(\<kappa>)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE"] "&E" by blast
  AOT_hence \<open>A!\<kappa>\<close>
    by (metis "\<equiv>\<^sub>d\<^sub>fE" "&E"(1) situations)
  AOT_thus \<open>\<kappa>\<down>\<close>
    by (metis "russell-axiom[exe,1].\<psi>_denotes_asm")
qed

AOT_theorem "rigid-pw:1": \<open>PossibleWorld(x) \<equiv> \<box>PossibleWorld(x)\<close>
proof(safe intro!: "\<equiv>I" "\<rightarrow>I")
  AOT_assume \<open>PossibleWorld(x)\<close>
  AOT_hence \<open>Situation(x) & \<diamond>\<forall>p(x \<Turnstile> p \<equiv> p)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE"] by blast
  AOT_hence \<open>\<box>Situation(x) & \<box>\<diamond>\<forall>p(x \<Turnstile> p \<equiv> p)\<close>
    by (metis "S5Basic:1" "&I" "&E"(1) "&E"(2) "\<equiv>E"(1) "possit-sit:1")
  AOT_hence 0: \<open>\<box>(Situation(x) & \<diamond>\<forall>p(x \<Turnstile> p \<equiv> p))\<close>
    by (metis "KBasic:3" "\<equiv>E"(2))
  AOT_show \<open>\<box>PossibleWorld(x)\<close>
    by (AOT_subst \<open>PossibleWorld(x)\<close> \<open>Situation(x) & \<diamond>\<forall>p(x \<Turnstile> p \<equiv> p)\<close>)
       (auto simp: "\<equiv>Df" "world:1" 0)
next
  AOT_show \<open>PossibleWorld(x)\<close> if \<open>\<box>PossibleWorld(x)\<close>
    using that "qml:2"[axiom_inst, THEN "\<rightarrow>E"] by blast
qed

AOT_theorem "rigid-pw:2": \<open>\<diamond>PossibleWorld(x) \<equiv> PossibleWorld(x)\<close>
  using "rigid-pw:1"
  by (meson "RE\<diamond>" "S5Basic:2" "\<equiv>E"(2) "\<equiv>E"(6) "Commutativity of \<equiv>")

AOT_theorem "rigid-pw:3": \<open>\<diamond>PossibleWorld(x) \<equiv> \<box>PossibleWorld(x)\<close>
  using "rigid-pw:1" "rigid-pw:2" by (meson "\<equiv>E"(5))

AOT_theorem "rigid-pw:4": \<open>\<^bold>\<A>PossibleWorld(x) \<equiv> PossibleWorld(x)\<close>
  by (metis "Act-Sub:3" "\<rightarrow>I" "\<equiv>I" "\<equiv>E"(6) "nec-imp-act" "rigid-pw:1" "rigid-pw:2")

AOT_register_rigid_restricted_type
  PossibleWorld: \<open>PossibleWorld(\<kappa>)\<close>
proof
  AOT_modally_strict {
    AOT_show \<open>\<exists>x PossibleWorld(x)\<close> using "world:2".
  }
next
  AOT_modally_strict {
    AOT_show \<open>PossibleWorld(\<kappa>) \<rightarrow> \<kappa>\<down>\<close> for \<kappa> using "world:3".
  }
next
  AOT_modally_strict {
    AOT_show \<open>\<forall>\<alpha>(PossibleWorld(\<alpha>) \<rightarrow> \<box>PossibleWorld(\<alpha>))\<close>
      by (meson GEN "\<rightarrow>I" "\<equiv>E"(1) "rigid-pw:1")
  }
qed
AOT_register_variable_names
  PossibleWorld: w

AOT_theorem "world-pos": \<open>Possible(w)\<close>
proof (safe intro!: "\<equiv>\<^sub>d\<^sub>fE"[OF "world:1", OF PossibleWorld.\<psi>, THEN "&E"an>(1)]
                    pos[THEN "\<equiv>\<^sub>d\<^sub>fI"] "&I" )
  AOT_have \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", OF PossibleWorld.\<psi>, THEN "&E"(2)].
 \open\diamond>\<forall>( <> p\rightarrow>p\close>
include"rans.h"
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
        =i-i_gl,
      AOT_assume \<openjava.lang.StringIndexOutOfBoundsException: Index 1 out of bounds for length 1
     AOT_hence \openw\<Turnstile>  < p  \forallE")by blast
java.lang.StringIndexOutOfBoundsException: Range [26, 25) out of bounds for length 57
      ultimately p "<equiv>"1 blast
    java.lang.StringIndexOutOfBoundsException: Index 5 out of bounds for length 5
  
  AOT_hence inode_set_ctime_currentinode);
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", OF PossibleWorld.\<psi>, THEN "&E"(1),
                    THEN "possit-sit:1"[THEN "\<equiv>E"(1)]]
    by (metis "KBasic:16" "&I" "vdash-properties:10")
  AOT_show \<open>\<diamond>Actual(w)\<close>
    by (AOT_subst \<open>Actual(w)\<close> \<open>Situation(w) & \<forall>p (w \<Turnstile> p \<rightarrow> p)\<close>)
       (auto simp: actual "\<equiv>Df" 0)
qed

AOT_theorem "world-cons:1": \<open>Consistent(w)\<close>
  using "world-pos"
  using "pos-cons-sit:1"[unconstrain s, THEN "\<rightarrow>E", THEN "\<rightarrow>E"]
  by (meson "\<equiv>\<^sub>d\<^sub>fE" "&E"(1) pos)

AOT_theorem "world-cons:2": \<open>\<not>TrivialSituation(w)\<close>
proof(rule "raa-cor:2")
  AOT_assume \<open>TrivialSituation(w)\<close>
  AOT_hence \<open>Situation(w) & \<forall>p w \<Turnstile> p\<close>
    using "df-null-trivial:2"[THEN "\<equiv>\<^sub>d\<^sub>fE"] by blast
  AOT_hence 0: \<open>\<box>w \<Turnstile> (\<exists>p (p & \<not>p))\<close>
    using "&E"
    by (metis "Buridan\<diamond>" "T\<diamond>" "&E"(2) "\<equiv>E"(1) "lem2:3"[unconstrain s, THEN "\<rightarrow>E"]
              "log-prop-prop:2" "rule-ui:1" "universal-cor" "\<rightarrow>E")
  AOT_have \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using PossibleWorld.\<psi> "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", THEN "&E"(2)] by metis
  AOT_hence \<open>\<forall>p \<diamond>(w \<Turnstile> p \<equiv> p)\<close>
    using "Buridan\<diamond>"[THEN "\<rightarrow>E"] by blast
  AOT_hence \<open>\<diamond>(w \<Turnstile> (\<exists>p (p & \<not>p)) \<equiv> (\<exists>p (p & \<not>p)))\<close>
    by (metis "log-prop-prop:2" "rule-ui:1")
  AOT_hence \<open>\<diamond>(w \<Turnstile> (\<exists>p (p & \<not>p)) \<rightarrow> (\<exists>p (p &&nbsp;\<not>p)))\<close>
    using "RM\<diamond>"[THEN "\<rightarrow>E"] "\<rightarrow>I" "\<equiv>E"(1) by meson
  AOT_hence \<open>\<diamond>(\<exists>p (p & \<not>p))\<close> using 0
    by (metis "KBasic2:4" "\<equiv>E"(1) "\<rightarrow>E")
  moreover AOT_have \<open>\<not>\<diamond>(\<exists>p (p & \<not>p))\<close>
    by (metis "instantiation" "KBasic2:1" RN "\<equiv>E"(1) "raa-cor:2")
  ultimately AOT_show \<open>\<diamond>(\<exists>p (p & \<not>p)) & \<not>\<diamond>(\<exists>p (p & \<not>p))\<close>
    using "&I" by blast
qed

AOT_theorem "rigid-truth-at:1": \<open>w \<Turnstile> p \<equiv> \<box>w \<Turnstile> p\<close>
  using "lem2:1"[unconstrain s, THEN "\<rightarrow>E",
                 OF PossibleWorld.\<psi>[THEN "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE"], THEN "&E"(1)]].

AOT_theorem "rigid-truth-at:2": \<open>\<diamond>w \<Turnstile> p \<equiv> w \<Turnstile> p\<close>
  using "lem2:2"[unconstrain s, THEN "\<rightarrow>E",
                 OF PossibleWorld.\<psi>[THEN "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE"], THEN "&E"(1)]].

AOT_theorem "rigid-truth-at:3": \<open>\<diamond>w \<Turnstile> p \<equiv> \<box>w \<Turnstile> p\<close>
  using "lem2:3"[unconstrain s, THEN "\<rightarrow>E",
                 OF PossibleWorld.\<psi>[THEN "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE"], THEN "&E"(1)]].

AOT_theorem "rigid-truth-at:4": \<open>\<^bold>\<A>w \<Turnstile> p \<equiv> w \<Turnstile> p\<close>
  using "lem2:4"[unconstrain s, THEN "\<rightarrow>E",
                 OF PossibleWorld.\<psi>[THEN "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE"], THEN "&E"(1)]].

AOT_theorem "rigid-truth-at:5": \<open>\<not>w \<Turnstile> p \<equiv> \<box>\<not>w \<Turnstile> p\<close>
  using "lem2:5"[unconstrain s, THEN "\<rightarrow>E",
                 OF PossibleWorld.\<psi>[THEN "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE"], THEN "&E"(1)]].

AOT_define Maximal :: \<open>\<tau> \<Rightarrow> \<phi>\<close> (\<open>Maximal'(_')\<close>)
  max: \<open>Maximal(s) \<equiv>\<^sub>d\<^sub>f \<forall>p (s \<Turnstile> p \<or> s \<Turnstile> \<not>p)\<close>

AOT_theorem "world-max": \<open>Maximal(w)\<close>
proof(safe intro!: PossibleWorld.\<psi>[THEN "\<equiv>\<^sub>d\<^sub>fE"[OF "world:1"], THEN "&E"</span>(1)]
                   GEN "\<equiv>\<^sub>d\<^sub>fI"[OF max] "&I" )
  fix q
  AOT_have \<open>\<diamond>(w \<Turnstile> q \<or> w \<Turnstile> \<not>q)\<close>
  proof(rule "RM\<diamond>"[THEN "\<rightarrow>E"]; (rule "\<rightarrow>I")?)
    AOT_modally_strict {
      AOT_assume \<open>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
      AOT_hence \<open>w \<Turnstile> q \<equiv> q\<close> and \<open>w \<Turnstile> \<not>q \<equiv> \<not>q\<close>
        using "\<forall>E"(1)[rotated, OF "log-prop-prop:2"] by blast+
      AOT_thus \<open>w \<Turnstile> q \<or> w \<Turnstile> \<not>q\<close>
        by (metis "\<or>I"(1) "\<or>I"(2) "\<equiv>E"(3) "reductio-aa:1")
    }
  next
    AOT_show \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
      using PossibleWorld.\<psi>[THEN "\<equiv>\<^sub>d\<^sub>fE"[OF "world:1"], THEN "&E"(2)].
  qed
  AOT_hence \<open>\<diamond>w \<Turnstile> q \<or> \<diamond>w \<Turnstile> \<not>q\<close>
    using "KBasic2:2"[THEN "\<equiv>E"(1)] by blast
  AOT_thus \<open>w \<Turnstile> q \<or> w \<Turnstile> \<not>q\<close>
    using "lem2:2"[unconstrain s, THEN "\<rightarrow>E", unvarify p,
                   OF PossibleWorld.\<psi>[THEN "\<equiv>\<^sub>d\<^sub>fE"[OF "world:1"], THEN "&E"(1)],
                   THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by (metis "\<or>I"(1) "\<or>I"(2) "\<or>E"(3) "raa-cor:2")
qed

AOT_theorem "world=maxpos:1": \<open>Maximal(x) \<rightarrow> \<box>Maximal(x)\<close>
proof (AOT_subst \<open>Maximal(x)\<close> \<open>Situation(x) & \<forall>p (x \<Turnstile> p \<or> x \<Turnstile> \<not>p)\<close>;
       safe intro!: max "\<equiv>Df" "\<rightarrow>I"; frule "&E"(1); drule "&E"(2))
  AOT_assume sit_x: \<open>Situation(x)\<close>
  AOT_hence nec_sit_x: \<open>\<box>Situation(x)\<close>
    by (metis "\<equiv>E"(1) "possit-sit:1")
  AOT_assume \<open>\<forall>p (x \<Turnstile> p \<or> x \<Turnstile> \<not>p)\<close>
  AOT_hence \<open>x \<Turnstile> p \<or> x \<Turnstile> \<not>p\<close> for p
    using "\<forall>E"(1)[rotated, OF "log-prop-prop:2"] by blast
  AOT_hence \<open>\<box>x \<Turnstile> p \<or> \<box>x \<Turnstile> \<not>p\<close> for p
    using "lem2:1"[unconstrain s, THEN "\<rightarrow>E", OF sit_x, unvarify p,
                   OF "log-prop-prop:2", THEN "\<equiv>E"(1)]
    by (metis "\<or>I"(1) "\<or>I"(2) "\<or>E"(2) "raa-cor:1")
  AOT_hence \<open>\<box>(x \<Turnstile> p \<or> x \<Turnstile> \<not>p)\<close> for p
    by (metis "KBasic:15" "\<rightarrow>E")
  AOT_hence \<open>\<forall>p \<box>(x \<Turnstile> p \<or> x \<Turnstile> \<not>p)\<close>
    by (rule GEN)
  AOT_hence \<open>\<box>\<forall>p (x \<Turnstile> p \<or> x \<Turnstile> \<not>p)\<close>
    by (rule BF[THEN "\<rightarrow>E"])
  AOT_thus \<open>\<box>(Situation(x) & \<forall>p (x \<Turnstile> p \<or> x \<Turnstile> \<not>p))\<close>
    using nec_sit_x by (metis "KBasic:3" "&I" "\<equiv>E"(2))
qed

AOT_theorem "world=maxpos:2": \<open>PossibleWorld(x) \<equiv> Maximal(x) & Possible(x)\<close>
proof(safe intro!: "\<equiv>I" "\<rightarrow>I" "&I" "world-pos"[unconstrain w, THEN "\<rightarrow>E"]
                   "world-max"[unconstrain w, THEN "\<rightarrow>E"];
      frule "&E"(2); drule "&E"(1))
  AOT_assume pos_x: \<open>Possible(x)\<close>
  AOT_have \<open>\<diamond>(Situation(x) & \<forall>p(x \<Turnstile> p \<rightarrow> p))\<close>
    apply (AOT_subst (reverse) \<open>Situation(x) & \<forall>p(x \<Turnstile> p \<rightarrow> p)\<close> \<open>Actual(x)\<close>)
     using actual "\<equiv>Df" apply presburger
    using "\<equiv>\<^sub>d\<^sub>fE" "&E"(2) pos pos_x by blast
  AOT_hence 0: \<open>\<diamond>\<forall>p(x \<Turnstile> p \<rightarrow> p)\<close>
    by (metis "KBasic2:3" "&E"(2) "vdash-properties:6")
  AOT_assume max_x: \<open>Maximal(x)\<close>
  AOT_hence sit_x: \<open>Situation(x)\<close> by (metis "\<equiv>\<^sub>d\<^sub>fE" max_x "&E"(1) max)
  AOT_have \<open>\<box>Maximal(x)\<close> using "world=maxpos:1"[THEN "\<rightarrow>E", OF max_x] by simp
  moreover AOT_have \<open>\<box>Maximal(x) \<rightarrow> \<box>(\<forall>p(x \<Turnstile> p \<rightarrow> p) \<rightarrow> \<forall>p (x \<Turnstile> p \<equiv> p))\<close>
  proof(safe intro!: "\<rightarrow>I" RM GEN)
    AOT_modally_strict {
      fix p
      AOT_assume 0: \<open>Maximal(x)\<close>
      AOT_assume 1: \<open>\<forall>p (x \<Turnstile> p \<rightarrow> p)\<close>
      AOT_show \<open>x \<Turnstile> p \<equiv> p\<close>
      proof(safe intro!: "\<equiv>I" "\<rightarrow>I" 1[THEN "\<forall>E"(2), THEN "\<rightarrow>E"]; rule "raa-cor:1")
        AOT_assume \<open>\<not>x \<Turnstile> p\<close>
        AOT_hence \<open>x \<Turnstile> \<not>p\<close>
          using 0[THEN "\<equiv>\<^sub>d\<^sub>fE"[OF max], THEN "&E"(2), THEN "\<forall>E"(2)]
                1 by (metis "\<or>E"(2))
        AOT_hence \<open>\<not>p\<close>
          using 1[THEN "\<forall>E"(1), OF "log-prop-prop:2", THEN "\<rightarrow>E"] by blast
        moreover AOT_assume p
        ultimately AOT_show \<open>p & \<not>p\<close> using "&I" by blast
      qed
    }
  qed
  ultimately AOT_have \<open>\<box>(\<forall>p(x \<Turnstile> p \<rightarrow> p) \<rightarrow> \<forall>p (x \<Turnstile> p \<equiv> p))\<close>
    using "\<rightarrow>E" by blast
  AOT_hence \<open>\<diamond>\<forall>p(x \<Turnstile> p \<rightarrow> p) \<rightarrow> \<diamond>\<forall>p(x \<Turnstile> p \<equiv> p)\<close>
    by (metis "KBasic:13"[THEN "\<rightarrow>E"])
  AOT_hence \<open>\<diamond>\<forall>p(x \<Turnstile> p \<equiv> p)\<close>
    using 0 "\<rightarrow>E" by blast
  AOT_thus \<open>PossibleWorld(x)\<close>
    using "\<equiv>\<^sub>d\<^sub>fI"[OF "world:1", OF "&I", OF sit_x] by blast
qed

AOT_define NecImpl :: \<open>\<phi> \<Rightarrow> \<phi> \<Rightarrow> \<phi>\<close> (infixl \<open>\<Rightarrow>\<close> 26)
  "nec-impl-p:1": \<open>p \<Rightarrow> q \<equiv>\<^sub>d\<^sub>f \<box>(p \<rightarrow> q)\<close>
AOT_define NecEquiv :: \<open>\<phi> \<Rightarrow> \<phi> \<Rightarrow> \<phi>\<close> (infixl \<open>\<Leftrightarrow>\<close> 21)
  "nec-impl-p:2": \<open>p \<Leftrightarrow> q \<equiv>\<^sub>d\<^sub>f (p \<Rightarrow> q) & (q \<Rightarrow> p)\<close>

AOT_theorem "nec-equiv-nec-im": \<open>p \<Leftrightarrow> q \<equiv> \<box>(p \<equiv> q)\<close>
proof(safe intro!: "\<equiv>I" "\<rightarrow>I")
  AOT_assume \<open>p \<Leftrightarrow> q\<close>
  AOT_hence \<open>(p \<Rightarrow> q)\<close> and \<open>(q \<Rightarrow> p)\<close>
    using "nec-impl-p:2"[THEN "\<equiv>\<^sub>d\<^sub>fE"] "&E" by blast+
  AOT_hence \<open>\<box>(p \<rightarrow> q)\<close> and \<open>\<box>(q \<rightarrow> p)\<close>
    using "nec-impl-p:1"[THEN "\<equiv>\<^sub>d\<^sub>fE"] by blast+
  AOT_thus \<open>\<box>(p \<equiv> q)\<close> by (metis "KBasic:4" "&I" "\<equiv>E"(2))
next
  AOT_assume \<open>\<box>(p \<equiv> q)\<close>
  AOT_hence \<open>\<box>(p \<rightarrow> q)\<close> and \<open>\<box>(q \<rightarrow> p)\<close>
    using "KBasic:4" "&E" "\<equiv>E"(1) by blast+
  AOT_hence \<open>(p \<Rightarrow> q)\<close> and \<open>(q \<Rightarrow> p)\<close>
    using "nec-impl-p:1"[THEN "\<equiv>\<^sub>d\<^sub>fI"] by blast+
  AOT_thus \<open>p \<Leftrightarrow> q\<close>
    using "nec-impl-p:2"[THEN "\<equiv>\<^sub>d\<^sub>fI"] "&I" by blast
qed

(* TODO: PLM: discuss these; still not in PLM *)
AOT_theorem world_closed_lem_1_a:
  \<open>(s \<Turnstile> (\<phi> & \<psi>)) \<rightarrow> (\<forall>p (s \<Turnstile> p \<equiv> p) \<rightarrow> (s \<Turnstile> \<phi> & s \<Turnstile> \<psi>))\<close>
proof(safe intro!: "\<rightarrow>I")
  AOT_assume \<open>\<forall> p (s \<Turnstile> p \<equiv> p)\<close>
  AOT_hence \<open>s \<Turnstile> (\<phi> & \<psi>) \<equiv> (\<phi> & \<psi>)\<close> and \<open>s \<Turnstile> \<phi> \<equiv> \<phi>\<close> and \<open>s \<Turnstile> \<psi> \<equiv> \<psi>\<close>
    using "\<forall>E"(1)[rotated, OF "log-prop-prop:2"] by blast+
  moreover AOT_assume \<open>s \<Turnstile> (\<phi> & \<psi>)\<close>
  ultimately AOT_show \<open>s \<Turnstile> \<phi> & s \<Turnstile> \<psi>\<close>
    by (metis "&I" "&E"(1) "&E"(2) "\<equiv>E"(1) "\<equiv>E"(2))
qed

AOT_theorem world_closed_lem_1_b:
  \<open>(s \<Turnstile> \<phi> & (\<phi> \<rightarrow> q)) \<rightarrow> (\<forall>p (s \<Turnstile> p \<equiv> p) \<rightarrow> s \<Turnstile> q)\<close>
proof(safe intro!: "\<rightarrow>I")
  AOT_assume \<open>\<forall> p (s \<Turnstile> p \<equiv> p)\<close>
  AOT_hence \<open>s \<Turnstile> \<phi> \<equiv> \<phi>\<close> for \<phi>
    using "\<forall>E"(1)[rotated, OF "log-prop-prop:2"] by blast
  moreover AOT_assume \<open>s \<Turnstile> \<phi> & (\<phi> \<rightarrow> q)\<close>
  ultimately AOT_show \<open>s \<Turnstile> q\<close>
    by (metis "&E"(1) "&E"(2) "\<equiv>E"(1) "\<equiv>E"(2) "\<rightarrow>E")
qed

AOT_theorem world_closed_lem_1_c:
  \<open>(s \<Turnstile> \<phi> & s \<Turnstile> (\<phi> \<rightarrow> \<psi>)) \<rightarrow> (\<forall>p (s \<Turnstile> p \<equiv> p) \<rightarrow> s \<Turnstile> \<psi>)\<close>
proof(safe intro!: "\<rightarrow>I")
  AOT_assume \<open>\<forall> p (s \<Turnstile> p \<equiv> p)\<close>
  AOT_hence \<open>s \<Turnstile> \<phi> \<equiv> \<phi>\<close> for \<phi>
    using "\<forall>E"(1)[rotated, OF "log-prop-prop:2"] by blast
  moreover AOT_assume \<open>s \<Turnstile> \<phi> & s \<Turnstile> (\<phi> \<rightarrow> \<psi>)\<close>
  ultimately AOT_show \<open>s \<Turnstile> \<psi>\<close>
    by (metis "&E"(1) "&E"(2) "\<equiv>E"(1) "\<equiv>E"(2) "\<rightarrow>E")
qed

AOT_theorem "world-closed-lem:1[0]":
  \<open>q \<rightarrow> (\<forall>p (s \<Turnstile> p \<equiv> p) \<rightarrow> s \<Turnstile> q)\<close>
  by (meson "\<rightarrow>I" "\<equiv>E"(2) "log-prop-prop:2" "rule-ui:1")

AOT_theorem "world-closed-lem:1[1]":
  \<open>s \<Turnstile> p\<^sub>1 & (p\<^sub>1 \<rightarrow> q) \<rightarrow> (\<forall>p (s \<Turnstile> p \<equiv> p) \<rightarrow> s \<Turnstile> q)\<close>
  using world_closed_lem_1_b.

AOT_theorem "world-closed-lem:1[2]":
  \<open>s \<Turnstile> p\<^sub>1 & s \<Turnstile> p\<^sub>2 & ((p\<^sub>1 & p\<^sub>2) \<rightarrow> q) \<rightarrow> (\<forall>p (s \<Turnstile> p \<equiv> p) \<rightarrow> s \<Turnstile> q)\<close>
  using world_closed_lem_1_b world_closed_lem_1_a
  by (metis (full_types) "&I" "&E" "\<rightarrow>I" "\<rightarrow>E")

AOT_theorem "world-closed-lem:1[3]":
  \<open>s \<Turnstile> p\<^sub>1 & s \<Turnstile> p\<^sub>2 & s \<Turnstile> p\<^sub>3 & ((p\<^sub>1 & p\<^sub>2 & p\<^sub>3) \<rightarrow> q) \<rightarrow> (\<forall>p (s \<Turnstile> p \<equiv> p) \<rightarrow> s \<Turnstile> q)\<close>
  using world_closed_lem_1_b world_closed_lem_1_a
  by (metis (full_types) "&I" "&E" "\<rightarrow>I" "\<rightarrow>E")

AOT_theorem "world-closed-lem:1[4]":
  \<open>s \<Turnstile> p\<^sub>1 & s \<Turnstile> p\<^sub>2 & s \<Turnstile> p\<^sub>3 & s \<Turnstile> p\<^sub>4 & ((p\<^sub>1 & p\<^sub>2 & p\<^sub>3 & p\<^sub>4) \<rightarrow> q) \<rightarrow>
   (\<forall>p (s \<Turnstile> p \<equiv> p) \<rightarrow> s \<Turnstile> q)\<close>
  using world_closed_lem_1_b world_closed_lem_1_a
  by (metis (full_types) "&I" "&E" "\<rightarrow>I" "\<rightarrow>E")

AOT_theorem "coherent:1": \<open>w \<Turnstile> \<not>p \<equiv> \<not>w \<Turnstile> p\<close>
proof(safe intro!: "\<equiv>I" "\<rightarrow>I")
  AOT_assume 1: \<open>w \<Turnstile> \<not>p\<close>
  AOT_show \<open>\<not>w \<Turnstile> p\<close>
  proof(rule "raa-cor:2")
    AOT_assume \<open>w \<Turnstile> p\<close>
    AOT_hence \<open>w \<Turnstile> p & w \<Turnstile> \<not>p\<close> using 1 "&I" by blast
    AOT_hence \<open>\<exists>q (w \<Turnstile> q & w \<Turnstile> \<not>q)\<close> by (rule "\<exists>I")
    moreover AOT_have \<open>\<not>\<exists>q (w \<Turnstile> q & w \<Turnstile> \<not>q)\<close>
      using "world-cons:1"[THEN "\<equiv>\<^sub>d\<^sub>fE"[OF cons], THEN "&E"(2)].
    ultimately AOT_show \<open>\<exists>q (w \<Turnstile> q & w \<Turnstile> \<not>q) & \<not>\<exists>q (w \<Turnstile> q & w \<Turnstile> \<not>q)\<close>
      using "&I" by blast
  qed
next
  AOT_assume \<open>\<not>w \<Turnstile> p\<close>
  AOT_thus \<open>w \<Turnstile> \<not>p\<close>
    using "world-max"[THEN "\<equiv>\<^sub>d\<^sub>fE"[OF max], THEN "&E"(2)]
    by (metis "\<or>E"(2) "log-prop-prop:2" "rule-ui:1")
qed

AOT_theorem "coherent:2": \<open>w \<Turnstile> p \<equiv> \<not>w \<Turnstile> \<not>p\<close>
  by (metis "coherent:1" "deduction-theorem" "\<equiv>I" "\<equiv>E"(1) "\<equiv>E"(2) "raa-cor:3")

AOT_theorem "act-world:1": \<open>\<exists>w \<forall>p (w \<Turnstile> p \<equiv> p)\<close>
proof -
  AOT_obtain s where s_prop: \<open>\<forall>p (s \<Turnstile> p \<equiv> p)\<close>
    using "sit-classical:6" "Situation.\<exists>E"[rotated] by meson
  AOT_hence \<open>\<diamond>\<forall>p (s \<Turnstile> p \<equiv> p)\<close>
    by (metis "T\<diamond>" "vdash-properties:10")
  AOT_hence \<open>PossibleWorld(s)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fI"] Situation.\<psi> "&I" by blast
  AOT_hence \<open>PossibleWorld(s) & \<forall>p (s \<Turnstile> p \<equiv> p)\<close>
    using "&I" s_prop by blast
  thus ?thesis by (rule "\<exists>I")
qed

AOT_theorem "act-world:2": \<open>\<exists>!w Actual(w)\<close>
proof -
  AOT_obtain w where w_prop: \<open>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "act-world:1" "PossibleWorld.\<exists>E"[rotated] by meson
  AOT_have sit_s: \<open>Situation(w)\<close>
    using PossibleWorld.\<psi> "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", THEN "&E"(1)] by blast
  show ?thesis
  proof (safe intro!: "uniqueness:1"[THEN "\<equiv>\<^sub>d\<^sub>fI"] "\<exists>I"(2) "&I" GEN "\<rightarrow>I"
                      PossibleWorld.\<psi> actual[THEN "\<equiv>\<^sub>d\<^sub>fI"] sit_s
                      "sit-identity"[unconstrain s, unconstrain s', THEN "\<rightarrow>E",
                                     THEN "\<rightarrow>E", THEN "\<equiv>E"(2)] "\<equiv>I"
                      w_prop[THEN "\<forall>E"(2), THEN "\<equiv>E"(1)])
    AOT_show \<open>PossibleWorld(w)\<close> using PossibleWorld.\<psi>.
  next
    AOT_show \<open>Situation(w)\<close>
      by (simp add: sit_s)
  next
    fix y p
    AOT_assume w_asm: \<open>PossibleWorld(y) & Actual(y)\<close>
    AOT_assume \<open>w \<Turnstile> p\<close>
    AOT_hence p: \<open>p\<close>
      using w_prop[THEN "\<forall>E"(2), THEN "\<equiv>E"(1)] by blast
    AOT_show \<open>y \<Turnstile> p\<close>
    proof(rule "raa-cor:1")
      AOT_assume \<open>\<not>y \<Turnstile> p\<close>
      AOT_hence \<open>y \<Turnstile> \<not>p\<close>
        by (metis "coherent:1"[unconstrain w, THEN "\<rightarrow>E"] "&E"(1) "\<equiv>E"(2) w_asm)
      AOT_hence \<open>\<not>p\<close>
        using w_asm[THEN "&E"(2), THEN actual[THEN "\<equiv>\<^sub>d\<^sub>fE"], THEN "&E"(2),
                    THEN "\<forall>E"(1), rotated, OF "log-prop-prop:2"]
              "\<rightarrow>E" by blast
      AOT_thus \<open>p & \<not>p\<close> using p "&I" by blast
    qed
  next
    AOT_show \<open>w \<Turnstile> p\<close> if \<open>y \<Turnstile> p\<close> and \<open>PossibleWorld(y) &&nbsp;Actual(y)\<close> for p y
      using that(2)[THEN "&E"(2), THEN actual[THEN "\<equiv>\<^sub>d\<^sub>fE"], THEN "&E"(2),
                    THEN "\<forall>E"(2), THEN "\<rightarrow>E", OF that(1)]
            w_prop[THEN "\<forall>E"(2), THEN "\<equiv>E"(2)] by blast
  next
    AOT_show \<open>Situation(y)\<close> if \<open>PossibleWorld(y) & Actual(y)\<close> for y
      using that[THEN "&E"(1)] "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", THEN "&E"(1)] by blast
  next
    AOT_show \<open>Situation(w)\<close>
      using sit_s by blast
  qed(simp)
qed

AOT_theorem "pre-walpha": \<open>\<^bold>\<iota>w Actual(w)\<down>\<close>
  using "A-Exists:2" "RA[2]" "act-world:2" "\<equiv>E"(2) by blast

AOT_define TheActualWorld :: \<open>\<kappa>\<^sub>s\<close> (\<open>\<^bold>w\<^sub>\<alpha>\<close>)
  "w-alpha": \<open>\<^bold>w\<^sub>\<alpha> =\<^sub>d\<^sub>f \<^bold>\<iota>w Actual(w)\<close>

(* TODO: not in PLM *)
AOT_theorem true_in_truth_act_true: \<open>\<top> \<Turnstile> p \<equiv> \<^bold>\<A>p\<close>
proof(safe intro!: "\<equiv>I" "\<rightarrow>I")
  AOT_have true_def: \<open>\<^bold>\<turnstile>\<^sub>\<box> \<top> = \<^bold>\<iota>x (A!x & \<forall>F (x[F] \<equiv> \<exists>p(p & F = [\<lambda>y p])))\<close>
    by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
  AOT_hence true_den: \<open>\<^bold>\<turnstile>\<^sub>\<box> \<top>\<down>\<close>
    using "t=t-proper:1" "vdash-properties:6" by blast
  {
    AOT_assume \<open>\<top> \<Turnstile> p\<close>
    AOT_hence \<open>\<top>[\<lambda>y p]\<close>
      by (metis "\<equiv>\<^sub>d\<^sub>fE" "con-dis-i-e:2:b" "prop-enc" "true-in-s")
    AOT_hence \<open>\<^bold>\<iota>x(A!x & \<forall>F (x[F] \<equiv> \<exists>q (q & F = [\<lambda>y q])))[\<lambda>y p]\<close>
      using "rule=E" true_def true_den by fast
    AOT_hence \<open>\<^bold>\<A>\<exists>q (q & [\<lambda>y p] = [\<lambda>y q])\<close>
      using "\<equiv>E"(1) "desc-nec-encode:1"[unvarify F] "prop-prop2:2" by fast
    AOT_hence \<open>\<exists>q \<^bold>\<A>(q & [\<lambda>y p] = [\<lambda>y q])\<close>
      by (metis "Act-Basic:10" "\<equiv>E"(1))
    then AOT_obtain q where \<open>\<^bold>\<A>(q & [\<lambda>y p] = [\<lambda>y q])\<close>
      using "\<exists>E"[rotated] by blast
    AOT_hence actq: \<open>\<^bold>\<A>q\<close> and \<open>\<^bold>\<A>[\<lambda>y p] = [\<lambda>y q]\<close>
      using "Act-Basic:2" "intro-elim:3:a" "&E" by blast+
    AOT_hence \<open>[\<lambda>y p] = [\<lambda>y q]\<close>
      using "id-act:1"[unvarify \<alpha> \<beta>, THEN "\<equiv>E"(2)] "prop-prop2:2" by blast
    AOT_hence \<open>p = q\<close>
      by (metis "intro-elim:3:b" "p-identity-thm2:3")
    AOT_thus \<open>\<^bold>\<A>p\<close>
      using actq "rule=E" id_sym by blast
  }
  {
    AOT_assume \<open>\<^bold>\<A>p\<close>
    AOT_hence \<open>\<^bold>\<A>(p & [\<lambda>y p] = [\<lambda>y p])\<close>
      by (auto intro!: "Act-Basic:2"[THEN "\<equiv>E"(2)] "&I"
               intro: "RA[2]" "=I"(1)[OF "prop-prop2:2"])
    AOT_hence \<open>\<exists>q \<^bold>\<A>(q & [\<lambda>y p] = [\<lambda>y q])\<close>
      using "\<exists>I" by fast
    AOT_hence \<open>\<^bold>\<A>\<exists>q (q & [\<lambda>y p] = [\<lambda>y q])\<close>
      by (metis "Act-Basic:10" "\<equiv>E"(2))
    AOT_hence \<open>\<^bold>\<iota>x(A!x & \<forall>F (x[F] \<equiv> \<exists>q (q & F = [\<lambda>y q])))[\<lambda>y p]\<close>
      using "\<equiv>E"(2) "desc-nec-encode:1"[unvarify F] "prop-prop2:2" by fast
    AOT_hence \<open>\<top>[\<lambda>y p]\<close>
      using "rule=E" true_def true_den id_sym by fast
    AOT_thus \<open>\<top> \<Turnstile> p\<close>
      by (safe intro!: "true-in-s"[THEN "\<equiv>\<^sub>d\<^sub>fI"] "&I" "possit-sit:6"
                       "prop-enc"[THEN "\<equiv>\<^sub>d\<^sub>fI"] true_den)
  }
qed

AOT_theorem "T-world": \<open>\<top> = \<^bold>w\<^sub>\<alpha>\<close>
proof -
  AOT_have true_den: \<open>\<^bold>\<turnstile>\<^sub>\<box> \<top>\<down>\<close>
    using "Situation.res-var:3" "possit-sit:6" "\<rightarrow>E" by blast
  AOT_have \<open>\<^bold>\<A>\<forall>p (\<top> \<Turnstile> p \<rightarrow> p)\<close>
  proof (safe intro!: "logic-actual-nec:3"[axiom_inst, THEN "\<equiv>E"(2)] GEN
                      "logic-actual-nec:2"[axiom_inst, THEN "\<equiv>E"(2)] "\<rightarrow>I")
    fix p
    AOT_assume \<open>\<^bold>\<A>\<top> \<Turnstile> p\<close>
    AOT_hence \<open>\<top> \<Turnstile> p\<close>
      using "lem2:4"[unconstrain s, unvarify \<beta>, OF true_den,
                     THEN "\<rightarrow>E", OF "possit-sit:6"] "\<equiv>E"(1) by blast
    AOT_thus \<open>\<^bold>\<A>p\<close> using true_in_truth_act_true "\<equiv>E"(1) by blast
  qed
  moreover AOT_have \<open>\<^bold>\<A>(Situation(\<kappa>) & \<forall>p (\<kappa> \<Turnstile> p \<rightarrow> p)) \<rightarrow> \<^bold>\<A>Actual(\<kappa>)\<close> for \<kappa>
    using actual[THEN "\<equiv>Df", THEN "conventions:3"[THEN "\<equiv>\<^sub>d\<^sub>fE", THEN "&E"pan>(2)],
                 THEN "RA[2]", THEN "act-cond"[THEN "\<rightarrow>E"]].
  ultimately AOT_have act_act_true: \<open>\<^bold>\<A>Actual(\<top>)\<close>
    using "possit-sit:4"[unvarify x, OF true_den, THEN "\<equiv>E"(2), OF "possit-sit:6"]
          "Act-Basic:2"[THEN "\<equiv>E"(2), OF "&I"] "\<rightarrow>E" by blast
  AOT_hence \<open>\<diamond>Actual(\<top>)\<close> by (metis "Act-Sub:3" "vdash-properties:10")
  AOT_hence \<open>Possible(\<top>)\<close>
    by (safe intro!: pos[THEN "\<equiv>\<^sub>d\<^sub>fI"] "&I" "possit-sit:6")
  moreover AOT_have \<open>Maximal(\<top>)\<close>
  proof (safe intro!: max[THEN "\<equiv>\<^sub>d\<^sub>fI"] "&I" "possit-sit:6" GEN)
    fix p
    AOT_have \<open>\<^bold>\<A>p \<or> \<^bold>\<A>\<not>p\<close>
      by (simp add: "Act-Basic:1")
    moreover AOT_have \<open>\<top> \<Turnstile> p\<close> if \<open>\<^bold>\<A>p\<close>
        using that true_in_truth_act_true[THEN "\<equiv>E"(2)] by blast
    moreover AOT_have \<open>\<top> \<Turnstile> \<not>p\<close> if \<open>\<^bold>\<A>\<not>p\<close>
      using that true_in_truth_act_true[unvarify p, THEN "\<equiv>E"(2)]
            "log-prop-prop:2" by blast
    ultimately AOT_show \<open>\<top> \<Turnstile> p \<or> \<top> \<Turnstile> \<not>p\<close>
      using "\<or>I"(3) "\<rightarrow>I" by blast
  qed
  ultimately AOT_have \<open>PossibleWorld(\<top>)\<close>
    by (safe intro!: "world=maxpos:2"[unvarify x, OF true_den, THEN "\<equiv>E"(2)] "&I")
  AOT_hence \<open>\<^bold>\<A>PossibleWorld(\<top>)\<close>
    using "rigid-pw:4"[unvarify x, OF true_den, THEN "\<equiv>E"(2)] by blast
  AOT_hence 1: \<open>\<^bold>\<A>(PossibleWorld(\<top>) & Actual(\<top>))\<close>
    using act_act_true "Act-Basic:2" "df-simplify:2" "intro-elim:3:b" by blast
  AOT_have \<open>\<^bold>w\<^sub>\<alpha> = \<^bold>\<iota>w(Actual(w))\<close>
    using "rule-id-df:1[zero]"[OF "w-alpha", OF "pre-walpha"] by simp
  moreover AOT_have w_act_den: \<open>\<^bold>w\<^sub>\<alpha>\<down>\<close>
    using calculation "t=t-proper:1" "\<rightarrow>E" by blast
  ultimately AOT_have \<open>\<forall>z (\<^bold>\<A>(PossibleWorld(z) & Actual(z)) \<rightarrow> z = \<^bold>w\<^sub>\<alpha>)\<close>
    using "nec-hintikka-scheme"[unvarify x] "\<equiv>E"(1) "&E" by blast
  AOT_thus \<open>\<top> = \<^bold>w\<^sub>\<alpha>\<close>
    using "\<forall>E"(1)[rotated, OF true_den] 1 "\<rightarrow>E" by blast
qed

AOT_act_theorem "truth-at-alpha:1": \<open>p \<equiv> \<^bold>w\<^sub>\<alpha> = \<^bold>\<iota>x (ExtensionOf(x, p))\<close>
  by (metis "rule=E" "T-world" "deduction-theorem" "ext-p-tv:3" id_sym "\<equiv>I"
            "\<equiv>E"(1) "\<equiv>E"(2) "q-True:1")

AOT_act_theorem "truth-at-alpha:2": \<open>p \<equiv> \<^bold>w\<^sub>\<alpha> \<Turnstile> p\<close>
proof -
  AOT_have \<open>PossibleWorld(\<^bold>w\<^sub>\<alpha>)\<close>
    using "&E"(1) "pre-walpha" "rule-id-df:2:b[zero]" "\<rightarrow>E"
          "w-alpha" "y-in:3" by blast
  AOT_hence sit_w_alpha: \<open>Situation(\<^bold>w\<^sub>\<alpha>)\<close>
    by (metis "\<equiv>\<^sub>d\<^sub>fE" "&E"(1) "world:1")
  AOT_have w_alpha_den: \<open>\<^bold>w\<^sub>\<alpha>\<down>\<close>
    using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
  AOT_have \<open>p \<equiv> \<top>\<^bold>\<Sigma>p\<close>
    using "q-True:3" by force
  moreover AOT_have \<open>\<top> = \<^bold>w\<^sub>\<alpha>\<close>
    using "T-world" by auto
  ultimately AOT_have \<open>p \<equiv> \<^bold>w\<^sub>\<alpha>\<^bold>\<Sigma>p\<close>
    using "rule=E" by fast
  moreover AOT_have \<open>\<^bold>w\<^sub>\<alpha> \<^bold>\<Sigma> p \<equiv> \<^bold>w\<^sub>\<alpha> \<Turnstile> p\<close>
    using lem1[unvarify x, OF w_alpha_den, THEN "\<rightarrow>E", OF sit_w_alpha]
    using "\<equiv>S"(1) "\<equiv>E"(1) "Commutativity of \<equiv>" "\<equiv>Df" sit_w_alpha "true-in-s" by blast
  ultimately AOT_show \<open>p \<equiv> \<^bold>w\<^sub>\<alpha> \<Turnstile> p\<close>
    by (metis "\<equiv>E"(5))
qed

AOT_theorem "alpha-world:1": \<open>PossibleWorld(\<^bold>w\<^sub>\<alpha>)\<close>
proof -
  AOT_have 0: \<open>\<^bold>w\<^sub>\<alpha> = \<^bold>\<iota>w Actual(w)\<close>
    using "pre-walpha" "rule-id-df:1[zero]" "w-alpha" by blast
  AOT_hence walpha_den: \<open>\<^bold>w\<^sub>\<alpha>\<down>\<close>
    by (metis "t=t-proper:1" "vdash-properties:6")
  AOT_have \<open>\<^bold>\<A>(PossibleWorld(\<^bold>w\<^sub>\<alpha>) & Actual(\<^bold>w\<^sub>\<alpha>))\<close>
    by (rule "actual-desc:2"[unvarify x, OF walpha_den, THEN "\<rightarrow>E"]) (fact 0)
  AOT_hence \<open>\<^bold>\<A>PossibleWorld(\<^bold>w\<^sub>\<alpha>)\<close>
    by (metis "Act-Basic:2" "&E"(1) "\<equiv>E"(1))
  AOT_thus \<open>PossibleWorld(\<^bold>w\<^sub>\<alpha>)\<close>
    using "rigid-pw:4"[unvarify x, OF walpha_den, THEN "\<equiv>E"(1)]
    by blast
qed

AOT_theorem "alpha-world:2": \<open>Maximal(\<^bold>w\<^sub>\<alpha>)\<close>
proof -
  AOT_have \<open>\<^bold>w\<^sub>\<alpha>\<down>\<close>
    using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
  then AOT_obtain x where x_def: \<open>x = \<^bold>w\<^sub>\<alpha>\<close>
    by (metis "instantiation" "rule=I:1" "existential:1" id_sym)
  AOT_hence \<open>PossibleWorld(x)\<close> using "alpha-world:1" "rule=E" id_sym by fast
  AOT_hence \<open>Maximal(x)\<close> by (metis "world-max"[unconstrain w, THEN "\<rightarrow>E"]) 
  AOT_thus \<open>Maximal(\<^bold>w\<^sub>\<alpha>)\<close> using x_def "rule=E" by blast
qed

AOT_theorem "t-at-alpha-strict": \<open>\<^bold>w\<^sub>\<alpha> \<Turnstile> p \<equiv> \<^bold>\<A>p\<close>
proof -
  AOT_have 0: \<open>\<^bold>w\<^sub>\<alpha> = \<^bold>\<iota>w Actual(w)\<close>
    using "pre-walpha" "rule-id-df:1[zero]" "w-alpha" by blast
  AOT_hence walpha_den: \<open>\<^bold>w\<^sub>\<alpha>\<down>\<close>
    by (metis "t=t-proper:1" "vdash-properties:6")
  AOT_have 1: \<open>\<^bold>\<A>(PossibleWorld(\<^bold>w\<^sub>\<alpha>) & Actual(\<^bold>w\<^sub>\<alpha>))\<close>
    by (rule "actual-desc:2"[unvarify x, OF walpha_den, THEN "\<rightarrow>E"]) (fact 0)
  AOT_have walpha_sit: \<open>Situation(\<^bold>w\<^sub>\<alpha>)\<close>
    by (meson "\<equiv>\<^sub>d\<^sub>fE" "alpha-world:2" "&E"(1) max)
  {
    fix p
    AOT_have 2: \<open>Situation(x) \<rightarrow> (\<^bold>\<A>x \<Turnstile> p \<equiv> x \<Turnstile> p)\<close> for x
      using "lem2:4"[unconstrain s] by blast
    AOT_assume \<open>\<^bold>w\<^sub>\<alpha> \<Turnstile> p\<close>
    AOT_hence \<theta>: \<open>\<^bold>\<A>\<^bold>w\<^sub>\<alpha> \<Turnstile> p\<close>
      using 2[unvarify x, OF walpha_den, THEN "\<rightarrow>E", OF walpha_sit, THEN "\<equiv>E"(2)]
      by argo
    AOT_have 3: \<open>\<^bold>\<A>Actual(\<^bold>w\<^sub>\<alpha>)\<close>
      using "1" "Act-Basic:2" "&E"(2) "\<equiv>E"(1) by blast
    AOT_have \<open>\<^bold>\<A>(Situation(\<^bold>w\<^sub>\<alpha>) & \<forall>q(\<^bold>w\<^sub>\<alpha> \<Turnstile> q \<rightarrow> q))\<close>
      apply (AOT_subst (reverse) \<open>Situation(\<^bold>w\<^sub>\<alpha>) & \<forall>q(\<^bold>w\<^sub>\<alpha> \<Turnstile> q \<rightarrow> q)\<close> \<open>Actual(\<^bold>w\<^sub>\<alpha>)\<close>)
       using actual "\<equiv>Df" apply blast
      by (fact 3)
    AOT_hence \<open>\<^bold>\<A>\<forall>q(\<^bold>w\<^sub>\<alpha> \<Turnstile> q \<rightarrow> q)\<close> by (metis "Act-Basic:2" "&E"(2) "\<equiv>E"(1))
    AOT_hence \<open>\<forall>q \<^bold>\<A>(\<^bold>w\<^sub>\<alpha> \<Turnstile> q \<rightarrow> q)\<close>
      using "logic-actual-nec:3"[axiom_inst, THEN "\<equiv>E"(1)] by blast
    AOT_hence \<open>\<^bold>\<A>(\<^bold>w\<^sub>\<alpha> \<Turnstile> p \<rightarrow> p)\<close> using "\<forall>E"(2) by blast
    AOT_hence \<open>\<^bold>\<A>(\<^bold>w\<^sub>\<alpha> \<Turnstile> p) \<rightarrow> \<^bold>\<A>p\<close> by (metis "act-cond" "vdash-properties:10")
    AOT_hence \<open>\<^bold>\<A>p\<close> using \<theta> "\<rightarrow>E" by blast
  }
  AOT_hence 2: \<open>\<^bold>w\<^sub>\<alpha> \<Turnstile> p \<rightarrow> \<^bold>\<A>p\<close> for p by (rule "\<rightarrow>I")
  AOT_have walpha_sit: \<open>Situation(\<^bold>w\<^sub>\<alpha>)\<close>
    using "\<equiv>\<^sub>d\<^sub>fE" "alpha-world:2" "&E"(1) max by blast
  show ?thesis
  proof(safe intro!: "\<equiv>I" "\<rightarrow>I" 2)
    AOT_assume actp: \<open>\<^bold>\<A>p\<close>
    AOT_show \<open>\<^bold>w\<^sub>\<alpha> \<Turnstile> p\<close>
    proof(rule "raa-cor:1")
      AOT_assume \<open>\<not>\<^bold>w\<^sub>\<alpha> \<Turnstile> p\<close>
      AOT_hence \<open>\<^bold>w\<^sub>\<alpha> \<Turnstile> \<not>p\<close>
        using "alpha-world:2"[THEN max[THEN "\<equiv>\<^sub>d\<^sub>fE"], THEN "&E"(2),
                              THEN "\<forall>E"(1), OF "log-prop-prop:2"]
        by (metis "\<or>E"(2))
      AOT_hence \<open>\<^bold>\<A>\<not>p\<close>
        using 2[unvarify p, OF "log-prop-prop:2", THEN "\<rightarrow>E"] by blast
      AOT_hence \<open>\<not>\<^bold>\<A>p\<close> by (metis "\<not>\<not>I" "Act-Sub:1" "\<equiv>E"(4))
      AOT_thus \<open>\<^bold>\<A>p & \<not>\<^bold>\<A>p\<close> using actp "&I" by blast
    qed
  qed
qed

AOT_act_theorem "not-act": \<open>w \<noteq> \<^bold>w\<^sub>\<alpha> \<rightarrow> \<not>Actual(w)\<close>
proof (rule "\<rightarrow>I"; rule "raa-cor:2")
  AOT_assume \<open>w \<noteq> \<^bold>w\<^sub>\<alpha>\<close>
  AOT_hence 0: \<open>\<not>(w = \<^bold>w\<^sub>\<alpha>)\<close> by (metis "\<equiv>\<^sub>d\<^sub>fE" "=-infix")
  AOT_have walpha_den: \<open>\<^bold>w\<^sub>\<alpha>\<down>\<close>
    using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
  AOT_have walpha_sit: \<open>Situation(\<^bold>w\<^sub>\<alpha>)\<close>
    using "\<equiv>\<^sub>d\<^sub>fE" "alpha-world:2" "&E"(1) max by blast
  AOT_assume act_w: \<open>Actual(w)\<close>
  AOT_hence w_sit: \<open>Situation(w)\<close> by (metis "\<equiv>\<^sub>d\<^sub>fE" actual "&E"(1))
  AOT_have sid: \<open>Situation(x') \<rightarrow> (w = x' \<equiv> \<forall>p (w \<Turnstile> p \<equiv> x' \<Turnstile> p))\<close> for x'
    using "sit-identity"[unconstrain s', unconstrain s, THEN "\<rightarrow>E", OF w_sit]
    by blast
  AOT_have \<open>w = \<^bold>w\<^sub>\<alpha>\<close>
  proof(safe intro!: GEN sid[unvarify x', OF walpha_den, THEN "\<rightarrow>E",
                             OF walpha_sit, THEN "\<equiv>E"(2)] "\<equiv>I" "\<rightarrow>I")
    fix p
    AOT_assume \<open>w \<Turnstile> p\<close>
    AOT_hence \<open>p\<close>
      using actual[THEN "\<equiv>\<^sub>d\<^sub>fE", OF act_w, THEN "&E"(2), THEN "\<forall>E"(2), THEN "\<rightarrow>E"]
      by blast
    AOT_hence \<open>\<^bold>\<A>p\<close>
      by (metis "RA[1]")
    AOT_thus \<open>\<^bold>w\<^sub>\<alpha> \<Turnstile> p\<close>
      using "t-at-alpha-strict"[THEN "\<equiv>E"(2)] by blast
  next
    fix p
    AOT_assume \<open>\<^bold>w\<^sub>\<alpha> \<Turnstile> p\<close>
    AOT_hence \<open>\<^bold>\<A>p\<close>
      using "t-at-alpha-strict"[THEN "\<equiv>E"(1)] by blast
    AOT_hence p: \<open>p\<close>
      using "logic-actual"[act_axiom_inst, THEN "\<rightarrow>E"] by blast
    AOT_show \<open>w \<Turnstile> p\<close>
    proof(rule "raa-cor:1")
      AOT_assume \<open>\<not>w \<Turnstile> p\<close>
      AOT_hence \<open>w \<Turnstile> \<not>p\<close>
        by (metis "coherent:1" "\<equiv>E"(2))
      AOT_hence \<open>\<not>p\<close>
        using actual[THEN "\<equiv>\<^sub>d\<^sub>fE", OF act_w, THEN "&E"(2), THEN "\<forall>E"(1),
                     OF "log-prop-prop:2", THEN "\<rightarrow>E"] by blast
      AOT_thus \<open>p & \<not>p\<close> using p "&I" by blast
    qed
  qed
  AOT_thus \<open>w = \<^bold>w\<^sub>\<alpha> & \<not>(w = \<^bold>w\<^sub>\<alpha>)\<close> using 0 "&I"an> by blast
qed

AOT_act_theorem "w-alpha-part": \<open>Actual(s) \<equiv> s \<unlhd> \<^bold>w\<^sub>\<alpha>\<close>
proof(safe intro!: "\<equiv>I" "\<rightarrow>I" "sit-part-whole"[THEN "\<equiv>\<^sub>d\<^sub>fI"] "&I" GEN
           dest!:  "sit-part-whole"[THEN "\<equiv>\<^sub>d\<^sub>fE"])
  AOT_show \<open>Situation(s)\<close> if \<open>Actual(s)\<close>
    using "\<equiv>\<^sub>d\<^sub>fE" actual "&E"(1) that by blast
next
  AOT_show \<open>Situation(\<^bold>w\<^sub>\<alpha>)\<close>
    using "\<equiv>\<^sub>d\<^sub>fE" "alpha-world:2" "&E"(1) max by blast
next
  fix p
  AOT_assume \<open>Actual(s)\<close>
  moreover AOT_assume \<open>s \<Turnstile> p\<close>
  ultimately AOT_have \<open>p\<close>
    using actual[THEN "\<equiv>\<^sub>d\<^sub>fE", THEN "&E"(2), THEN "\<forall>E"(2), THEN "\<rightarrow>E"] by blast
  AOT_thus \<open>\<^bold>w\<^sub>\<alpha> \<Turnstile> p\<close>
     by (metis "\<equiv>E"(1) "truth-at-alpha:2")
next
  AOT_assume 0: \<open>Situation(s) & Situation(\<^bold>w\<^sub>\<alpha>) & \<forall>p (s \<Turnstile> p \<rightarrow> \<^bold>w\<^sub>\<alpha> \<Turnstile> p)\<close>
  AOT_hence \<open>s \<Turnstile> p \<rightarrow> \<^bold>w\<^sub>\<alpha> \<Turnstile> p\<close> for p
    using "&E" "\<forall>E"(2) by blast
  AOT_hence \<open>s \<Turnstile> p \<rightarrow> p\<close> for p
    by (metis "\<rightarrow>I" "\<equiv>E"(2) "truth-at-alpha:2" "\<rightarrow>E")
  AOT_hence \<open>\<forall>p (s \<Turnstile> p \<rightarrow> p)\<close> by (rule GEN)
  AOT_thus \<open>Actual(s)\<close>
    using actual[THEN "\<equiv>\<^sub>d\<^sub>fI", OF "&I", OF 0[THEN "&E"(1), THEN "&E"(1)]] by blast
qed

AOT_act_theorem "act-world2:1": \<open>\<^bold>w\<^sub>\<alpha> \<Turnstile> p \<equiv> [\<lambda>y p]\<^bold>w\<^sub>\<alpha>\<close>
  apply (AOT_subst \<open>[\<lambda>y p]\<^bold>w\<^sub>\<alpha>\<close> p)
   apply (rule "beta-C-meta"[THEN "\<rightarrow>E", OF "prop-prop2:2", unvarify \<nu>\<^sub>1\<nu>\<^sub>n])
  using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" apply blast
  using "\<equiv>E"(2) "Commutativity of \<equiv>" "truth-at-alpha:2" by blast

AOT_act_theorem "act-world2:2": \<open>p \<equiv> \<^bold>w\<^sub>\<alpha> \<Turnstile> [\<lambda>y p]\<^bold>w\<^sub>\<alpha>\<close>
proof -
  AOT_have \<open>p \<equiv> [\<lambda>y p]\<^bold>w\<^sub>\<alpha>\<close>
    apply (rule "beta-C-meta"[THEN "\<rightarrow>E", OF "prop-prop2:2",
                              unvarify \<nu>\<^sub>1\<nu>\<^sub>n, symmetric])
    using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
  also AOT_have \<open>\<dots> \<equiv> \<^bold>w\<^sub>\<alpha> \<Turnstile> [\<lambda>y p]\<^bold>w\<^sub>\<alpha>\<close>
    by (meson "log-prop-prop:2" "rule-ui:1" "truth-at-alpha:2" "universal-cor")
  finally show ?thesis.
qed

AOT_theorem "fund-lem:1": \<open>\<diamond>p \<rightarrow> \<diamond>\<exists>w (w \<Turnstile> p)\<close>
proof (rule "RM\<diamond>"; rule "\<rightarrow>I"; rule "raa-cor:1")
  AOT_modally_strict {
    AOT_obtain w where w_prop: \<open>\<forall>q (w \<Turnstile> q \<equiv> q)\<close>
      using "act-world:1" "PossibleWorld.\<exists>E"[rotated] by meson
    AOT_assume p: \<open>p\<close>
    AOT_assume 0: \<open>\<not>\<exists>w (w \<Turnstile> p)\<close>
    AOT_have \<open>\<forall>w \<not>(w \<Turnstile> p)\<close>
      apply (AOT_subst \<open>PossibleWorld(x) \<rightarrow> \<not>x \<Turnstile> p\<close>
                       \<open>\<not>(PossibleWorld(x) & x \<Turnstile> p)\<close> for: x)
      apply (metis "&I" "&E"(1) "&E"(2) "\<rightarrow>I" "\<equiv>I" "modus-tollens:2")
      using "0" "cqt-further:4" "vdash-properties:10" by blast
    AOT_hence \<open>\<not>(w \<Turnstile> p)\<close>
      using PossibleWorld.\<psi> "rule-ui:3" "\<rightarrow>E" by blast
    AOT_hence \<open>\<not>p\<close>
      using w_prop[THEN "\<forall>E"(2), THEN "\<equiv>E"(2)] 
      by (metis "raa-cor:3")
    AOT_thus \<open>p & \<not>p\<close>
      using p "&I" by blast
  }
qed

AOT_theorem "fund-lem:2": \<open>\<diamond>\<exists>w (w \<Turnstile> p) \<rightarrow> \<exists>w (w \<Turnstile> p)\<close>
proof (rule "\<rightarrow>I")
  AOT_assume \<open>\<diamond>\<exists>w (w \<Turnstile> p)\<close>
  AOT_hence \<open>\<exists>w \<diamond>(w \<Turnstile> p)\<close>
    using "PossibleWorld.res-var-bound-reas[BF\<diamond>]"[THEN "\<rightarrow>E"] by auto
  then AOT_obtain w where \<open>\<diamond>(w \<Turnstile> p)\<close>
    using "PossibleWorld.\<exists>E"[rotated] by meson
  moreover AOT_have \<open>Situation(w)\<close>
    by (metis "\<equiv>\<^sub>d\<^sub>fE" "&E"(1) pos "world-pos")
  ultimately AOT_have \<open>w \<Turnstile> p\<close>
    using "lem2:2"[unconstrain s, THEN "\<rightarrow>E"]  "\<equiv>E" by blast
  AOT_thus \<open>\<exists>w w \<Turnstile> p\<close>
    by (rule "PossibleWorld.\<exists>I")
qed

AOT_theorem "fund-lem:3": \<open>p \<rightarrow> \<forall>s(\<forall>q (s \<Turnstile> q \<equiv> q) \<rightarrow> s \<Turnstile> p)\<close>
proof(safe intro!: "\<rightarrow>I" Situation.GEN)
  fix s
  AOT_assume \<open>p\<close>
  moreover AOT_assume \<open>\<forall>q (s \<Turnstile> q \<equiv> q)\<close>
  ultimately AOT_show \<open>s \<Turnstile> p\<close>
    using "\<forall>E"(2) "\<equiv>E"(2) by blast
qed

AOT_theorem "fund-lem:4": \<open>\<box>p \<rightarrow> \<box>\<forall>s(\<forall>q (s \<Turnstile> q \<equiv> q) \<rightarrow> s \<Turnstile> p)\<close>
  using "fund-lem:3" by (rule RM)

AOT_theorem "fund-lem:5": \<open>\<box>\<forall>s \<phi>{s} \<rightarrow> \<forall>s \<box>\<phi>{s}\<close>
proof(safe intro!: "\<rightarrow>I" Situation.GEN)
  fix s
  AOT_assume \<open>\<box>\<forall>s \<phi>{s}\<close>
  AOT_hence \<open>\<forall>s \<box>\<phi>{s}\<close>
    using "Situation.res-var-bound-reas[CBF]"[THEN "\<rightarrow>E"] by blast
  AOT_thus \<open>\<box>\<phi>{s}\<close>
    using "Situation.\<forall>E" by fast
qed

text\<open>Note: not explicit in PLM.\<close>
AOT_theorem "fund-lem:5[world]": \<open>\<box>\<forall>w \<phi>{w} \<rightarrow> \<forall>w \<box>\<phi>{w}\<close>
proof(safe intro!: "\<rightarrow>I" PossibleWorld.GEN)
  fix w
  AOT_assume \<open>\<box>\<forall>w \<phi>{w}\<close>
  AOT_hence \<open>\<forall>w \<box>\<phi>{w}\<close>
    using "PossibleWorld.res-var-bound-reas[CBF]"[THEN "\<rightarrow>E"] by blast
  AOT_thus \<open>\<box>\<phi>{w}\<close>
    using "PossibleWorld.\<forall>E" by fast
qed

AOT_theorem "fund-lem:6": \<open>\<forall>w w \<Turnstile> p \<rightarrow> \<box>\<forall>w w \<Turnstile> p\<close>
proof(rule "\<rightarrow>I")
  AOT_assume \<open>\<forall>w (w \<Turnstile> p)\<close>
  AOT_hence 1: \<open>PossibleWorld(w) \<rightarrow> (w \<Turnstile> p)\<close> for w
    using "\<forall>E"(2) by blast
  AOT_show \<open>\<box>\<forall>w w \<Turnstile> p\<close>
  proof(rule "raa-cor:1")
    AOT_assume \<open>\<not>\<box>\<forall>w w \<Turnstile> p\<close>
    AOT_hence \<open>\<diamond>\<not>\<forall>w w \<Turnstile> p\<close>
      by (metis "KBasic:11" "\<equiv>E"(1))
    AOT_hence \<open>\<diamond>\<exists>x (\<not>(PossibleWorld(x) \<rightarrow> x \<Turnstile> p))\<close>
      apply (rule "RM\<diamond>"[THEN "\<rightarrow>E", rotated])
      by (simp add: "cqt-further:2")
    AOT_hence \<open>\<exists>x \<diamond>(\<not>(PossibleWorld(x) \<rightarrow> x \<Turnstile> p))\<close>
      by (metis "BF\<diamond>" "vdash-properties:10")
    then AOT_obtain x where x_prop: \<open>\<diamond>\<not>(PossibleWorld(x) \<rightarrow> x \<Turnstile> p)\<close>
      using "\<exists>E"[rotated] by blast
    AOT_have \<open>\<diamond>(PossibleWorld(x) & \<not>x \<Turnstile> p)\<close>
      apply (AOT_subst \<open>PossibleWorld(x) & \<not>x \<Turnstile> p\<close>
                       \<open>\<not>(PossibleWorld(x) \<rightarrow> x \<Turnstile> p)\<close>)
       apply (meson "\<equiv>E"(6) "oth-class-taut:1:b" "oth-class-taut:3:a")
      by(fact x_prop)
    AOT_hence 2: \<open>\<diamond>PossibleWorld(x) & \<diamond>\<not>x \<Turnstile> p\<close>
      by (metis "KBasic2:3" "vdash-properties:10")
    AOT_hence \<open>PossibleWorld(x)\<close>
      using "&E"(1) "\<equiv>E"(1) "rigid-pw:2" by blast
    AOT_hence \<open>\<box>(x \<Turnstile> p)\<close>
      using 2[THEN "&E"(2)]  1[unconstrain w, THEN "\<rightarrow>E"] "\<rightarrow>E"
            "rigid-truth-at:1"[unconstrain w, THEN "\<rightarrow>E"]
      by (metis "\<equiv>E"(1))
    moreover AOT_have \<open>\<not>\<box>(x \<Turnstile> p)\<close>
      using 2[THEN "&E"(2)] by (metis "\<not>\<not>I" "KBasic:12" "\<equiv>E"(4))
    ultimately AOT_show \<open>p & \<not>p\<close> for p
      by (metis "raa-cor:3")
  qed
qed

AOT_theorem "fund-lem:7": \<open>\<box>\<forall>w(w \<Turnstile> p) \<rightarrow> \<box>p\<close>
proof(rule RM; rule "\<rightarrow>I")
  AOT_modally_strict {
    AOT_obtain w where w_prop: \<open>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
      using "act-world:1" "PossibleWorld.\<exists>E"[rotated] by meson
    AOT_assume \<open>\<forall>w (w \<Turnstile> p)\<close>
    AOT_hence \<open>w \<Turnstile> p\<close>
      using "PossibleWorld.\<forall>E" by fast
    AOT_thus \<open>p\<close>
      using w_prop[THEN "\<forall>E"(2), THEN "\<equiv>E"(1)] by blast
  }
qed

AOT_theorem "fund:1": \<open>\<diamond>p \<equiv> \<exists>w w \<Turnstile> p\<close>
proof (rule "\<equiv>I"; rule "\<rightarrow>I")
  AOT_assume \<open>\<diamond>p\<close>
  AOT_thus \<open>\<exists>w w \<Turnstile> p\<close>
    by (metis "fund-lem:1" "fund-lem:2" "\<rightarrow>E")
next
  AOT_assume \<open>\<exists>w w \<Turnstile> p\<close>
  then AOT_obtain w where w_prop: \<open>w \<Turnstile> p\<close>
    using "PossibleWorld.\<exists>E"[rotated] by meson
  AOT_hence \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", THEN "&E"(2)] PossibleWorld.\<psi> "&E"> by blast
  AOT_hence \<open>\<forall>p \<diamond>(w \<Turnstile> p \<equiv> p)\<close>
    by (metis "Buridan\<diamond>" "\<rightarrow>E")
  AOT_hence 1: \<open>\<diamond>(w \<Turnstile> p \<equiv> p)\<close>
    by (metis "log-prop-prop:2" "rule-ui:1")
  AOT_have \<open>\<diamond>((w \<Turnstile> p \<rightarrow> p) & (p \<rightarrow> w \<Turnstile> p))\<close>
    apply (AOT_subst \<open>(w \<Turnstile> p \<rightarrow> p) & (p \<rightarrow> w \<Turnstile> p)\<close> \<open>w \<Turnstile> p \<equiv> p\<close>)
     apply (meson "conventions:3" "\<equiv>E"(6) "oth-class-taut:3:a" "\<equiv>Df")
    by (fact 1)
  AOT_hence \<open>\<diamond>(w \<Turnstile> p \<rightarrow> p)\<close>
    by (metis "RM\<diamond>" "Conjunction Simplification"(1) "\<rightarrow>E")
  moreover AOT_have \<open>\<box>(w \<Turnstile> p)\<close>
    using w_prop by (metis "\<equiv>E"(1) "rigid-truth-at:1")
  ultimately AOT_show \<open>\<diamond>p\<close>
    by (metis "KBasic2:4" "\<equiv>E"(1) "\<rightarrow>E")
qed

AOT_theorem "fund:2": \<open>\<box>p \<equiv> \<forall>w (w \<Turnstile> p)\<close>
proof -
  AOT_have 0: \<open>\<forall>w (w \<Turnstile> \<not>p \<equiv> \<not>w \<Turnstile> p)\<close>
    apply (rule PossibleWorld.GEN)
    using "coherent:1" by blast
  AOT_have \<open>\<diamond>\<not>p \<equiv> \<exists>w (w \<Turnstile> \<not>p)\<close>
    using "fund:1"[unvarify p, OF "log-prop-prop:2"] by blast
  also AOT_have \<open>\<dots> \<equiv> \<exists>w \<not>(w \<Turnstile> p)\<close>
  proof(safe intro!: "\<equiv>I" "\<rightarrow>I")
    AOT_assume \<open>\<exists>w w \<Turnstile> \<not>p\<close>
    then AOT_obtain w where w_prop: \<open>w \<Turnstile> \<not>p\<close>
      using "PossibleWorld.\<exists>E"[rotated] by meson
    AOT_hence \<open>\<not>w \<Turnstile> p\<close>
      using 0[THEN "PossibleWorld.\<forall>E", THEN "\<equiv>E"(1)] "&E" by blast
    AOT_thus \<open>\<exists>w \<not>w \<Turnstile> p\<close>
      by (rule "PossibleWorld.\<exists>I")
  next
    AOT_assume \<open>\<exists>w \<not>w \<Turnstile> p\<close>
    then AOT_obtain w where w_prop: \<open>\<not>w \<Turnstile> p\<close>
      using "PossibleWorld.\<exists>E"[rotated] by meson
    AOT_hence \<open>w \<Turnstile> \<not>p\<close>
      using 0[THEN "\<forall>E"(2), THEN "\<rightarrow>E", THEN "\<equiv>E"(1)] "&E"
      by (metis "coherent:1" "\<equiv>E"(2))
    AOT_thus \<open>\<exists>w w \<Turnstile> \<not>p\<close>
      by (rule "PossibleWorld.\<exists>I")
  qed
  finally AOT_have \<open>\<not>\<diamond>\<not>p \<equiv> \<not>\<exists>w \<not>w \<Turnstile> p\<close>
    by (meson "\<equiv>E"(1) "oth-class-taut:4:b")
  AOT_hence \<open>\<box>p \<equiv> \<not>\<exists>w \<not>w \<Turnstile> p\<close>
    by (metis "KBasic:12" "\<equiv>E"(5))
  also AOT_have \<open>\<dots> \<equiv> \<forall>w w \<Turnstile> p\<close>
  proof(safe intro!: "\<equiv>I" "\<rightarrow>I")
    AOT_assume \<open>\<not>\<exists>w \<not>w \<Turnstile> p\<close>
    AOT_hence 0: \<open>\<forall>x (\<not>(PossibleWorld(x) & \<not>x \<Turnstile> p))\<close>
      by (metis "cqt-further:4" "\<rightarrow>E")
    AOT_show \<open>\<forall>w w \<Turnstile> p\<close>
      apply (AOT_subst \<open>PossibleWorld(x) \<rightarrow> x \<Turnstile> p\<close>
                       \<open>\<not>(PossibleWorld(x) & \<not>x \<Turnstile> p)\<close> for: x)
       using "oth-class-taut:1:a" apply presburger
      by (fact 0)
  next
    AOT_assume 0: \<open>\<forall>w w \<Turnstile> p\<close>
    AOT_have \<open>\<forall>x (\<not>(PossibleWorld(x) & \<not>x \<Turnstile> p))\<close>
      by (AOT_subst (reverse) \<open>\<not>(PossibleWorld(x) & \<not>x \<Turnstile> p)\<close>
                              \<open>PossibleWorld(x) \<rightarrow> x \<Turnstile> p\<close> for: x)
         (auto simp: "oth-class-taut:1:a" 0)
    AOT_thus \<open>\<not>\<exists>w \<not>w \<Turnstile> p\<close>
      by (metis "\<exists>E" "raa-cor:3" "rule-ui:3")
  qed
  finally AOT_show \<open>\<box>p \<equiv> \<forall>w w \<Turnstile> p\<close>.
qed

AOT_theorem "fund:3": \<open>\<not>\<diamond>p \<equiv> \<not>\<exists>w w \<Turnstile> p\<close>
  by (metis (full_types) "contraposition:1[1]" "\<rightarrow>I" "fund:1" "\<equiv>I" "\<equiv>E"(1,2))

AOT_theorem "fund:4": \<open>\<not>\<box>p \<equiv> \<exists>w \<not>w \<Turnstile>p\<close>
  apply (AOT_subst \<open>\<exists>w \<not>w \<Turnstile> p\<close> \<open>\<not> \<forall>w w \<Turnstile> p\<close>)
   apply (AOT_subst \<open>PossibleWorld(x) \<rightarrow> x \<Turnstile> p\<close>
                    \<open>\<not>(PossibleWorld(x) & \<not>x \<Turnstile> p)\<close> for: x)
  by (auto simp add: "oth-class-taut:1:a" "conventions:4" "\<equiv>Df" RN
                     "fund:2" "rule-sub-lem:1:a")

AOT_theorem "nec-dia-w:1": \<open>\<box>p \<equiv> \<exists>w w \<Turnstile> \<box>p\<close>
proof -
  AOT_have \<open>\<box>p \<equiv> \<diamond>\<box>p\<close>
    using "S5Basic:2" by blast
  also AOT_have \<open>... \<equiv> \<exists>w w \<Turnstile> \<box>p\<close>
    using "fund:1"[unvarify p, OF "log-prop-prop:2"] by blast
  finally show ?thesis.
qed

AOT_theorem "nec-dia-w:2": \<open>\<box>p \<equiv> \<forall>w w \<Turnstile> \<box>p\<close>
proof -
  AOT_have \<open>\<box>p \<equiv> \<box>\<box>p\<close>
    using 4 "qml:2"[axiom_inst] "\<equiv>I" by blast
  also AOT_have \<open>... \<equiv> \<forall>w w \<Turnstile> \<box>p\<close>
    using "fund:2"[unvarify p, OF "log-prop-prop:2"] by blast
  finally show ?thesis.
qed

AOT_theorem "nec-dia-w:3": \<open>\<diamond>p \<equiv> \<exists>w w \<Turnstile> \<diamond>p\<close>
proof -
  AOT_have \<open>\<diamond>p \<equiv> \<diamond>\<diamond>p\<close>
    by (simp add: "4\<diamond>" "T\<diamond>" "\<equiv>I")
  also AOT_have \<open>... \<equiv> \<exists>w w \<Turnstile> \<diamond>p\<close>
    using "fund:1"[unvarify p, OF "log-prop-prop:2"] by blast
  finally show ?thesis.
qed

AOT_theorem "nec-dia-w:4": \<open>\<diamond>p \<equiv> \<forall>w w \<Turnstile> \<diamond>p\<close>
proof -
  AOT_have \<open>\<diamond>p \<equiv> \<box>\<diamond>p\<close>
    by (simp add: "S5Basic:1")
  also AOT_have \<open>... \<equiv> \<forall>w w \<Turnstile> \<diamond>p\<close>
    using "fund:2"[unvarify p, OF "log-prop-prop:2"] by blast
  finally show ?thesis.
qed

AOT_theorem "conj-dist-w:1": \<open>w \<Turnstile> (p & q) \<equiv> ((w \<Turnstile> p) & (w \<Turnstile> q))\<close>
proof(safe intro!: "\<equiv>I" "\<rightarrow>I")
  AOT_assume \<open>w \<Turnstile> (p & q)\<close>
  AOT_hence 0: \<open>\<box>w \<Turnstile> (p & q)\<close>
    using "rigid-truth-at:1"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by blast
  AOT_modally_strict {
    AOT_have \<open>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> ((w \<Turnstile> (\<phi> & \<psi>)) \<rightarrow> (w \<Turnstile> \<phi> & w \<Turnstile> \<psi>))\<close> for w \<phi> \<psi>
    proof(safe intro!: "\<rightarrow>I")
      AOT_assume \<open>\<forall> p (w \<Turnstile> p \<equiv> p)\<close>
      AOT_hence \<open>w \<Turnstile> (\<phi> & \<psi>) \<equiv> (\<phi> & \<psi>)\<close> and \<open>w \<Turnstile> \<phi> \<equiv> \<phi>\<close> and \<open>w \<Turnstile> \<psi> \<equiv> \<psi>\<close>
        using "\<forall>E"(1)[rotated, OF "log-prop-prop:2"] by blast+
      moreover AOT_assume \<open>w \<Turnstile> (\<phi> & \<psi>)\<close>
      ultimately AOT_show \<open>w \<Turnstile> \<phi> & w \<Turnstile> \<psi>\<close>
        by (metis "&I" "&E"(1) "&E"(2) "\<equiv>E"(1) "\<equiv>E"(2))
    qed
  }
  AOT_hence \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> \<diamond>(w \<Turnstile> (\<phi> & \<psi>) \<rightarrow> w \<Turnstile> \<phi> & w \<Turnstile> \<psi>)\<close> for w \<phi> \<psi>
    by (rule "RM\<diamond>")
  moreover AOT_have pos: \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", OF PossibleWorld.\<psi>] "&E" by blast
  ultimately AOT_have \<open>\<diamond>(w \<Turnstile> (p & q) \<rightarrow> w \<Turnstile> p & w \<Turnstile> q)\<close> using "\<rightarrow>E" by blast
  AOT_hence \<open>\<diamond>(w \<Turnstile> p) & \<diamond>(w \<Turnstile> q)\<close>
    by (metis 0 "KBasic2:3" "KBasic2:4" "\<equiv>E"(1) "vdash-properties:10")
  AOT_thus \<open>w \<Turnstile> p & w \<Turnstile> q\<close>
    using "rigid-truth-at:2"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
          "&E" "&I" by meson
next
  AOT_assume \<open>w \<Turnstile> p & w \<Turnstile> q\<close>
  AOT_hence \<open>\<box>w \<Turnstile> p & \<box>w \<Turnstile> q\<close>
    using "rigid-truth-at:1"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
          "&E" "&I" by blast
  AOT_hence 0: \<open>\<box>(w \<Turnstile> p & w \<Turnstile> q)\<close>
    by (metis "KBasic:3" "\<equiv>E"(2))
  AOT_modally_strict {
    AOT_have \<open>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> ((w \<Turnstile> \<phi> & w \<Turnstile> \<psi>) \<rightarrow> (w \<Turnstile> (\<phi> & \<psi>)))\<close> for w \<phi> \<psi>
    proof(safe intro!: "\<rightarrow>I")
      AOT_assume \<open>\<forall> p (w \<Turnstile> p \<equiv> p)\<close>
      AOT_hence \<open>w \<Turnstile> (\<phi> & \<psi>) \<equiv> (\<phi> & \<psi>)\<close> and \<open>w \<Turnstile> \<phi> \<equiv> \<phi>\<close> and \<open>w \<Turnstile> \<psi> \<equiv> \<psi>\<close>
        using "\<forall>E"(1)[rotated, OF "log-prop-prop:2"] by blast+
      moreover AOT_assume \<open>w \<Turnstile> \<phi> & w \<Turnstile> \<psi>\<close>
      ultimately AOT_show \<open>w \<Turnstile> (\<phi> & \<psi>)\<close>
        by (metis "&I" "&E"(1) "&E"(2) "\<equiv>E"(1) "\<equiv>E"(2))
    qed
  }
  AOT_hence \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> \<diamond>((w \<Turnstile> \<phi> & w \<Turnstile> \<psi>) \<rightarrow> w \<Turnstile> (\<phi> & \<psi>))\<close> for w \<phi> \<psi>
    by (rule "RM\<diamond>")
  moreover AOT_have pos: \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", OF PossibleWorld.\<psi>] "&E" by blast
  ultimately AOT_have \<open>\<diamond>((w \<Turnstile> p & w \<Turnstile> q) \<rightarrow> w \<Turnstile> (p & q))\<close>
    using "\<rightarrow>E" by blast
  AOT_hence \<open>\<diamond>(w \<Turnstile> (p & q))\<close>
    by (metis 0 "KBasic2:4" "\<equiv>E"(1) "vdash-properties:10")
  AOT_thus \<open>w \<Turnstile> (p & q)\<close>
    using "rigid-truth-at:2"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by blast
qed

AOT_theorem "conj-dist-w:2": \<open>w \<Turnstile> (p \<rightarrow> q) \<equiv> ((w \<Turnstile> p) \<rightarrow> (w \<Turnstile> q))\<close>
proof(safe intro!: "\<equiv>I" "\<rightarrow>I")
  AOT_assume \<open>w \<Turnstile> (p \<rightarrow> q)\<close>
  AOT_hence 0: \<open>\<box>w \<Turnstile> (p \<rightarrow> q)\<close>
    using "rigid-truth-at:1"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by blast
  AOT_assume \<open>w \<Turnstile> p\<close>
  AOT_hence 1: \<open>\<box>w \<Turnstile> p\<close>
    by (metis "T\<diamond>" "\<equiv>E"(1) "rigid-truth-at:3" "\<rightarrow>E")
  AOT_modally_strict {
    AOT_have \<open>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> ((w \<Turnstile> (\<phi> \<rightarrow> \<psi>)) \<rightarrow> (w \<Turnstile> \<phi> \<rightarrow> w \<Turnstile> \<psi>))\<close> for w \<phi> \<psi>
    proof(safe intro!: "\<rightarrow>I")
      AOT_assume \<open>\<forall> p (w \<Turnstile> p \<equiv> p)\<close>
      AOT_hence \<open>w \<Turnstile> (\<phi> \<rightarrow> \<psi>) \<equiv> (\<phi> \<rightarrow> \<psi>)\<close> and \<open>w \<Turnstile> \<phi> \<equiv> \<phi>\<close> and \<open>w \<Turnstile> \<psi> \<equiv> \<psi>\<close>
        using "\<forall>E"(1)[rotated, OF "log-prop-prop:2"] by blast+
      moreover AOT_assume \<open>w \<Turnstile> (\<phi> \<rightarrow> \<psi>)\<close>
      moreover AOT_assume \<open>w \<Turnstile> \<phi>\<close>
      ultimately AOT_show \<open>w \<Turnstile> \<psi>\<close>
        by (metis "\<equiv>E"(1) "\<equiv>E"(2) "\<rightarrow>E")
    qed
  }
  AOT_hence \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> \<diamond>(w \<Turnstile> (\<phi> \<rightarrow> \<psi>) \<rightarrow> (w \<Turnstile> \<phi> \<rightarrow> w \<Turnstile> \<psi>))\<close> for w \<phi> \<psi>
    by (rule "RM\<diamond>")
  moreover AOT_have pos: \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", OF PossibleWorld.\<psi>] "&E" by blast
  ultimately AOT_have \<open>\<diamond>(w \<Turnstile> (p \<rightarrow> q) \<rightarrow> (w \<Turnstile> p \<rightarrow> w \<Turnstile> q))\<close>
    using "\<rightarrow>E" by blast
  AOT_hence \<open>\<diamond>(w \<Turnstile> p \<rightarrow> w \<Turnstile> q)\<close>
    by (metis 0 "KBasic2:4" "\<equiv>E"(1) "\<rightarrow>E")
  AOT_hence \<open>\<diamond>w \<Turnstile> q\<close> 
    by (metis 1 "KBasic2:4" "\<equiv>E"(1) "\<rightarrow>E")
  AOT_thus \<open>w \<Turnstile> q\<close>
    using "rigid-truth-at:2"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
          "&E" "&I" by meson
next
  AOT_assume \<open>w \<Turnstile> p \<rightarrow> w \<Turnstile> q\<close>
  AOT_hence \<open>\<not>(w \<Turnstile> p) \<or> w \<Turnstile> q\<close>
    by (metis "\<or>I"(1) "\<or>I"(2) "reductio-aa:1" "\<rightarrow>E")
  AOT_hence \<open>w \<Turnstile> \<not>p \<or> w \<Turnstile> q\<close>
    by (metis "coherent:1" "\<or>I"(1) "\<or>I"(2) "\<or>E"(2) "\<equiv>E"(2) "reductio-aa:1")
  AOT_hence 0: \<open>\<box>(w \<Turnstile> \<not>p \<or> w \<Turnstile> q)\<close>
    using "rigid-truth-at:1"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by (metis "KBasic:15" "\<or>I"(1) "\<or>I"(2) "\<or>E"(2) "reductio-aa:1" "\<rightarrow>E")
  AOT_modally_strict {
    AOT_have \<open>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> ((w \<Turnstile> \<not>\<phi> \<or> w \<Turnstile> \<psi>) \<rightarrow> (w \<Turnstile> (\<phi> \<rightarrow> \<psi>)))\<close> for w \<phi> \<psi>
    proof(safe intro!: "\<rightarrow>I")
      AOT_assume \<open>\<forall> p (w \<Turnstile> p \<equiv> p)\<close>
      moreover AOT_assume \<open>w \<Turnstile> \<not>\<phi> \<or> w \<Turnstile> \<psi>\<close>
      ultimately AOT_show \<open>w \<Turnstile> (\<phi> \<rightarrow> \<psi>)\<close>
        by (metis "\<or>E"(2) "\<rightarrow>I" "\<equiv>E"(1) "\<equiv>E"(2) "log-prop-prop:2"
                  "reductio-aa:1" "rule-ui:1")
    qed
  }
  AOT_hence \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> \<diamond>((w \<Turnstile> \<not>\<phi> \<or> w \<Turnstile> \<psi>) \<rightarrow> w \<Turnstile> (\<phi> \<rightarrow> \<psi>))\<close> for w \<phi> \<psi>
    by (rule "RM\<diamond>")
  moreover AOT_have pos: \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", OF PossibleWorld.\<psi>] "&E" by blast
  ultimately AOT_have \<open>\<diamond>((w \<Turnstile> \<not>p \<or> w \<Turnstile> q) \<rightarrow> w \<Turnstile> (p \<rightarrow> q))\<close>
    using "\<rightarrow>E" by blast
  AOT_hence \<open>\<diamond>(w \<Turnstile> (p \<rightarrow> q))\<close>
    by (metis 0 "KBasic2:4" "\<equiv>E"(1) "\<rightarrow>E")
  AOT_thus \<open>w \<Turnstile> (p \<rightarrow> q)\<close>
    using "rigid-truth-at:2"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by blast
qed

AOT_theorem "conj-dist-w:3": \<open>w \<Turnstile> (p \<or> q) \<equiv> ((w \<Turnstile> p) \<or> (w \<Turnstile> q))\<close>
proof(safe intro!: "\<equiv>I" "\<rightarrow>I")
  AOT_assume \<open>w \<Turnstile> (p \<or> q)\<close>
  AOT_hence 0: \<open>\<box>w \<Turnstile> (p \<or> q)\<close>
    using "rigid-truth-at:1"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by blast
  AOT_modally_strict {
    AOT_have \<open>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> ((w \<Turnstile> (\<phi> \<or> \<psi>)) \<rightarrow> (w \<Turnstile> \<phi> \<or> w \<Turnstile> \<psi>))\<close> for w \<phi> \<psi>
    proof(safe intro!: "\<rightarrow>I")
      AOT_assume \<open>\<forall> p (w \<Turnstile> p \<equiv> p)\<close>
      AOT_hence \<open>w \<Turnstile> (\<phi> \<or> \<psi>) \<equiv> (\<phi> \<or> \<psi>)\<close> and \<open>w \<Turnstile> \<phi> \<equiv> \<phi>\<close> and \<open>w \<Turnstile> \<psi> \<equiv> \<psi>\<close>
        using "\<forall>E"(1)[rotated, OF "log-prop-prop:2"] by blast+
      moreover AOT_assume \<open>w \<Turnstile> (\<phi> \<or> \<psi>)\<close>
      ultimately AOT_show \<open>w \<Turnstile> \<phi> \<or> w \<Turnstile> \<psi>\<close>
        by (metis "\<or>I"(1) "\<or>I"(2) "\<or>E"(3) "\<equiv>E"(1) "\<equiv>E"(2) "reductio-aa:1")
    qed
  }
  AOT_hence \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> \<diamond>(w \<Turnstile> (\<phi> \<or> \<psi>) \<rightarrow> (w \<Turnstile> \<phi> \<or> w \<Turnstile> \<psi>))\<close> for w \<phi> \<psi>
    by (rule "RM\<diamond>")
  moreover AOT_have pos: \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", OF PossibleWorld.\<psi>] "&E" by blast
  ultimately AOT_have \<open>\<diamond>(w \<Turnstile> (p \<or> q) \<rightarrow> (w \<Turnstile> p \<or> w \<Turnstile> q))\<close> using "\<rightarrow>E" by blast
  AOT_hence \<open>\<diamond>(w \<Turnstile> p \<or> w \<Turnstile> q)\<close>
    by (metis 0 "KBasic2:4" "\<equiv>E"(1) "vdash-properties:10")
  AOT_hence \<open>\<diamond>w \<Turnstile> p \<or> \<diamond>w \<Turnstile> q\<close>
    using "KBasic2:2"[THEN "\<equiv>E"(1)] by blast
  AOT_thus \<open>w \<Turnstile> p \<or> w \<Turnstile> q\<close>
    using "rigid-truth-at:2"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by (metis "\<or>I"(1) "\<or>I"(2) "\<or>E"(2) "reductio-aa:1")
next
  AOT_assume \<open>w \<Turnstile> p \<or> w \<Turnstile> q\<close>
  AOT_hence 0: \<open>\<box>(w \<Turnstile> p \<or> w \<Turnstile> q)\<close>
    using "rigid-truth-at:1"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by (metis "KBasic:15" "\<or>I"(1) "\<or>I"(2) "\<or>E"(2) "reductio-aa:1" "\<rightarrow>E")
  AOT_modally_strict {
    AOT_have \<open>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> ((w \<Turnstile> \<phi> \<or> w \<Turnstile> \<psi>) \<rightarrow> (w \<Turnstile> (\<phi> \<or> \<psi>)))\<close> for w \<phi> \<psi>
    proof(safe intro!: "\<rightarrow>I")
      AOT_assume \<open>\<forall> p (w \<Turnstile> p \<equiv> p)\<close>
      moreover AOT_assume \<open>w \<Turnstile> \<phi> \<or> w \<Turnstile> \<psi>\<close>
      ultimately AOT_show \<open>w \<Turnstile> (\<phi> \<or> \<psi>)\<close>
        by (metis "\<or>I"(1) "\<or>I"(2) "\<or>E"(2) "\<equiv>E"(1) "\<equiv>E"(2)
                  "log-prop-prop:2" "reductio-aa:1" "rule-ui:1")
    qed
  }
  AOT_hence \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> \<diamond>((w \<Turnstile> \<phi> \<or> w \<Turnstile> \<psi>) \<rightarrow> w \<Turnstile> (\<phi> \<or> \<psi>))\<close> for w \<phi> \<psi>
    by (rule "RM\<diamond>")
  moreover AOT_have pos: \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", OF PossibleWorld.\<psi>] "&E" by blast
  ultimately AOT_have \<open>\<diamond>((w \<Turnstile> p \<or> w \<Turnstile> q) \<rightarrow> w \<Turnstile> (p \<or> q))\<close>
    using "\<rightarrow>E" by blast
  AOT_hence \<open>\<diamond>(w \<Turnstile> (p \<or> q))\<close>
    by (metis 0 "KBasic2:4" "\<equiv>E"(1) "\<rightarrow>E")
  AOT_thus \<open>w \<Turnstile> (p \<or> q)\<close>
    using "rigid-truth-at:2"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by blast
qed

AOT_theorem "conj-dist-w:4": \<open>w \<Turnstile> (p \<equiv> q) \<equiv> ((w \<Turnstile> p) \<equiv> (w \<Turnstile> q))\<close>
proof(rule "\<equiv>I"; rule "\<rightarrow>I")
  AOT_assume \<open>w \<Turnstile> (p \<equiv> q)\<close>
  AOT_hence 0: \<open>\<box>w \<Turnstile> (p \<equiv> q)\<close>
    using "rigid-truth-at:1"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by blast
  AOT_modally_strict {
    AOT_have \<open>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> ((w \<Turnstile> (\<phi> \<equiv> \<psi>)) \<rightarrow> (w \<Turnstile> \<phi> \<equiv> w \<Turnstile> \<psi>))\<close> for w \<phi> \<psi>
    proof(safe intro!: "\<rightarrow>I")
      AOT_assume \<open>\<forall> p (w \<Turnstile> p \<equiv> p)\<close>
      AOT_hence \<open>w \<Turnstile> (\<phi> \<equiv> \<psi>) \<equiv> (\<phi> \<equiv> \<psi>)\<close> and \<open>w \<Turnstile> \<phi> \<equiv> \<phi>\<close> and \<open>w \<Turnstile> \<psi> \<equiv> \<psi>\<close>
        using "\<forall>E"(1)[rotated, OF "log-prop-prop:2"] by blast+
      moreover AOT_assume \<open>w \<Turnstile> (\<phi> \<equiv> \<psi>)\<close>
      ultimately AOT_show \<open>w \<Turnstile> \<phi> \<equiv> w \<Turnstile> \<psi>\<close>
        by (metis "\<equiv>E"(2) "\<equiv>E"(5) "Commutativity of \<equiv>")
    qed
  }
  AOT_hence \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> \<diamond>(w \<Turnstile> (\<phi> \<equiv> \<psi>) \<rightarrow> (w \<Turnstile> \<phi> \<equiv> w \<Turnstile> \<psi>))\<close> for w \<phi> \<psi>
    by (rule "RM\<diamond>")
  moreover AOT_have pos: \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", OF PossibleWorld.\<psi>] "&E" by blast
  ultimately AOT_have \<open>\<diamond>(w \<Turnstile> (p \<equiv> q) \<rightarrow> (w \<Turnstile> p \<equiv> w \<Turnstile> q))\<close>
    using "\<rightarrow>E" by blast
  AOT_hence 1: \<open>\<diamond>(w \<Turnstile> p \<equiv> w \<Turnstile> q)\<close>
    by (metis 0 "KBasic2:4" "\<equiv>E"(1) "vdash-properties:10")
  AOT_have \<open>\<diamond>((w \<Turnstile> p \<rightarrow> w \<Turnstile> q) & (w \<Turnstile> q \<rightarrow> w \<Turnstile> p))\<close>
    apply (AOT_subst \<open>(w \<Turnstile> p \<rightarrow> w \<Turnstile> q) & (w \<Turnstile> q \<rightarrow> w \<Turnstile> p)\<close> \<open>w \<Turnstile> p \<equiv> w \<Turnstile> q\<close>)
     apply (meson "\<equiv>\<^sub>d\<^sub>fE" "conventions:3" "\<rightarrow>I" "df-rules-formulas[4]" "\<equiv>I")
    by (fact 1)
  AOT_hence 2: \<open>\<diamond>(w \<Turnstile> p \<rightarrow> w \<Turnstile> q) & \<diamond>(w \<Turnstile> q \<rightarrow> w \<Turnstile> p)\<close>
    by (metis "KBasic2:3" "vdash-properties:10")
  AOT_have \<open>\<diamond>(\<not>w \<Turnstile> p \<or> w \<Turnstile> q)\<close> and \<open>\<diamond>(\<not>w \<Turnstile> q \<or> w \<Turnstile> p)\<close>
     apply (AOT_subst (reverse) \<open>\<not>w \<Turnstile> p \<or> w \<Turnstile> q\<close> \<open>w \<Turnstile> p \<rightarrow> w \<Turnstile> q\<close>)
      apply (simp add: "oth-class-taut:1:c")
     apply (fact 2[THEN "&E"(1)])
    apply (AOT_subst (reverse) \<open>\<not>w \<Turnstile> q \<or> w \<Turnstile> p\<close> \<open>w \<Turnstile> q \<rightarrow> w \<Turnstile> p\<close>)
     apply (simp add: "oth-class-taut:1:c")
    by (fact 2[THEN "&E"(2)])
  AOT_hence \<open>\<diamond>(\<not>w \<Turnstile> p) \<or> \<diamond>w \<Turnstile> q\<close> and \<open>\<diamond>\<not>w \<Turnstile> q \<or> \<diamond>w \<Turnstile> p\<close>
    using "KBasic2:2" "\<equiv>E"(1) by blast+
  AOT_hence \<open>\<not>\<box>w \<Turnstile> p \<or> \<diamond>w \<Turnstile> q\<close> and \<open>\<not>\<box>w \<Turnstile> q \<or> \<diamond>w \<Turnstile> p\<close>
    by (metis "KBasic:11" "\<or>I"(1) "\<or>I"(2) "\<or>E"(2) "\<equiv>E"(2) "raa-cor:1")+
  AOT_thus \<open>w \<Turnstile> p \<equiv> w \<Turnstile> q\<close>
    using "rigid-truth-at:2"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by (metis "\<not>\<not>I" "T\<diamond>" "\<or>E"(2) "\<rightarrow>I" "\<equiv>I" "\<equiv>E"(1) "rigid-truth-at:3")
next
  AOT_have \<open>\<box>PossibleWorld(w)\<close>
    using "\<equiv>E"(1) "rigid-pw:1" PossibleWorld.\<psi> by blast
  moreover {
    fix p
    AOT_modally_strict {
      AOT_have \<open>PossibleWorld(w) \<rightarrow> (w \<Turnstile> p \<rightarrow> \<box>w \<Turnstile> p)\<close>
        using "rigid-truth-at:1" "\<rightarrow>I"
        by (metis "\<equiv>E"(1))
    }
    AOT_hence \<open>\<box>PossibleWorld(w) \<rightarrow> \<box>(w \<Turnstile> p \<rightarrow> \<box>w \<Turnstile> p)\<close>
      by (rule RM)
  }
  ultimately AOT_have 1: \<open>\<box>(w \<Turnstile> p \<rightarrow> \<box>w \<Turnstile> p)\<close> for p
    by (metis "\<rightarrow>E")
  AOT_assume \<open>w \<Turnstile> p \<equiv> w \<Turnstile> q\<close>
  AOT_hence 0: \<open>\<box>(w \<Turnstile> p \<equiv> w \<Turnstile> q)\<close>
    using "sc-eq-box-box:5"[THEN "\<rightarrow>E", THEN "qml:2"[axiom_inst, THEN "\<rightarrow>E"],
                            THEN "\<rightarrow>E", OF "&I"]
          by (metis "1")
  AOT_modally_strict {
    AOT_have \<open>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> ((w \<Turnstile> \<phi> \<equiv> w \<Turnstile> \<psi>) \<rightarrow> (w \<Turnstile> (\<phi> \<equiv> \<psi>)))\<close> for w \<phi> \<psi>
    proof(safe intro!: "\<rightarrow>I")
      AOT_assume \<open>\<forall> p (w \<Turnstile> p \<equiv> p)\<close>
      moreover AOT_assume \<open>w \<Turnstile> \<phi> \<equiv> w \<Turnstile> \<psi>\<close>
      ultimately AOT_show \<open>w \<Turnstile> (\<phi> \<equiv> \<psi>)\<close>
        by (metis "\<equiv>E"(2) "\<equiv>E"(6) "log-prop-prop:2" "rule-ui:1")
    qed
  }
  AOT_hence \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> \<diamond>((w \<Turnstile> \<phi> \<equiv> w \<Turnstile> \<psi>) \<rightarrow> w \<Turnstile> (\<phi> \<equiv> \<psi>))\<close> for w \<phi> \<psi>
    by (rule "RM\<diamond>")
  moreover AOT_have pos: \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", OF PossibleWorld.\<psi>] "&E" by blast
  ultimately AOT_have \<open>\<diamond>((w \<Turnstile> p \<equiv>  w \<Turnstile> q) \<rightarrow> w \<Turnstile> (p \<equiv> q))\<close>
    using "\<rightarrow>E" by blast
  AOT_hence \<open>\<diamond>(w \<Turnstile> (p \<equiv> q))\<close>
    by (metis 0 "KBasic2:4" "\<equiv>E"(1) "\<rightarrow>E")
  AOT_thus \<open>w \<Turnstile> (p \<equiv> q)\<close>
    using "rigid-truth-at:2"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by blast
qed

AOT_theorem "conj-dist-w:5": \<open>w \<Turnstile> (\<forall>\<alpha> \<phi>{\<alpha>}) \<equiv> (\<forall> \<alpha> (w \<Turnstile> \<phi>{\<alpha>}))\<close>
proof(safe intro!: "\<equiv>I" "\<rightarrow>I" GEN)
  AOT_assume \<open>w \<Turnstile> (\<forall>\<alpha> \<phi>{\<alpha>})\<close>
  AOT_hence 0: \<open>\<box>w \<Turnstile> (\<forall>\<alpha> \<phi>{\<alpha>})\<close>
    using "rigid-truth-at:1"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by blast
  AOT_modally_strict {
    AOT_have \<open>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> ((w \<Turnstile> (\<forall>\<alpha> \<phi>{\<alpha>})) \<rightarrow> (\<forall>\<alpha> w \<Turnstile> \<phi>{\<alpha>}))\<close> for w
    proof(safe intro!: "\<rightarrow>I" GEN)
      AOT_assume \<open>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
      moreover AOT_assume \<open>w \<Turnstile> (\<forall>\<alpha> \<phi>{\<alpha>})\<close>
      ultimately AOT_show \<open>w \<Turnstile> \<phi>{\<alpha>}\<close> for \<alpha>
        by (metis "\<equiv>E"(1) "\<equiv>E"(2) "log-prop-prop:2" "rule-ui:1" "rule-ui:3")
    qed
  }
  AOT_hence \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> \<diamond>(w \<Turnstile> (\<forall>\<alpha> \<phi>{\<alpha>}) \<rightarrow> (\<forall>\<alpha> w \<Turnstile> \<phi>{\<alpha>}))\<close> for w
    by (rule "RM\<diamond>")
  moreover AOT_have pos: \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", OF PossibleWorld.\<psi>] "&E" by blast
  ultimately AOT_have \<open>\<diamond>(w \<Turnstile> (\<forall>\<alpha> \<phi>{\<alpha>}) \<rightarrow> (\<forall>\<alpha> w \<Turnstile> \<phi>{\<alpha>}))\<close> using "\<rightarrow>E" by blast
  AOT_hence \<open>\<diamond>(\<forall>\<alpha> w \<Turnstile> \<phi>{\<alpha>})\<close>
    by (metis 0 "KBasic2:4" "\<equiv>E"(1) "\<rightarrow>E")
  AOT_hence \<open>\<forall>\<alpha> \<diamond>w \<Turnstile> \<phi>{\<alpha>}\<close>
    by (metis "Buridan\<diamond>" "\<rightarrow>E")
  AOT_thus \<open>w \<Turnstile> \<phi>{\<alpha>}\<close> for \<alpha>
    using "rigid-truth-at:2"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
          "\<forall>E"(2) by blast
next
  AOT_assume \<open>\<forall>\<alpha> w \<Turnstile> \<phi>{\<alpha>}\<close>
  AOT_hence \<open>w \<Turnstile> \<phi>{\<alpha>}\<close> for \<alpha> using "\<forall>E"(2) by blast
  AOT_hence \<open>\<box>w \<Turnstile> \<phi>{\<alpha>}\<close> for \<alpha>
    using "rigid-truth-at:1"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
          "&E" "&I" by blast
  AOT_hence \<open>\<forall>\<alpha> \<box>w \<Turnstile> \<phi>{\<alpha>}\<close> by (rule GEN)
  AOT_hence 0: \<open>\<box>\<forall>\<alpha> w \<Turnstile> \<phi>{\<alpha>}\<close> by (rule BF[THEN "\<rightarrow>E"])
  AOT_modally_strict {
    AOT_have \<open>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> ((\<forall>\<alpha> w \<Turnstile> \<phi>{\<alpha>}) \<rightarrow> (w \<Turnstile> (\<forall>\<alpha> \<phi>{\<alpha>})))\<close> for w
    proof(safe intro!: "\<rightarrow>I")
      AOT_assume \<open>\<forall> p (w \<Turnstile> p \<equiv> p)\<close>
      moreover AOT_assume \<open>\<forall>\<alpha> w \<Turnstile> \<phi>{\<alpha>}\<close>
      ultimately AOT_show \<open>w \<Turnstile> (\<forall>\<alpha> \<phi>{\<alpha>})\<close>
        by (metis "\<equiv>E"(1) "\<equiv>E"(2) "log-prop-prop:2" "rule-ui:1"
                  "rule-ui:3" "universal-cor")
    qed
  }
  AOT_hence \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> \<diamond>((\<forall>\<alpha> w \<Turnstile> \<phi>{\<alpha>}) \<rightarrow> w \<Turnstile> (\<forall>\<alpha> \<phi>{\<alpha>}))\<close> for w
    by (rule "RM\<diamond>")
  moreover AOT_have pos: \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", OF PossibleWorld.\<psi>] "&E" by blast
  ultimately AOT_have \<open>\<diamond>((\<forall>\<alpha> w \<Turnstile> \<phi>{\<alpha>}) \<rightarrow> w \<Turnstile> (\<forall>\<alpha> \<phi>{\<alpha>}))\<close>
    using "\<rightarrow>E" by blast
  AOT_hence \<open>\<diamond>(w \<Turnstile> (\<forall>\<alpha> \<phi>{\<alpha>}))\<close>
    by (metis 0 "KBasic2:4" "\<equiv>E"(1) "\<rightarrow>E")
  AOT_thus \<open>w \<Turnstile> (\<forall>\<alpha> \<phi>{\<alpha>})\<close>
    using "rigid-truth-at:2"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by blast
qed

AOT_theorem "conj-dist-w:6": \<open>w \<Turnstile> (\<exists>\<alpha> \<phi>{\<alpha>}) \<equiv> (\<exists> \<alpha> (w \<Turnstile> \<phi>{\<alpha>}))\<close>
proof(safe intro!: "\<equiv>I" "\<rightarrow>I" GEN)
  AOT_assume \<open>w \<Turnstile> (\<exists>\<alpha> \<phi>{\<alpha>})\<close>
  AOT_hence 0: \<open>\<box>w \<Turnstile> (\<exists>\<alpha> \<phi>{\<alpha>})\<close>
    using "rigid-truth-at:1"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by blast
  AOT_modally_strict {
    AOT_have \<open>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> ((w \<Turnstile> (\<exists>\<alpha> \<phi>{\<alpha>})) \<rightarrow> (\<exists>\<alpha> w \<Turnstile> \<phi>{\<alpha>}))\<close> for w
    proof(safe intro!: "\<rightarrow>I" GEN)
      AOT_assume \<open>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
      moreover AOT_assume \<open>w \<Turnstile> (\<exists>\<alpha> \<phi>{\<alpha>})\<close>
      ultimately AOT_show \<open>\<exists> \<alpha> (w \<Turnstile> \<phi>{\<alpha>})\<close>
        by (metis "\<exists>E" "\<exists>I"(2) "\<equiv>E"(1,2) "log-prop-prop:2" "rule-ui:1") 
    qed
  }
  AOT_hence \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> \<diamond>(w \<Turnstile> (\<exists>\<alpha> \<phi>{\<alpha>}) \<rightarrow> (\<exists>\<alpha> w \<Turnstile> \<phi>{\<alpha>}))\<close> for w
    by (rule "RM\<diamond>")
  moreover AOT_have pos: \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", OF PossibleWorld.\<psi>] "&E" by blast
  ultimately AOT_have \<open>\<diamond>(w \<Turnstile> (\<exists>\<alpha> \<phi>{\<alpha>}) \<rightarrow> (\<exists>\<alpha> w \<Turnstile> \<phi>{\<alpha>}))\<close> using "\<rightarrow>E" by blast
  AOT_hence \<open>\<diamond>(\<exists>\<alpha> w \<Turnstile> \<phi>{\<alpha>})\<close>
    by (metis 0 "KBasic2:4" "\<equiv>E"(1) "\<rightarrow>E")
  AOT_hence \<open>\<exists>\<alpha> \<diamond>w \<Turnstile> \<phi>{\<alpha>}\<close>
    by (metis "BF\<diamond>" "\<rightarrow>E")
  then AOT_obtain \<alpha> where \<open>\<diamond>w \<Turnstile> \<phi>{\<alpha>}\<close>
    using "\<exists>E"[rotated] by blast
  AOT_hence \<open>w \<Turnstile> \<phi>{\<alpha>}\<close>
    using "rigid-truth-at:2"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"] by blast
  AOT_thus \<open>\<exists> \<alpha> w \<Turnstile> \<phi>{\<alpha>}\<close> by (rule "\<exists>I")
next
  AOT_assume \<open>\<exists>\<alpha> w \<Turnstile> \<phi>{\<alpha>}\<close>
  then AOT_obtain \<alpha> where \<open>w \<Turnstile> \<phi>{\<alpha>}\<close> using "\<exists>E"[rotated] by blast
  AOT_hence \<open>\<box>w \<Turnstile> \<phi>{\<alpha>}\<close>
    using "rigid-truth-at:1"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
          "&E" "&I" by blast
  AOT_hence \<open>\<exists>\<alpha> \<box>w \<Turnstile> \<phi>{\<alpha>}\<close>
    by (rule "\<exists>I")
  AOT_hence 0: \<open>\<box>\<exists>\<alpha> w \<Turnstile> \<phi>{\<alpha>}\<close>
    by (metis Buridan "\<rightarrow>E")
  AOT_modally_strict {
    AOT_have \<open>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> ((\<exists>\<alpha> w \<Turnstile> \<phi>{\<alpha>}) \<rightarrow> (w \<Turnstile> (\<exists>\<alpha> \<phi>{\<alpha>})))\<close> for w
    proof(safe intro!: "\<rightarrow>I")
      AOT_assume \<open>\<forall> p (w \<Turnstile> p \<equiv> p)\<close>
      moreover AOT_assume \<open>\<exists>\<alpha> w \<Turnstile> \<phi>{\<alpha>}\<close>
      then AOT_obtain \<alpha> where \<open>w \<Turnstile> \<phi>{\<alpha>}\<close>
        using "\<exists>E"[rotated] by blast
      ultimately AOT_show \<open>w \<Turnstile> (\<exists>\<alpha> \<phi>{\<alpha>})\<close>
        by (metis "\<exists>I"(2) "\<equiv>E"(1,2) "log-prop-prop:2" "rule-ui:1")
    qed
  }
  AOT_hence \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p) \<rightarrow> \<diamond>((\<exists>\<alpha> w \<Turnstile> \<phi>{\<alpha>}) \<rightarrow> w \<Turnstile> (\<exists>\<alpha> \<phi>{\<alpha>}))\<close> for w
    by (rule "RM\<diamond>")
  moreover AOT_have pos: \<open>\<diamond>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "world:1"[THEN "\<equiv>\<^sub>d\<^sub>fE", OF PossibleWorld.\<psi>] "&E" by blast
  ultimately AOT_have \<open>\<diamond>((\<exists>\<alpha> w \<Turnstile> \<phi>{\<alpha>}) \<rightarrow> w \<Turnstile> (\<exists>\<alpha> \<phi>{\<alpha>}))\<close>
    using "\<rightarrow>E" by blast
  AOT_hence \<open>\<diamond>(w \<Turnstile> (\<exists>\<alpha> \<phi>{\<alpha>}))\<close>
    by (metis 0 "KBasic2:4" "\<equiv>E"(1) "\<rightarrow>E")
  AOT_thus \<open>w \<Turnstile> (\<exists>\<alpha> \<phi>{\<alpha>})\<close>
    using "rigid-truth-at:2"[unvarify p, THEN "\<equiv>E"(1), OF "log-prop-prop:2"]
    by blast
qed

AOT_theorem "conj-dist-w:7": \<open>(w \<Turnstile> \<box>p) \<rightarrow> \<box>w \<Turnstile> p\<close>
proof(rule "\<rightarrow>I")
  AOT_assume \<open>w \<Turnstile> \<box>p\<close>
  AOT_hence \<open>\<exists>w w \<Turnstile> \<box>p\<close> by (rule "PossibleWorld.\<exists>I")
  AOT_hence \<open>\<diamond>\<box>p\<close> using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "\<equiv>E"(2)]
    by blast
  AOT_hence \<open>\<box>p\<close>
    by (metis "5\<diamond>" "\<rightarrow>E")
  AOT_hence 1: \<open>\<box>\<box>p\<close>
    by (metis "S5Basic:6" "\<equiv>E"(1))
  AOT_have \<open>\<box>\<forall>w w \<Turnstile> p\<close>
    by (AOT_subst (reverse) \<open>\<forall>w w \<Turnstile> p\<close> \<open>\<box>p\<close>)
       (auto simp add: "fund:2" 1)
  AOT_hence \<open>\<forall>w \<box>w \<Turnstile> p\<close>
    using "fund-lem:5[world]"[THEN "\<rightarrow>E"] by simp
  AOT_thus \<open>\<box>w \<Turnstile> p\<close>
    using "\<rightarrow>E" "PossibleWorld.\<forall>E" by fast
qed

AOT_theorem "conj-dist-w:8": \<open>\<exists>w\<exists>p((\<box>w \<Turnstile> p) & \<not>w \<Turnstile> \<box>p)\<close>
proof -
  AOT_obtain r where A: r and \<open>\<diamond>\<not>r\<close>
    by (metis "&E"(1) "&E"(2) "\<equiv>\<^sub>d\<^sub>fE" "\<exists>E" "cont-tf:1" "cont-tf-thm:1")
  AOT_hence B: \<open>\<not>\<box>r\<close>
    by (metis "KBasic:11" "\<equiv>E"(2))
  AOT_have \<open>\<diamond>r\<close>
    using A "T\<diamond>"[THEN "\<rightarrow>E"] by simp
  AOT_hence \<open>\<exists>w w \<Turnstile> r\<close>
    using "fund:1"[THEN "\<equiv>E"(1)] by blast
  then AOT_obtain w where w: \<open>w \<Turnstile> r\<close>
    using "PossibleWorld.\<exists>E"[rotated] by meson
  AOT_hence \<open>\<box>w \<Turnstile> r\<close>
    by (metis "T\<diamond>" "\<equiv>E"(1) "rigid-truth-at:3" "vdash-properties:10")
  moreover AOT_have \<open>\<not>w \<Turnstile> \<box>r\<close>
  proof(rule "raa-cor:2")
    AOT_assume \<open>w \<Turnstile> \<box>r\<close>
    AOT_hence \<open>\<exists>w w \<Turnstile> \<box>r\<close>
      by (rule "PossibleWorld.\<exists>I")
    AOT_hence \<open>\<box>r\<close>
      by (metis "\<equiv>E"(2) "nec-dia-w:1")
    AOT_thus \<open>\<box>r & \<not>\<box>r\<close>
      using B "&I" by blast
  qed
  ultimately AOT_have \<open>\<box>w \<Turnstile> r & \<not>w \<Turnstile> \<box>r\<close>
    by (rule "&I")
  AOT_hence \<open>\<exists>p (\<box>w \<Turnstile> p & \<not>w \<Turnstile> \<box>p)\<close>
    by (rule "\<exists>I")
  thus ?thesis
    by (rule "PossibleWorld.\<exists>I")
qed

AOT_theorem "conj-dist-w:9": \<open>(\<diamond>w \<Turnstile> p) \<rightarrow> w \<Turnstile> \<diamond>p\<close>
proof(rule "\<rightarrow>I"; rule "raa-cor:1")
  AOT_assume \<open>\<diamond>w \<Turnstile> p\<close>
  AOT_hence 0: \<open>w \<Turnstile> p\<close>
    by (metis "\<equiv>E"(1) "rigid-truth-at:2")
  AOT_assume \<open>\<not>w \<Turnstile> \<diamond>p\<close>
  AOT_hence 1: \<open>w \<Turnstile> \<not>\<diamond>p\<close>
    using "coherent:1"[unvarify p, THEN "\<equiv>E"(2), OF "log-prop-prop:2"] by blast
  moreover AOT_have \<open>w \<Turnstile> (\<not>\<diamond>p \<rightarrow> \<not>p)\<close>
    using "T\<diamond>"[THEN "contraposition:1[1]", THEN RN]
          "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "\<equiv>E"(1), THEN "\<forall>E"(2),
                   THEN "\<rightarrow>E", rotated, OF PossibleWorld.\<psi>]
          by blast
  ultimately AOT_have \<open>w \<Turnstile> \<not>p\<close>
    using "conj-dist-w:2"[unvarify p q, OF "log-prop-prop:2", OF "log-prop-prop:2",
                          THEN "\<equiv>E"(1), THEN "\<rightarrow>E"]
    by blast
  AOT_hence \<open>w \<Turnstile> p & w \<Turnstile> \<not>p\<close> using 0 "&I" by blast
  AOT_thus \<open>p & \<not>p\<close>
    by (metis "coherent:1" "Conjunction Simplification"(1,2) "\<equiv>E"(4)
              "modus-tollens:1" "raa-cor:3")
qed

AOT_theorem "conj-dist-w:10": \<open>\<exists>w\<exists>p((w \<Turnstile> \<diamond>p) & \<not>\<diamond>w \<Turnstile> p)\<close>
proof -
  AOT_obtain w where w: \<open>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "act-world:1" "PossibleWorld.\<exists>E"[rotated] by meson
  AOT_obtain r where \<open>\<not>r\<close> and \<open>\<diamond>r\<close>
    using "cont-tf-thm:2" "cont-tf:2"[THEN "\<equiv>\<^sub>d\<^sub>fE"] "&E" "\<exists>E"[rotated] by metis
  AOT_hence \<open>w \<Turnstile> \<not>r\<close> and 0: \<open>w \<Turnstile> \<diamond>r\<close>
    using w[THEN "\<forall>E"(1), OF "log-prop-prop:2", THEN "\<equiv>E"(2)] by blast+
  AOT_hence \<open>\<not>w \<Turnstile> r\<close> using "coherent:1"[THEN "\<equiv>E"(1)] by blast
  AOT_hence \<open>\<not>\<diamond>w \<Turnstile> r\<close> by (metis "\<equiv>E"(4) "rigid-truth-at:2")
  AOT_hence \<open>w \<Turnstile> \<diamond>r & \<not>\<diamond>w \<Turnstile> r\<close> using 0 "&I"n> by blast
  AOT_hence \<open>\<exists>p (w \<Turnstile> \<diamond>p & \<not>\<diamond>w \<Turnstile> p)\<close> by (rule "\<exists>I")
  thus ?thesis by (rule "PossibleWorld.\<exists>I")
qed

AOT_theorem "two-worlds-exist:1": \<open>\<exists>p(ContingentlyTrue(p)) \<rightarrow> \<exists>w (\<not>Actual(w))\<close>
proof(rule "\<rightarrow>I")
  AOT_assume \<open>\<exists>p ContingentlyTrue(p)\<close>
  then AOT_obtain p where \<open>ContingentlyTrue(p)\<close>
    using "\<exists>E"[rotated] by blast
  AOT_hence p: \<open>p & \<diamond>\<not>p\<close>
    by (metis "\<equiv>\<^sub>d\<^sub>fE" "cont-tf:1")
  AOT_hence \<open>\<exists>w w \<Turnstile> \<not>p\<close>
    using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "\<equiv>E"(1)] "&E" by blast
  then AOT_obtain w where w: \<open>w \<Turnstile> \<not>p\<close>
    using "PossibleWorld.\<exists>E"[rotated] by meson
  AOT_have \<open>\<not>Actual(w)\<close>
  proof(rule "raa-cor:2")
    AOT_assume \<open>Actual(w)\<close>
    AOT_hence \<open>w \<Turnstile> p\<close>
      using p[THEN "&E"(1)] actual[THEN "\<equiv>\<^sub>d\<^sub>fE", THEN "&E"(2)]
      by (metis "log-prop-prop:2" "raa-cor:3" "rule-ui:1" "\<rightarrow>E" w)
    moreover AOT_have \<open>\<not>(w \<Turnstile> p)\<close>
      by (metis "coherent:1" "\<equiv>E"(4) "reductio-aa:2" w) 
    ultimately AOT_show \<open>w \<Turnstile> p & \<not>(w \<Turnstile> p)\<close>
      using "&I" by blast
  qed
  AOT_thus \<open>\<exists>w \<not>Actual(w)\<close>
    by (rule "PossibleWorld.\<exists>I")
qed


AOT_theorem "two-worlds-exist:2": \<open>\<exists>p(ContingentlyFalse(p)) \<rightarrow> \<exists>w (\<not>Actual(w))\<close>
proof(rule "\<rightarrow>I")
  AOT_assume \<open>\<exists>p ContingentlyFalse(p)\<close>
  then AOT_obtain p where \<open>ContingentlyFalse(p)\<close>
    using "\<exists>E"[rotated] by blast
  AOT_hence p: \<open>\<not>p & \<diamond>p\<close>
    by (metis "\<equiv>\<^sub>d\<^sub>fE" "cont-tf:2")
  AOT_hence \<open>\<exists>w w \<Turnstile> p\<close>
    using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "\<equiv>E"(1)] "&E" by blast
  then AOT_obtain w where w: \<open>w \<Turnstile> p\<close>
    using "PossibleWorld.\<exists>E"[rotated] by meson
  moreover AOT_have \<open>\<not>Actual(w)\<close>
  proof(rule "raa-cor:2")
    AOT_assume \<open>Actual(w)\<close>
    AOT_hence \<open>w \<Turnstile> \<not>p\<close>
      using p[THEN "&E"(1)] actual[THEN "\<equiv>\<^sub>d\<^sub>fE", THEN "&E"(2)]
      by (metis "log-prop-prop:2" "raa-cor:3" "rule-ui:1" "\<rightarrow>E" w)
    moreover AOT_have \<open>\<not>(w \<Turnstile> p)\<close>
      using calculation by (metis "coherent:1" "\<equiv>E"(4) "reductio-aa:2") 
    AOT_thus \<open>w \<Turnstile> p & \<not>(w \<Turnstile> p)\<close>
      using "&I" w by metis
  qed
  AOT_thus \<open>\<exists>w \<not>Actual(w)\<close>
    by (rule "PossibleWorld.\<exists>I")
qed

AOT_theorem "two-worlds-exist:3": \<open>\<exists>w \<not>Actual(w)\<close>
  using "cont-tf-thm:1" "two-worlds-exist:1" "\<rightarrow>E" by blast

AOT_theorem "two-worlds-exist:4": \<open>\<exists>w\<exists>w'(w \<noteq> w')\<close>
proof -
  AOT_obtain w where w: \<open>Actual(w)\<close>
    using "act-world:2"[THEN "uniqueness:1"[THEN "\<equiv>\<^sub>d\<^sub>fE"],
                        THEN "cqt-further:5"[THEN "\<rightarrow>E"]]
          "PossibleWorld.\<exists>E"[rotated] "&E"
    by blast
  moreover AOT_obtain w' where w': \<open>\<not>Actual(w')\<close>
    using "two-worlds-exist:3" "PossibleWorld.\<exists>E"[rotated] by meson
  AOT_have \<open>\<not>(w = w')\<close>
  proof(rule "raa-cor:2")
    AOT_assume \<open>w = w'\<close>
    AOT_thus \<open>p & \<not>p\<close> for p
      using w w' "&E" by (metis "rule=E" "raa-cor:3")
  qed
  AOT_hence \<open>w \<noteq> w'\<close>
    by (metis "\<equiv>\<^sub>d\<^sub>fI" "=-infix")
  AOT_hence \<open>\<exists>w' w \<noteq> w'\<close>
    by (rule "PossibleWorld.\<exists>I")
  thus ?thesis
    by (rule "PossibleWorld.\<exists>I")
qed

(* TODO: more theorems *)

AOT_theorem "w-rel:1": \<open>[\<lambda>x \<phi>{x}]\<down> \<rightarrow> [\<lambda>x w \<Turnstile> \<phi>{x}]\<down>\<close>
proof(rule "\<rightarrow>I")
  AOT_assume \<open>[\<lambda>x \<phi>{x}]\<down>\<close>
  AOT_hence \<open>\<box>[\<lambda>x \<phi>{x}]\<down>\<close>
    by (metis "exist-nec" "\<rightarrow>E")
  moreover AOT_have
    \<open>\<box>[\<lambda>x \<phi>{x}]\<down> \<rightarrow> \<box>\<forall>x\<forall>y(\<forall>F([F]x \<equiv> [F]y) \<rightarrow> ((w \<Turnstile> \<phi>{x}) \<equiv> ( w \<Turnstile> \<phi>{y})))\<close>
  proof (rule RM; rule "\<rightarrow>I"; rule GEN; rule GEN; rule "\<rightarrow>I")
    AOT_modally_strict {
      fix x y
      AOT_assume \<open>[\<lambda>x \<phi>{x}]\<down>\<close>
      AOT_hence \<open>\<forall>x\<forall>y (\<forall>F ([F]x \<equiv> [F]y) \<rightarrow> \<box>(\<phi>{x} \<equiv> \<phi>{y}))\<close>
        using "&E" "kirchner-thm-cor:1"[THEN "\<rightarrow>E"] by blast
      AOT_hence \<open>\<forall>F ([F]x \<equiv> [F]y) \<rightarrow> \<box>(\<phi>{x} \<equiv> \<phi>{y})\<close>
        using "\<forall>E"(2) by blast
      moreover AOT_assume \<open>\<forall>F ([F]x \<equiv> [F]y)\<close>
      ultimately AOT_have \<open>\<box>(\<phi>{x} \<equiv> \<phi>{y})\<close>
        using "\<rightarrow>E" by blast
      AOT_hence \<open>\<forall>w (w \<Turnstile> (\<phi>{x} \<equiv> \<phi>{y}))\<close>
        using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "\<equiv>E"(1)] by blast
      AOT_hence \<open>w \<Turnstile> (\<phi>{x} \<equiv> \<phi>{y})\<close>
        using "\<forall>E"(2) using PossibleWorld.\<psi> "\<rightarrow>E" by blast
      AOT_thus \<open>(w \<Turnstile> \<phi>{x}) \<equiv> (w \<Turnstile> \<phi>{y})\<close>
        using "conj-dist-w:4"[unvarify p q, OF "log-prop-prop:2",
                              OF "log-prop-prop:2", THEN "\<equiv>E"(1)] by blast
    }
  qed
  ultimately AOT_have \<open>\<box>\<forall>x\<forall>y(\<forall>F([F]x \<equiv> [F]y) \<rightarrow> ((w \<Turnstile> \<phi>{x}) \<equiv> ( w \<Turnstile> \<phi>{y})))\<close>
    using "\<rightarrow>E" by blast
  AOT_thus \<open>[\<lambda>x w \<Turnstile> \<phi>{x}]\<down>\<close>
    using "kirchner-thm:1"[THEN "\<equiv>E"(2)] by fast
qed

AOT_theorem "w-rel:2": \<open>[\<lambda>x\<^sub>1...x\<^sub>n \<phi>{x\<^sub>1...x\<^sub>n}]\<down> \<rightarrow> [\<lambda>x\<^sub>1...x\<^sub>n w \<Turnstile> \<phi>{x\<^sub>1...x\<^sub>n}]\<down>\<close>
proof(rule "\<rightarrow>I")
  AOT_assume \<open>[\<lambda>x\<^sub>1...x\<^sub>n \<phi>{x\<^sub>1...x\<^sub>n}]\<down>\<close>
  AOT_hence \<open>\<box>[\<lambda>x\<^sub>1...x\<^sub>n \<phi>{x\<^sub>1...x\<^sub>n}]\<down>\<close>
    by (metis "exist-nec" "\<rightarrow>E")
  moreover AOT_have \<open>\<box>[\<lambda>x\<^sub>1...x\<^sub>n \<phi>{x\<^sub>1...x\<^sub>n}]\<down> \<rightarrow> \<box>\<forall>x\<^sub>1...\<forall>x\<^sub>n\<forall>y\<^sub>1...\<forall>y\<^sub>n(
    \<forall>F([F]x\<^sub>1...x\<^sub>n \<equiv> [F]y\<^sub>1...y\<^sub>n) \<rightarrow> ((w \<Turnstile> \<phi>{x\<^sub>1...x\<^sub>n}) \<equiv> ( w \<Turnstile> \<phi>{y\<^sub>1...y\<^sub>n})))\<close>
  proof (rule RM; rule "\<rightarrow>I"; rule GEN; rule GEN; rule "\<rightarrow>I")
    AOT_modally_strict {
      fix x\<^sub>1x\<^sub>n y\<^sub>1y\<^sub>n
      AOT_assume \<open>[\<lambda>x\<^sub>1...x\<^sub>n \<phi>{x\<^sub>1...x\<^sub>n}]\<down>\<close>
      AOT_hence \<open>\<forall>x\<^sub>1...\<forall>x\<^sub>n\<forall>y\<^sub>1...\<forall>y\<^sub>n (
        \<forall>F ([F]x\<^sub>1...x\<^sub>n \<equiv> [F]y\<^sub>1...y\<^sub>n) \<rightarrow> \<box>(\<phi>{x\<^sub>1...x\<^sub>n} \<equiv> \<phi>{y\<^sub>1...y\<^sub>n}))\<close>
        using "&E" "kirchner-thm-cor:2"[THEN "\<rightarrow>E"] by blast
      AOT_hence \<open>\<forall>F ([F]x\<^sub>1...x\<^sub>n \<equiv> [F]y\<^sub>1...y\<^sub>n) \<rightarrow> \<box>(\<phi>{x\<^sub>1...x\<^sub>n} \<equiv> \<phi>{y\<^sub>1...y\<^sub>n})\<close>
        using "\<forall>E"(2) by blast
      moreover AOT_assume \<open>\<forall>F ([F]x\<^sub>1...x\<^sub>n \<equiv> [F]y\<^sub>1...y\<^sub>n)\<close>
      ultimately AOT_have \<open>\<box>(\<phi>{x\<^sub>1...x\<^sub>n} \<equiv> \<phi>{y\<^sub>1...y\<^sub>n})\<close>
        using "\<rightarrow>E" by blast
      AOT_hence \<open>\<forall>w (w \<Turnstile> (\<phi>{x\<^sub>1...x\<^sub>n} \<equiv> \<phi>{y\<^sub>1...y\<^sub>n}))\<close>
        using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "\<equiv>E"(1)] by blast
      AOT_hence \<open>w \<Turnstile> (\<phi>{x\<^sub>1...x\<^sub>n} \<equiv> \<phi>{y\<^sub>1...y\<^sub>n})\<close>
        using "\<forall>E"(2) using PossibleWorld.\<psi> "\<rightarrow>E" by blast
      AOT_thus \<open>(w \<Turnstile> \<phi>{x\<^sub>1...x\<^sub>n}) \<equiv> (w \<Turnstile> \<phi>{y\<^sub>1...y\<^sub>n})\<close>
        using "conj-dist-w:4"[unvarify p q, OF "log-prop-prop:2",
                              OF "log-prop-prop:2", THEN "\<equiv>E"(1)] by blast
    }
  qed
  ultimately AOT_have \<open>\<box>\<forall>x\<^sub>1...\<forall>x\<^sub>n\<forall>y\<^sub>1...\<forall>y\<^sub>n(
      \<forall>F([F]x\<^sub>1...x\<^sub>n \<equiv> [F]y\<^sub>1...y\<^sub>n) \<rightarrow> ((w \<Turnstile> \<phi>{x\<^sub>1...x\<^sub>n}) \<equiv> ( w \<Turnstile> \<phi>{y\<^sub>1...y\<^sub>n})))\<close>
    using "\<rightarrow>E" by blast
  AOT_thus \<open>[\<lambda>x\<^sub>1...x\<^sub>n w \<Turnstile> \<phi>{x\<^sub>1...x\<^sub>n}]\<down>\<close>
    using "kirchner-thm:2"[THEN "\<equiv>E"(2)] by fast
qed

AOT_theorem "w-rel:3": \<open>[\<lambda>x\<^sub>1...x\<^sub>n w \<Turnstile> [F]x\<^sub>1...x\<^sub>n]\<down>\<close>
  by (rule "w-rel:2"[THEN "\<rightarrow>E"]) "cqt:2[lambda]"

AOT_define WorldIndexedRelation :: \<open>\<Pi> \<Rightarrow> \<tau> \<Rightarrow> \<Pi>\<close> (\<open>_\<^sub>_\<close>)
  "w-index": \<open>[F]\<^sub>w =\<^sub>d\<^sub>f [\<lambda>x\<^sub>1...x\<^sub>n w \<Turnstile> [F]x\<^sub>1...x\<^sub>n]\<close>

AOT_define Rigid :: \<open>\<tau> \<Rightarrow> \<phi>\<close> (\<open>Rigid'(_')\<close>)
  "df-rigid-rel:1":
\<open>Rigid(F) \<equiv>\<^sub>d\<^sub>f F\<down> & \<box>\<forall>x\<^sub>1...\<forall>x\<^sub>n([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)\<close>

AOT_define Rigidifies :: \<open>\<tau> \<Rightarrow> \<tau> \<Rightarrow> \<phi>\<close> (\<open>Rigidifies'(_,_')\<close>)
  "df-rigid-rel:2":
\<open>Rigidifies(F, G) \<equiv>\<^sub>d\<^sub>f Rigid(F) & \<forall>x\<^sub>1...\<forall>x\<^sub>n([F]x\<^sub>1...x\<^sub>n \<equiv> [G]x\<^sub>1...x\<^sub>n)\<close>

AOT_theorem "rigid-der:1": \<open>[[F]\<^sub>w]x\<^sub>1...x\<^sub>n \<equiv> w \<Turnstile> [F]x\<^sub>1...x\<^sub>n\<close>
  apply (rule "rule-id-df:2:b[2]"[where \<tau>="\<lambda> (\<Pi>, \<kappa>). \<guillemotleft>[\<Pi>]\<^sub>\<kappa>\<guillemotright>" and
                                        \<sigma>="\<lambda>(\<Pi>, \<kappa>). \<guillemotleft>[\<lambda>x\<^sub>1...x\<^sub>n \<kappa> \<Turnstile> [\<Pi>]x\<^sub>1...x\<^sub>n]\<guillemotright>",
                                  simplified, OF "w-index"])
   apply (fact "w-rel:3")
  apply (rule "beta-C-meta"[THEN "\<rightarrow>E"])
  by (fact "w-rel:3")

AOT_theorem "rigid-der:2": \<open>Rigid([G]\<^sub>w)\<close>
proof(safe intro!: "\<equiv>\<^sub>d\<^sub>fI"[OF "df-rigid-rel:1"] "&I")
  AOT_show \<open>[G]\<^sub>w\<down>\<close>
    by (rule "rule-id-df:2:b[2]"[where \<tau>="\<lambda> (\<Pi>, \<kappa>). \<guillemotleft>[\<Pi>]\<^sub>\<kappa>\<guillemotright>" and
                                       \<sigma>="\<lambda>(\<Pi>, \<kappa>). \<guillemotleft>[\<lambda>x\<^sub>1...x\<^sub>n \<kappa> \<Turnstile> [\<Pi>]x\<^sub>1...x\<^sub>n]\<guillemotright>",
                                 simplified, OF "w-index"])
       (fact "w-rel:3")+
next
  AOT_have \<open>\<box>\<forall>x\<^sub>1...\<forall>x\<^sub>n ([[G]\<^sub>w]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[[G]\<^sub>w]x\<^sub>1...x\<^sub>n)\<close>
  proof(rule RN; safe intro!: "\<rightarrow>I" GEN)
    AOT_modally_strict {
      AOT_have assms: \<open>PossibleWorld(w)\<close> using PossibleWorld.\<psi>.
      AOT_hence nec_pw_w: \<open>\<box>PossibleWorld(w)\<close>
        using "\<equiv>E"(1) "rigid-pw:1" by blast
      fix x\<^sub>1x\<^sub>n
      AOT_assume \<open>[[G]\<^sub>w]x\<^sub>1...x\<^sub>n\<close>
      AOT_hence \<open>[\<lambda>x\<^sub>1...x\<^sub>n w \<Turnstile> [G]x\<^sub>1...x\<^sub>n]x\<^sub>1...x\<^sub>n\<close>
        using "rule-id-df:2:a[2]"[where \<tau>="\<lambda> (\<Pi>, \<kappa>). \<guillemotleft>[\<Pi>]\<^sub>\<kappa>\<guillemotright>" and
                                        \<sigma>="\<lambda>(\<Pi>, \<kappa>). \<guillemotleft>[\<lambda>x\<^sub>1...x\<^sub>n \<kappa> \<Turnstile> [\<Pi>]x\<^sub>1...x\<^sub>n]\<guillemotright>",
                                        simplified, OF "w-index", OF "w-rel:3"]
        by fast
      AOT_hence \<open>w \<Turnstile> [G]x\<^sub>1...x\<^sub>n\<close>
        by (metis "\<beta>\<rightarrow>C"(1))
      AOT_hence \<open>\<box>w \<Turnstile> [G]x\<^sub>1...x\<^sub>n\<close>
        using "rigid-truth-at:1"[unvarify p, OF "log-prop-prop:2", THEN "\<equiv>E"(1)]
        by blast
      moreover AOT_have \<open>\<box>w \<Turnstile> [G]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[\<lambda>x\<^sub>1...x\<^sub>n w \<Turnstile> [G]x\<^sub>1...x\<^sub>n]x\<^sub>1...x\<^sub>n\<close>
      proof (rule RM; rule "\<rightarrow>I")
        AOT_modally_strict {
          AOT_assume \<open>w \<Turnstile> [G]x\<^sub>1...x\<^sub>n\<close>
          AOT_thus \<open>[\<lambda>x\<^sub>1...x\<^sub>n w \<Turnstile> [G]x\<^sub>1...x\<^sub>n]x\<^sub>1...x\<^sub>n\<close>
            by (auto intro!: "\<beta>\<leftarrow>C"(1) simp: "w-rel:3" "cqt:2")
        }
      qed
      ultimately AOT_have 1: \<open>\<box>[\<lambda>x\<^sub>1...x\<^sub>n w \<Turnstile> [G]x\<^sub>1...x\<^sub>n]x\<^sub>1...x\<^sub>n\<close>
        using "\<rightarrow>E" by blast
      AOT_show \<open>\<box>[[G]\<^sub>w]x\<^sub>1...x\<^sub>n\<close>
        by (rule "rule-id-df:2:b[2]"[where \<tau>="\<lambda> (\<Pi>, \<kappa>). \<guillemotleft>[\<Pi>]\<^sub>\<kappa>\<guillemotright>" and
                                           \<sigma>="\<lambda>(\<Pi>, \<kappa>). \<guillemotleft>[\<lambda>x\<^sub>1...x\<^sub>n \<kappa> \<Turnstile> [\<Pi>]x\<^sub>1...x\<^sub>n]\<guillemotright>",
                                     simplified, OF "w-index"])
           (auto simp: 1 "w-rel:3")
    }
  qed
  AOT_thus \<open>\<box>\<forall>x\<^sub>1...\<forall>x\<^sub>n ([[G]\<^sub>w]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[[G]\<^sub>w]x\<^sub>1...x\<^sub>n)\<close>
    using "\<rightarrow>E" by blast
qed

AOT_theorem "rigid-der:3": \<open>\<exists>F Rigidifies(F, G)\<close>
proof -
  AOT_obtain w where w: \<open>\<forall>p (w \<Turnstile> p \<equiv> p)\<close>
    using "act-world:1" "PossibleWorld.\<exists>E"[rotated] by meson
  show ?thesis
  proof (rule "\<exists>I"(1)[where \<tau>=\<open>\<guillemotleft>[G]\<^sub>w\<guillemotright>\<close>])
    AOT_show \<open>Rigidifies([G]\<^sub>w, [G])\<close>
    proof(safe intro!: "\<equiv>\<^sub>d\<^sub>fI"[OF "df-rigid-rel:2"] "&I" GEN)
      AOT_show \<open>Rigid([G]\<^sub>w)\<close>
        using "rigid-der:2" by blast
    next
      fix x\<^sub>1x\<^sub>n
      AOT_have \<open>[[G]\<^sub>w]x\<^sub>1...x\<^sub>n \<equiv> [\<lambda>x\<^sub>1...x\<^sub>n w \<Turnstile> [G]x\<^sub>1...x\<^sub>n]x\<^sub>1...x\<^sub>n\<close>
      proof(rule "\<equiv>I"; rule "\<rightarrow>I")
        AOT_assume \<open>[[G]\<^sub>w]x\<^sub>1...x\<^sub>n\<close>
        AOT_thus \<open>[\<lambda>x\<^sub>1...x\<^sub>n w \<Turnstile> [G]x\<^sub>1...x\<^sub>n]x\<^sub>1...x\<^sub>n\<close>
          by (rule "rule-id-df:2:a[2]"
                      [where \<tau>="\<lambda> (\<Pi>, \<kappa>). \<guillemotleft>[\<Pi>]\<^sub>\<kappa>\<guillemotright>" and
                             \<sigma>="\<lambda>(\<Pi>, \<kappa>). \<guillemotleft>[\<lambda>x\<^sub>1...x\<^sub>n \<kappa> \<Turnstile> [\<Pi>]x\<^sub>1...x\<^sub>n]\<guillemotright>",
                       simplified, OF "w-index", OF "w-rel:3"])
      next
        AOT_assume \<open>[\<lambda>x\<^sub>1...x\<^sub>n w \<Turnstile> [G]x\<^sub>1...x\<^sub>n]x\<^sub>1...x\<^sub>n\<close>
        AOT_thus \<open>[[G]\<^sub>w]x\<^sub>1...x\<^sub>n\<close>
          by (rule "rule-id-df:2:b[2]"
                      [where \<tau>="\<lambda> (\<Pi>, \<kappa>). \<guillemotleft>[\<Pi>]\<^sub>\<kappa>\<guillemotright>" and
                             \<sigma>="\<lambda>(\<Pi>, \<kappa>). \<guillemotleft>[\<lambda>x\<^sub>1...x\<^sub>n \<kappa> \<Turnstile> [\<Pi>]x\<^sub>1...x\<^sub>n]\<guillemotright>",
                       simplified, OF "w-index", OF "w-rel:3"])
      qed
      also AOT_have \<open>\<dots> \<equiv> w \<Turnstile> [G]x\<^sub>1...x\<^sub>n\<close>
        by (rule "beta-C-meta"[THEN "\<rightarrow>E"])
           (fact "w-rel:3")
      also AOT_have \<open>\<dots> \<equiv> [G]x\<^sub>1...x\<^sub>n\<close>
        using w[THEN "\<forall>E"(1), OF "log-prop-prop:2"] by blast
      finally AOT_show \<open>[[G]\<^sub>w]x\<^sub>1...x\<^sub>n \<equiv> [G]x\<^sub>1...x\<^sub>n\<close>.
    qed
  next
    AOT_show \<open>[G]\<^sub>w\<down>\<close>
      by (rule "rule-id-df:2:b[2]"[where \<tau>="\<lambda> (\<Pi>, \<kappa>). \<guillemotleft>[\<Pi>]\<^sub>\<kappa>\<guillemotright>"
                                     and \<sigma>="\<lambda>(\<Pi>, \<kappa>). \<guillemotleft>[\<lambda>x\<^sub>1...x\<^sub>n \<kappa> \<Turnstile> [\<Pi>]x\<^sub>1...x\<^sub>n]\<guillemotright>",
                                   simplified, OF "w-index"])
         (auto simp: "w-rel:3")
  qed
qed

AOT_theorem "rigid-rel-thms:1":
  \<open>\<box>(\<forall>x\<^sub>1...\<forall>x\<^sub>n ([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)) \<equiv> \<forall>x\<^sub>1...\<forall>x\<^sub>n(\<diamond>[F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)\<close>
proof(safe intro!: "\<equiv>I" "\<rightarrow>I" GEN)
  fix x\<^sub>1x\<^sub>n
  AOT_assume \<open>\<box>\<forall>x\<^sub>1...\<forall>x\<^sub>n ([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)\<close>
  AOT_hence \<open>\<forall>x\<^sub>1...\<forall>x\<^sub>n \<box>([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)\<close>
    by (metis "\<rightarrow>E" GEN RM "cqt-orig:3")
  AOT_hence \<open>\<box>([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)\<close>
    using "\<forall>E"(2) by blast
  AOT_hence \<open>\<diamond>[F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n\<close>
    by (metis "\<equiv>E"(1) "sc-eq-box-box:1")
  moreover AOT_assume \<open>\<diamond>[F]x\<^sub>1...x\<^sub>n\<close>
  ultimately AOT_show \<open>\<box>[F]x\<^sub>1...x\<^sub>n\<close>
    using "\<rightarrow>E" by blast
next
  AOT_assume \<open>\<forall>x\<^sub>1...\<forall>x\<^sub>n (\<diamond>[F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)\<close>
  AOT_hence \<open>\<diamond>[F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n\<close> for x\<^sub>1x\<^sub>n
    using "\<forall>E"(2) by blast
  AOT_hence \<open>\<box>([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)\<close> for x\<^sub>1x\<^sub>n
    by (metis "\<equiv>E"(2) "sc-eq-box-box:1")
  AOT_hence 0: \<open>\<forall>x\<^sub>1...\<forall>x\<^sub>n \<box>([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)\<close>
    by (rule GEN)
  AOT_thus \<open>\<box>(\<forall>x\<^sub>1...\<forall>x\<^sub>n ([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n))\<close>
    using "BF" "vdash-properties:10" by blast
qed

AOT_theorem "rigid-rel-thms:2":
  \<open>\<box>(\<forall>x\<^sub>1...\<forall>x\<^sub>n ([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)) \<equiv> \<forall>x\<^sub>1...\<forall>x\<^sub>n(\<box>[F]x\<^sub>1...x\<^sub>n \<or> \<box>\<not>[F]x\<^sub>1...x\<^sub>n)\<close>
proof(safe intro!: "\<equiv>I" "\<rightarrow>I")
  AOT_assume \<open>\<box>(\<forall>x\<^sub>1...\<forall>x\<^sub>n ([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n))\<close>
  AOT_hence 0: \<open>\<forall>x\<^sub>1...\<forall>x\<^sub>n \<box>([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)\<close>
    using CBF[THEN "\<rightarrow>E"] by blast
  AOT_show \<open>\<forall>x\<^sub>1...\<forall>x\<^sub>n(\<box>[F]x\<^sub>1...x\<^sub>n \<or> \<box>\<not>[F]x\<^sub>1...x\<^sub>n)\<close>
  proof(rule GEN)
    fix x\<^sub>1x\<^sub>n
    AOT_have 1: \<open>\<box>([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)\<close>
      using 0[THEN "\<forall>E"(2)].
    AOT_hence 2: \<open>\<diamond>[F]x\<^sub>1...x\<^sub>n \<rightarrow> [F]x\<^sub>1...x\<^sub>n\<close>
      using "B\<diamond>" "Hypothetical Syllogism" "K\<diamond>" "vdash-properties:10" by blast
    AOT_have \<open>[F]x\<^sub>1...x\<^sub>n \<or> \<not>[F]x\<^sub>1...x\<^sub>n\<close>
      using "exc-mid".
    moreover {
      AOT_assume \<open>[F]x\<^sub>1...x\<^sub>n\<close>
      AOT_hence \<open>\<box>[F]x\<^sub>1...x\<^sub>n\<close>
        using 1[THEN "qml:2"[axiom_inst, THEN "\<rightarrow>E"], THEN "\<rightarrow>E"] by blast
    }
    moreover {
      AOT_assume 3: \<open>\<not>[F]x\<^sub>1...x\<^sub>n\<close>
      AOT_have \<open>\<box>\<not>[F]x\<^sub>1...x\<^sub>n\<close>
      proof(rule "raa-cor:1")
        AOT_assume \<open>\<not>\<box>\<not>[F]x\<^sub>1...x\<^sub>n\<close>
        AOT_hence \<open>\<diamond>[F]x\<^sub>1...x\<^sub>n\<close>
          by (AOT_subst_def "conventions:5")
        AOT_hence \<open>[F]x\<^sub>1...x\<^sub>n\<close> using 2[THEN "\<rightarrow>E"] by blast
        AOT_thus \<open>[F]x\<^sub>1...x\<^sub>n & \<not>[F]x\<^sub>1...x\<^sub>n\<close>
          using 3 "&I" by blast
      qed
    }
    ultimately AOT_show \<open>\<box>[F]x\<^sub>1...x\<^sub>n \<or> \<box>\<not>[F]x\<^sub>1...x\<^sub>n\<close>
      by (metis "\<or>I"(1,2) "raa-cor:1")
  qed
next
  AOT_assume 0: \<open>\<forall>x\<^sub>1...\<forall>x\<^sub>n(\<box>[F]x\<^sub>1...x\<^sub>n \<or> \<box>\<not>[F]x\<^sub>1...x\<^sub>n)\<close>
  {
    fix x\<^sub>1x\<^sub>n
    AOT_have \<open>\<box>[F]x\<^sub>1...x\<^sub>n \<or> \<box>\<not>[F]x\<^sub>1...x\<^sub>n\<close> using 0[THEN "\<forall>E"(2)] by blast
    moreover {
      AOT_assume \<open>\<box>[F]x\<^sub>1...x\<^sub>n\<close>
      AOT_hence \<open>\<box>\<box>[F]x\<^sub>1...x\<^sub>n\<close>
        using "S5Basic:6"[THEN "\<equiv>E"(1)] by blast
      AOT_hence \<open>\<box>([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)\<close>
        using "KBasic:1"[THEN "\<rightarrow>E"] by blast
    }
    moreover {
      AOT_assume \<open>\<box>\<not>[F]x\<^sub>1...x\<^sub>n\<close>
      AOT_hence \<open>\<box>([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)\<close>
        using "KBasic:2"[THEN "\<rightarrow>E"] by blast
    }
    ultimately AOT_have \<open>\<box>([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)\<close>
      using "con-dis-i-e:4:b" "raa-cor:1" by blast
  }
  AOT_hence \<open>\<forall>x\<^sub>1...\<forall>x\<^sub>n \<box>([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n)\<close>
    by (rule GEN)
  AOT_thus \<open>\<box>(\<forall>x\<^sub>1...\<forall>x\<^sub>n ([F]x\<^sub>1...x\<^sub>n \<rightarrow> \<box>[F]x\<^sub>1...x\<^sub>n))\<close>
    using BF[THEN "\<rightarrow>E"] by fast
qed

 "rigidrel-thms:3: \<open>igid( <>\forall>\^1..<orall>\box[]\<^>.x<sub> <>\box>\<not[F]\^>1..\<^subn\close>
  by (AOT_subst_thm "df-rigid-java.lang.StringIndexOutOfBoundsException: Range [0, 33) out of bounds for length 0
      AOT_subst_thm "rigid-rel-thms:2")
     (simp add: "oth-class-taut:3:a")

(*<*)
end
(*>*)