# Theory AOT_misc

```theory AOT_misc
imports AOT_NaturalNumbers
begin

section‹Miscellaneous Theorems›

AOT_theorem PossiblyNumbersEmptyPropertyImpliesZero:
‹◇Numbers(x,[λz O!z & z ≠⇩E z]) → x = 0›
proof(rule "→I")
AOT_have ‹Rigid([λz O!z & z ≠⇩E z])›
proof (safe intro!: "df-rigid-rel:1"[THEN "≡⇩d⇩fI"] "&I" "cqt:2";
rule RN; safe intro!: GEN "→I")
AOT_modally_strict {
fix x
AOT_assume ‹[λz O!z & z ≠⇩E z]x›
AOT_hence ‹O!x & x ≠⇩E x› by (rule "β→C")
moreover AOT_have ‹x =⇩E x› using calculation[THEN "&E"(1)]
by (metis "ord=Eequiv:1" "vdash-properties:10")
ultimately AOT_have ‹x =⇩E x & ¬x =⇩E x›
by (metis "con-dis-i-e:1" "con-dis-i-e:2:b" "intro-elim:3:a" "thm-neg=E")
AOT_thus ‹□[λz O!z & z ≠⇩E z]x› using "raa-cor:1" by blast
}
qed
AOT_hence ‹□∀x (Numbers(x,[λz O!z & z ≠⇩E z]) → □Numbers(x,[λz O!z & z ≠⇩E z]))›
by (safe intro!: "num-cont:2"[unvarify G, THEN "→E"] "cqt:2")
AOT_hence ‹∀x □(Numbers(x,[λz O!z & z ≠⇩E z]) → □Numbers(x,[λz O!z & z ≠⇩E z]))›
using "BFs:2"[THEN "→E"] by blast
AOT_hence ‹□(Numbers(x,[λz O!z & z ≠⇩E z]) → □Numbers(x,[λz O!z & z ≠⇩E z]))›
using "∀E"(2) by auto
moreover AOT_assume ‹◇Numbers(x,[λz O!z & z ≠⇩E z])›
ultimately AOT_have ‹❙𝒜Numbers(x,[λz O!z & z ≠⇩E z])›
using "sc-eq-box-box:1"[THEN "≡E"(1), THEN "→E", THEN "nec-imp-act"[THEN "→E"]]
by blast
AOT_hence ‹Numbers(x,[λz ❙𝒜[λz O!z & z ≠⇩E z]z])›
by (safe intro!: "eq-num:1"[unvarify G, THEN "≡E"(1)] "cqt:2")
AOT_hence ‹x = #[λz O!z & z ≠⇩E z]›
by (safe intro!: "eq-num:2"[unvarify G, THEN "≡E"(1)] "cqt:2")
AOT_thus ‹x = 0›
using "cqt:2"(1) "rule-id-df:2:b[zero]" "rule=E" "zero:1" by blast
qed

AOT_define Numbers' :: ‹τ ⇒ τ ⇒ φ› (‹Numbers'''(_,_')›)
‹Numbers'(x, G) ≡⇩d⇩f A!x & G↓ & ∀F (x[F] ≡ F ≈⇩E G)›
AOT_theorem Numbers'equiv: ‹Numbers'(x,G) ≡ A!x & ∀F (x[F] ≡ F ≈⇩E G)›
by (AOT_subst_def Numbers')
(auto intro!: "≡I" "→I" "&I" "cqt:2" dest: "&E")

AOT_theorem Numbers'DistinctZeroes:
‹∃x∃y (◇Numbers'(x,[λz O!z & z ≠⇩E z]) & ◇Numbers'(y,[λz O!z & z ≠⇩E z]) & x ≠ y)›
proof -
AOT_obtain w⇩1 where ‹∃w w⇩1 ≠ w›
using "two-worlds-exist:4" "PossibleWorld.∃E"[rotated] by fast
then AOT_obtain w⇩2 where distinct_worlds: ‹w⇩1 ≠ w⇩2›
using "PossibleWorld.∃E"[rotated] by blast
AOT_obtain x where x_prop:
‹A!x & ∀F (x[F] ≡ w⇩1 ⊨ F ≈⇩E [λz O!z & z ≠⇩E z])›
using "A-objects"[axiom_inst] "∃E"[rotated] by fast
moreover AOT_obtain y where y_prop:
‹A!y & ∀F (y[F] ≡ w⇩2 ⊨ F ≈⇩E [λz O!z & z ≠⇩E z])›
using "A-objects"[axiom_inst] "∃E"[rotated] by fast
moreover {
fix x w
AOT_assume x_prop: ‹A!x & ∀F (x[F] ≡ w ⊨ F ≈⇩E [λz O!z & z ≠⇩E z])›
AOT_have ‹∀F w ⊨ (x[F] ≡ F ≈⇩E [λz O!z & z ≠⇩E z])›
proof(safe intro!: GEN "conj-dist-w:4"[unvarify p q, OF "log-prop-prop:2",
OF "log-prop-prop:2",THEN "≡E"(2)] "≡I" "→I")
fix F
AOT_assume ‹w ⊨ x[F]›
AOT_hence ‹◇x[F]›
using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(2),
OF "PossibleWorld.∃I"] by blast
AOT_hence ‹x[F]›
by (metis "en-eq:3[1]" "intro-elim:3:a")
AOT_thus ‹w ⊨ (F ≈⇩E [λz O!z & z ≠⇩E z])›
using x_prop[THEN "&E"(2), THEN "∀E"(2), THEN "≡E"(1)] by blast
next
fix F
AOT_assume ‹w ⊨ (F ≈⇩E [λz O!z & z ≠⇩E z])›
AOT_hence ‹x[F]›
using x_prop[THEN "&E"(2), THEN "∀E"(2), THEN "≡E"(2)] by blast
AOT_hence ‹□x[F]›
using "pre-en-eq:1[1]"[THEN "→E"] by blast
AOT_thus ‹w ⊨ x[F]›
using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)]
"PossibleWorld.∀E" by fast
qed
AOT_hence ‹w ⊨ ∀F (x[F] ≡ F ≈⇩E [λz O!z & z ≠⇩E z])›
using "conj-dist-w:5"[THEN "≡E"(2)] by fast
moreover {
AOT_have ‹□[λz O!z & z ≠⇩E z]↓›
by (safe intro!: RN "cqt:2")
AOT_hence ‹w ⊨ [λz O!z & z ≠⇩E z]↓›
using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1),
THEN "PossibleWorld.∀E"] by blast
}
moreover {
AOT_have ‹□A!x›
using x_prop[THEN "&E"(1)] by (metis "oa-facts:2" "→E")
AOT_hence ‹w ⊨ A!x›
using "fund:2"[unvarify p, OF "log-prop-prop:2",
THEN "≡E"(1), THEN "PossibleWorld.∀E"] by blast
}
ultimately AOT_have ‹w ⊨ (A!x & [λz O!z & z ≠⇩E z]↓ &
∀F (x[F] ≡ F ≈⇩E [λz O!z & z ≠⇩E z]))›
using "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
OF "log-prop-prop:2", THEN "≡E"(2), OF "&I"] by auto
AOT_hence ‹∃w w ⊨ (A!x & [λz O!z & z ≠⇩E z]↓ &
∀F (x[F] ≡ F ≈⇩E [λz O!z & z ≠⇩E z]))›
using "PossibleWorld.∃I" by auto
AOT_hence ‹◇(A!x & [λz O!z & z ≠⇩E z]↓ & ∀F (x[F] ≡ F ≈⇩E [λz O!z & z ≠⇩E z]))›
using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(2)] by blast
AOT_hence ‹◇Numbers'(x,[λz O!z & z ≠⇩E z])›
by (AOT_subst_def Numbers')
}
ultimately AOT_have ‹◇Numbers'(x,[λz O!z & z ≠⇩E z])›
and ‹◇Numbers'(y,[λz O!z & z ≠⇩E z])›
by auto
moreover AOT_have ‹x ≠ y›
proof (rule "ab-obey:2"[THEN "→E"])
AOT_have ‹□¬∃u [λz O!z & z ≠⇩E z]u›
proof (safe intro!: RN "raa-cor:2")
AOT_modally_strict {
AOT_assume ‹∃u [λz O!z & z ≠⇩E z]u›
then AOT_obtain u where ‹[λz O!z & z ≠⇩E z]u›
using "Ordinary.∃E"[rotated] by blast
AOT_hence ‹O!u & u ≠⇩E u›
by (rule "β→C")
AOT_hence ‹¬(u =⇩E u)›
by (metis "con-dis-taut:2" "intro-elim:3:d" "modus-tollens:1"
"raa-cor:3" "thm-neg=E")
AOT_hence ‹u =⇩E u & ¬u =⇩E u›
by (metis "modus-tollens:1" "ord=Eequiv:1" "raa-cor:3" Ordinary.ψ)
AOT_thus ‹p & ¬p› for p
by (metis "raa-cor:1")
}
qed
AOT_hence nec_not_ex: ‹∀w w ⊨ ¬∃u [λz O!z & z ≠⇩E z]u›
using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
AOT_have ‹□([λy p]x ≡ p)› for x p
by (safe intro!: RN "beta-C-meta"[THEN "→E"] "cqt:2")
AOT_hence ‹∀w w ⊨ ([λy p]x ≡ p)› for x p
using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
AOT_hence world_prop_beta: ‹∀w (w ⊨ [λy p]x ≡ w ⊨ p)› for x p
using "conj-dist-w:4"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)]
"PossibleWorld.∀E" "PossibleWorld.∀I" by meson

AOT_have ‹∃p (w⇩1 ⊨ p & ¬w⇩2 ⊨ p)›
proof(rule "raa-cor:1")
AOT_assume 0: ‹¬∃p (w⇩1 ⊨ p & ¬w⇩2 ⊨ p)›
AOT_have 1: ‹w⇩1 ⊨ p → w⇩2 ⊨ p› for p
proof(safe intro!: GEN "→I")
AOT_assume ‹w⇩1 ⊨ p›
AOT_thus ‹w⇩2 ⊨ p›
using 0 "con-dis-i-e:1" "∃I"(2) "raa-cor:4" by fast
qed
moreover AOT_have ‹w⇩2 ⊨ p → w⇩1 ⊨ p› for p
proof(safe intro!: GEN "→I")
AOT_assume ‹w⇩2 ⊨ p›
AOT_hence ‹¬w⇩2 ⊨ ¬p›
using "coherent:2" "intro-elim:3:a" by blast
AOT_hence ‹¬w⇩1 ⊨ ¬p›
using 1["∀I" p, THEN "∀E"(1), OF "log-prop-prop:2"]
by (metis "modus-tollens:1")
AOT_thus ‹w⇩1 ⊨ p›
using "coherent:1" "intro-elim:3:b" "reductio-aa:1" by blast
qed
ultimately AOT_have ‹w⇩1 ⊨ p ≡ w⇩2 ⊨ p› for p
by (metis "intro-elim:2")
AOT_hence ‹w⇩1 = w⇩2›
using "sit-identity"[unconstrain s, THEN "→E",
OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)],
unconstrain s', THEN "→E",
OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)],
THEN "≡E"(2)] GEN by fast
AOT_thus ‹w⇩1 = w⇩2 & ¬w⇩1 = w⇩2›
using  "=-infix" "≡⇩d⇩fE" "con-dis-i-e:1" distinct_worlds by blast
qed
then AOT_obtain p where 0: ‹w⇩1 ⊨ p & ¬w⇩2 ⊨ p›
using "∃E"[rotated] by blast
AOT_have ‹y[λy p]›
proof (safe intro!: y_prop[THEN "&E"(2), THEN "∀E"(1), THEN "≡E"(2)] "cqt:2")
AOT_show ‹w⇩2 ⊨ [λy p] ≈⇩E [λz O!z & z ≠⇩E z]›
proof (safe intro!:  "cqt:2" "empty-approx:1"[unvarify F H, THEN RN,
THEN "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)],
THEN "PossibleWorld.∀E",
THEN "conj-dist-w:2"[unvarify p q, OF "log-prop-prop:2",
OF "log-prop-prop:2", THEN "≡E"(1)],
THEN "→E"]
"conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
OF "log-prop-prop:2", THEN "≡E"(2)] "&I")
AOT_have ‹¬w⇩2 ⊨ ∃u [λy p]u›
proof (rule "raa-cor:2")
AOT_assume ‹w⇩2 ⊨ ∃u [λy p]u›
AOT_hence ‹∃x w⇩2 ⊨ (O!x & [λy p]x)›
by (metis "conj-dist-w:6" "intro-elim:3:a")
then AOT_obtain x where ‹w⇩2 ⊨ (O!x & [λy p]x)›
using "∃E"[rotated] by blast
AOT_hence ‹w⇩2 ⊨ [λy p]x›
using "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
OF "log-prop-prop:2", THEN "≡E"(1), THEN "&E"(2)] by blast
AOT_hence ‹w⇩2 ⊨ p›
using world_prop_beta[THEN "PossibleWorld.∀E", THEN "≡E"(1)] by blast
AOT_thus ‹w⇩2 ⊨ p & ¬w⇩2 ⊨ p›
using 0[THEN "&E"(2)] "&I" by blast
qed
AOT_thus ‹w⇩2 ⊨ ¬∃u [λy p]u›
by (safe intro!: "coherent:1"[unvarify p, OF "log-prop-prop:2",
THEN "≡E"(2)])
next
AOT_show ‹w⇩2 ⊨ ¬∃v [λz O!z & z ≠⇩E z]v›
using nec_not_ex[THEN "PossibleWorld.∀E"] by blast
qed
qed
moreover AOT_have ‹¬x[λy p]›
proof(rule "raa-cor:2")
AOT_assume ‹x[λy p]›
AOT_hence "w⇩1 ⊨ [λy p] ≈⇩E [λz O!z & z ≠⇩E z]"
using x_prop[THEN "&E"(2), THEN "∀E"(1), THEN "≡E"(1)]
"prop-prop2:2" by blast
AOT_hence "¬w⇩1 ⊨ ¬[λy p] ≈⇩E [λz O!z & z ≠⇩E z]"
using "coherent:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
moreover AOT_have "w⇩1 ⊨ ¬([λy p] ≈⇩E [λz O!z & z ≠⇩E z])"
proof (safe intro!: "cqt:2" "empty-approx:2"[unvarify F H, THEN RN,
THEN "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)],
THEN "PossibleWorld.∀E",
THEN "conj-dist-w:2"[unvarify p q, OF "log-prop-prop:2",
OF "log-prop-prop:2", THEN "≡E"(1)], THEN "→E"]
"conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
OF "log-prop-prop:2", THEN "≡E"(2)] "&I")
fix u
AOT_have ‹w⇩1 ⊨ O!u›
using Ordinary.ψ[THEN RN,
THEN "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)],
THEN "PossibleWorld.∀E"] by simp
moreover AOT_have ‹w⇩1 ⊨ [λy p]u›
by (safe intro!: world_prop_beta[THEN "PossibleWorld.∀E", THEN "≡E"(2)]
0[THEN "&E"(1)])
ultimately AOT_have ‹w⇩1 ⊨ (O!u & [λy p]u)›
using "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
OF "log-prop-prop:2", THEN "≡E"(2),
OF "&I"] by blast
AOT_hence ‹∃x w⇩1 ⊨ (O!x & [λy p]x)›
by (rule "∃I")
AOT_thus ‹w⇩1 ⊨ ∃u [λy p]u›
by (metis "conj-dist-w:6" "intro-elim:3:b")
next
AOT_show ‹w⇩1 ⊨ ¬∃v [λz O!z & z ≠⇩E z]v›
using "PossibleWorld.∀E" nec_not_ex by fastforce
qed
ultimately AOT_show ‹p & ¬p› for p
using "raa-cor:3" by blast
qed
ultimately AOT_have ‹y[λy p] & ¬x[λy p]›
using "&I" by blast
AOT_hence ‹∃F (y[F] & ¬x[F])›
by (metis "existential:1" "prop-prop2:2")
AOT_thus ‹∃F (x[F] & ¬y[F]) ∨ ∃F (y[F] & ¬x[F])›
by (rule "∨I")
qed
ultimately AOT_have ‹◇Numbers'(x,[λz O!z & z ≠⇩E z]) &
◇Numbers'(y,[λz O!z & z ≠⇩E z]) & x ≠ y›
using "&I" by blast
AOT_thus ‹∃x∃y (◇Numbers'(x,[λz O!z & z ≠⇩E z]) &
◇Numbers'(y,[λz O!z & z ≠⇩E z]) & x ≠ y)›
using "∃I"(2)[where β=x] "∃I"(2)[where β=y] by auto
qed

AOT_theorem restricted_identity:
‹x =⇩ℛ y ≡ (InDomainOf(x,ℛ) & InDomainOf(y,ℛ) & x = y)›
by (auto intro!: "≡I" "→I" "&I"
dest: "id-R-thm:2"[THEN "→E"] "&E"
"id-R-thm:3"[THEN "→E"]
"id-R-thm:4"[THEN "→E", OF "∨I"(1), THEN "≡E"(2)])

AOT_theorem induction': ‹∀F ([F]0 & ∀n([F]n → [F]n❙') → ∀n [F]n)›
proof(rule GEN; rule "→I")
fix F n
AOT_assume A: ‹[F]0 & ∀n([F]n → [F]n❙')›
AOT_have ‹∀n∀m([ℙ]nm → ([F]n → [F]m))›
proof(safe intro!: "Number.GEN" "→I")
fix n m
AOT_assume ‹[ℙ]nm›
moreover AOT_have ‹[ℙ]n n❙'›
using "suc-thm".
ultimately AOT_have m_eq_suc_n: ‹m = n❙'›
using "pred-func:1"[unvarify z, OF "def-suc[den2]", THEN "→E", OF "&I"]
by blast
AOT_assume ‹[F]n›
AOT_hence ‹[F]n❙'›
using A[THEN "&E"(2), THEN "Number.∀E", THEN "→E"] by blast
AOT_thus ‹[F]m›
using m_eq_suc_n[symmetric] "rule=E" by fast
qed
AOT_thus ‹∀n[F]n›
using induction[THEN "∀E"(2), THEN "→E", OF "&I", OF A[THEN "&E"(1)]]
by simp
qed

AOT_define ExtensionOf :: ‹τ ⇒ Π ⇒ φ› (‹ExtensionOf'(_,_')›)
"exten-property:1": ‹ExtensionOf(x,[G]) ≡⇩d⇩f A!x & G↓ & ∀F(x[F] ≡ ∀z([F]z ≡ [G]z))›

AOT_define OrdinaryExtensionOf :: ‹τ ⇒ Π ⇒ φ› (‹OrdinaryExtensionOf'(_,_')›)
‹OrdinaryExtensionOf(x,[G]) ≡⇩d⇩f A!x & G↓ & ∀F(x[F] ≡ ∀z(O!z → ([F]z ≡ [G]z)))›

AOT_theorem BeingOrdinaryExtensionOfDenotes:
‹[λx OrdinaryExtensionOf(x,[G])]↓›
proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
AOT_show ‹[λx A!x & G↓ & [λx ∀F(x[F] ≡ ∀z(O!z → ([F]z ≡ [G]z)))]x]↓›
by "cqt:2"
next
AOT_show ‹□∀x (A!x & G↓ & [λx ∀F (x[F] ≡ ∀z (O!z → ([F]z ≡ [G]z)))]x ≡
OrdinaryExtensionOf(x,[G]))›
proof(safe intro!: RN GEN)
AOT_modally_strict {
fix x
AOT_modally_strict {
AOT_have ‹[λx ∀F (x[F] ≡ ∀z (O!z → ([F]z ≡ [G]z)))]↓›
proof (safe intro!: "Comprehension_3"[THEN "→E"] RN GEN
"→I" "≡I" Ordinary.GEN)
AOT_modally_strict {
fix F H u
AOT_assume ‹□H ≡⇩E F›
AOT_hence ‹∀u([H]u ≡ [F]u)›
using eqE[THEN "≡⇩d⇩fE", THEN "&E"(2)] "qml:2"[axiom_inst, THEN "→E"]
by blast
AOT_hence 0: ‹[H]u ≡ [F]u› using "Ordinary.∀E" by fast
{
AOT_assume ‹∀u([F]u ≡ [G]u)›
AOT_hence 1: ‹[F]u ≡ [G]u› using "Ordinary.∀E" by fast
AOT_show ‹[G]u› if ‹[H]u› using 0 1 "≡E"(1) that by blast
AOT_show ‹[H]u› if ‹[G]u› using 0 1 "≡E"(2) that by blast
}
{
AOT_assume ‹∀u([H]u ≡ [G]u)›
AOT_hence 1: ‹[H]u ≡ [G]u› using "Ordinary.∀E" by fast
AOT_show ‹[G]u› if ‹[F]u› using 0 1 "≡E"(1,2) that by blast
AOT_show ‹[F]u› if ‹[G]u› using 0 1 "≡E"(1,2) that by blast
}
}
qed
}
AOT_thus ‹(A!x & G↓ & [λx ∀F (x[F] ≡ ∀z (O!z → ([F]z ≡ [G]z)))]x) ≡
OrdinaryExtensionOf(x,[G])›
apply (AOT_subst_def OrdinaryExtensionOf)
apply (AOT_subst ‹[λx ∀F (x[F] ≡ ∀z (O!z → ([F]z ≡ [G]z)))]x›
‹∀F (x[F] ≡ ∀z (O!z → ([F]z ≡ [G]z)))›)
by (auto intro!: "beta-C-meta"[THEN "→E"] simp: "oth-class-taut:3:a")
}
qed
qed

text‹Fragments of PLM's theory of Concepts.›

AOT_define FimpG :: ‹Π ⇒ Π ⇒ φ› (infixl ‹⇒› 50)
"F-imp-G": ‹[G] ⇒ [F] ≡⇩d⇩f F↓ & G↓ & □∀x ([G]x → [F]x)›

AOT_define concept :: ‹Π› (‹C!›)
concepts: ‹C! =⇩d⇩f A!›

AOT_register_rigid_restricted_type
Concept: ‹C!κ›
proof
AOT_modally_strict {
AOT_have ‹∃x A!x›
using "o-objects-exist:2" "qml:2"[axiom_inst] "→E" by blast
AOT_thus ‹∃x C!x›
using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"] "rule=E" id_sym
by fast
}
next
AOT_modally_strict {
AOT_show ‹C!κ → κ↓› for κ
using "cqt:5:a"[axiom_inst, THEN "→E", THEN "&E"(2)] "→I"
by blast
}
next
AOT_modally_strict {
AOT_have ‹∀x(A!x → □A!x)›
AOT_thus ‹∀x(C!x → □C!x)›
using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"] "rule=E" id_sym
by fast
}
qed

AOT_register_variable_names
Concept: c d e

AOT_theorem "concept-comp:1": ‹∃x(C!x & ∀F(x[F] ≡ φ{F}))›
using concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2", symmetric]
"A-objects"[axiom_inst]
"rule=E" by fast

AOT_theorem "concept-comp:2": ‹∃!x(C!x & ∀F(x[F] ≡ φ{F}))›
using concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2", symmetric]
"A-objects!"
"rule=E" by fast

AOT_theorem "concept-comp:3": ‹❙ιx(C!x & ∀F(x[F] ≡ φ{F}))↓›
using "concept-comp:2" "A-Exists:2"[THEN "≡E"(2)] "RA[2]" by blast

AOT_theorem "concept-comp:4":
‹❙ιx(C!x & ∀F(x[F] ≡ φ{F})) = ❙ιx(A!x & ∀F(x[F] ≡ φ{F}))›
using "=I"(1)[OF "concept-comp:3"]
"rule=E"[rotated]
concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2"]
by fast

AOT_define conceptInclusion :: ‹τ ⇒ τ ⇒ φ› (infixl ‹≼› 100)
"con:1": ‹c ≼ d ≡⇩d⇩f ∀F(c[F] → d[F])›

AOT_define conceptOf :: ‹τ ⇒ τ ⇒ φ› (‹ConceptOf'(_,_')›)
"concept-of-G": ‹ConceptOf(c,G) ≡⇩d⇩f G↓ & ∀F (c[F] ≡ [G] ⇒ [F])›

AOT_theorem ConceptOfOrdinaryProperty: ‹([H] ⇒ O!) → [λx ConceptOf(x,H)]↓›
proof(rule "→I")
AOT_assume ‹[H] ⇒ O!›
AOT_hence ‹□∀x([H]x → O!x)›
using "F-imp-G"[THEN "≡⇩d⇩fE"] "&E" by blast
AOT_hence ‹□□∀x([H]x → O!x)›
using "S5Basic:6"[THEN "≡E"(1)] by blast
moreover AOT_have ‹□□∀x([H]x → O!x) →
□∀F∀G(□(G ≡⇩E F) → ([H] ⇒ [F] ≡ [H] ⇒ [G]))›
proof(rule RM; safe intro!: "→I" GEN "≡I")
AOT_modally_strict {
fix F G
AOT_assume 0: ‹□∀x([H]x → O!x)›
AOT_assume ‹□G ≡⇩E F›
AOT_hence 1: ‹□∀u([G]u ≡ [F]u)›
by (AOT_subst_thm eqE[THEN "≡Df", THEN "≡S"(1), OF "&I",
OF "cqt:2[const_var]"[axiom_inst],
OF "cqt:2[const_var]"[axiom_inst], symmetric])
{
AOT_assume ‹[H] ⇒ [F]›
AOT_hence ‹□∀x([H]x → [F]x)›
using "F-imp-G"[THEN "≡⇩d⇩fE"] "&E" by blast
moreover AOT_modally_strict {
AOT_assume ‹∀x([H]x → O!x)›
moreover AOT_assume ‹∀u([G]u ≡ [F]u)›
moreover AOT_assume ‹∀x([H]x → [F]x)›
ultimately AOT_have ‹[H]x → [G]x› for x
by (auto intro!: "→I" dest!: "∀E"(2) dest: "→E" "≡E")
AOT_hence ‹∀x([H]x → [G]x)›
by (rule GEN)
}
ultimately AOT_have ‹□∀x([H]x → [G]x)›
using "RN[prem]"[where
Γ="{«∀x([H]x → O!x)», «∀u([G]u ≡ [F]u)», «∀x([H]x → [F]x)»}"]
using 0 1 by fast
AOT_thus ‹[H] ⇒ [G]›
by (AOT_subst_def "F-imp-G")
(safe intro!: "cqt:2" "&I")
}
{
AOT_assume ‹[H] ⇒ [G]›
AOT_hence ‹□∀x([H]x → [G]x)›
using "F-imp-G"[THEN "≡⇩d⇩fE"] "&E" by blast
moreover AOT_modally_strict {
AOT_assume ‹∀x([H]x → O!x)›
moreover AOT_assume ‹∀u([G]u ≡ [F]u)›
moreover AOT_assume ‹∀x([H]x → [G]x)›
ultimately AOT_have ‹[H]x → [F]x› for x
by (auto intro!: "→I" dest!: "∀E"(2) dest: "→E" "≡E")
AOT_hence ‹∀x([H]x → [F]x)›
by (rule GEN)
}
ultimately AOT_have ‹□∀x([H]x → [F]x)›
using "RN[prem]"[where
Γ="{«∀x([H]x → O!x)», «∀u([G]u ≡ [F]u)», «∀x([H]x → [G]x)»}"]
using 0 1 by fast
AOT_thus ‹[H] ⇒ [F]›
by (AOT_subst_def "F-imp-G")
(safe intro!: "cqt:2" "&I")
}
}
qed
ultimately AOT_have ‹□∀F∀G(□(G ≡⇩E F) → ([H] ⇒ [F] ≡ [H] ⇒ [G]))›
using "→E" by blast
AOT_hence 0: ‹[λx ∀F(x[F] ≡ ([H] ⇒ [F]))]↓›
using Comprehension_3[THEN "→E"] by blast
AOT_show ‹[λx ConceptOf(x,H)]↓›
proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
AOT_show ‹[λx C!x & [λx ∀F(x[F] ≡ ([H] ⇒ [F]))]x]↓› by "cqt:2"
next
AOT_show ‹□∀x (C!x & [λx ∀F (x[F] ≡ [H] ⇒ [F])]x ≡ ConceptOf(x,H))›
proof (rule "RN[prem]"[where Γ=‹{«[λx ∀F(x[F] ≡ ([H] ⇒ [F]))]↓»}›, simplified])
AOT_modally_strict {
AOT_assume 0: ‹[λx ∀F (x[F] ≡ [H] ⇒ [F])]↓›
AOT_show ‹∀x (C!x & [λx ∀F (x[F] ≡ [H] ⇒ [F])]x ≡ ConceptOf(x,H))›
proof(safe intro!: GEN "≡I" "→I" "&I")
fix x
AOT_assume ‹C!x & [λx ∀F (x[F] ≡ [H] ⇒ [F])]x›
AOT_thus ‹ConceptOf(x,H)›
by (AOT_subst_def "concept-of-G")
(auto intro!: "&I" "cqt:2" dest: "&E" "β→C")
next
fix x
AOT_assume ‹ConceptOf(x,H)›
AOT_hence ‹C!x & (H↓ & ∀F(x[F] ≡ [H] ⇒ [F]))›
by (AOT_subst_def (reverse) "concept-of-G")
AOT_thus ‹C!x› and ‹[λx ∀F(x[F] ≡ [H] ⇒ [F])]x›
by (auto intro!: "β←C" 0 "cqt:2" dest: "&E")
qed
}
next
AOT_show ‹□[λx ∀F(x[F] ≡ ([H] ⇒ [F]))]↓›
using "exist-nec"[THEN "→E"] 0 by blast
qed
qed
qed

AOT_theorem "con-exists:1": ‹∃c ConceptOf(c,G)›
proof -
AOT_obtain c where ‹∀F (c[F] ≡ [G] ⇒ [F])›
using "concept-comp:1" "Concept.∃E"[rotated] by meson
AOT_hence ‹ConceptOf(c,G)›
by (auto intro!: "concept-of-G"[THEN "≡⇩d⇩fI"] "&I" "cqt:2" Concept.ψ)
thus ?thesis by (rule "Concept.∃I")
qed

AOT_theorem "con-exists:2": ‹∃!c ConceptOf(c,G)›
proof -
AOT_have ‹∃!c ∀F (c[F] ≡ [G] ⇒ [F])›
using "concept-comp:2" by simp
moreover {
AOT_modally_strict {
fix x
AOT_assume ‹∀F (x[F] ≡ [G] ⇒ [F])›
moreover AOT_have ‹[G] ⇒ [G]›
by (safe intro!: "F-imp-G"[THEN "≡⇩d⇩fI"] "&I" "cqt:2" RN GEN "→I")
ultimately AOT_have ‹x[G]›
using "∀E"(2) "≡E" by blast
AOT_hence ‹A!x›
using "encoders-are-abstract"[THEN "→E", OF "∃I"(2)] by simp
AOT_hence ‹C!x›
using concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2", symmetric]
"rule=E"[rotated]
by fast
}
}
ultimately show ?thesis
by (AOT_subst ‹ConceptOf(c,G)› ‹∀F (c[F] ≡ [G] ⇒ [F])› for: c;
AOT_subst_def "concept-of-G")
(auto intro!: "≡I" "→I" "&I" "cqt:2" Concept.ψ dest: "&E")
qed

AOT_theorem "con-exists:3": ‹❙ιc ConceptOf(c,G)↓›
by (safe intro!: "A-Exists:2"[THEN "≡E"(2)] "con-exists:2"[THEN "RA[2]"])

AOT_define theConceptOfG :: ‹τ ⇒ κ⇩s› (‹❙c⇩_›)
"concept-G": ‹❙c⇩G =⇩d⇩f ❙ιc ConceptOf(c, G)›

AOT_theorem "concept-G[den]": ‹❙c⇩G↓›
by (auto intro!: "rule-id-df:1"[OF "concept-G"]
"t=t-proper:1"[THEN "→E"]
"con-exists:3")

AOT_theorem "concept-G[concept]": ‹C!❙c⇩G›
proof -
AOT_have ‹❙𝒜(C!❙c⇩G & ConceptOf(❙c⇩G, G))›
by (auto intro!: "actual-desc:2"[unvarify x, THEN "→E"]
"rule-id-df:1"[OF "concept-G"]
"concept-G[den]"
"con-exists:3")
AOT_hence ‹❙𝒜C!❙c⇩G›
by (metis "Act-Basic:2" "con-dis-i-e:2:a" "intro-elim:3:a")
AOT_hence ‹❙𝒜A!❙c⇩G›
using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"]
"rule=E" by fast
AOT_hence ‹A!❙c⇩G›
using "oa-facts:8"[unvarify x, THEN "≡E"(2)] "concept-G[den]" by blast
thus ?thesis
using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2", symmetric]
"rule=E" by fast
qed

AOT_theorem "conG-strict": ‹❙c⇩G = ❙ιc ∀F(c[F] ≡ [G] ⇒ [F])›
proof (rule "id-eq:3"[unvarify α β γ, THEN "→E"])
AOT_have ‹□∀x (C!x & ConceptOf(x,G) ≡ C!x & ∀F (x[F] ≡ [G] ⇒ [F]))›
by (auto intro!: "concept-of-G"[THEN "≡⇩d⇩fI"] RN GEN "≡I" "→I" "&I" "cqt:2"
dest: "&E";
auto dest: "∀E"(2) "≡E"(1,2) dest!: "&E"(2) "concept-of-G"[THEN "≡⇩d⇩fE"])
AOT_thus ‹❙c⇩G = ❙ιc ConceptOf(c, G) & ❙ιc ConceptOf(c, G) = ❙ιc ∀F(c[F] ≡ [G] ⇒ [F])›
by (auto intro!: "&I" "rule-id-df:1"[OF "concept-G"] "con-exists:3"
"equiv-desc-eq:3"[THEN "→E"])
qed(auto simp: "concept-G[den]" "con-exists:3" "concept-comp:3")

AOT_theorem "conG-lemma:1": ‹∀F(❙c⇩G[F] ≡ [G] ⇒ [F])›
proof(safe intro!: GEN "≡I" "→I")
fix F
AOT_have ‹❙𝒜∀F(❙c⇩G[F] ≡ [G] ⇒ [F])›
using "actual-desc:4"[THEN "→E", OF "concept-comp:3",
THEN "Act-Basic:2"[THEN "≡E"(1)],
THEN "&E"(2)]
"conG-strict"[symmetric] "rule=E" by fast
AOT_hence ‹❙𝒜(❙c⇩G[F] ≡ [G] ⇒ [F])›
using "logic-actual-nec:3"[axiom_inst, THEN "≡E"(1)] "∀E"(2)
by blast
AOT_hence 0: ‹❙𝒜❙c⇩G[F] ≡ ❙𝒜[G] ⇒ [F]›
using "Act-Basic:5"[THEN "≡E"(1)] by blast
{
AOT_assume ‹❙c⇩G[F]›
AOT_hence ‹❙𝒜❙c⇩G[F]›
by(safe intro!: "en-eq:10[1]"[unvarify x⇩1, THEN "≡E"(2)]
"concept-G[den]")
AOT_hence ‹❙𝒜[G] ⇒ [F]›
using 0[THEN "≡E"(1)] by blast
AOT_hence ‹❙𝒜(F↓ & G↓ & □∀x([G]x → [F]x))›
by (AOT_subst_def (reverse) "F-imp-G")
AOT_hence ‹❙𝒜□∀x([G]x → [F]x)›
using "Act-Basic:2"[THEN "≡E"(1)] "&E" by blast
AOT_hence ‹□∀x([G]x → [F]x)›
using "qml-act:2"[axiom_inst, THEN "≡E"(2)] by simp
AOT_thus ‹[G] ⇒ [F]›
by (AOT_subst_def "F-imp-G"; auto intro!: "&I" "cqt:2")
}
{
AOT_assume ‹[G] ⇒ [F]›
AOT_hence ‹□∀x([G]x → [F]x)›
by (safe dest!: "F-imp-G"[THEN "≡⇩d⇩fE"] "&E"(2))
AOT_hence ‹❙𝒜□∀x([G]x → [F]x)›
using "qml-act:2"[axiom_inst, THEN "≡E"(1)] by simp
AOT_hence ‹❙𝒜(F↓ & G↓ & □∀x([G]x → [F]x))›
by (auto intro!: "Act-Basic:2"[THEN "≡E"(2)] "&I" "cqt:2"
intro: "RA[2]")
AOT_hence ‹❙𝒜([G] ⇒ [F])›
by (AOT_subst_def "F-imp-G")
AOT_hence ‹❙𝒜❙c⇩G[F]›
using 0[THEN "≡E"(2)] by blast
AOT_thus ‹❙c⇩G[F]›
by(safe intro!: "en-eq:10[1]"[unvarify x⇩1, THEN "≡E"(1)]
"concept-G[den]")
}
qed

AOT_theorem conH_enc_ord:
‹([H] ⇒ O!) → □∀F ∀G (□G ≡⇩E F → (❙c⇩H[F] ≡ ❙c⇩H[G]))›
proof(rule "→I")
AOT_assume 0: ‹[H] ⇒ O!›
AOT_have 0: ‹□([H] ⇒ O!)›
apply (AOT_subst_def "F-imp-G")
using 0[THEN "≡⇩d⇩fE"[OF "F-imp-G"]]
by (auto intro!: "KBasic:3"[THEN "≡E"(2)] "&I" "exist-nec"[THEN "→E"]
dest: "&E" 4[THEN "→E"])
moreover AOT_have ‹□([H] ⇒ O!) → □∀F ∀G (□G ≡⇩E F → (❙c⇩H[F] ≡ ❙c⇩H[G]))›
proof(rule RM; safe intro!: "→I" GEN)
AOT_modally_strict {
fix F G
AOT_assume ‹[H] ⇒ O!›
AOT_hence 0: ‹□∀x ([H]x → O!x)›
by (safe dest!: "F-imp-G"[THEN "≡⇩d⇩fE"] "&E"(2))
AOT_assume 1: ‹□G ≡⇩E F›
AOT_assume ‹❙c⇩H[F]›
AOT_hence ‹[H] ⇒ [F]›
using "conG-lemma:1"[THEN "∀E"(2), THEN "≡E"(1)] by simp
AOT_hence 2: ‹□∀x ([H]x → [F]x)›
by (safe dest!: "F-imp-G"[THEN "≡⇩d⇩fE"] "&E"(2))
AOT_modally_strict {
AOT_assume 0: ‹∀x ([H]x → O!x)›
AOT_assume 1: ‹∀x ([H]x → [F]x)›
AOT_assume 2: ‹G ≡⇩E F›
AOT_have ‹∀x ([H]x → [G]x)›
proof(safe intro!: GEN "→I")
fix x
AOT_assume ‹[H]x›
AOT_hence ‹O!x› and ‹[F]x›
using 0 1 "∀E"(2) "→E" by blast+
AOT_thus ‹[G]x›
using 2[THEN eqE[THEN "≡⇩d⇩fE"], THEN "&E"(2)]
"∀E"(2) "→E" "≡E"(2) calculation by blast
qed
}
AOT_hence ‹□∀x ([H]x → [G]x)›
using "RN[prem]"[where Γ=‹{«∀x ([H]x → O!x)»,
«∀x ([H]x → [F]x)»,
«G ≡⇩E F»}›, simplified] 0 1 2 by fast
AOT_hence ‹[H] ⇒ [G]›
by (safe intro!: "F-imp-G"[THEN "≡⇩d⇩fI"] "&I" "cqt:2")
AOT_hence ‹❙c⇩H[G]›
using "conG-lemma:1"[THEN "∀E"(2), THEN "≡E"(2)] by simp
} note 0 = this
AOT_modally_strict {
fix F G
AOT_assume ‹[H] ⇒ O!›
moreover AOT_assume ‹□G ≡⇩E F›
moreover AOT_have ‹□F ≡⇩E G›
by (AOT_subst ‹F ≡⇩E G› ‹G ≡⇩E F›)
(auto intro!: calculation(2)
eqE[THEN "≡⇩d⇩fI"]
"≡I" "→I" "&I" "cqt:2" Ordinary.GEN
dest!: eqE[THEN "≡⇩d⇩fE"] "&E"(2)
dest: "≡E"(1,2) "Ordinary.∀E")
ultimately AOT_show ‹(❙c⇩H[F] ≡ ❙c⇩H[G])›
using 0 "≡I" "→I" by auto
}
qed
ultimately AOT_show ‹□∀F ∀G (□G ≡⇩E F → (❙c⇩H[F] ≡ ❙c⇩H[G]))›
using "→E" by blast
qed

AOT_theorem concept_inclusion_denotes_1:
‹([H] ⇒ O!) → [λx ❙c⇩H ≼ x]↓›
proof(rule "→I")
AOT_assume 0: ‹[H] ⇒ O!›
AOT_show ‹[λx ❙c⇩H ≼ x]↓›
proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
AOT_show ‹[λx C!x & ∀F(❙c⇩H[F] → x[F])]↓›
by (safe intro!: conjunction_denotes[THEN "→E", OF "&I"]
Comprehension_2'[THEN "→E"]
conH_enc_ord[THEN "→E", OF 0]) "cqt:2"
next
AOT_show ‹□∀x (C!x & ∀F (❙c⇩H[F] → x[F]) ≡ ❙c⇩H ≼ x)›
by (safe intro!: RN GEN; AOT_subst_def "con:1")
(auto intro!: "≡I" "→I" "&I" "concept-G[concept]" dest: "&E")
qed
qed

AOT_theorem concept_inclusion_denotes_2:
‹([H] ⇒ O!) → [λx x ≼ ❙c⇩H]↓›
proof(rule "→I")
AOT_assume 0: ‹[H] ⇒ O!›
AOT_show ‹[λx x ≼ ❙c⇩H]↓›
proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
AOT_show ‹[λx C!x & ∀F(x[F] → ❙c⇩H[F])]↓›
by (safe intro!: conjunction_denotes[THEN "→E", OF "&I"]
Comprehension_1'[THEN "→E"]
conH_enc_ord[THEN "→E", OF 0]) "cqt:2"
next
AOT_show ‹□∀x (C!x & ∀F (x[F] → ❙c⇩H[F]) ≡ x ≼ ❙c⇩H)›
by (safe intro!: RN GEN; AOT_subst_def "con:1")
(auto intro!: "≡I" "→I" "&I" "concept-G[concept]" dest: "&E")
qed
qed

AOT_define ThickForm :: ‹τ ⇒ τ ⇒ φ› (‹FormOf'(_,_')›)
"tform-of": ‹FormOf(x,G) ≡⇩d⇩f A!x & G↓ & ∀F(x[F] ≡ [G] ⇒ [F])›

AOT_theorem FormOfOrdinaryProperty: ‹([H] ⇒ O!) → [λx FormOf(x,H)]↓›
proof(rule "→I")
AOT_assume 0: ‹[H] ⇒ [O!]›
AOT_show ‹[λx FormOf(x,H)]↓›
proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
AOT_show ‹[λx ConceptOf(x,H)]↓›
using 0 ConceptOfOrdinaryProperty[THEN "→E"] by blast
AOT_show ‹□∀x (ConceptOf(x,H) ≡ FormOf(x,H))›
proof(safe intro!: RN GEN)
AOT_modally_strict {
fix x
AOT_modally_strict {
AOT_have ‹A!x ≡ A!x›
AOT_hence ‹C!x ≡ A!x›
using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"]
"rule=E" id_sym by fast
}
AOT_thus ‹ConceptOf(x,H) ≡ FormOf(x,H)›
by (AOT_subst_def "tform-of";
AOT_subst_def "concept-of-G";
AOT_subst ‹C!x› ‹A!x›)
(auto intro!: "≡I" "→I" "&I" dest: "&E")
}
qed
qed
qed

AOT_theorem equal_E_rigid_one_to_one: ‹Rigid⇩1⇩-⇩1((=⇩E))›
proof (safe intro!: "df-1-1:2"[THEN "≡⇩d⇩fI"] "&I" "df-1-1:1"[THEN "≡⇩d⇩fI"]
GEN "→I" "df-rigid-rel:1"[THEN "≡⇩d⇩fI"] "=E[denotes]")
fix x y z
AOT_assume ‹x =⇩E z & y =⇩E z›
AOT_thus ‹x = y›
by (metis "rule=E" "&E"(1) "Conjunction Simplification"(2)
"=E-simple:2" id_sym "→E")
next
AOT_have ‹∀x∀y □(x =⇩E y → □x =⇩E y)›
proof(rule GEN; rule GEN)
AOT_show ‹□(x =⇩E y → □x =⇩E y)› for x y
by (meson RN "deduction-theorem" "id-nec3:1" "≡E"(1))
qed
AOT_hence ‹∀x⇩1...∀x⇩n □([(=⇩E)]x⇩1...x⇩n → □[(=⇩E)]x⇩1...x⇩n)›
by (rule tuple_forall[THEN "≡⇩d⇩fI"])
AOT_thus ‹□∀x⇩1...∀x⇩n ([(=⇩E)]x⇩1...x⇩n → □[(=⇩E)]x⇩1...x⇩n)›
using BF[THEN "→E"] by fast
qed

AOT_theorem equal_E_domain: ‹InDomainOf(x,(=⇩E)) ≡ O!x›
proof(safe intro!: "≡I" "→I")
AOT_assume ‹InDomainOf(x,(=⇩E))›
AOT_hence ‹∃y x =⇩E y›
by (metis "≡⇩d⇩fE" "df-1-1:5")
then AOT_obtain y where ‹x =⇩E y›
using "∃E"[rotated] by blast
AOT_thus ‹O!x›
using "=E-simple:1"[THEN "≡E"(1)] "&E" by blast
next
AOT_assume ‹O!x›
AOT_hence ‹x =⇩E x›
by (metis "ord=Eequiv:1"[THEN "→E"])
AOT_hence ‹∃y x =⇩E y›
using "∃I"(2) by fast
AOT_thus ‹InDomainOf(x,(=⇩E))›
by (metis "≡⇩d⇩fI" "df-1-1:5")
qed

AOT_theorem shared_urelement_projection_identity:
assumes ‹∀y [λx (y[λz [R]zx])]↓›
shows ‹∀F([F]a ≡ [F]b) → [λz [R]za] = [λz [R]zb]›
proof(rule "→I")
AOT_assume 0: ‹∀F([F]a ≡ [F]b)›
{
fix z
AOT_have ‹[λx (z[λz [R]zx])]↓›
using assms[THEN "∀E"(2)].
AOT_hence 1: ‹∀x ∀y (∀F ([F]x ≡ [F]y) → □(z[λz [R]zx] ≡ z[λz [R]zy]))›
using "kirchner-thm-cor:1"[THEN "→E"]
by blast
AOT_have ‹□(z[λz [R]za] ≡ z[λz [R]zb])›
using 1[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", OF 0] by blast
}
AOT_hence ‹∀z □(z[λz [R]za] ≡ z[λz [R]zb])›
by (rule GEN)
AOT_hence ‹□∀z(z[λz [R]za] ≡ z[λz [R]zb])›
by (rule BF[THEN "→E"])
AOT_thus ‹[λz [R]za] = [λz [R]zb]›
by (AOT_subst_def "identity:2")
(auto intro!: "&I" "cqt:2")
qed

AOT_theorem shared_urelement_exemplification_identity:
assumes ‹∀y [λx (y[λz [G]x])]↓›
shows ‹∀F([F]a ≡ [F]b) → ([G]a) = ([G]b)›
proof(rule "→I")
AOT_assume 0: ‹∀F([F]a ≡ [F]b)›
{
fix z
AOT_have ‹[λx (z[λz [G]x])]↓›
using assms[THEN "∀E"(2)].
AOT_hence 1: ‹∀x ∀y (∀F ([F]x ≡ [F]y) → □(z[λz [G]x] ≡ z[λz [G]y]))›
using "kirchner-thm-cor:1"[THEN "→E"]
by blast
AOT_have ‹□(z[λz [G]a] ≡ z[λz [G]b])›
using 1[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", OF 0] by blast
}
AOT_hence ‹∀z □(z[λz [G]a] ≡ z[λz [G]b])›
by (rule GEN)
AOT_hence ‹□∀z(z[λz [G]a] ≡ z[λz [G]b])›
by (rule BF[THEN "→E"])
AOT_hence ‹[λz [G]a] = [λz [G]b]›
by (AOT_subst_def "identity:2")
(auto intro!: "&I" "cqt:2")
AOT_thus ‹([G]a) = ([G]b)›
by (safe intro!: "identity:4"[THEN "≡⇩d⇩fI"] "&I" "log-prop-prop:2")
qed

text‹The assumptions of the theorems above are derivable, if the additional
introduction rules for the upcoming extension of @{thm "cqt:2[lambda]"}
are explicitly allowed (while they are currently not part of the
abstraction layer).›