# Theory AOT_NaturalNumbers

(*<*)
theory AOT_NaturalNumbers
imports AOT_PossibleWorlds AOT_ExtendedRelationComprehension
abbrevs one-to-one = 1-1
and onto = onto
begin
(*>*)

section‹Natural Numbers›

AOT_define CorrelatesOneToOne :: τ  τ  τ  φ (‹_ |: _ 1-1 _›)
"1-1-cor": R |: F 1-1 G df R & F & G &
x ([F]x  ∃!y([G]y & [R]xy)) &
y ([G]y  ∃!x([F]x & [R]xy))

AOT_define MapsTo :: τ  τ  τ  φ (‹_ |: _  _›)
"fFG:1": R |: F  G df R & F & G & x ([F]x  ∃!y([G]y & [R]xy))

AOT_define MapsToOneToOne :: τ  τ  τ  φ (‹_ |: _ 1-1 _›)
"fFG:2": R |: F 1-1 G df
R |: F  G & xyz (([F]x & [F]y & [G]z)  ([R]xz & [R]yz  x = y))

AOT_define MapsOnto :: τ  τ  τ  φ (‹_ |: _ onto _›)
"fFG:3": R |: F onto G df R |: F  G & y ([G]y  x([F]x & [R]xy))

AOT_define MapsOneToOneOnto :: τ  τ  τ  φ (‹_ |: _ 1-1onto _›)
"fFG:4": R |: F 1-1onto G df R |: F 1-1 G & R |: F onto G

AOT_theorem "eq-1-1": R |: F 1-1 G  R |: F 1-1onto G
proof(rule "≡I"; rule "→I")
AOT_assume R |: F 1-1 G
AOT_hence A: x ([F]x  ∃!y([G]y & [R]xy))
and B: y ([G]y  ∃!x([F]x & [R]xy))
using "dfE"[OF "1-1-cor"] "&E" by blast+
AOT_have C: R |: F  G
proof (rule "dfI"[OF "fFG:1"]; rule "&I")
AOT_show R & F & G
using [axiom_inst] "&I" by metis
next
AOT_show x ([F]x  ∃!y([G]y & [R]xy)) by (rule A)
qed
AOT_show R |: F 1-1onto G
proof (rule "dfI"[OF "fFG:4"]; rule "&I")
AOT_show R |: F 1-1 G
proof (rule "dfI"[OF "fFG:2"]; rule "&I")
AOT_show R |: F  G using C.
next
AOT_show xyz ([F]x & [F]y & [G]z  ([R]xz & [R]yz  x = y))
proof(rule GEN; rule GEN; rule GEN; rule "→I"; rule "→I")
fix x y z
AOT_assume 1: [F]x & [F]y & [G]z
moreover AOT_assume 2: [R]xz & [R]yz
ultimately AOT_have 3: ∃!x ([F]x & [R]xz)
using B "&E" "∀E" "→E" by fast
AOT_show x = y
by (rule "uni-most"[THEN "→E", OF 3, THEN "∀E"(2)[where β=x],
THEN "∀E"(2)[where β=y], THEN "→E"])
(metis "&I" "&E" 1 2)
qed
qed
next
AOT_show R |: F onto G
proof (rule "dfI"[OF "fFG:3"]; rule "&I")
AOT_show R |: F  G using C.
next
AOT_show y ([G]y  x ([F]x & [R]xy))
proof(rule GEN; rule "→I")
fix y
AOT_assume [G]y
AOT_hence ∃!x ([F]x & [R]xy)
using B[THEN "∀E"(2), THEN "→E"] by blast
AOT_hence x ([F]x & [R]xy & β (([F]β & [R]βy)  β = x))
using [THEN "dfE"] by blast
then AOT_obtain x where [F]x & [R]xy
using "∃E"[rotated] "&E" by blast
AOT_thus x ([F]x & [R]xy) by (rule "∃I")
qed
qed
qed
next
AOT_assume R |: F 1-1onto G
AOT_hence R |: F 1-1 G and R |: F onto G
using "dfE"[OF "fFG:4"] "&E" by blast+
AOT_hence C: R |: F  G
and D: xyz ([F]x & [F]y & [G]z  ([R]xz & [R]yz  x = y))
and E: y ([G]y  x ([F]x & [R]xy))
using "dfE"[OF "fFG:2"] "dfE"[OF "fFG:3"] "&E" by blast+
AOT_show R |: F 1-1 G
proof(rule "1-1-cor"[THEN "dfI"]; safe intro!: "&I" [axiom_inst])
AOT_show x ([F]x  ∃!y ([G]y & [R]xy))
using "dfE"[OF "fFG:1", OF C] "&E" by blast
next
AOT_show y ([G]y  ∃!x ([F]x & [R]xy))
proof (rule "GEN"; rule "→I")
fix y
AOT_assume 0: [G]y
AOT_hence x ([F]x & [R]xy)
using E "∀E" "→E" by fast
then AOT_obtain a where a_prop: [F]a & [R]ay
using "∃E"[rotated] by blast
moreover AOT_have z ([F]z & [R]zy  z = a)
proof (rule GEN; rule "→I")
fix z
AOT_assume [F]z & [R]zy
AOT_thus z = a
using D[THEN "∀E"(2)[where β=z], THEN "∀E"(2)[where β=a],
THEN "∀E"(2)[where β=y], THEN "→E", THEN "→E"]
a_prop 0 "&E" "&I" by metis
qed
ultimately AOT_have x ([F]x & [R]xy & z ([F]z & [R]zy  z = x))
using "&I" "∃I"(2) by fast
AOT_thus ∃!x ([F]x & [R]xy)
using [THEN "dfI"] by fast
qed
qed
qed

text‹We have already introduced the restricted type of Ordinary objects in the
Extended Relation Comprehension theory. However, make sure all variable names
are defined as expected (avoiding conflicts with situations
of possible world theory).›
AOT_register_variable_names
Ordinary: u v r t s

AOT_theorem "equi:1": ∃!u φ{u}  u (φ{u} & v (φ{v}  v =E u))
proof(rule "≡I"; rule "→I")
AOT_assume ∃!u φ{u}
AOT_hence ∃!x (O!x & φ{x}).
AOT_hence x (O!x & φ{x} & β (O!β & φ{β}  β = x))
using [THEN "dfE"] by blast
then AOT_obtain x where x_prop: O!x & φ{x} & β (O!β & φ{β}  β = x)
using "∃E"[rotated] by blast
{
fix β
AOT_assume beta_ord: O!β
moreover AOT_assume φ{β}
ultimately AOT_have β = x
using x_prop[THEN "&E"(2), THEN "∀E"(2)[where β=β]] "&I" "→E" by blast
AOT_hence β =E x
using [THEN "→E", OF "∨I"(1)[OF beta_ord],
THEN "qml:2"[axiom_inst, THEN "→E"],
THEN "≡E"(1)]
by blast
}
AOT_hence (O!β  (φ{β}  β =E x)) for β
using "→I" by blast
AOT_hence β(O!β  (φ{β}  β =E x))
by (rule GEN)
AOT_hence O!x & φ{x} & y (O!y  (φ{y}  y =E x))
using x_prop[THEN "&E"(1)] "&I" by blast
AOT_hence O!x & (φ{x} & y (O!y  (φ{y}  y =E x)))
using "&E" "&I" by meson
AOT_thus u (φ{u} & v (φ{v}  v =E u))
using "∃I" by fast
next
AOT_assume u (φ{u} & v (φ{v}  v =E u))
AOT_hence x (O!x & (φ{x} & y (O!y  (φ{y}  y =E x))))
by blast
then AOT_obtain x where x_prop: O!x & (φ{x} & y (O!y  (φ{y}  y =E x)))
using "∃E"[rotated] by blast
AOT_have y ([O!]y & φ{y}  y = x)
proof(rule GEN; rule "→I")
fix y
AOT_assume O!y & φ{y}
AOT_hence y =E x
using x_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2)[where β=y]]
"→E" "&E" by blast
AOT_thus y = x
using [THEN "→E", OF "∨I"(2)[OF x_prop[THEN "&E"(1)]],
THEN "qml:2"[axiom_inst, THEN "→E"], THEN "≡E"(2)] by blast
qed
AOT_hence [O!]x & φ{x} & y ([O!]y & φ{y}  y = x)
using x_prop "&E" "&I" by meson
AOT_hence x ([O!]x & φ{x} & y ([O!]y & φ{y}  y = x))
by (rule "∃I")
AOT_hence ∃!x (O!x & φ{x})
by (rule [THEN "dfI"])
AOT_thus ∃!u φ{u}.
qed

AOT_define CorrelatesEOneToOne :: τ  τ  τ  φ (‹_ |: _ 1-1E _›)
"equi:2": R |: F 1-1E G df R & F & G &
u ([F]u  ∃!v([G]v & [R]uv)) &
v ([G]v  ∃!u([F]u & [R]uv))

AOT_define EquinumerousE :: τ  τ  φ (infixl "E" 50)
"equi:3": F E G df R (R |: F 1-1E G)

text‹Note: not explicitly in PLM.›
AOT_theorem eq_den_1: Π if Π E Π'
proof -
AOT_have R (R |: Π 1-1E Π')
using "equi:3"[THEN "dfE"] that by blast
then AOT_obtain R where R |: Π 1-1E Π'
using "∃E"[rotated] by blast
AOT_thus Π
using "equi:2"[THEN "dfE"] "&E" by blast
qed

text‹Note: not explicitly in PLM.›
AOT_theorem eq_den_2: Π' if Π E Π'
proof -
AOT_have R (R |: Π 1-1E Π')
using "equi:3"[THEN "dfE"] that by blast
then AOT_obtain R where R |: Π 1-1E Π'
using "∃E"[rotated] by blast
AOT_thus Π'
using "equi:2"[THEN "dfE"] "&E" by blast+
qed

AOT_theorem "eq-part:1": F E F
proof (safe intro!: "&I" GEN "→I" [axiom_inst]
"dfI"[OF "equi:3"] "dfI"[OF "equi:2"] "∃I"(1))
fix x
AOT_assume 1: O!x
AOT_assume 2: [F]x
AOT_show ∃!v ([F]v & x =E v)
proof(rule "equi:1"[THEN "≡E"(2)];
rule "∃I"(2)[where β=x];
safe dest!: "&E"(2)
intro!:  "&I" "→I" 1 2 Ordinary.GEN [THEN "→E", OF 1])
AOT_show v =E x if x =E v for v
by (metis that [THEN "→E"])
qed
next
fix y
AOT_assume 1: O!y
AOT_assume 2: [F]y
AOT_show ∃!u ([F]u & u =E y)
by(safe dest!: "&E"(2)
intro!: "equi:1"[THEN "≡E"(2)] "∃I"(2)[where β=y]
"&I" "→I" 1 2 GEN [THEN "→E", OF 1])
qed(auto simp: )

AOT_theorem "eq-part:2": F E G  G E F
proof (rule "→I")
AOT_assume F E G
AOT_hence R R |: F 1-1E G
using "equi:3"[THEN "dfE"] by blast
then AOT_obtain R where R |: F 1-1E G
using "∃E"[rotated] by blast
AOT_hence 0: R & F & G & u ([F]u  ∃!v([G]v & [R]uv)) &
v ([G]v  ∃!u([F]u & [R]uv))
using "equi:2"[THEN "dfE"] by blast

AOT_have xy [R]yx] & G & F & u ([G]u  ∃!v([F]v & xy [R]yx]uv)) &
v ([F]v  ∃!u([G]u & xy [R]yx]uv))
proof (AOT_subst xy [R]yx]yx [R]xy for: x y;
(safe intro!: "&I" [axiom_inst] 0[THEN "&E"(2)]
0[THEN "&E"(1), THEN "&E"(2)]; "cqt:2[lambda]")?)
AOT_modally_strict {
AOT_have xy [R]yx]xy if [R]yx for y x
by (auto intro!: "β←C"(1) "cqt:2"
simp: "&I" "ex:1:a" prod_denotesI  that)
moreover AOT_have [R]yx if xy [R]yx]xy for y x
using "β→C"(1)[where φ="λ(x,y). _ (x,y)" and κ1κn="(_,_)",
simplified, OF that, simplified].
ultimately AOT_show xy [R]yx]αβ  [R]βα for α β
by (metis  "≡I")
}
qed
AOT_hence xy [R]yx] |: G 1-1E F
using "equi:2"[THEN "dfI"] by blast
AOT_hence R R |: G 1-1E F
by (rule "∃I"(1)) "cqt:2[lambda]"
AOT_thus G E F
using "equi:3"[THEN "dfI"] by blast
qed

text‹Note: not explicitly in PLM.›
AOT_theorem "eq-part:2[terms]": Π E Π'  Π' E Π
using [unvarify F G] eq_den_1 eq_den_2 "→I" by meson
declare [THEN "→E", sym]

AOT_theorem "eq-part:3": (F E G & G E H)  F E H
proof (rule "→I")
AOT_assume F E G & G E H
then AOT_obtain R1 and R2 where
R1 |: F 1-1E G
and R2 |: G 1-1E H
using "equi:3"[THEN "dfE"] "&E" "∃E"[rotated] by metis
AOT_hence θ: u ([F]u  ∃!v([G]v & [R1]uv)) & v ([G]v  ∃!u([F]u & [R1]uv))
and ξ: u ([G]u  ∃!v([H]v & [R2]uv)) & v ([H]v  ∃!u([G]u & [R2]uv))
using "equi:2"[THEN "dfE", THEN "&E"(2)]
"equi:2"[THEN "dfE", THEN "&E"(1), THEN "&E"(2)]
"&I" by blast+
AOT_have R R = xy O!x & O!y & v ([G]v & [R1]xv & [R2]vy)]
by (rule ) cqt_2_lambda_inst_prover
then AOT_obtain R where R_def: R = xy O!x & O!y & v ([G]v & [R1]xv & [R2]vy)]
using "∃E"[rotated] by blast
AOT_have 1: ∃!v (([H]v & [R]uv)) if a: [O!]u and b: [F]u for u
proof (rule "≡E"(2)[OF "equi:1"])
AOT_obtain b where
b_prop: [O!]b & ([G]b & [R1]ub & v ([G]v & [R1]uv  v =E b))
using θ[THEN "&E"(1), THEN "∀E"(2), THEN "→E", THEN "→E",
OF a b, THEN "≡E"(1)[OF "equi:1"]]
"∃E"[rotated] by blast
AOT_obtain c where
c_prop: "[O!]c & ([H]c & [R2]bc & v ([H]v & [R2]bv  v =E c))"
using ξ[THEN "&E"(1), THEN "∀E"(2)[where β=b], THEN "→E",
OF b_prop[THEN "&E"(1)], THEN "→E",
OF b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(1)],
THEN "≡E"(1)[OF "equi:1"]]
"∃E"[rotated] by blast
AOT_show v ([H]v & [R]uv & v' ([H]v' & [R]uv'  v' =E v))
proof (safe intro!: "&I" GEN "→I" "∃I"(2)[where β=c])
AOT_show O!c using c_prop "&E" by blast
next
AOT_show [H]c using c_prop "&E" by blast
next
AOT_have 0: [O!]u & [O!]c & v ([G]v & [R1]uv & [R2]vc)
by (safe intro!: "&I" a c_prop[THEN "&E"(1)] "∃I"(2)[where β=b]
b_prop[THEN "&E"(1)] b_prop[THEN "&E"(2), THEN "&E"(1)]
c_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)])
AOT_show [R]uc
by (auto intro: "rule=E"[rotated, OF R_def[symmetric]]
intro!: "β←C"(1) "cqt:2"
simp: "&I" "ex:1:a" prod_denotesI  0)
next
fix x
AOT_assume ordx: O!x
AOT_assume [H]x & [R]ux
AOT_hence hx: [H]x and [R]ux using "&E" by blast+
AOT_hence xy O!x & O!y & v ([G]v & [R1]xv & [R2]vy)]ux
using "rule=E"[rotated, OF R_def] by fast
AOT_hence O!u & O!x & v ([G]v & [R1]uv & [R2]vx)
by (rule "β→C"(1)[where φ="λ(κ,κ'). _ κ κ'" and κ1κn="(_,_)", simplified])
then AOT_obtain z where z_prop: O!z & ([G]z & [R1]uz & [R2]zx)
using "&E" "∃E"[rotated] by blast
AOT_hence z =E b
using b_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2)[where β=z]]
using "&E" "→E" by metis
AOT_hence z = b
by (metis [THEN "→E"])
AOT_hence [R2]bx
using z_prop[THEN "&E"(2), THEN "&E"(2)] "rule=E" by fast
AOT_thus x =E c
using c_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2)[where β=x],
THEN "→E", THEN "→E", OF ordx]
hx "&I" by blast
qed
qed
AOT_have 2: ∃!u (([F]u & [R]uv)) if a: [O!]v and b: [H]v for v
proof (rule "≡E"(2)[OF "equi:1"])
AOT_obtain b where
b_prop: [O!]b & ([G]b & [R2]bv & u ([G]u & [R2]uv  u =E b))
using ξ[THEN "&E"(2), THEN "∀E"(2), THEN "→E", THEN "→E",
OF a b, THEN "≡E"(1)[OF "equi:1"]]
"∃E"[rotated] by blast
AOT_obtain c where
c_prop: "[O!]c & ([F]c & [R1]cb & v ([F]v & [R1]vb  v =E c))"
using θ[THEN "&E"(2), THEN "∀E"(2)[where β=b], THEN "→E",
OF b_prop[THEN "&E"(1)], THEN "→E",
OF b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(1)],
THEN "≡E"(1)[OF "equi:1"]]
"∃E"[rotated] by blast
AOT_show u ([F]u & [R]uv & v' ([F]v' & [R]v'v  v' =E u))
proof (safe intro!: "&I" GEN "→I" "∃I"(2)[where β=c])
AOT_show O!c using c_prop "&E" by blast
next
AOT_show [F]c using c_prop "&E" by blast
next
AOT_have [O!]c & [O!]v & u ([G]u & [R1]cu & [R2]uv)
by (safe intro!: "&I" a "∃I"(2)[where β=b]
c_prop[THEN "&E"(1)] b_prop[THEN "&E"(1)]
b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(1)]
b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)]
c_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)])
AOT_thus [R]cv
by (auto intro: "rule=E"[rotated, OF R_def[symmetric]]
intro!: "β←C"(1) "cqt:2"
simp: "&I" "ex:1:a" prod_denotesI )
next
fix x
AOT_assume ordx: O!x
AOT_assume [F]x & [R]xv
AOT_hence hx: [F]x and [R]xv using "&E" by blast+
AOT_hence xy O!x & O!y & v ([G]v & [R1]xv & [R2]vy)]xv
using "rule=E"[rotated, OF R_def] by fast
AOT_hence O!x & O!v & u ([G]u & [R1]xu & [R2]uv)
by (rule "β→C"(1)[where φ="λ(κ,κ'). _ κ κ'" and κ1κn="(_,_)", simplified])
then AOT_obtain z where z_prop: O!z & ([G]z & [R1]xz & [R2]zv)
using "&E" "∃E"[rotated] by blast
AOT_hence z =E b
using b_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2)[where β=z]]
using "&E" "→E" "&I" by metis
AOT_hence z = b
by (metis [THEN "→E"])
AOT_hence [R1]xb
using z_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)] "rule=E" by fast
AOT_thus x =E c
using c_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2)[where β=x],
THEN "→E", THEN "→E", OF ordx]
hx "&I" by blast
qed
qed
AOT_show F E H
apply (rule "equi:3"[THEN "dfI"])
apply (rule "∃I"(2)[where β=R])
by (auto intro!: 1 2 "equi:2"[THEN "dfI"] "&I" [axiom_inst]
Ordinary.GEN "→I" Ordinary.ψ)
qed

text‹Note: not explicitly in PLM.›
AOT_theorem "eq-part:3[terms]": Π E Π'' if Π E Π' and Π' E Π''
using [unvarify F G H, THEN "→E"] eq_den_1 eq_den_2 "→I" "&I"
by (metis that(1) that(2))
declare [trans]

AOT_theorem "eq-part:4": F E G  H (H E F  H E G)
proof(rule "≡I"; rule "→I")
AOT_assume 0: F E G
AOT_hence 1: G E F using [THEN "→E"] by blast
AOT_show H (H E F  H E G)
proof (rule GEN; rule "≡I"; rule "→I")
AOT_show H E G if H E F for H using 0
by (meson "&I"  that )
next
AOT_show H E F if H E G for H using 1
by (metis "&I"  that )
qed
next
AOT_assume H (H E F  H E G)
AOT_hence F E F  F E G using "∀E" by blast
AOT_thus F E G using  "≡E" by blast
qed

AOT_define MapsE :: τ  τ  τ  φ ("_ |: _ ⟶E _")
"equi-rem:1":
R |: F ⟶E G df R & F & G & u ([F]u  ∃!v ([G]v & [R]uv))

AOT_define MapsEOneToOne :: τ  τ  τ  φ ("_ |: _ 1-1⟶E _")
"equi-rem:2":
R |: F 1-1⟶E G df
R |: F ⟶E G & tuv (([F]t & [F]u & [G]v)  ([R]tv & [R]uv  t =E u))

AOT_define MapsEOnto :: τ  τ  τ  φ ("_ |: _ ontoE _")
"equi-rem:3":
R |: F ontoE G df R |: F ⟶E G & v ([G]v  u ([F]u & [R]uv))

AOT_define MapsEOneToOneOnto :: τ  τ  τ  φ ("_ |: _ 1-1ontoE _")
"equi-rem:4":
R |: F 1-1ontoE G df R |: F 1-1⟶E G & R |: F ontoE G

AOT_theorem "equi-rem-thm":
R |: F 1-1E G  R |: F 1-1ontoE G
proof -
AOT_have R |: F 1-1E G  R |: x O!x & [F]x] 1-1 x O!x & [G]x]
proof(safe intro!: "≡I" "→I" "&I")
AOT_assume R |: F 1-1E G
AOT_hence u ([F]u  ∃!v ([G]v & [R]uv))
and v ([G]v  ∃!u ([F]u & [R]uv))
using "equi:2"[THEN "dfE"] "&E" by blast+
AOT_hence a: ([F]u  ∃!v ([G]v & [R]uv))
and b: ([G]v  ∃!u ([F]u & [R]uv)) for u v
using  by fast+
AOT_have (x [O!]x & [F]x]x  ∃!y (x [O!]x & [G]x]y & [R]xy)) for x
apply (AOT_subst x [O!]x & [F]x]x [O!]x & [F]x)
apply (rule [THEN "→E"])
apply "cqt:2[lambda]"
apply (AOT_subst x [O!]x & [G]x]x [O!]x & [G]x for: x)
apply (rule [THEN "→E"])
apply "cqt:2[lambda]"
apply (AOT_subst O!y & [G]y & [R]xy O!y & ([G]y & [R]xy) for: y)
apply (meson "≡E"(6)  )
apply (rule "→I") apply (frule "&E"(1)) apply (drule "&E"(2))
by (fact a[unconstrain u, THEN "→E", THEN "→E", of x])
AOT_hence A: x (x [O!]x & [F]x]x  ∃!y (x [O!]x & [G]x]y & [R]xy))
by (rule GEN)
AOT_have (x [O!]x & [G]x]y  ∃!x (x [O!]x & [F]x]x & [R]xy)) for y
apply (AOT_subst x [O!]x & [G]x]y [O!]y & [G]y)
apply (rule [THEN "→E"])
apply "cqt:2[lambda]"
apply (AOT_subst x [O!]x & [F]x]x [O!]x & [F]x for: x)
apply (rule [THEN "→E"])
apply "cqt:2[lambda]"
apply (AOT_subst O!x & [F]x & [R]xy O!x & ([F]x & [R]xy) for: x)
apply (meson "≡E"(6)  )
apply (rule "→I") apply (frule "&E"(1)) apply (drule "&E"(2))
by (fact b[unconstrain v, THEN "→E", THEN "→E", of y])
AOT_hence B: y (x [O!]x & [G]x]y  ∃!x (x [O!]x & [F]x]x & [R]xy))
by (rule GEN)
AOT_show R |: x [O!]x & [F]x] 1-1 x [O!]x & [G]x]
by (safe intro!: "1-1-cor"[THEN "dfI"] "&I"
[axiom_inst] A B)
"cqt:2[lambda]"+
next
AOT_assume R |: x [O!]x & [F]x] 1-1 x [O!]x & [G]x]
AOT_hence a: (x [O!]x & [F]x]x  ∃!y (x [O!]x & [G]x]y & [R]xy)) and
b: (x [O!]x & [G]x]y  ∃!x (x [O!]x & [F]x]x & [R]xy)) for x y
using "1-1-cor"[THEN "dfE"] "&E" "∀E"(2) by blast+
AOT_have [F]u  ∃!v ([G]v & [R]uv) for u
proof (safe intro!: "→I")
AOT_assume fu: [F]u
AOT_have 0: x [O!]x & [F]x]u
by (auto intro!: "β←C"(1) "cqt:2" [axiom_inst]
Ordinary.ψ fu "&I")
AOT_show ∃!v ([G]v & [R]uv)
apply (AOT_subst [O!]x & ([G]x & [R]ux)
([O!]x & [G]x) & [R]ux for: x)
apply (simp add: )
apply (AOT_subst (reverse) [O!]x & [G]x
x [O!]x & [G]x]x for: x)
apply (rule [THEN "→E"])
apply "cqt:2[lambda]"
using a[THEN "→E", OF 0] by blast
qed
AOT_hence A: u ([F]u  ∃!v ([G]v & [R]uv))
by (rule Ordinary.GEN)
AOT_have [G]v  ∃!u ([F]u & [R]uv) for v
proof (safe intro!: "→I")
AOT_assume gu: [G]v
AOT_have 0: x [O!]x & [G]x]v
by (auto intro!: "β←C"(1) "cqt:2" [axiom_inst]
Ordinary.ψ gu "&I")
AOT_show ∃!u ([F]u & [R]uv)
apply (AOT_subst [O!]x & ([F]x & [R]xv) ([O!]x & [F]x) & [R]xv for: x)
apply (simp add: )
apply (AOT_subst (reverse) [O!]x & [F]xx [O!]x & [F]x]x  for: x)
apply (rule [THEN "→E"])
apply "cqt:2[lambda]"
using b[THEN "→E", OF 0] by blast
qed
AOT_hence B: v ([G]v  ∃!u ([F]u & [R]uv)) by (rule Ordinary.GEN)
AOT_show R |: F 1-1E G
by (safe intro!: "equi:2"[THEN "dfI"] "&I" A B [axiom_inst])
qed
also AOT_have   R |: F 1-1ontoE G
proof(safe intro!: "≡I" "→I" "&I")
AOT_assume R |: x [O!]x & [F]x] 1-1 x [O!]x & [G]x]
AOT_hence a: (x [O!]x & [F]x]x  ∃!y (x [O!]x & [G]x]y & [R]xy)) and
b: (x [O!]x & [G]x]y  ∃!x (x [O!]x & [F]x]x & [R]xy)) for x y
using "1-1-cor"[THEN "dfE"] "&E" "∀E"(2) by blast+
AOT_show R |: F 1-1ontoE G
proof (safe intro!: [THEN "dfI"] "&I" [THEN "dfI"]
[THEN "dfI"] [THEN "dfI"]
[axiom_inst] Ordinary.GEN "→I")
fix u
AOT_assume fu: [F]u
AOT_have 0: x [O!]x & [F]x]u
by (auto intro!: "β←C"(1) "cqt:2" [axiom_inst]
Ordinary.ψ fu "&I")
AOT_hence 1: ∃!y (x [O!]x & [G]x]y & [R]uy)
using a[THEN "→E"] by blast
AOT_show ∃!v ([G]v & [R]uv)
apply (AOT_subst [O!]x & ([G]x & [R]ux) ([O!]x & [G]x) & [R]ux for: x)
apply (simp add: )
apply (AOT_subst (reverse) [O!]x & [G]x x [O!]x & [G]x]x for: x)
apply (rule [THEN "→E"])
apply "cqt:2[lambda]"
by (fact 1)
next
fix t u v
AOT_assume [F]t & [F]u & [G]v and rtv_tuv: [R]tv & [R]uv
AOT_hence oft: x O!x & [F]x]t and
ofu: x O!x & [F]x]u and
ogv: x O!x & [G]x]v
by (auto intro!: "β←C"(1) "cqt:2" "&I"
simp: Ordinary.ψ dest: "&E")
AOT_hence ∃!x (x [O!]x & [F]x]x & [R]xv)
using b[THEN "→E"] by blast
then AOT_obtain a where
a_prop: x [O!]x & [F]x]a & [R]av &
x ((x [O!]x & [F]x]x & [R]xv)  x = a)
using [THEN "dfE"] "∃E"[rotated] by blast
AOT_hence ua: u = a
using ofu rtv_tuv[THEN "&E"(2)] "∀E"(2) "→E" "&I" "&E"(2) by blast
moreover AOT_have ta: t = a
using a_prop oft rtv_tuv[THEN "&E"(1)] "∀E"(2) "→E" "&I" "&E"(2) by blast
ultimately AOT_have t = u by (metis "rule=E" id_sym)
AOT_thus t =E u
using "rule=E" id_sym  Ordinary.ψ ta ua "→E" by fast
next
fix u
AOT_assume [F]u
AOT_hence x O!x & [F]x]u
by (auto intro!: "β←C"(1) "cqt:2" "&I"
simp: [axiom_inst]  Ordinary.ψ)
AOT_hence ∃!y (x [O!]x & [G]x]y & [R]uy)
using a[THEN "→E"] by blast
then AOT_obtain a where
a_prop: x [O!]x & [G]x]a & [R]ua &
x ((x [O!]x & [G]x]x & [R]ux)  x = a)
using [THEN "dfE"] "∃E"[rotated] by blast
AOT_have O!a & [G]a
by (rule "β→C"(1)) (auto simp: a_prop[THEN "&E"(1), THEN "&E"(1)])
AOT_hence O!a and [G]a using "&E" by blast+
moreover AOT_have v ([G]v & [R]uv  v =E a)
proof(safe intro!: Ordinary.GEN "→I"; frule "&E"(1); drule "&E"(2))
fix v
AOT_assume [G]v and ruv: [R]uv
AOT_hence x [O!]x & [G]x]v
by (auto intro!: "β←C"(1) "cqt:2" "&I" simp: Ordinary.ψ)
AOT_hence v = a
using a_prop[THEN "&E"(2), THEN "∀E"(2), THEN "→E", OF "&I"] ruv by blast
AOT_thus v =E a
using "rule=E"  Ordinary.ψ "→E" by fast
qed
ultimately AOT_have O!a & ([G]a & [R]ua & v' ([G]v' & [R]uv'  v' =E a))
using "∃I" "&I" a_prop[THEN "&E"(1), THEN "&E"(2)] by simp
AOT_hence v ([G]v & [R]uv & v' ([G]v' & [R]uv'  v' =E v))
by (rule "∃I")
AOT_thus ∃!v ([G]v & [R]uv)
by (rule "equi:1"[THEN "≡E"(2)])
next
fix v
AOT_assume [G]v
AOT_hence x O!x & [G]x]v
by (auto intro!: "β←C"(1) "cqt:2" "&I" Ordinary.ψ)
AOT_hence ∃!x (x [O!]x & [F]x]x & [R]xv)
using b[THEN "→E"] by blast
then AOT_obtain a where
a_prop: x [O!]x & [F]x]a & [R]av &
y (x [O!]x & [F]x]y & [R]yv  y = a)
using [THEN "dfE", THEN "∃E"[rotated]] by blast
AOT_have O!a & [F]a
by (rule "β→C"(1)) (auto simp: a_prop[THEN "&E"(1), THEN "&E"(1)])
AOT_hence O!a & ([F]a & [R]av)
using a_prop[THEN "&E"(1), THEN "&E"(2)] "&E" "&I" by metis
AOT_thus u ([F]u & [R]uv)
by (rule "∃I")
qed
next
AOT_assume R |: F 1-1ontoE G
AOT_hence 1: R |: F 1-1⟶E G
and 2: R |: F ontoE G
using [THEN "dfE"] "&E" by blast+
AOT_hence 3: R |: F ⟶E G
and A: t u v ([F]t & [F]u & [G]v  ([R]tv & [R]uv  t =E u))
using [THEN "dfE", OF 1] "&E" by blast+
AOT_hence B: u ([F]u  ∃!v ([G]v & [R]uv))
using [THEN "dfE"] "&E" by blast
AOT_have C: v ([G]v  u ([F]u & [R]uv))
using [THEN "dfE", OF 2] "&E" by blast
AOT_show R |: x [O!]x & [F]x] 1-1 x [O!]x & [G]x]
proof (rule "1-1-cor"[THEN "dfI"];
safe intro!: "&I" "cqt:2" GEN "→I")
fix x
AOT_assume 1: x [O!]x & [F]x]x
AOT_have O!x & [F]x
by (rule "β→C"(1)) (auto simp: 1)
AOT_hence ∃!v ([G]v & [R]xv)
using B[THEN "∀E"(2), THEN "→E", THEN "→E"] "&E" by blast
then AOT_obtain y where
y_prop: O!y & ([G]y & [R]xy & u ([G]u & [R]xu  u =E y))
using "equi:1"[THEN "≡E"(1)] "∃E"[rotated] by fastforce
AOT_hence x O!x & [G]x]y
by (auto intro!: "β←C"(1) "cqt:2" "&I" dest: "&E")
moreover AOT_have z (x O!x & [G]x]z & [R]xz  z = y)
proof(safe intro!: GEN "→I"; frule "&E"(1); drule "&E"(2))
fix z
AOT_assume 1: x [O!]x & [G]x]z
AOT_have 2: O!z & [G]z
by (rule "β→C"(1)) (auto simp: 1)
moreover AOT_assume [R]xz
ultimately AOT_have z =E y
using y_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2),
THEN "→E", THEN "→E", rotated, OF "&I"] "&E"
by blast
AOT_thus z = y
using 2[THEN "&E"(1)] by (metis  "→E")
qed
ultimately AOT_have x O!x & [G]x]y & [R]xy &
z (x O!x & [G]x]z & [R]xz  z = y)
using y_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)] "&I" by auto
AOT_hence y (x O!x & [G]x]y & [R]xy &
z (x O!x & [G]x]z & [R]xz  z = y))
by (rule "∃I")
AOT_thus ∃!y (x [O!]x & [G]x]y & [R]xy)
using [THEN "dfI"] by fast
next
fix y
AOT_assume 1: x [O!]x & [G]x]y
AOT_have oy_gy: O!y & [G]y
by (rule "β→C"(1)) (auto simp: 1)
AOT_hence u ([F]u & [R]uy)
using C[THEN "∀E"(2), THEN "→E", THEN "→E"] "&E" by blast
then AOT_obtain x where x_prop: O!x & ([F]x & [R]xy)
using "∃E"[rotated] by blast
AOT_hence ofx: x O!x & [F]x]x
by (auto intro!: "β←C"(1) "cqt:2" "&I" dest: "&E")
AOT_have α (x [O!]x & [F]x]α & [R]αy &
β (x [O!]x & [F]x]β & [R]βy  β = α))
proof (safe intro!: "∃I"(2)[where β=x] "&I" GEN "→I")
AOT_show x O!x & [F]x]x using ofx.
next
AOT_show [R]xy using x_prop[THEN "&E"(2), THEN "&E"(2)].
next
fix z
AOT_assume 1: x [O!]x & [F]x]z & [R]zy
AOT_have oz_fz: O!z & [F]z
by (rule "β→C"(1)) (auto simp: 1[THEN "&E"(1)])
AOT_have z =E x
using A[THEN "∀E"(2)[where β=z], THEN "→E", THEN "∀E"(2)[where β=x],
THEN "→E", THEN "∀E"(2)[where β=y], THEN "→E",
THEN "→E", THEN "→E", OF oz_fz[THEN "&E"(1)],
OF x_prop[THEN "&E"(1)], OF oy_gy[THEN "&E"(1)], OF "&I", OF "&I",
OF oz_fz[THEN "&E"(2)], OF x_prop[THEN "&E"(2), THEN "&E"(1)],
OF oy_gy[THEN "&E"(2)], OF "&I", OF 1[THEN "&E"(2)],
OF x_prop[THEN "&E"(2), THEN "&E"(2)]].
AOT_thus z = x
by (metis  )
qed
AOT_thus ∃!x (x [O!]x & [F]x]x & [R]xy)
by (rule [THEN "dfI"])
qed
qed
finally show ?thesis.
qed

AOT_theorem "empty-approx:1": (¬u [F]u & ¬v [H]v)  F E H
proof(rule "→I"; frule "&E"(1); drule "&E"(2))
AOT_assume 0: ¬u [F]u and 1: ¬v [H]v
AOT_have u ([F]u  ∃!v ([H]v & [R]uv)) for R
proof(rule Ordinary.GEN; rule "→I"; rule )
fix u
AOT_assume [F]u
AOT_hence u [F]u using  "&I" by fast
AOT_thus u [F]u & ¬u [F]u using "&I" 0 by blast
qed
moreover AOT_have v ([H]v  ∃!u ([F]u & [R]uv)) for R
proof(rule Ordinary.GEN; rule "→I"; rule )
fix v
AOT_assume [H]v
AOT_hence v [H]v using  "&I" by fast
AOT_thus v [H]v & ¬v [H]v using 1 "&I" by blast
qed
ultimately AOT_have R |: F 1-1E H for R
apply (safe intro!: "equi:2"[THEN "dfI"] "&I" GEN [axiom_inst])
using "∀E" by blast+
AOT_hence R R |: F 1-1E H by (rule "∃I")
AOT_thus F E H
by (rule "equi:3"[THEN "dfI"])
qed

AOT_theorem "empty-approx:2": (u [F]u & ¬v [H]v)  ¬(F E H)
proof(rule "→I"; frule "&E"(1); drule "&E"(2); rule )
AOT_assume 1: u [F]u and 2: ¬v [H]v
AOT_obtain b where b_prop: O!b & [F]b
using 1 "∃E"[rotated] by blast
AOT_assume F E H
AOT_hence R R |: F 1-1E H
by (rule "equi:3"[THEN "dfE"])
then AOT_obtain R where R |: F 1-1E H
using "∃E"[rotated] by blast
AOT_hence θ: u ([F]u  ∃!v ([H]v & [R]uv))
using "equi:2"[THEN "dfE"] "&E" by blast+
AOT_have ∃!v ([H]v & [R]bv) for u
using θ[THEN "∀E"(2)[where β=b], THEN "→E", THEN "→E",
OF b_prop[THEN "&E"(1)], OF b_prop[THEN "&E"(2)]].
AOT_hence v ([H]v & [R]bv & u ([H]u & [R]bu  u =E v))
by (rule "equi:1"[THEN "≡E"(1)])
then AOT_obtain x where O!x & ([H]x & [R]bx & u ([H]u & [R]bu  u =E x))
using "∃E"[rotated] by blast
AOT_hence O!x & [H]x using "&E" "&I" by blast
AOT_hence v [H]v by (rule "∃I")
AOT_thus v [H]v & ¬v [H]v using 2 "&I" by blast
qed

AOT_define FminusU :: Π  τ  Π ("_-_")
"F-u": [F]-x =df z [F]z & z E x]

text‹Note: not explicitly in PLM.›
AOT_theorem "F-u[den]": [F]-x
by (rule "=dfI"(1)[OF "F-u", where τ1τn="(_,_)", simplified]; "cqt:2[lambda]")
AOT_theorem "F-u[equiv]": [[F]-x]y  ([F]y & y E x)
by (auto intro: "F-u"[THEN "=dfI"(1), where τ1τn="(_,_)", simplified]
intro!: "cqt:2" [THEN "→E", THEN "∀E"(2)])

AOT_theorem eqP': F E G & [F]u & [G]v  [F]-u E [G]-v
proof (rule "→I"; frule "&E"(2); drule "&E"(1); frule "&E"(2); drule "&E"(1))
AOT_assume F E G
AOT_hence R R |: F 1-1E G
using "equi:3"[THEN "dfE"] by blast
then AOT_obtain R where R_prop: R |: F 1-1E G
using "∃E"[rotated] by blast
AOT_hence A: u ([F]u  ∃!v ([G]v & [R]uv))
and B: v ([G]v  ∃!u ([F]u & [R]uv))
using "equi:2"[THEN "dfE"] "&E" by blast+
AOT_have R |: F 1-1ontoE G
using [THEN "≡E"(1), OF R_prop].
AOT_hence R |: F 1-1⟶E G & R |: F ontoE G
using [THEN "dfE"] by blast
AOT_hence C: tuv (([F]t & [F]u & [G]v)  ([R]tv & [R]uv  t =E u))
using [THEN "dfE"] "&E" by blast
AOT_assume fu: [F]u
AOT_assume gv: [G]v
AOT_have z [Π]z & z E κ] for Π κ
by "cqt:2[lambda]"
note Π_minus_κI = [
where τ=(λ(Π, κ). «[Π]-κ»), simplified, OF "F-u", simplified, OF this]
and Π_minus_κE = [
where τ=(λ(Π, κ). «[Π]-κ»), simplified, OF "F-u", simplified, OF this]
AOT_have Π_minus_κ_den: [Π]-κ for Π κ
by (rule Π_minus_κI) "cqt:2[lambda]"+
{
fix R
AOT_assume R_prop: R |: F 1-1E G
AOT_hence A: u ([F]u  ∃!v ([G]v & [R]uv))
and B: v ([G]v  ∃!u ([F]u & [R]uv))
using "equi:2"[THEN "dfE"] "&E" by blast+
AOT_have R |: F 1-1ontoE G
using [THEN "≡E"(1), OF R_prop].
AOT_hence R |: F 1-1⟶E G & R |: F ontoE G
using [THEN "dfE"] by blast
AOT_hence C: tuv (([F]t & [F]u & [G]v)  ([R]tv & [R]uv  t =E u))
using [THEN "dfE"] "&E" by blast

AOT_assume Ruv: [R]uv
AOT_have R |: [F]-u 1-1E [G]-v
proof(safe intro!: "equi:2"[THEN "dfI"] "&I" [axiom_inst]
Π_minus_κ_den Ordinary.GEN "→I")
fix u'
AOT_assume [[F]-u]u'
AOT_hence 0: z [F]z & z E u]u'
using Π_minus_κE by fast
AOT_have 0: [F]u' & u' E u
by (rule "β→C"(1)[where κ1κn=]) (fact 0)
AOT_have ∃!v ([G]v & [R]u'v)
using A[THEN [where α=u'], THEN "→E", OF 0[THEN "&E"(1)]].
then AOT_obtain v' where
v'_prop: [G]v' & [R]u'v' &  t ([G]t & [R]u't  t =E v')
using "equi:1"[THEN "≡E"(1)] [rotated] by fastforce

AOT_show ∃!v' ([[G]-v]v' & [R]u'v')
proof (safe intro!: "equi:1"[THEN "≡E"(2)] [where β=v']
"&I" Ordinary.GEN "→I")
AOT_show [[G]-v]v'
proof (rule Π_minus_κI;
safe intro!: "β←C"(1) "cqt:2" "&I" [THEN "≡E"(2)])
AOT_show [G]v' using v'_prop "&E" by blast
next
AOT_show ¬v' =E v
proof (rule )
AOT_assume v' =E v
AOT_hence v' = v by (metis  "→E")
AOT_hence Ruv': [R]uv' using "rule=E" Ruv id_sym by fast
AOT_have u' =E u
by (rule C[THEN , THEN ,
THEN [where α=v'], THEN "→E", THEN "→E"])
(safe intro!: "&I" 0[THEN "&E"(1)] fu
v'_prop[THEN "&E"(1), THEN "&E"(1)]
Ruv' v'_prop[THEN "&E"(1), THEN "&E"(2)])
moreover AOT_have ¬(u' =E u)
using "0" "&E"(2) "≡E"(1)  by blast
ultimately AOT_show u' =E u & ¬u' =E u using "&I" by blast
qed
qed
next
AOT_show [R]u'v' using v'_prop "&E" by blast
next
fix t
AOT_assume t_prop: [[G]-v]t & [R]u't
AOT_have gt_t_noteq_v: [G]t & t E v
apply (rule "β→C"(1)[where κ1κn=])
apply (rule Π_minus_κE)
by (fact t_prop[THEN "&E"(1)])
AOT_show t =E v'
using v'_prop[THEN "&E"(2), THEN , THEN "→E",
OF "&I", OF gt_t_noteq_v[THEN "&E"(1)],
OF t_prop[THEN "&E"(2)]].
qed
next
fix v'
AOT_assume G_minus_v_v': [[G]-v]v'
AOT_have gt_t_noteq_v: [G]v' & v' E v
apply (rule "β→C"(1)[where κ1κn=])
apply (rule Π_minus_κE)
by (fact G_minus_v_v')
AOT_have ∃!u([F]u & [R]uv')
using B[THEN , THEN "→E", OF gt_t_noteq_v[THEN "&E"(1)]].
then AOT_obtain u' where
u'_prop: [F]u' & [R]u'v' & t ([F]t & [R]tv'  t =E u')
using "equi:1"[THEN "≡E"(1)] [rotated] by fastforce
AOT_show ∃!u' ([[F]-u]u' & [R]u'v')
proof (safe intro!: "equi:1"[THEN "≡E"(2)] [where β=u'] "&I"
u'_prop[THEN "&E"(1), THEN "&E"(2)] Ordinary.GEN "→I")
AOT_show [[F]-u]u'
proof (rule Π_minus_κI;
safe intro!: "β←C"(1) "cqt:2" "&I" [THEN "≡E"(2)]
u'_prop[THEN "&E"(1), THEN "&E"(1)]; rule )
AOT_assume u'_eq_u: u' =E u
AOT_hence u' = u
using   by blast
AOT_hence Ru'v: [R]u'v using "rule=E" Ruv id_sym by fast
AOT_have v' E v
using "&E"(2) gt_t_noteq_v by blast
AOT_hence v'_noteq_v: ¬(v' =E v) by (metis "≡E"(1) )
AOT_have u ([G]u & [R]u'u & v ([G]v & [R]u'v  v =E u))
using A[THEN , THEN "→E",
OF u'_prop[THEN "&E"(1), THEN "&E"(1)],
THEN "equi:1"[THEN "≡E"(1)]].
then AOT_obtain t where
t_prop: [G]t & [R]u't & v ([G]v & [R]u'v  v =E t)
using [rotated] by meson
AOT_have v =E t if [G]v and [R]u'v for v
using t_prop[THEN "&E"(2), THEN , THEN "→E",
OF "&I", OF that].
AOT_hence v' =E t and v =E t
by (auto simp: gt_t_noteq_v[THEN "&E"(1)] Ru'v gv
u'_prop[THEN "&E"(1), THEN "&E"(2)])
AOT_hence v' =E v
using "rule=E"  id_sym "→E" by fast
AOT_thus v' =E v & ¬v' =E v
using v'_noteq_v "&I" by blast
qed
next
fix t
AOT_assume 0: [[F]-u]t & [R]tv'
moreover AOT_have [F]t & t E u
apply (rule "β→C"(1)[where κ1κn=])
apply (rule Π_minus_κE)
by (fact 0[THEN "&E"(1)])
ultimately AOT_show t =E u'
using u'_prop[THEN "&E"(2), THEN , THEN "→E", OF "&I"]
"&E" by blast
qed
qed
AOT_hence R R |: [F]-u 1-1E [G]-v
by (rule "∃I")
} note 1 = this
moreover {
AOT_assume not_Ruv: ¬[R]uv
AOT_have ∃!v ([G]v & [R]uv)
using A[THEN , THEN "→E", OF fu].
then AOT_obtain b where
b_prop: O!b & ([G]b & [R]ub & t([G]t & [R]ut  t =E b))
using "equi:1"[THEN "≡E"(1)] "∃E"[rotated] by fastforce
AOT_hence ob: O!b and gb: [G]b and Rub: [R]ub
using "&E" by blast+
AOT_have O!t  ([G]t & [R]ut  t =E b) for t
using b_prop "&E"(2) "∀E"(2) by blast
AOT_hence b_unique: t =E b if O!t and [G]t and [R]ut for t
by (metis Adjunction   that)
AOT_have not_v_eq_b: ¬(v =E b)
proof(rule )
AOT_assume v =E b
AOT_hence 0: v = b
by (metis  "→E")
AOT_have [R]uv
using b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)]
"rule=E"[rotated, OF 0[symmetric]] by fast
AOT_thus [R]uv & ¬[R]uv
using not_Ruv "&I" by blast
qed
AOT_have not_b_eq_v: ¬(b =E v)
using  not_v_eq_b  by blast
AOT_have ∃!u ([F]u & [R]uv)
using B[THEN , THEN "→E", OF gv].
then AOT_obtain a where
a_prop: O!a & ([F]a & [R]av & t([F]t & [R]tv  t =E a))
using "equi:1"[THEN "≡E"(1)] "∃E"[rotated] by fastforce
AOT_hence Oa: O!a and fa: [F]a and Rav: [R]av
using "&E" by blast+
AOT_have O!t  ([F]t & [R]tv  t =E a) for t
using a_prop "&E" "∀E"(2) by blast
AOT_hence a_unique: t =E a if O!t and [F]t and [R]tv for t
by (metis Adjunction   that)
AOT_have not_u_eq_a: ¬(u =E a)
proof(rule )
AOT_assume u =E a
AOT_hence 0: u = a
by (metis  "→E")
AOT_have [R]uv
using a_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)]
"rule=E"[rotated, OF 0[symmetric]] by fast
AOT_thus [R]uv & ¬[R]uv
using not_Ruv "&I" by blast
qed
AOT_have not_a_eq_u: ¬(a =E u)
using  not_u_eq_a  by blast
let ?R = «u'v' (u' E u & v' E v & [R]u'v')
(u' =E a & v' =E b)
(u' =E u & v' =E v)]»
AOT_have [«?R»] by "cqt:2[lambda]"
AOT_hence  β β = [«?R»]
using  "≡E"(1) by fast
then AOT_obtain R1 where R1_def: R1 = [«?R»]
using "∃E"[rotated] by blast
AOT_have Rxy1: [R]xy if [R1]xy and x E u and x E a for x y
proof -
AOT_have 0: [«?R»]xy
by (rule "rule=E"[rotated, OF R1_def]) (fact that(1))
AOT_have (x E u & y E v & [R]xy)  (x =E a & y =E b)  (x =E u & y =E v)
using "β→C"(1)[OF 0] by simp
AOT_hence x E u & y E v & [R]xy using that(2,3)
by (metis "∨E"(3) (1) "≡E"(1)
)
AOT_thus [R]xy using "&E" by blast+
qed
AOT_have Rxy2: [R]xy  if [R1]xy and y E v and y E b for x y
proof -
AOT_have 0: [«?R»]xy
by (rule "rule=E"[rotated, OF R1_def]) (fact that(1))
AOT_have (x E u & y E v & [R]xy)  (x =E a & y =E b)  (x =E u & y =E v)
using "β→C"(1)[OF 0] by simp
AOT_hence x E u & y E v & [R]xy
using that(2,3)
by (metis "∨E"(3) (2) "≡E"(1)
)
AOT_thus [R]xy using "&E" by blast+
qed
AOT_have R1xy: [R1]xy if [R]xy and x E u and y E v for x y
by (rule "rule=E"[rotated, OF R1_def[symmetric]])
(auto intro!: "β←C"(1) "cqt:2"
simp: "&I" "ex:1:a" prod_denotesI  that "∨I"(1))
AOT_have R1ab: [R1]ab
apply (rule "rule=E"[rotated, OF R1_def[symmetric]])
apply (safe intro!: "β←C"(1) "cqt:2" prod_denotesI "&I")
by (meson a_prop b_prop "&I" "&E"(1) "∨I"(1) "∨I"(2)  "→E")
AOT_have R1uv: [R1]uv
apply (rule "rule=E"[rotated, OF R1_def[symmetric]])
apply (safe intro!: "β←C"(1) "cqt:2" prod_denotesI "&I")
by (meson "&I" "∨I"(2)  Ordinary.ψ "→E")
moreover AOT_have R1 |: F 1-1E G
proof (safe intro!: "equi:2"[THEN "dfI"] "&I" "cqt:2" Ordinary.GEN "→I")
fix u'
AOT_assume fu': [F]u'
{
AOT_assume not_u'_eq_u: ¬(u' =E u) and not_u'_eq_a: ¬(u' =E a)
AOT_hence u'_noteq_u: u' E u and u'_noteq_a: u' E a
by (metis "≡E"(2) )+
AOT_have ∃!v ([G]v & [R]u'v)
using A[THEN , THEN "→E", OF fu'].
AOT_hence v ([G]v & [R]u'v & t ([G]t & [R]u't  t =E v))
using "equi:1"[THEN "≡E"(1)] by simp
then AOT_obtain v' where
v'_prop: [G]v' & [R]u'v' & t ([G]t & [R]u't  t =E v')
using [rotated] by meson
AOT_hence gv': [G]v' and Ru'v': [R]u'v'
using "&E" by blast+
AOT_have not_v'_eq_v: ¬v' =E v
proof (rule )
AOT_assume v' =E v
AOT_hence v' = v
by (metis  "→E")
AOT_hence Ru'v: [R]u'v
using "rule=E" Ru'v' by fast
AOT_have u' =E a
using a_unique[OF Ordinary.ψ, OF fu', OF Ru'v].
AOT_thus u' =E a & ¬u' =E a
using not_u'_eq_a "&I" by blast
qed
AOT_hence v'_noteq_v: v' E v
using "≡E"(2)  by blast
AOT_have t ([G]t & [R]u't  t =E v')
using v'_prop "&E" by blast
AOT_hence [G]t & [R]u't  t =E v' for t
using  by meson
AOT_hence v'_unique: t =E v' if [G]t and [R]u't for t
by (metis "&I" that "→E")

AOT_have [G]v' & [R1]u'v' & t ([G]t & [R1]u't  t =E v')
proof (safe intro!: "&I" gv' R1xy Ru'v' u'_noteq_u u'_noteq_a "→I"
Ordinary.GEN [THEN "≡E"(2)] not_v'_eq_v)
fix t
AOT_assume 1: [G]t & [R1]u't
AOT_have [R]u't
using Rxy1[OF 1[THEN "&E"(2)], OF u'_noteq_u, OF u'_noteq_a].
AOT_thus t =E v'
using v'_unique 1[THEN "&E"(1)] by blast
qed
AOT_hence v ([G]v & [R1]u'v & t ([G]t & [R1]u't  t =E v))
by (rule )
AOT_hence ∃!v ([G]v & [R1]u'v)
by (rule "equi:1"[THEN "≡E"(2)])
}
moreover {
AOT_assume 0: u' =E u
AOT_hence u'_eq_u: u' = u
using  "→E" by blast
AOT_have ∃!v ([G]v & [R1]u'v)
proof (safe intro!: "equi:1"[THEN "≡E"(2)] [where β=v]
"&I" Ordinary.GEN "→I" gv)
AOT_show [R1]u'v
apply (rule "rule=E"[rotated, OF R1_def[symmetric]])
apply (safe intro!: "β←C"(1) "cqt:2" "&I" prod_denotesI)
by (safe intro!: "∨I"(2) "&I" 0 [THEN "→E", OF Ordinary.ψ])
next
fix v'
AOT_assume [G]v' & [R1]u'v'
AOT_hence 0: [R1]uv'
using "rule=E"[rotated, OF u'_eq_u] "&E"(2) by fast
AOT_have 1: [«?R»]uv'
by (rule "rule=E"[rotated, OF R1_def]) (fact 0)
AOT_have 2: (u E u & v' E v & [R]uv')
(u =E a & v' =E b)
(u =E u & v' =E v)
using "β→C"(1)[OF 1] by simp
AOT_have ¬u E u
using "≡E"(4)   Ordinary.ψ
by blast
AOT_hence ¬((u E u & v' E v & [R]uv')  (u =E a & v' =E b))
using not_u_eq_a
by (metis "∨E"(2) (1)
)
AOT_hence (u =E u & v' =E v)
using 2 by (metis "∨E"(2))
AOT_thus v' =E v
using "&E" by blast
qed
}
moreover {
AOT_assume 0: u' =E a
AOT_hence u'_eq_a: u' = a
using  "→E" by blast
AOT_have ∃!v ([G]v & [R1]u'v)
proof (safe intro!: "equi:1"[THEN "≡E"(2)] "∃I"(2)[where β=b] "&I"
Ordinary.GEN "→I" b_prop[THEN "&E"(1)]
b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(1)])
AOT_show [R1]u'b
apply (rule "rule=E"[rotated, OF R1_def[symmetric]])
apply (safe intro!: "β←C"(1) "cqt:2" "&I" prod_denotesI)
apply (rule "∨I"(1); rule "∨I"(2); rule "&I")
apply (fact 0)
using b_prop "&E"(1)  "→E" by blast
next
fix v'
AOT_assume gv'_R1u'v': [G]v' & [R1]u'v'
AOT_hence 0: [R1]av'
using u'_eq_a by (meson "rule=E" "&E"(2))
AOT_have 1: [«?R»]av'
by (rule "rule=E"[rotated, OF R1_def]) (fact 0)
AOT_have (a E u & v' E v & [R]av')
(a =E a & v' =E b)
(a =E u & v' =E v)
using "β→C"(1)[OF 1] by simp
moreover {
AOT_assume 0: a E u & v' E v & [R]av'
AOT_have ∃!v ([G]v & [R]u'v)
using A[THEN , THEN "→E", OF fu'].
AOT_hence ∃!v ([G]v & [R]av)
using u'_eq_a "rule=E" by fast
AOT_hence v ([G]v & [R]av & t ([G]t & [R]at  t =E v))
using "equi:1"[THEN "≡E"(1)] by fast
then AOT_obtain s where
s_prop: [G]s & [R]as & t ([G]t & [R]at  t =E s)
using [rotated] by meson
AOT_have v' =E s
using s_prop[THEN "&E"(2), THEN ]
gv'_R1u'v'[THEN "&E"(1)] 0[THEN "&E"(2)]
by (metis "&I" )
moreover AOT_have v =E s
using s_prop[THEN "&E"(2), THEN ] gv Rav
by (metis "&I" "→E")
ultimately AOT_have v' =E v
by (metis "&I"   "→E")
moreover AOT_have ¬(v' =E v)
using 0<