Theory AOT_NaturalNumbers

1(*<*)
2theory AOT_NaturalNumbers
3  imports AOT_PossibleWorlds AOT_ExtendedRelationComprehension
4  abbrevs one-to-one = 1-1
5      and onto = onto
6begin
7(*>*)
8
9sectionNatural Numbers
10 
11AOT_define CorrelatesOneToOne :: τ  τ  τ  φ (_ |: _ 1-1 _)
12  "1-1-cor": R |: F 1-1 G df R & F & G &
13                                   x ([F]x  ∃!y([G]y & [R]xy)) &
14                                   y ([G]y  ∃!x([F]x & [R]xy))
15
16AOT_define MapsTo :: τ  τ  τ  φ (_ |: _  _)
17  "fFG:1": R |: F  G df R & F & G & x ([F]x  ∃!y([G]y & [R]xy))
18
19AOT_define MapsToOneToOne :: τ  τ  τ  φ (_ |: _ 1-1 _)
20  "fFG:2": R |: F 1-1 G df
21      R |: F  G & xyz (([F]x & [F]y & [G]z)  ([R]xz & [R]yz  x = y))
22
23AOT_define MapsOnto :: τ  τ  τ  φ (_ |: _ onto _)
24  "fFG:3": R |: F onto G df R |: F  G & y ([G]y  x([F]x & [R]xy))
25
26AOT_define MapsOneToOneOnto :: τ  τ  τ  φ (_ |: _ 1-1onto _)
27  "fFG:4": R |: F 1-1onto G df R |: F 1-1 G & R |: F onto G
28
29AOT_theorem "eq-1-1": R |: F 1-1 G  R |: F 1-1onto G
30proof(rule "≡I"; rule "→I")
31  AOT_assume R |: F 1-1 G
32  AOT_hence A: x ([F]x  ∃!y([G]y & [R]xy))
33        and B: y ([G]y  ∃!x([F]x & [R]xy))
34    using "dfE"[OF "1-1-cor"] "&E" by blast+
35  AOT_have C: R |: F  G
36  proof (rule "dfI"[OF "fFG:1"]; rule "&I")
37    AOT_show R & F & G
38      using "cqt:2[const_var]"[axiom_inst] "&I" by metis
39  next
40    AOT_show x ([F]x  ∃!y([G]y & [R]xy)) by (rule A)
41  qed
42  AOT_show R |: F 1-1onto G
43  proof (rule "dfI"[OF "fFG:4"]; rule "&I")
44    AOT_show R |: F 1-1 G
45    proof (rule "dfI"[OF "fFG:2"]; rule "&I")
46      AOT_show R |: F  G using C.
47    next
48      AOT_show xyz ([F]x & [F]y & [G]z  ([R]xz & [R]yz  x = y))
49      proof(rule GEN; rule GEN; rule GEN; rule "→I"; rule "→I")
50        fix x y z
51        AOT_assume 1: [F]x & [F]y & [G]z
52        moreover AOT_assume 2: [R]xz & [R]yz
53        ultimately AOT_have 3: ∃!x ([F]x & [R]xz)
54          using B "&E" "∀E" "→E" by fast
55        AOT_show x = y
56          by (rule "uni-most"[THEN "→E", OF 3, THEN "∀E"(2)[where β=x],
57                              THEN "∀E"(2)[where β=y], THEN "→E"])
58             (metis "&I" "&E" 1 2)
59      qed
60    qed
61  next
62    AOT_show R |: F onto G
63    proof (rule "dfI"[OF "fFG:3"]; rule "&I")
64      AOT_show R |: F  G using C.
65    next
66      AOT_show y ([G]y  x ([F]x & [R]xy))
67      proof(rule GEN; rule "→I")
68        fix y
69        AOT_assume [G]y
70        AOT_hence ∃!x ([F]x & [R]xy)
71          using B[THEN "∀E"(2), THEN "→E"] by blast
72        AOT_hence x ([F]x & [R]xy & β (([F]β & [R]βy)  β = x))
73          using "uniqueness:1"[THEN "dfE"] by blast
74        then AOT_obtain x where [F]x & [R]xy
75          using "∃E"[rotated] "&E" by blast
76        AOT_thus x ([F]x & [R]xy) by (rule "∃I")
77      qed
78    qed
79  qed
80next
81  AOT_assume R |: F 1-1onto G
82  AOT_hence R |: F 1-1 G and R |: F onto G
83    using "dfE"[OF "fFG:4"] "&E" by blast+
84  AOT_hence C: R |: F  G
85    and D: xyz ([F]x & [F]y & [G]z  ([R]xz & [R]yz  x = y))
86    and E: y ([G]y  x ([F]x & [R]xy))
87    using "dfE"[OF "fFG:2"] "dfE"[OF "fFG:3"] "&E" by blast+
88  AOT_show R |: F 1-1 G
89  proof(rule "1-1-cor"[THEN "dfI"]; safe intro!: "&I" "cqt:2[const_var]"[axiom_inst])
90    AOT_show x ([F]x  ∃!y ([G]y & [R]xy))
91      using "dfE"[OF "fFG:1", OF C] "&E" by blast
92  next
93    AOT_show y ([G]y  ∃!x ([F]x & [R]xy))
94    proof (rule "GEN"; rule "→I")
95      fix y
96      AOT_assume 0: [G]y
97      AOT_hence x ([F]x & [R]xy)
98        using E "∀E" "→E" by fast
99      then AOT_obtain a where a_prop: [F]a & [R]ay
100        using "∃E"[rotated] by blast
101      moreover AOT_have z ([F]z & [R]zy  z = a)
102      proof (rule GEN; rule "→I")
103        fix z
104        AOT_assume [F]z & [R]zy
105        AOT_thus z = a
106          using D[THEN "∀E"(2)[where β=z], THEN "∀E"(2)[where β=a],
107                  THEN "∀E"(2)[where β=y], THEN "→E", THEN "→E"]
108                a_prop 0 "&E" "&I" by metis
109      qed
110      ultimately AOT_have x ([F]x & [R]xy & z ([F]z & [R]zy  z = x))
111        using "&I" "∃I"(2) by fast
112      AOT_thus ∃!x ([F]x & [R]xy)
113        using "uniqueness:1"[THEN "dfI"] by fast
114    qed
115  qed
116qed
117
118textWe have already introduced the restricted type of Ordinary objects in the
119     Extended Relation Comprehension theory. However, make sure all variable names
120     are defined as expected (avoiding conflicts with situations
121     of possible world theory).
122AOT_register_variable_names
123  Ordinary: u v r t s
124
125AOT_theorem "equi:1": ∃!u φ{u}  u (φ{u} & v (φ{v}  v =E u))
126proof(rule "≡I"; rule "→I")
127  AOT_assume ∃!u φ{u}
128  AOT_hence ∃!x (O!x & φ{x}).
129  AOT_hence x (O!x & φ{x} & β (O!β & φ{β}  β = x))
130    using "uniqueness:1"[THEN "dfE"] by blast
131  then AOT_obtain x where x_prop: O!x & φ{x} & β (O!β & φ{β}  β = x)
132    using "∃E"[rotated] by blast
133  {
134    fix β
135    AOT_assume beta_ord: O!β
136    moreover AOT_assume φ{β}
137    ultimately AOT_have β = x
138      using x_prop[THEN "&E"(2), THEN "∀E"(2)[where β=β]] "&I" "→E" by blast
139    AOT_hence β =E x
140      using "ord-=E=:1"[THEN "→E", OF "∨I"(1)[OF beta_ord],
141                        THEN "qml:2"[axiom_inst, THEN "→E"],
142                        THEN "≡E"(1)]
143      by blast
144  }
145  AOT_hence (O!β  (φ{β}  β =E x)) for β
146    using "→I" by blast
147  AOT_hence β(O!β  (φ{β}  β =E x))
148    by (rule GEN)
149  AOT_hence O!x & φ{x} & y (O!y  (φ{y}  y =E x))
150    using x_prop[THEN "&E"(1)] "&I" by blast
151  AOT_hence O!x & (φ{x} & y (O!y  (φ{y}  y =E x)))
152    using "&E" "&I" by meson
153  AOT_thus u (φ{u} & v (φ{v}  v =E u))
154    using "∃I" by fast
155next
156  AOT_assume u (φ{u} & v (φ{v}  v =E u))
157  AOT_hence x (O!x & (φ{x} & y (O!y  (φ{y}  y =E x))))
158    by blast
159  then AOT_obtain x where x_prop: O!x & (φ{x} & y (O!y  (φ{y}  y =E x)))
160    using "∃E"[rotated] by blast
161  AOT_have y ([O!]y & φ{y}  y = x)
162  proof(rule GEN; rule "→I")
163    fix y
164    AOT_assume O!y & φ{y}
165    AOT_hence y =E x
166      using x_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2)[where β=y]]
167            "→E" "&E" by blast
168    AOT_thus y = x
169      using "ord-=E=:1"[THEN "→E", OF "∨I"(2)[OF x_prop[THEN "&E"(1)]],
170                        THEN "qml:2"[axiom_inst, THEN "→E"], THEN "≡E"(2)] by blast
171  qed
172  AOT_hence [O!]x & φ{x} & y ([O!]y & φ{y}  y = x)
173    using x_prop "&E" "&I" by meson
174  AOT_hence x ([O!]x & φ{x} & y ([O!]y & φ{y}  y = x))
175    by (rule "∃I")
176  AOT_hence ∃!x (O!x & φ{x})
177    by (rule "uniqueness:1"[THEN "dfI"])
178  AOT_thus ∃!u φ{u}.
179qed
180
181AOT_define CorrelatesEOneToOne :: τ  τ  τ  φ (_ |: _ 1-1E _)
182  "equi:2": R |: F 1-1E G df R & F & G &
183                               u ([F]u  ∃!v([G]v & [R]uv)) &
184                               v ([G]v  ∃!u([F]u & [R]uv))
185
186AOT_define EquinumerousE :: τ  τ  φ (infixl "E" 50)
187  "equi:3": F E G df R (R |: F 1-1E G)
188
189textNote: not explicitly in PLM.
190AOT_theorem eq_den_1: Π if Π E Π'
191proof -
192  AOT_have R (R |: Π 1-1E Π')
193    using "equi:3"[THEN "dfE"] that by blast
194  then AOT_obtain R where R |: Π 1-1E Π'
195    using "∃E"[rotated] by blast
196  AOT_thus Π
197    using "equi:2"[THEN "dfE"] "&E" by blast
198qed
199
200textNote: not explicitly in PLM.
201AOT_theorem eq_den_2: Π' if Π E Π'
202proof -
203  AOT_have R (R |: Π 1-1E Π')
204    using "equi:3"[THEN "dfE"] that by blast
205  then AOT_obtain R where R |: Π 1-1E Π'
206    using "∃E"[rotated] by blast
207  AOT_thus Π'
208    using "equi:2"[THEN "dfE"] "&E" by blast+
209qed
210
211AOT_theorem "eq-part:1": F E F
212proof (safe intro!: "&I" GEN "→I" "cqt:2[const_var]"[axiom_inst]
213                    "dfI"[OF "equi:3"] "dfI"[OF "equi:2"] "∃I"(1))
214  fix x
215  AOT_assume 1: O!x
216  AOT_assume 2: [F]x
217  AOT_show ∃!v ([F]v & x =E v)
218  proof(rule "equi:1"[THEN "≡E"(2)];
219        rule "∃I"(2)[where β=x];
220        safe dest!: "&E"(2)
221             intro!:  "&I" "→I" 1 2 Ordinary.GEN "ord=Eequiv:1"[THEN "→E", OF 1])
222    AOT_show v =E x if x =E v for v
223      by (metis that "ord=Eequiv:2"[THEN "→E"])
224  qed
225next
226  fix y
227  AOT_assume 1: O!y
228  AOT_assume 2: [F]y
229  AOT_show ∃!u ([F]u & u =E y)
230    by(safe dest!: "&E"(2)
231            intro!: "equi:1"[THEN "≡E"(2)] "∃I"(2)[where β=y]
232                    "&I" "→I" 1 2 GEN "ord=Eequiv:1"[THEN "→E", OF 1])
233qed(auto simp: "=E[denotes]")
234
235
236AOT_theorem "eq-part:2": F E G  G E F
237proof (rule "→I")
238  AOT_assume F E G
239  AOT_hence R R |: F 1-1E G
240    using "equi:3"[THEN "dfE"] by blast
241  then AOT_obtain R where R |: F 1-1E G
242    using "∃E"[rotated] by blast
243  AOT_hence 0: R & F & G & u ([F]u  ∃!v([G]v & [R]uv)) &
244                            v ([G]v  ∃!u([F]u & [R]uv))
245    using "equi:2"[THEN "dfE"] by blast
246
247  AOT_have xy [R]yx] & G & F & u ([G]u  ∃!v([F]v & xy [R]yx]uv)) &
248                            v ([F]v  ∃!u([G]u & xy [R]yx]uv))
249  proof (AOT_subst xy [R]yx]yx [R]xy for: x y;
250        (safe intro!: "&I" "cqt:2[const_var]"[axiom_inst] 0[THEN "&E"(2)]
251                      0[THEN "&E"(1), THEN "&E"(2)]; "cqt:2[lambda]")?)
252    AOT_modally_strict {
253      AOT_have xy [R]yx]xy if [R]yx for y x
254        by (auto intro!: "β←C"(1) "cqt:2"
255                 simp: "&I" "ex:1:a" prod_denotesI "rule-ui:3" that)
256      moreover AOT_have [R]yx if xy [R]yx]xy for y x
257        using "β→C"(1)[where φ="λ(x,y). _ (x,y)" and κ1κn="(_,_)",
258                        simplified, OF that, simplified].
259      ultimately AOT_show xy [R]yx]αβ  [R]βα for α β
260        by (metis "deduction-theorem" "≡I")
261    }
262  qed
263  AOT_hence xy [R]yx] |: G 1-1E F
264    using "equi:2"[THEN "dfI"] by blast
265  AOT_hence R R |: G 1-1E F
266    by (rule "∃I"(1)) "cqt:2[lambda]"
267  AOT_thus G E F
268    using "equi:3"[THEN "dfI"] by blast
269qed
270
271textNote: not explicitly in PLM.
272AOT_theorem "eq-part:2[terms]": Π E Π'  Π' E Π
273  using "eq-part:2"[unvarify F G] eq_den_1 eq_den_2 "→I" by meson
274declare "eq-part:2[terms]"[THEN "→E", sym]
275
276AOT_theorem "eq-part:3": (F E G & G E H)  F E H
277proof (rule "→I")
278  AOT_assume F E G & G E H
279  then AOT_obtain R1 and R2 where
280       R1 |: F 1-1E G
281   and R2 |: G 1-1E H
282    using "equi:3"[THEN "dfE"] "&E" "∃E"[rotated] by metis
283  AOT_hence θ: u ([F]u  ∃!v([G]v & [R1]uv)) & v ([G]v  ∃!u([F]u & [R1]uv))
284        and ξ: u ([G]u  ∃!v([H]v & [R2]uv)) & v ([H]v  ∃!u([G]u & [R2]uv))
285    using "equi:2"[THEN "dfE", THEN "&E"(2)]
286          "equi:2"[THEN "dfE", THEN "&E"(1), THEN "&E"(2)]
287          "&I" by blast+
288  AOT_have R R = xy O!x & O!y & v ([G]v & [R1]xv & [R2]vy)]
289    by (rule "free-thms:3[lambda]") cqt_2_lambda_inst_prover
290  then AOT_obtain R where R_def: R = xy O!x & O!y & v ([G]v & [R1]xv & [R2]vy)]
291    using "∃E"[rotated] by blast
292  AOT_have 1: ∃!v (([H]v & [R]uv)) if a: [O!]u and b: [F]u for u
293  proof (rule "≡E"(2)[OF "equi:1"])
294    AOT_obtain b where
295      b_prop: [O!]b & ([G]b & [R1]ub & v ([G]v & [R1]uv  v =E b))
296      using θ[THEN "&E"(1), THEN "∀E"(2), THEN "→E", THEN "→E",
297              OF a b, THEN "≡E"(1)[OF "equi:1"]]
298            "∃E"[rotated] by blast
299    AOT_obtain c where
300      c_prop: "[O!]c & ([H]c & [R2]bc & v ([H]v & [R2]bv  v =E c))"
301      using ξ[THEN "&E"(1), THEN "∀E"(2)[where β=b], THEN "→E",
302              OF b_prop[THEN "&E"(1)], THEN "→E",
303              OF b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(1)],
304              THEN "≡E"(1)[OF "equi:1"]]
305    "∃E"[rotated] by blast
306    AOT_show v ([H]v & [R]uv & v' ([H]v' & [R]uv'  v' =E v))
307    proof (safe intro!: "&I" GEN "→I" "∃I"(2)[where β=c])
308      AOT_show O!c using c_prop "&E" by blast
309    next
310      AOT_show [H]c using c_prop "&E" by blast
311    next
312      AOT_have 0: [O!]u & [O!]c & v ([G]v & [R1]uv & [R2]vc)
313        by (safe intro!: "&I" a c_prop[THEN "&E"(1)] "∃I"(2)[where β=b]
314                         b_prop[THEN "&E"(1)] b_prop[THEN "&E"(2), THEN "&E"(1)]
315                         c_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)])
316      AOT_show [R]uc
317        by (auto intro: "rule=E"[rotated, OF R_def[symmetric]]
318                 intro!: "β←C"(1) "cqt:2"
319                 simp: "&I" "ex:1:a" prod_denotesI "rule-ui:3" 0)
320    next
321      fix x
322      AOT_assume ordx: O!x
323      AOT_assume [H]x & [R]ux
324      AOT_hence hx: [H]x and [R]ux using "&E" by blast+
325      AOT_hence xy O!x & O!y & v ([G]v & [R1]xv & [R2]vy)]ux
326        using "rule=E"[rotated, OF R_def] by fast
327      AOT_hence O!u & O!x & v ([G]v & [R1]uv & [R2]vx)
328        by (rule "β→C"(1)[where φ="λ(κ,κ'). _ κ κ'" and κ1κn="(_,_)", simplified])
329      then AOT_obtain z where z_prop: O!z & ([G]z & [R1]uz & [R2]zx)
330        using "&E" "∃E"[rotated] by blast
331      AOT_hence z =E b
332        using b_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2)[where β=z]]
333        using "&E" "→E" by metis
334      AOT_hence z = b
335        by (metis "=E-simple:2"[THEN "→E"])
336      AOT_hence [R2]bx
337        using z_prop[THEN "&E"(2), THEN "&E"(2)] "rule=E" by fast
338      AOT_thus x =E c
339        using c_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2)[where β=x],
340                     THEN "→E", THEN "→E", OF ordx]
341              hx "&I" by blast
342    qed
343  qed
344  AOT_have 2: ∃!u (([F]u & [R]uv)) if a: [O!]v and b: [H]v for v
345  proof (rule "≡E"(2)[OF "equi:1"])
346    AOT_obtain b where
347      b_prop: [O!]b & ([G]b & [R2]bv & u ([G]u & [R2]uv  u =E b))
348      using ξ[THEN "&E"(2), THEN "∀E"(2), THEN "→E", THEN "→E",
349              OF a b, THEN "≡E"(1)[OF "equi:1"]]
350            "∃E"[rotated] by blast
351    AOT_obtain c where
352      c_prop: "[O!]c & ([F]c & [R1]cb & v ([F]v & [R1]vb  v =E c))"
353      using θ[THEN "&E"(2), THEN "∀E"(2)[where β=b], THEN "→E",
354              OF b_prop[THEN "&E"(1)], THEN "→E",
355              OF b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(1)],
356              THEN "≡E"(1)[OF "equi:1"]]
357    "∃E"[rotated] by blast
358    AOT_show u ([F]u & [R]uv & v' ([F]v' & [R]v'v  v' =E u))
359    proof (safe intro!: "&I" GEN "→I" "∃I"(2)[where β=c])
360      AOT_show O!c using c_prop "&E" by blast
361    next
362      AOT_show [F]c using c_prop "&E" by blast
363    next
364      AOT_have [O!]c & [O!]v & u ([G]u & [R1]cu & [R2]uv)
365        by (safe intro!: "&I" a "∃I"(2)[where β=b] 
366                     c_prop[THEN "&E"(1)] b_prop[THEN "&E"(1)]
367                     b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(1)]
368                     b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)]
369                     c_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)])
370      AOT_thus [R]cv
371        by (auto intro: "rule=E"[rotated, OF R_def[symmetric]]
372                 intro!: "β←C"(1) "cqt:2"
373                 simp: "&I" "ex:1:a" prod_denotesI "rule-ui:3")
374    next
375      fix x
376      AOT_assume ordx: O!x
377      AOT_assume [F]x & [R]xv
378      AOT_hence hx: [F]x and [R]xv using "&E" by blast+
379      AOT_hence xy O!x & O!y & v ([G]v & [R1]xv & [R2]vy)]xv
380        using "rule=E"[rotated, OF R_def] by fast
381      AOT_hence O!x & O!v & u ([G]u & [R1]xu & [R2]uv)
382        by (rule "β→C"(1)[where φ="λ(κ,κ'). _ κ κ'" and κ1κn="(_,_)", simplified])
383      then AOT_obtain z where z_prop: O!z & ([G]z & [R1]xz & [R2]zv)
384        using "&E" "∃E"[rotated] by blast
385      AOT_hence z =E b
386        using b_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2)[where β=z]]
387        using "&E" "→E" "&I" by metis
388      AOT_hence z = b
389        by (metis "=E-simple:2"[THEN "→E"])
390      AOT_hence [R1]xb
391        using z_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)] "rule=E" by fast
392      AOT_thus x =E c
393        using c_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2)[where β=x],
394                     THEN "→E", THEN "→E", OF ordx]
395              hx "&I" by blast
396    qed
397  qed
398  AOT_show F E H
399    apply (rule "equi:3"[THEN "dfI"])
400    apply (rule "∃I"(2)[where β=R])
401    by (auto intro!: 1 2 "equi:2"[THEN "dfI"] "&I" "cqt:2[const_var]"[axiom_inst]
402                     Ordinary.GEN "→I" Ordinary.ψ)
403qed
404
405textNote: not explicitly in PLM.
406AOT_theorem "eq-part:3[terms]": Π E Π'' if Π E Π' and Π' E Π''
407  using "eq-part:3"[unvarify F G H, THEN "→E"] eq_den_1 eq_den_2 "→I" "&I"
408  by (metis that(1) that(2))
409declare "eq-part:3[terms]"[trans]
410
411AOT_theorem "eq-part:4": F E G  H (H E F  H E G)
412proof(rule "≡I"; rule "→I")
413  AOT_assume 0: F E G
414  AOT_hence 1: G E F using "eq-part:2"[THEN "→E"] by blast
415  AOT_show H (H E F  H E G)
416  proof (rule GEN; rule "≡I"; rule "→I")
417    AOT_show H E G if H E F for H using 0
418      by (meson "&I" "eq-part:3" that "vdash-properties:6")
419  next
420    AOT_show H E F if H E G for H using 1
421      by (metis "&I" "eq-part:3" that "vdash-properties:6")
422  qed
423next
424  AOT_assume H (H E F  H E G)
425  AOT_hence F E F  F E G using "∀E" by blast
426  AOT_thus F E G using "eq-part:1" "≡E" by blast
427qed
428
429AOT_define MapsE :: τ  τ  τ  φ ("_ |: _ ⟶E _")
430  "equi-rem:1":
431  R |: F ⟶E G df R & F & G & u ([F]u  ∃!v ([G]v & [R]uv))
432
433AOT_define MapsEOneToOne :: τ  τ  τ  φ ("_ |: _ 1-1⟶E _")
434  "equi-rem:2":
435  R |: F 1-1⟶E G df
436      R |: F ⟶E G & tuv (([F]t & [F]u & [G]v)  ([R]tv & [R]uv  t =E u))
437
438AOT_define MapsEOnto :: τ  τ  τ  φ ("_ |: _ ontoE _")
439  "equi-rem:3":
440  R |: F ontoE G df R |: F ⟶E G & v ([G]v  u ([F]u & [R]uv))
441
442AOT_define MapsEOneToOneOnto :: τ  τ  τ  φ ("_ |: _ 1-1ontoE _")
443  "equi-rem:4":
444  R |: F 1-1ontoE G df R |: F 1-1⟶E G & R |: F ontoE G
445
446AOT_theorem "equi-rem-thm":
447  R |: F 1-1E G  R |: F 1-1ontoE G
448proof -
449  AOT_have R |: F 1-1E G  R |: x O!x & [F]x] 1-1 x O!x & [G]x]
450  proof(safe intro!: "≡I" "→I" "&I")
451    AOT_assume R |: F 1-1E G
452    AOT_hence u ([F]u  ∃!v ([G]v & [R]uv))
453          and v ([G]v  ∃!u ([F]u & [R]uv))
454      using "equi:2"[THEN "dfE"] "&E" by blast+
455    AOT_hence a: ([F]u  ∃!v ([G]v & [R]uv))
456          and b: ([G]v  ∃!u ([F]u & [R]uv)) for u v
457      using "Ordinary.∀E" by fast+
458    AOT_have (x [O!]x & [F]x]x  ∃!y (x [O!]x & [G]x]y & [R]xy)) for x
459      apply (AOT_subst x [O!]x & [F]x]x [O!]x & [F]x)
460       apply (rule "beta-C-meta"[THEN "→E"])
461       apply "cqt:2[lambda]"
462      apply (AOT_subst x [O!]x & [G]x]x [O!]x & [G]x for: x)
463       apply (rule "beta-C-meta"[THEN "→E"])
464       apply "cqt:2[lambda]"
465      apply (AOT_subst O!y & [G]y & [R]xy O!y & ([G]y & [R]xy) for: y)
466       apply (meson "≡E"(6) "Associativity of &" "oth-class-taut:3:a")
467      apply (rule "→I") apply (frule "&E"(1)) apply (drule "&E"(2))
468      by (fact a[unconstrain u, THEN "→E", THEN "→E", of x])
469    AOT_hence A: x (x [O!]x & [F]x]x  ∃!y (x [O!]x & [G]x]y & [R]xy))
470      by (rule GEN)
471    AOT_have (x [O!]x & [G]x]y  ∃!x (x [O!]x & [F]x]x & [R]xy)) for y
472      apply (AOT_subst x [O!]x & [G]x]y [O!]y & [G]y)
473       apply (rule "beta-C-meta"[THEN "→E"])
474       apply "cqt:2[lambda]"
475      apply (AOT_subst x [O!]x & [F]x]x [O!]x & [F]x for: x)
476       apply (rule "beta-C-meta"[THEN "→E"])
477       apply "cqt:2[lambda]"
478      apply (AOT_subst O!x & [F]x & [R]xy O!x & ([F]x & [R]xy) for: x)
479       apply (meson "≡E"(6) "Associativity of &" "oth-class-taut:3:a")
480      apply (rule "→I") apply (frule "&E"(1)) apply (drule "&E"(2))
481      by (fact b[unconstrain v, THEN "→E", THEN "→E", of y])
482    AOT_hence B: y (x [O!]x & [G]x]y  ∃!x (x [O!]x & [F]x]x & [R]xy))
483      by (rule GEN)
484    AOT_show R |: x [O!]x & [F]x] 1-1 x [O!]x & [G]x]
485      by (safe intro!: "1-1-cor"[THEN "dfI"] "&I"
486                       "cqt:2[const_var]"[axiom_inst] A B)
487          "cqt:2[lambda]"+
488  next
489    AOT_assume R |: x [O!]x & [F]x] 1-1 x [O!]x & [G]x]
490    AOT_hence a: (x [O!]x & [F]x]x  ∃!y (x [O!]x & [G]x]y & [R]xy)) and 
491              b: (x [O!]x & [G]x]y  ∃!x (x [O!]x & [F]x]x & [R]xy)) for x y
492      using "1-1-cor"[THEN "dfE"] "&E" "∀E"(2) by blast+
493    AOT_have [F]u  ∃!v ([G]v & [R]uv) for u
494    proof (safe intro!: "→I")
495      AOT_assume fu: [F]u
496      AOT_have 0: x [O!]x & [F]x]u
497        by (auto intro!: "β←C"(1) "cqt:2" "cqt:2[const_var]"[axiom_inst]
498                         Ordinary.ψ fu "&I")
499      AOT_show ∃!v ([G]v & [R]uv)
500        apply (AOT_subst [O!]x & ([G]x & [R]ux)
501                         ([O!]x & [G]x) & [R]ux for: x)
502         apply (simp add: "Associativity of &")
503        apply (AOT_subst (reverse) [O!]x & [G]x
504                                   x [O!]x & [G]x]x for: x)
505         apply (rule "beta-C-meta"[THEN "→E"])
506         apply "cqt:2[lambda]"
507        using a[THEN "→E", OF 0] by blast
508    qed
509    AOT_hence A: u ([F]u  ∃!v ([G]v & [R]uv))
510      by (rule Ordinary.GEN)
511    AOT_have [G]v  ∃!u ([F]u & [R]uv) for v
512    proof (safe intro!: "→I")
513      AOT_assume gu: [G]v
514      AOT_have 0: x [O!]x & [G]x]v
515        by (auto intro!: "β←C"(1) "cqt:2" "cqt:2[const_var]"[axiom_inst]
516                         Ordinary.ψ gu "&I")
517      AOT_show ∃!u ([F]u & [R]uv)
518        apply (AOT_subst [O!]x & ([F]x & [R]xv) ([O!]x & [F]x) & [R]xv for: x)
519         apply (simp add: "Associativity of &")
520        apply (AOT_subst (reverse) [O!]x & [F]xx [O!]x & [F]x]x  for: x)
521         apply (rule "beta-C-meta"[THEN "→E"])
522         apply "cqt:2[lambda]"
523        using b[THEN "→E", OF 0] by blast
524    qed
525    AOT_hence B: v ([G]v  ∃!u ([F]u & [R]uv)) by (rule Ordinary.GEN)
526    AOT_show R |: F 1-1E G
527      by (safe intro!: "equi:2"[THEN "dfI"] "&I" A B "cqt:2[const_var]"[axiom_inst])
528  qed
529  also AOT_have   R |: F 1-1ontoE G
530  proof(safe intro!: "≡I" "→I" "&I")
531    AOT_assume R |: x [O!]x & [F]x] 1-1 x [O!]x & [G]x]
532    AOT_hence a: (x [O!]x & [F]x]x  ∃!y (x [O!]x & [G]x]y & [R]xy)) and 
533              b: (x [O!]x & [G]x]y  ∃!x (x [O!]x & [F]x]x & [R]xy)) for x y
534      using "1-1-cor"[THEN "dfE"] "&E" "∀E"(2) by blast+
535    AOT_show R |: F 1-1ontoE G
536    proof (safe intro!: "equi-rem:4"[THEN "dfI"] "&I" "equi-rem:3"[THEN "dfI"]
537                        "equi-rem:2"[THEN "dfI"] "equi-rem:1"[THEN "dfI"]
538                        "cqt:2[const_var]"[axiom_inst] Ordinary.GEN "→I")
539      fix u
540      AOT_assume fu: [F]u
541      AOT_have 0: x [O!]x & [F]x]u
542        by (auto intro!: "β←C"(1) "cqt:2" "cqt:2[const_var]"[axiom_inst]
543                         Ordinary.ψ fu "&I")
544      AOT_hence 1: ∃!y (x [O!]x & [G]x]y & [R]uy)
545        using a[THEN "→E"] by blast
546      AOT_show ∃!v ([G]v & [R]uv)
547        apply (AOT_subst [O!]x & ([G]x & [R]ux) ([O!]x & [G]x) & [R]ux for: x)
548         apply (simp add: "Associativity of &")
549        apply (AOT_subst (reverse) [O!]x & [G]x x [O!]x & [G]x]x for: x)
550         apply (rule "beta-C-meta"[THEN "→E"])
551         apply "cqt:2[lambda]"
552        by (fact 1)
553    next
554      fix t u v
555      AOT_assume [F]t & [F]u & [G]v and rtv_tuv: [R]tv & [R]uv
556      AOT_hence oft: x O!x & [F]x]t and
557                ofu: x O!x & [F]x]u and
558                ogv: x O!x & [G]x]v
559        by (auto intro!: "β←C"(1) "cqt:2" "&I"
560                 simp: Ordinary.ψ dest: "&E")
561      AOT_hence ∃!x (x [O!]x & [F]x]x & [R]xv)
562        using b[THEN "→E"] by blast
563      then AOT_obtain a where
564          a_prop: x [O!]x & [F]x]a & [R]av &
565                   x ((x [O!]x & [F]x]x & [R]xv)  x = a)
566        using "uniqueness:1"[THEN "dfE"] "∃E"[rotated] by blast
567      AOT_hence ua: u = a
568        using ofu rtv_tuv[THEN "&E"(2)] "∀E"(2) "→E" "&I" "&E"(2) by blast
569      moreover AOT_have ta: t = a
570        using a_prop oft rtv_tuv[THEN "&E"(1)] "∀E"(2) "→E" "&I" "&E"(2) by blast
571      ultimately AOT_have t = u by (metis "rule=E" id_sym)
572      AOT_thus t =E u
573        using "rule=E" id_sym "ord=Eequiv:1" Ordinary.ψ ta ua "→E" by fast
574    next
575      fix u
576      AOT_assume [F]u
577      AOT_hence x O!x & [F]x]u
578        by (auto intro!: "β←C"(1) "cqt:2" "&I"
579                 simp: "cqt:2[const_var]"[axiom_inst]  Ordinary.ψ)
580      AOT_hence ∃!y (x [O!]x & [G]x]y & [R]uy)
581        using a[THEN "→E"] by blast
582      then AOT_obtain a where
583        a_prop: x [O!]x & [G]x]a & [R]ua &
584                 x ((x [O!]x & [G]x]x & [R]ux)  x = a)
585        using "uniqueness:1"[THEN "dfE"] "∃E"[rotated] by blast
586      AOT_have O!a & [G]a
587        by (rule "β→C"(1)) (auto simp: a_prop[THEN "&E"(1), THEN "&E"(1)])
588      AOT_hence O!a and [G]a using "&E" by blast+
589      moreover AOT_have v ([G]v & [R]uv  v =E a)
590      proof(safe intro!: Ordinary.GEN "→I"; frule "&E"(1); drule "&E"(2))
591        fix v
592        AOT_assume [G]v and ruv: [R]uv
593        AOT_hence x [O!]x & [G]x]v
594          by (auto intro!: "β←C"(1) "cqt:2" "&I" simp: Ordinary.ψ)
595        AOT_hence v = a
596          using a_prop[THEN "&E"(2), THEN "∀E"(2), THEN "→E", OF "&I"] ruv by blast
597        AOT_thus v =E a
598          using "rule=E" "ord=Eequiv:1" Ordinary.ψ "→E" by fast
599      qed
600      ultimately AOT_have O!a & ([G]a & [R]ua & v' ([G]v' & [R]uv'  v' =E a))
601        using "∃I" "&I" a_prop[THEN "&E"(1), THEN "&E"(2)] by simp
602      AOT_hence v ([G]v & [R]uv & v' ([G]v' & [R]uv'  v' =E v))
603        by (rule "∃I")
604      AOT_thus ∃!v ([G]v & [R]uv)
605        by (rule "equi:1"[THEN "≡E"(2)])
606    next
607      fix v
608      AOT_assume [G]v
609      AOT_hence x O!x & [G]x]v
610        by (auto intro!: "β←C"(1) "cqt:2" "&I" Ordinary.ψ)
611      AOT_hence ∃!x (x [O!]x & [F]x]x & [R]xv)
612        using b[THEN "→E"] by blast
613      then AOT_obtain a where
614        a_prop: x [O!]x & [F]x]a & [R]av &
615                 y (x [O!]x & [F]x]y & [R]yv  y = a)
616        using "uniqueness:1"[THEN "dfE", THEN "∃E"[rotated]] by blast
617      AOT_have O!a & [F]a
618        by (rule "β→C"(1)) (auto simp: a_prop[THEN "&E"(1), THEN "&E"(1)])
619      AOT_hence O!a & ([F]a & [R]av)
620        using a_prop[THEN "&E"(1), THEN "&E"(2)] "&E" "&I" by metis
621      AOT_thus u ([F]u & [R]uv)
622        by (rule "∃I")
623    qed
624  next
625    AOT_assume R |: F 1-1ontoE G
626    AOT_hence 1: R |: F 1-1⟶E G
627          and 2: R |: F ontoE G
628      using "equi-rem:4"[THEN "dfE"] "&E" by blast+
629    AOT_hence 3: R |: F ⟶E G
630          and A: t u v ([F]t & [F]u & [G]v  ([R]tv & [R]uv  t =E u))
631      using "equi-rem:2"[THEN "dfE", OF 1] "&E" by blast+
632    AOT_hence B: u ([F]u  ∃!v ([G]v & [R]uv))
633      using "equi-rem:1"[THEN "dfE"] "&E" by blast
634    AOT_have C: v ([G]v  u ([F]u & [R]uv))
635      using "equi-rem:3"[THEN "dfE", OF 2] "&E" by blast
636    AOT_show R |: x [O!]x & [F]x] 1-1 x [O!]x & [G]x]
637    proof (rule "1-1-cor"[THEN "dfI"];
638           safe intro!: "&I" "cqt:2" GEN "→I")
639      fix x
640      AOT_assume 1: x [O!]x & [F]x]x
641      AOT_have O!x & [F]x
642        by (rule "β→C"(1)) (auto simp: 1)
643      AOT_hence ∃!v ([G]v & [R]xv)
644        using B[THEN "∀E"(2), THEN "→E", THEN "→E"] "&E" by blast
645      then AOT_obtain y where
646        y_prop: O!y & ([G]y & [R]xy & u ([G]u & [R]xu  u =E y))
647        using "equi:1"[THEN "≡E"(1)] "∃E"[rotated] by fastforce
648      AOT_hence x O!x & [G]x]y
649        by (auto intro!: "β←C"(1) "cqt:2" "&I" dest: "&E")
650      moreover AOT_have z (x O!x & [G]x]z & [R]xz  z = y)
651      proof(safe intro!: GEN "→I"; frule "&E"(1); drule "&E"(2))
652        fix z
653        AOT_assume 1: x [O!]x & [G]x]z
654        AOT_have 2: O!z & [G]z
655          by (rule "β→C"(1)) (auto simp: 1)
656        moreover AOT_assume [R]xz
657        ultimately AOT_have z =E y
658          using y_prop[THEN "&E"(2), THEN "&E"(2), THEN "∀E"(2),
659                       THEN "→E", THEN "→E", rotated, OF "&I"] "&E"
660          by blast
661        AOT_thus z = y
662          using 2[THEN "&E"(1)] by (metis "=E-simple:2" "→E")
663      qed
664      ultimately AOT_have x O!x & [G]x]y & [R]xy &
665                           z (x O!x & [G]x]z & [R]xz  z = y)
666        using y_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)] "&I" by auto
667      AOT_hence y (x O!x & [G]x]y & [R]xy &
668                    z (x O!x & [G]x]z & [R]xz  z = y))
669        by (rule "∃I")
670      AOT_thus ∃!y (x [O!]x & [G]x]y & [R]xy)
671        using "uniqueness:1"[THEN "dfI"] by fast
672    next
673      fix y
674      AOT_assume 1: x [O!]x & [G]x]y
675      AOT_have oy_gy: O!y & [G]y
676        by (rule "β→C"(1)) (auto simp: 1)
677      AOT_hence u ([F]u & [R]uy)
678        using C[THEN "∀E"(2), THEN "→E", THEN "→E"] "&E" by blast
679      then AOT_obtain x where x_prop: O!x & ([F]x & [R]xy)
680        using "∃E"[rotated] by blast
681      AOT_hence ofx: x O!x & [F]x]x
682        by (auto intro!: "β←C"(1) "cqt:2" "&I" dest: "&E")
683      AOT_have α (x [O!]x & [F]x]α & [R]αy &
684                    β (x [O!]x & [F]x]β & [R]βy  β = α))
685      proof (safe intro!: "∃I"(2)[where β=x] "&I" GEN "→I")
686        AOT_show x O!x & [F]x]x using ofx.
687      next
688        AOT_show [R]xy using x_prop[THEN "&E"(2), THEN "&E"(2)].
689      next
690        fix z
691        AOT_assume 1: x [O!]x & [F]x]z & [R]zy
692        AOT_have oz_fz: O!z & [F]z
693          by (rule "β→C"(1)) (auto simp: 1[THEN "&E"(1)])
694        AOT_have z =E x
695          using A[THEN "∀E"(2)[where β=z], THEN "→E", THEN "∀E"(2)[where β=x],
696                  THEN "→E", THEN "∀E"(2)[where β=y], THEN "→E",
697                  THEN "→E", THEN "→E", OF oz_fz[THEN "&E"(1)],
698                  OF x_prop[THEN "&E"(1)], OF oy_gy[THEN "&E"(1)], OF "&I", OF "&I",
699                  OF oz_fz[THEN "&E"(2)], OF x_prop[THEN "&E"(2), THEN "&E"(1)],
700                  OF oy_gy[THEN "&E"(2)], OF "&I", OF 1[THEN "&E"(2)],
701                  OF x_prop[THEN "&E"(2), THEN "&E"(2)]].
702        AOT_thus z = x
703          by (metis "=E-simple:2" "vdash-properties:10")
704      qed
705      AOT_thus ∃!x (x [O!]x & [F]x]x & [R]xy)
706        by (rule "uniqueness:1"[THEN "dfI"])
707    qed
708  qed
709  finally show ?thesis.
710qed
711
712AOT_theorem "empty-approx:1": (¬u [F]u & ¬v [H]v)  F E H
713proof(rule "→I"; frule "&E"(1); drule "&E"(2))
714  AOT_assume 0: ¬u [F]u and 1: ¬v [H]v
715  AOT_have u ([F]u  ∃!v ([H]v & [R]uv)) for R
716  proof(rule Ordinary.GEN; rule "→I"; rule "raa-cor:1")
717    fix u
718    AOT_assume [F]u
719    AOT_hence u [F]u using "Ordinary.∃I" "&I" by fast
720    AOT_thus u [F]u & ¬u [F]u using "&I" 0 by blast
721  qed
722  moreover AOT_have v ([H]v  ∃!u ([F]u & [R]uv)) for R
723  proof(rule Ordinary.GEN; rule "→I"; rule "raa-cor:1")
724    fix v
725    AOT_assume [H]v
726    AOT_hence v [H]v using "Ordinary.∃I" "&I" by fast
727    AOT_thus v [H]v & ¬v [H]v using 1 "&I" by blast
728  qed
729  ultimately AOT_have R |: F 1-1E H for R
730    apply (safe intro!: "equi:2"[THEN "dfI"] "&I" GEN "cqt:2[const_var]"[axiom_inst])
731    using "∀E" by blast+
732  AOT_hence R R |: F 1-1E H by (rule "∃I")
733  AOT_thus F E H
734    by (rule "equi:3"[THEN "dfI"])
735qed
736
737AOT_theorem "empty-approx:2": (u [F]u & ¬v [H]v)  ¬(F E H)
738proof(rule "→I"; frule "&E"(1); drule "&E"(2); rule "raa-cor:2")
739  AOT_assume 1: u [F]u and 2: ¬v [H]v
740  AOT_obtain b where b_prop: O!b & [F]b
741    using 1 "∃E"[rotated] by blast
742  AOT_assume F E H
743  AOT_hence R R |: F 1-1E H
744    by (rule "equi:3"[THEN "dfE"])
745  then AOT_obtain R where R |: F 1-1E H
746    using "∃E"[rotated] by blast
747  AOT_hence θ: u ([F]u  ∃!v ([H]v & [R]uv))
748    using "equi:2"[THEN "dfE"] "&E" by blast+
749  AOT_have ∃!v ([H]v & [R]bv) for u
750    using θ[THEN "∀E"(2)[where β=b], THEN "→E", THEN "→E",
751            OF b_prop[THEN "&E"(1)], OF b_prop[THEN "&E"(2)]].
752  AOT_hence v ([H]v & [R]bv & u ([H]u & [R]bu  u =E v))
753    by (rule "equi:1"[THEN "≡E"(1)])
754  then AOT_obtain x where O!x & ([H]x & [R]bx & u ([H]u & [R]bu  u =E x))
755    using "∃E"[rotated] by blast
756  AOT_hence O!x & [H]x using "&E" "&I" by blast
757  AOT_hence v [H]v by (rule "∃I")
758  AOT_thus v [H]v & ¬v [H]v using 2 "&I" by blast
759qed
760
761
762AOT_define FminusU :: Π  τ  Π ("_-_")
763  "F-u": [F]-x =df z [F]z & z E x]
764
765textNote: not explicitly in PLM.
766AOT_theorem "F-u[den]": [F]-x
767  by (rule "=dfI"(1)[OF "F-u", where τ1τn="(_,_)", simplified]; "cqt:2[lambda]")
768AOT_theorem "F-u[equiv]": [[F]-x]y  ([F]y & y E x)
769  by (auto intro: "F-u"[THEN "=dfI"(1), where τ1τn="(_,_)", simplified]
770           intro!: "cqt:2" "beta-C-cor:2"[THEN "→E", THEN "∀E"(2)])
771
772AOT_theorem eqP': F E G & [F]u & [G]v  [F]-u E [G]-v
773proof (rule "→I"; frule "&E"(2); drule "&E"(1); frule "&E"(2); drule "&E"(1))
774  AOT_assume F E G
775  AOT_hence R R |: F 1-1E G
776    using "equi:3"[THEN "dfE"] by blast
777  then AOT_obtain R where R_prop: R |: F 1-1E G
778    using "∃E"[rotated] by blast
779  AOT_hence A: u ([F]u  ∃!v ([G]v & [R]uv))
780        and B: v ([G]v  ∃!u ([F]u & [R]uv))
781    using "equi:2"[THEN "dfE"] "&E" by blast+
782  AOT_have R |: F 1-1ontoE G
783    using "equi-rem-thm"[THEN "≡E"(1), OF R_prop].
784  AOT_hence R |: F 1-1⟶E G & R |: F ontoE G
785    using "equi-rem:4"[THEN "dfE"] by blast
786  AOT_hence C: tuv (([F]t & [F]u & [G]v)  ([R]tv & [R]uv  t =E u))
787    using "equi-rem:2"[THEN "dfE"] "&E" by blast
788  AOT_assume fu: [F]u
789  AOT_assume gv: [G]v
790  AOT_have z [Π]z & z E κ] for Π κ
791    by "cqt:2[lambda]"
792  note Π_minus_κI = "rule-id-df:2:b[2]"[
793      where τ=(λ(Π, κ). «[Π]-κ»), simplified, OF "F-u", simplified, OF this]
794   and Π_minus_κE = "rule-id-df:2:a[2]"[
795      where τ=(λ(Π, κ). «[Π]-κ»), simplified, OF "F-u", simplified, OF this]
796  AOT_have Π_minus_κ_den: [Π]-κ for Π κ
797    by (rule Π_minus_κI) "cqt:2[lambda]"+
798  {
799    fix R
800    AOT_assume R_prop: R |: F 1-1E G
801    AOT_hence A: u ([F]u  ∃!v ([G]v & [R]uv))
802          and B: v ([G]v  ∃!u ([F]u & [R]uv))
803      using "equi:2"[THEN "dfE"] "&E" by blast+
804    AOT_have R |: F 1-1ontoE G
805      using "equi-rem-thm"[THEN "≡E"(1), OF R_prop].
806    AOT_hence R |: F 1-1⟶E G & R |: F ontoE G
807      using "equi-rem:4"[THEN "dfE"] by blast
808    AOT_hence C: tuv (([F]t & [F]u & [G]v)  ([R]tv & [R]uv  t =E u))
809      using "equi-rem:2"[THEN "dfE"] "&E" by blast
810
811    AOT_assume Ruv: [R]uv
812    AOT_have R |: [F]-u 1-1E [G]-v
813    proof(safe intro!: "equi:2"[THEN "dfI"] "&I" "cqt:2[const_var]"[axiom_inst]
814                       Π_minus_κ_den Ordinary.GEN "→I")
815      fix u'
816      AOT_assume [[F]-u]u'
817      AOT_hence 0: z [F]z & z E u]u'
818        using Π_minus_κE by fast
819      AOT_have 0: [F]u' & u' E u
820        by (rule "β→C"(1)[where κ1κn="AOT_term_of_var (Ordinary.Rep u')"]) (fact 0)
821      AOT_have ∃!v ([G]v & [R]u'v)
822        using A[THEN "Ordinary.∀E"[where α=u'], THEN "→E", OF 0[THEN "&E"(1)]].
823      then AOT_obtain v' where
824        v'_prop: [G]v' & [R]u'v' &  t ([G]t & [R]u't  t =E v')
825        using "equi:1"[THEN "≡E"(1)] "Ordinary.∃E"[rotated] by fastforce
826
827      AOT_show ∃!v' ([[G]-v]v' & [R]u'v')
828      proof (safe intro!: "equi:1"[THEN "≡E"(2)] "Ordinary.∃I"[where β=v']
829                          "&I" Ordinary.GEN "→I")
830        AOT_show [[G]-v]v'
831        proof (rule Π_minus_κI; 
832               safe intro!: "β←C"(1) "cqt:2" "&I" "thm-neg=E"[THEN "≡E"(2)])
833          AOT_show [G]v' using v'_prop "&E" by blast
834        next
835          AOT_show ¬v' =E v
836          proof (rule "raa-cor:2")
837            AOT_assume v' =E v
838            AOT_hence v' = v by (metis "=E-simple:2" "→E")
839            AOT_hence Ruv': [R]uv' using "rule=E" Ruv id_sym by fast
840            AOT_have u' =E u
841              by (rule C[THEN "Ordinary.∀E", THEN "Ordinary.∀E",
842                         THEN "Ordinary.∀E"[where α=v'], THEN "→E", THEN "→E"])
843                 (safe intro!: "&I" 0[THEN "&E"(1)] fu
844                               v'_prop[THEN "&E"(1), THEN "&E"(1)]
845                               Ruv' v'_prop[THEN "&E"(1), THEN "&E"(2)])
846            moreover AOT_have ¬(u' =E u)
847              using "0" "&E"(2) "≡E"(1) "thm-neg=E" by blast
848            ultimately AOT_show u' =E u & ¬u' =E u using "&I" by blast
849          qed
850        qed
851      next
852        AOT_show [R]u'v' using v'_prop "&E" by blast
853      next
854        fix t
855        AOT_assume t_prop: [[G]-v]t & [R]u't
856        AOT_have gt_t_noteq_v: [G]t & t E v
857          apply (rule "β→C"(1)[where κ1κn="AOT_term_of_var (Ordinary.Rep t)"])
858          apply (rule Π_minus_κE)
859          by (fact t_prop[THEN "&E"(1)])
860        AOT_show t =E v'
861          using v'_prop[THEN "&E"(2), THEN "Ordinary.∀E", THEN "→E",
862                        OF "&I", OF gt_t_noteq_v[THEN "&E"(1)],
863                        OF t_prop[THEN "&E"(2)]].
864      qed
865    next
866      fix v'
867      AOT_assume G_minus_v_v': [[G]-v]v'
868      AOT_have gt_t_noteq_v: [G]v' & v' E v
869        apply (rule "β→C"(1)[where κ1κn="AOT_term_of_var (Ordinary.Rep v')"])
870        apply (rule Π_minus_κE)
871        by (fact G_minus_v_v')
872      AOT_have ∃!u([F]u & [R]uv')
873        using B[THEN "Ordinary.∀E", THEN "→E", OF gt_t_noteq_v[THEN "&E"(1)]].
874      then AOT_obtain u' where
875        u'_prop: [F]u' & [R]u'v' & t ([F]t & [R]tv'  t =E u')
876        using "equi:1"[THEN "≡E"(1)] "Ordinary.∃E"[rotated] by fastforce
877      AOT_show ∃!u' ([[F]-u]u' & [R]u'v')
878      proof (safe intro!: "equi:1"[THEN "≡E"(2)] "Ordinary.∃I"[where β=u'] "&I"
879                          u'_prop[THEN "&E"(1), THEN "&E"(2)] Ordinary.GEN "→I")
880        AOT_show [[F]-u]u'
881        proof (rule Π_minus_κI;
882               safe intro!: "β←C"(1) "cqt:2" "&I" "thm-neg=E"[THEN "≡E"(2)]
883               u'_prop[THEN "&E"(1), THEN "&E"(1)]; rule "raa-cor:2")
884          AOT_assume u'_eq_u: u' =E u
885          AOT_hence u' = u
886            using "=E-simple:2" "vdash-properties:10" by blast
887          AOT_hence Ru'v: [R]u'v using "rule=E" Ruv id_sym by fast
888          AOT_have v' E v
889            using "&E"(2) gt_t_noteq_v by blast
890          AOT_hence v'_noteq_v: ¬(v' =E v) by (metis "≡E"(1) "thm-neg=E")
891          AOT_have u ([G]u & [R]u'u & v ([G]v & [R]u'v  v =E u))
892            using A[THEN "Ordinary.∀E", THEN "→E",
893                    OF u'_prop[THEN "&E"(1), THEN "&E"(1)],
894                    THEN "equi:1"[THEN "≡E"(1)]].
895          then AOT_obtain t where
896            t_prop: [G]t & [R]u't & v ([G]v & [R]u'v  v =E t)
897            using "Ordinary.∃E"[rotated] by meson
898          AOT_have v =E t if [G]v and [R]u'v for v
899            using t_prop[THEN "&E"(2), THEN "Ordinary.∀E", THEN "→E",
900                         OF "&I", OF that].
901          AOT_hence v' =E t and v =E t
902            by (auto simp: gt_t_noteq_v[THEN "&E"(1)] Ru'v gv
903                           u'_prop[THEN "&E"(1), THEN "&E"(2)])
904          AOT_hence v' =E v
905            using "rule=E" "=E-simple:2" id_sym "→E" by fast
906          AOT_thus v' =E v & ¬v' =E v
907            using v'_noteq_v "&I" by blast
908        qed
909      next
910        fix t
911        AOT_assume 0: [[F]-u]t & [R]tv'
912        moreover AOT_have [F]t & t E u
913          apply (rule "β→C"(1)[where κ1κn="AOT_term_of_var (Ordinary.Rep t)"])
914          apply (rule Π_minus_κE)
915          by (fact 0[THEN "&E"(1)])
916        ultimately AOT_show t =E u'
917          using u'_prop[THEN "&E"(2), THEN "Ordinary.∀E", THEN "→E", OF "&I"]
918                "&E" by blast
919      qed
920    qed
921    AOT_hence R R |: [F]-u 1-1E [G]-v
922      by (rule "∃I")
923  } note 1 = this
924  moreover {
925    AOT_assume not_Ruv: ¬[R]uv
926    AOT_have ∃!v ([G]v & [R]uv)
927      using A[THEN "Ordinary.∀E", THEN "→E", OF fu].
928    then AOT_obtain b where
929      b_prop: O!b & ([G]b & [R]ub & t([G]t & [R]ut  t =E b))
930      using "equi:1"[THEN "≡E"(1)] "∃E"[rotated] by fastforce
931    AOT_hence ob: O!b and gb: [G]b and Rub: [R]ub
932      using "&E" by blast+
933    AOT_have O!t  ([G]t & [R]ut  t =E b) for t
934      using b_prop "&E"(2) "∀E"(2) by blast
935    AOT_hence b_unique: t =E b if O!t and [G]t and [R]ut for t
936      by (metis Adjunction "modus-tollens:1" "reductio-aa:1" that)
937    AOT_have not_v_eq_b: ¬(v =E b)
938    proof(rule "raa-cor:2")
939      AOT_assume v =E b
940      AOT_hence 0: v = b
941        by (metis "=E-simple:2" "→E")
942      AOT_have [R]uv
943        using b_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)]
944              "rule=E"[rotated, OF 0[symmetric]] by fast
945      AOT_thus [R]uv & ¬[R]uv
946        using not_Ruv "&I" by blast
947    qed
948    AOT_have not_b_eq_v: ¬(b =E v)
949      using "modus-tollens:1" not_v_eq_b "ord=Eequiv:2" by blast
950    AOT_have ∃!u ([F]u & [R]uv)
951      using B[THEN "Ordinary.∀E", THEN "→E", OF gv].
952    then AOT_obtain a where
953      a_prop: O!a & ([F]a & [R]av & t([F]t & [R]tv  t =E a))
954      using "equi:1"[THEN "≡E"(1)] "∃E"[rotated] by fastforce
955    AOT_hence Oa: O!a and fa: [F]a and Rav: [R]av
956      using "&E" by blast+
957    AOT_have O!t  ([F]t & [R]tv  t =E a) for t
958      using a_prop "&E" "∀E"(2) by blast
959    AOT_hence a_unique: t =E a if O!t and [F]t and [R]tv for t
960      by (metis Adjunction "modus-tollens:1" "reductio-aa:1" that) 
961    AOT_have not_u_eq_a: ¬(u =E a)
962    proof(rule "raa-cor:2")
963      AOT_assume u =E a
964      AOT_hence 0: u = a
965        by (metis "=E-simple:2" "→E")
966      AOT_have [R]uv
967        using a_prop[THEN "&E"(2), THEN "&E"(1), THEN "&E"(2)]
968              "rule=E"[rotated, OF 0[symmetric]] by fast
969      AOT_thus [R]uv & ¬[R]uv
970        using not_Ruv "&I" by blast
971    qed
972    AOT_have not_a_eq_u: ¬(a =E u)
973      using "modus-tollens:1" not_u_eq_a "ord=Eequiv:2" by blast
974    let ?R = «u'v' (u' E u & v' E v & [R]u'v') 
975                      (u' =E a & v' =E b) 
976                      (u' =E u & v' =E v)]»
977    AOT_have [«?R»] by "cqt:2[lambda]"
978    AOT_hence  β β = [«?R»]
979      using "free-thms:1" "≡E"(1) by fast
980    then AOT_obtain R1 where R1_def: R1 = [«?R»]
981      using "∃E"[rotated] by blast
982    AOT_have Rxy1: [R]xy if [R1]xy and x E u and x E a for x y
983    proof -
984      AOT_have 0: [«?R»]xy
985        by (rule "rule=E"[rotated, OF R1_def]) (fact that(1))
986      AOT_have (x E u & y E v & [R]xy)  (x =E a & y =E b)  (x =E u & y =E v)
987        using "β→C"(1)[OF 0] by simp
988      AOT_hence x E u & y E v & [R]xy using that(2,3)
989        by (metis "∨E"(3) "Conjunction Simplification"(1) "≡E"(1)
990                  "modus-tollens:1" "thm-neg=E")
991      AOT_thus [R]xy using "&E" by blast+
992    qed
993    AOT_have Rxy2: [R]xy  if [R1]xy and y E v and y E b for x y
994    proof -
995      AOT_have 0: [«?R»]xy
996        by (rule "rule=E"[rotated, OF R1_def]) (fact that(1))
997      AOT_have (x E u & y E v & [R]xy)  (x =E a & y =E b)  (x =E u & y =E v)
998        using "β→C"(1)[OF 0] by simp
999      AOT_hence x E u & y E v & [R]xy
1000        using that(2,3)
1001        by (metis "∨E"(3) "Conjunction Simplification"(2) "≡E"(1)
1002                  "modus-tollens:1" "thm-neg=E")
1003      AOT_thus [R]xy using "&E" by blast+
1004    qed
1005    AOT_have R1xy: [R1]xy if [R]xy and x E u and y E v for x y
1006      by (rule "rule=E"[rotated, OF R1_def[symmetric]])
1007         (auto intro!: "β←C"(1) "cqt:2"
1008                 simp: "&I" "ex:1:a" prod_denotesI "rule-ui:3" that "∨I"(1))
1009    AOT_have R1ab: [R1]ab
1010      apply (rule "rule=E"[rotated, OF R1_def[symmetric]])
1011      apply (safe intro!: "β←C"(1) "cqt:2" prod_denotesI "&I")
1012      by (meson a_prop b_prop "&I" "&E"(1) "∨I"(1) "∨I"(2) "ord=Eequiv:1" "→E")
1013    AOT_have R1uv: [R1]uv
1014      apply (rule "rule=E"[rotated, OF R1_def[symmetric]])
1015      apply (safe intro!: "β←C"(1) "cqt:2" prod_denotesI "&I")
1016      by (meson "&I" "∨I"(2) "ord=Eequiv:1" Ordinary.ψ "→E")
1017    moreover AOT_have R1 |: F 1-1E G
1018    proof (safe intro!: "equi:2"[THEN "dfI"] "&I" "cqt:2" Ordinary.GEN "→I")
1019      fix u'
1020      AOT_assume fu': [F]u'
1021      {
1022        AOT_assume not_u'_eq_u: ¬(u' =E u) and not_u'_eq_a: ¬(u' =E a)
1023        AOT_hence u'_noteq_u: u' E u and u'_noteq_a: u' E a
1024          by (metis "≡E"(2) "thm-neg=E")+
1025        AOT_have ∃!v ([G]v & [R]u'v)
1026          using A[THEN "Ordinary.∀E", THEN "→E", OF fu'].
1027        AOT_hence v ([G]v & [R]u'v & t ([G]t & [R]u't  t =E v))
1028          using "equi:1"[THEN "≡E"(1)] by simp
1029        then AOT_obtain v' where
1030          v'_prop: [G]v' & [R]u'v' & t ([G]t & [R]u't  t =E v')
1031          using "Ordinary.∃E"[rotated] by meson
1032        AOT_hence gv': [G]v' and Ru'v': [R]u'v'
1033          using "&E" by blast+
1034        AOT_have not_v'_eq_v: ¬v' =E v
1035        proof (rule "raa-cor:2")
1036          AOT_assume v' =E v
1037          AOT_hence v' = v
1038            by (metis "=E-simple:2" "→E")
1039          AOT_hence Ru'v: [R]u'v
1040            using "rule=E" Ru'v' by fast
1041          AOT_have u' =E a
1042            using a_unique[OF Ordinary.ψ, OF fu', OF Ru'v].
1043          AOT_thus u' =E a & ¬u' =E a
1044            using not_u'_eq_a "&I" by blast
1045        qed
1046        AOT_hence v'_noteq_v: v' E v
1047          using "≡E"(2) "thm-neg=E" by blast
1048        AOT_have t ([G]t & [R]u't  t =E v')
1049          using v'_prop "&E" by blast
1050        AOT_hence [G]t & [R]u't  t =E v' for t
1051          using "Ordinary.∀E" by meson
1052        AOT_hence v'_unique: t =E v' if [G]t and [R]u't for t
1053          by (metis "&I" that "→E")
1054
1055        AOT_have [G]v' & [R1]u'v' & t ([G]t & [R1]u't  t =E v')
1056        proof (safe intro!: "&I" gv' R1xy Ru'v' u'_noteq_u u'_noteq_a "→I"
1057                            Ordinary.GEN "thm-neg=E"[THEN "≡E"(2)] not_v'_eq_v)
1058          fix t
1059          AOT_assume 1: [G]t & [R1]u't
1060          AOT_have [R]u't
1061            using Rxy1[OF 1[THEN "&E"(2)], OF u'_noteq_u, OF u'_noteq_a].
1062          AOT_thus t =E v'
1063            using v'_unique 1[THEN "&E"(1)] by blast
1064        qed
1065        AOT_hence v ([G]v & [R1]u'v & t ([G]t & [R1]u't  t =E v))
1066          by (rule "Ordinary.∃I")
1067        AOT_hence ∃!v ([G]v & [R1]u'v)
1068          by (rule "equi:1"[THEN "≡E"(2)])
1069      }
1070      moreover {
1071        AOT_assume 0: u' =E u
1072        AOT_hence u'_eq_u: u' = u
1073          using "=E-simple:2" "→E" by blast
1074        AOT_have ∃!v ([G]v & [R1]u'v)
1075        proof (safe intro!: "equi:1"[THEN "≡E"(2)] "Ordinary.∃I"[where β=v]
1076                            "&I" Ordinary.GEN "→I" gv)
1077          AOT_show [R1]u'v
1078            apply (rule "rule=E"[rotated, OF R1_def[symmetric]])
1079            apply (safe intro!: "β←C"(1) "cqt:2" "&I" prod_denotesI)
1080            by (safe intro!: "∨I"(2) "&I" 0 "ord=Eequiv:1"[THEN "→E", OF Ordinary.ψ])
1081        next
1082          fix v'
1083          AOT_assume [G]v' & [R1]u'v'
1084          AOT_hence 0: [R1]uv'
1085            using "rule=E"[rotated, OF u'_eq_u] "&E"(2) by fast
1086          AOT_have 1: [«?R»]uv'
1087            by (rule "rule=E"[rotated, OF R1_def]) (fact 0)
1088          AOT_have 2: (u E u & v' E v & [R]uv') 
1089                       (u =E a & v' =E b) 
1090                       (u =E u & v' =E v)
1091            using "β→C"(1)[OF 1] by simp
1092          AOT_have ¬u E u
1093            using "≡E"(4) "modus-tollens:1" "ord=Eequiv:1" Ordinary.ψ
1094                  "reductio-aa:2" "thm-neg=E" by blast
1095          AOT_hence ¬((u E u & v' E v & [R]uv')  (u =E a & v' =E b))
1096            using not_u_eq_a
1097            by (metis "∨E"(2) "Conjunction Simplification"(1)
1098                      "modus-tollens:1" "reductio-aa:1")
1099          AOT_hence (u =E u & v' =E v)
1100            using 2 by (metis "∨E"(2))
1101          AOT_thus v' =E v
1102            using "&E" by blast