diff --git a/thys/ZFC_in_HOL/Cantor_NF.thy b/thys/ZFC_in_HOL/Cantor_NF.thy
new file mode 100644
--- /dev/null
+++ b/thys/ZFC_in_HOL/Cantor_NF.thy
@@ -0,0 +1,1423 @@
+section \<open>Cantor Normal Form\<close>
+
+theory Cantor_NF
+  imports Ordinal_Exp
+begin
+
+subsection \<open>Cantor normal form\<close>
+
+text \<open>Lemma 5.1\<close>
+lemma cnf_1:
+  assumes \<alpha>: "\<alpha> \<in> elts \<beta>" "Ord \<beta>" and "m > 0"
+  shows "\<omega>\<up>\<alpha> * ord_of_nat n < \<omega>\<up>\<beta> * ord_of_nat m"
+proof -
+  have \<dagger>: "\<omega>\<up>succ \<alpha> \<le> \<omega>\<up>\<beta>"
+    using Ord_mem_iff_less_TC assms oexp_mono succ_le_TC_iff by auto
+  have "\<omega>\<up>\<alpha> * ord_of_nat n < \<omega>\<up>\<alpha> * \<omega>"
+    using Ord_in_Ord OrdmemD assms by auto
+  also have "\<dots> = \<omega>\<up>succ \<alpha>"
+    using Ord_in_Ord \<alpha> by auto
+  also have "\<dots> \<le> \<omega>\<up>\<beta>"
+    using "\<dagger>" by blast
+  also have "\<dots> \<le> \<omega>\<up>\<beta> * ord_of_nat m"
+    using \<open>m > 0\<close> le_mult by auto
+  finally show ?thesis .
+qed
+
+
+fun Cantor_sum  where
+  Cantor_sum_Nil: "Cantor_sum [] ms = 0"
+| Cantor_sum_Nil2: "Cantor_sum (\<alpha>#\<alpha>s) [] = 0"
+| Cantor_sum_Cons: "Cantor_sum (\<alpha>#\<alpha>s) (m#ms) = (\<omega>\<up>\<alpha>) * ord_of_nat m + Cantor_sum \<alpha>s ms"
+
+
+abbreviation Cantor_dec :: "V list \<Rightarrow> bool" where
+  "Cantor_dec \<equiv> sorted_wrt (>)"
+
+lemma Ord_Cantor_sum:
+  assumes "List.set \<alpha>s \<subseteq> ON"
+  shows "Ord (Cantor_sum \<alpha>s ms)"
+  using assms
+proof (induction \<alpha>s arbitrary: ms)
+  case (Cons a \<alpha>s ms)
+  then show ?case
+    by (cases ms) auto
+qed auto
+
+lemma Cantor_dec_Cons_iff [simp]: "Cantor_dec (\<alpha>#\<beta>#\<beta>s) \<longleftrightarrow> \<beta> < \<alpha> \<and> Cantor_dec (\<beta>#\<beta>s)"
+  by auto
+
+
+text \<open>Lemma 5.2. The second and third premises aren't really necessary, but their
+      removal requires quite a lot of work.\<close>
+lemma cnf_2:
+  assumes "List.set (\<alpha>#\<alpha>s) \<subseteq> ON" "list.set ms \<subseteq> {0<..}" "length \<alpha>s = length ms"
+    and "Cantor_dec (\<alpha>#\<alpha>s)"
+  shows "\<omega>\<up>\<alpha> > Cantor_sum \<alpha>s ms"
+  using assms
+proof (induction ms arbitrary: \<alpha> \<alpha>s)
+  case Nil
+  then obtain \<alpha>0 where \<alpha>0: "(\<alpha>#\<alpha>s) = [\<alpha>0]"
+    by (metis length_0_conv)
+  then have "Ord \<alpha>0"
+    using Nil.prems(1) by auto
+  then show ?case
+    using \<alpha>0 zero_less_Limit by auto
+next
+  case (Cons m1 ms)
+  then obtain \<alpha>0 \<alpha>1 \<alpha>s' where \<alpha>01: "(\<alpha>#\<alpha>s) = \<alpha>0#\<alpha>1#\<alpha>s'"
+    by (metis (no_types, lifting) Cons.prems(3) Suc_length_conv)
+  then have "Ord \<alpha>0" "Ord \<alpha>1"
+    using Cons.prems(1) \<alpha>01 by auto
+  have *: "\<omega>\<up>\<alpha>0 * ord_of_nat 1 > \<omega>\<up>\<alpha>1 * ord_of_nat m1"
+  proof (rule cnf_1)
+    show "\<alpha>1 \<in> elts \<alpha>0"
+      using Cons.prems \<alpha>01 by (simp add: Ord_mem_iff_lt \<open>Ord \<alpha>0\<close> \<open>Ord \<alpha>1\<close>)
+  qed (use \<open>Ord \<alpha>0\<close> in auto)
+  show ?case
+  proof (cases ms)
+    case Nil
+    then show ?thesis
+      using * one_V_def Cons.prems(3) \<alpha>01 by auto
+  next
+    case (Cons m2 ms')
+    then obtain \<alpha>2 \<alpha>s'' where \<alpha>02: "(\<alpha>#\<alpha>s) = \<alpha>0#\<alpha>1#\<alpha>2#\<alpha>s''"
+      by (metis Cons.prems(3) Suc_length_conv \<alpha>01 length_tl list.sel(3))
+    then have "Ord \<alpha>2"
+      using Cons.prems(1) by auto
+    have "m1 > 0" "m2 > 0"
+      using Cons.prems Cons by auto
+    have "\<omega>\<up>\<alpha>1 * ord_of_nat m1 + \<omega>\<up>\<alpha>1 * ord_of_nat m1 = (\<omega>\<up>\<alpha>1 * ord_of_nat m1) * ord_of_nat 2"
+      by (simp add: mult_succ eval_nat_numeral)
+    also have "\<dots> < \<omega>\<up>\<alpha>0"
+      using cnf_1 [of concl: "\<alpha>1" "m1 * 2" "\<alpha>0" 1] Cons.prems \<alpha>01 one_V_def
+      by (simp add: mult.assoc ord_of_nat_mult Ord_mem_iff_lt)
+    finally have II: "\<omega>\<up>\<alpha>1 * ord_of_nat m1 + \<omega>\<up>\<alpha>1 * ord_of_nat m1 < \<omega>\<up>\<alpha>0"
+      by simp
+    have "Cantor_sum (tl \<alpha>s) ms < \<omega>\<up>hd \<alpha>s"
+    proof (rule Cons.IH)
+      show "Cantor_dec (hd \<alpha>s # tl \<alpha>s)"
+        using \<open>Cantor_dec (\<alpha>#\<alpha>s)\<close> \<alpha>01 by auto
+    qed (use Cons.prems \<alpha>01 in auto)
+    then have "Cantor_sum (\<alpha>2 # \<alpha>s'') ms < \<omega>\<up>\<alpha>1"
+      using \<alpha>02 by auto
+    also have "\<dots> \<le> \<omega>\<up>\<alpha>1 * ord_of_nat m1"
+      by (simp add: \<open>0 < m1\<close> le_mult)
+    finally show ?thesis
+      using II \<alpha>02 dual_order.strict_trans by fastforce
+  qed
+qed
+
+proposition Cantor_nf_exists:
+  assumes "Ord \<alpha>"
+  obtains \<alpha>s ms where "List.set \<alpha>s \<subseteq> ON" "list.set ms \<subseteq> {0<..}" "length \<alpha>s = length ms"
+    and "Cantor_dec \<alpha>s"
+    and "\<alpha> = Cantor_sum \<alpha>s ms"
+  using assms
+proof (induction \<alpha> arbitrary: thesis rule: Ord_induct)
+  case (step \<alpha>)
+  show ?case
+  proof (cases "\<alpha> = 0")
+    case True
+    have "Cantor_sum [] [] = 0"
+      by simp
+    with True show ?thesis
+      using length_pos_if_in_set step.prems subset_eq
+      by (metis length_0_conv not_gr_zero sorted_wrt.simps(1))
+  next
+    case False
+    define \<alpha>hat where "\<alpha>hat \<equiv> Sup {\<gamma> \<in> ON. \<omega>\<up>\<gamma> \<le> \<alpha>}"
+    then have "Ord \<alpha>hat"
+      using Ord_Sup assms by fastforce
+    have "\<And>\<xi>. \<lbrakk>Ord \<xi>; \<omega>\<up>\<xi> \<le> \<alpha>\<rbrakk> \<Longrightarrow> \<xi> \<le> \<omega>\<up>\<alpha>"
+      by (metis Ord_\<omega> OrdmemD le_oexp' order_trans step.hyps one_V_def succ_in_omega zero_in_omega)
+    then have "{\<gamma> \<in> ON. \<omega>\<up>\<gamma> \<le> \<alpha>} \<subseteq> elts (succ (\<omega>\<up>\<alpha>))"
+      using Ord_mem_iff_lt step.hyps by force
+    then have sma: "small {\<gamma> \<in> ON. \<omega>\<up>\<gamma> \<le> \<alpha>}"
+      by (meson down)
+    have le: "\<omega>\<up>\<alpha>hat \<le> \<alpha>"
+    proof (rule ccontr)
+      assume "\<not> \<omega>\<up>\<alpha>hat \<le> \<alpha>"
+      then have \<dagger>: "\<alpha> \<in> elts (\<omega>\<up>\<alpha>hat)"
+        by (meson Ord_\<omega> Ord_linear2 Ord_mem_iff_lt Ord_oexp \<open>Ord \<alpha>hat\<close> step.hyps)
+      obtain \<gamma> where "Ord \<gamma>" "\<omega>\<up>\<gamma> \<le> \<alpha>" "\<alpha> < \<gamma>"
+        using \<open>Ord \<alpha>hat\<close>
+      proof (cases \<alpha>hat rule: Ord_cases)
+        case 0
+        with \<dagger> show thesis
+          by (auto simp: False)
+      next
+        case (succ \<beta>)
+        have "succ \<beta> \<in> {\<gamma> \<in> ON. \<omega>\<up>\<gamma> \<le> \<alpha>}"
+          by (rule succ_in_Sup_Ord) (use succ \<alpha>hat_def sma in auto)
+        then have "\<omega>\<up>succ \<beta> \<le> \<alpha>"
+          by blast
+        with \<dagger> show thesis
+          using \<open>\<not> \<omega>\<up>\<alpha>hat \<le> \<alpha>\<close> succ by blast
+      next
+        case limit
+        with \<dagger> show thesis
+          apply (clarsimp simp: oexp_Limit \<alpha>hat_def)
+          by (meson Ord_\<omega> Ord_in_Ord Ord_linear_le mem_not_refl oexp_mono_le omega_nonzero vsubsetD)
+      qed
+      then show False
+        by (metis Ord_\<omega> OrdmemD leD le_less_trans le_oexp' one_V_def succ_in_omega zero_in_omega)
+    qed
+    have False if "\<nexists>M. \<alpha> < \<omega>\<up>\<alpha>hat * ord_of_nat M"
+    proof -
+      have \<dagger>: "\<omega>\<up>\<alpha>hat * ord_of_nat M \<le> \<alpha>" for M
+        by (meson that Ord_\<omega> Ord_linear2 Ord_mult Ord_oexp Ord_ord_of_nat \<open>Ord \<alpha>hat\<close> step.hyps)
+      have "\<not> \<omega>\<up>succ \<alpha>hat \<le> \<alpha>"
+        using Ord_mem_iff_lt \<alpha>hat_def \<open>Ord \<alpha>hat\<close> sma elts_succ by blast
+      then have "\<alpha> < \<omega>\<up>succ \<alpha>hat"
+        by (meson Ord_\<omega> Ord_linear2 Ord_oexp Ord_succ \<open>Ord \<alpha>hat\<close> step.hyps)
+      also have "\<dots> = \<omega>\<up>\<alpha>hat * \<omega>"
+        using \<open>Ord \<alpha>hat\<close> oexp_succ by blast
+      also have "\<dots> = Sup (range (\<lambda>m. \<omega>\<up>\<alpha>hat * ord_of_nat m))"
+        by (simp add: mult_Limit) (auto simp: \<omega>_def image_image)
+      also have "\<dots> \<le> \<alpha>"
+        using \<dagger> by blast
+      finally show False
+        by simp
+    qed
+    then obtain M where M: "\<omega>\<up>\<alpha>hat * ord_of_nat M > \<alpha>"
+      by blast
+    have bound: "i \<le> M" if "\<omega>\<up>\<alpha>hat * ord_of_nat i \<le> \<alpha>" for i
+    proof -
+      have "\<omega>\<up>\<alpha>hat * ord_of_nat i < \<omega>\<up>\<alpha>hat * ord_of_nat M"
+        using M dual_order.strict_trans2 that by blast
+      then show ?thesis
+        using \<open>Ord \<alpha>hat\<close> less_V_def by auto
+    qed
+    define mhat where "mhat \<equiv> Greatest (\<lambda>m. \<omega>\<up>\<alpha>hat * ord_of_nat m \<le> \<alpha>)"
+    have mhat_ge: "m \<le> mhat" if "\<omega>\<up>\<alpha>hat * ord_of_nat m \<le> \<alpha>" for m
+      unfolding mhat_def
+      by (metis (mono_tags, lifting) Greatest_le_nat bound that)
+    have mhat: "\<omega>\<up>\<alpha>hat * ord_of_nat mhat \<le> \<alpha>"
+      unfolding mhat_def
+      by (rule GreatestI_nat [where k=0 and b=M]) (use bound in auto)
+    then obtain \<xi> where "Ord \<xi>" "\<xi> \<le> \<alpha>" and \<xi>: "\<alpha> = \<omega>\<up>\<alpha>hat * ord_of_nat mhat + \<xi>"
+      by (metis Ord_\<omega> Ord_mult Ord_oexp Ord_ord_of_nat \<open>Ord \<alpha>hat\<close> step.hyps le_Ord_diff)
+    have False if "\<xi> = \<alpha>"
+    proof -
+      have "\<xi> \<ge> \<omega>\<up>\<alpha>hat"
+        by (simp add: le that)
+      then obtain \<zeta> where "Ord \<zeta>" "\<zeta> \<le> \<xi>" and \<zeta>: "\<xi> = \<omega>\<up>\<alpha>hat + \<zeta>"
+        by (metis Ord_\<omega> Ord_oexp \<open>Ord \<alpha>hat\<close> \<open>Ord \<xi>\<close> le_Ord_diff)
+      then have "\<alpha> = \<omega>\<up>\<alpha>hat * ord_of_nat mhat + \<omega>\<up>\<alpha>hat + \<zeta>"
+        by (simp add: \<xi> add.assoc)
+      then have "\<omega>\<up>\<alpha>hat * ord_of_nat (Suc mhat) \<le> \<alpha>"
+        by (metis add_le_cancel_left add.right_neutral le_0 mult_succ ord_of_nat.simps(2))
+      then show False
+        using Suc_n_not_le_n mhat_ge by blast
+    qed
+    then have \<xi>in\<alpha>: "\<xi> \<in> elts \<alpha>"
+      using Ord_mem_iff_lt \<open>Ord \<xi>\<close> \<open>\<xi> \<le> \<alpha>\<close> less_V_def step.hyps by auto
+    show thesis
+    proof (cases "\<xi> = 0")
+      case True
+      show thesis
+      proof (rule step.prems)
+        show "\<alpha> = Cantor_sum [\<alpha>hat] [mhat]"
+          by (simp add: True \<xi>)
+      qed (use \<xi> True \<open>\<alpha> \<noteq> 0\<close> \<open>Ord \<alpha>hat\<close> in auto)
+    next
+      case False
+      obtain \<beta>s ns where sub: "List.set \<beta>s \<subseteq> ON" "list.set ns \<subseteq> {0<..}"
+        and len_eq: "length \<beta>s = length ns"
+        and dec: "Cantor_dec \<beta>s"
+        and \<xi>eq: "\<xi> = Cantor_sum \<beta>s ns"
+        using step.IH [OF \<xi>in\<alpha>] by blast
+      then have "length \<beta>s > 0" "length ns > 0"
+        using False Cantor_sum.simps(1) \<open>\<xi> = Cantor_sum \<beta>s ns\<close> by auto
+      then obtain \<beta>0 n0 \<beta>s' ns' where \<beta>0: "\<beta>s = \<beta>0 # \<beta>s'" and "Ord \<beta>0"
+        and n0: "ns = n0 # ns'" and "n0 > 0"
+        using sub by (auto simp: neq_Nil_conv)
+      moreover have False if "\<beta>0 > \<alpha>hat"
+      proof -
+        have "\<omega>\<up>\<beta>0 \<le> \<omega>\<up>\<beta>0 * ord_of_nat n0 + u" for u
+          using \<open>n0 > 0\<close>
+          by (metis add_le_cancel_left Ord_ord_of_nat add.right_neutral dual_order.trans gr_implies_not_zero le_0 le_mult ord_of_eq_0_iff)
+        moreover have "\<omega>\<up>\<beta>0 > \<alpha>"
+          using that \<open>Ord \<beta>0\<close>
+          by (metis (no_types, lifting) Ord_\<omega> Ord_linear2 Ord_oexp Sup_upper \<alpha>hat_def leD mem_Collect_eq sma step.hyps)
+        ultimately have "\<xi> \<ge> \<omega>\<up>\<beta>0"
+          by (simp add: \<xi>eq \<beta>0 n0)
+        then show ?thesis
+          using \<open>\<alpha> < \<omega>\<up>\<beta>0\<close> \<open>\<xi> \<le> \<alpha>\<close> by auto
+      qed
+      ultimately have "\<beta>0 \<le> \<alpha>hat"
+        using Ord_linear2 \<open>Ord \<alpha>hat\<close> by auto
+      then consider "\<beta>0 < \<alpha>hat" | "\<beta>0 = \<alpha>hat"
+        using dual_order.order_iff_strict by auto
+      then show ?thesis
+      proof cases
+        case 1
+        show ?thesis
+        proof (rule step.prems)
+          show "list.set (\<alpha>hat#\<beta>s) \<subseteq> ON"
+            using sub by (auto simp: \<open>Ord \<alpha>hat\<close>)
+          show "list.set (mhat#ns) \<subseteq> {0::nat<..}"
+            using sub using \<open>\<xi> = \<alpha> \<Longrightarrow> False\<close> \<xi> by fastforce
+          show "Cantor_dec (\<alpha>hat#\<beta>s)"
+            using that \<open>\<beta>0 < \<alpha>hat\<close> \<open>Ord \<alpha>hat\<close> \<open>Ord \<beta>0\<close> Ord_mem_iff_lt \<beta>0 dec less_Suc_eq_0_disj
+            by (force simp: \<beta>0 n0)
+          show "length (\<alpha>hat#\<beta>s) = length (mhat#ns)"
+            by (auto simp: len_eq)
+          show "\<alpha> = Cantor_sum (\<alpha>hat#\<beta>s) (mhat#ns)"
+            by (simp add: \<xi> \<xi>eq \<beta>0 n0)
+        qed
+      next
+        case 2
+        show ?thesis
+        proof (rule step.prems)
+          show "list.set \<beta>s \<subseteq> ON"
+            by (simp add: sub(1))
+          show "list.set ((n0+mhat)#ns') \<subseteq> {0::nat<..}"
+            using n0 sub(2) by auto
+          show "length (\<beta>s::V list) = length ((n0+mhat)#ns')"
+            by (simp add: len_eq n0)
+          show "Cantor_dec \<beta>s"
+            using that \<beta>0 dec by auto
+          show "\<alpha> = Cantor_sum \<beta>s ((n0+mhat)#ns')"
+            using 2
+            by (simp add: add_mult_distrib \<beta>0 \<xi> \<xi>eq add.assoc add.commute n0 ord_of_nat_add)
+        qed
+      qed
+    qed
+  qed
+qed
+
+lemma Cantor_sum_0E:
+  assumes "Cantor_sum \<alpha>s ms = 0" "List.set \<alpha>s \<subseteq> ON" "list.set ms \<subseteq> {0<..}" "length \<alpha>s = length ms"
+  shows "\<alpha>s = []"
+  using assms
+proof (induction \<alpha>s arbitrary: ms)
+  case Nil
+  then show ?case
+    by auto
+next
+  case (Cons a list)
+  then obtain m ms' where "ms = m#ms'" "m \<noteq> 0" "list.set ms' \<subseteq> {0<..}"
+    by simp (metis Suc_length_conv greaterThan_iff insert_subset list.set(2))
+  with Cons show ?case by auto
+qed
+
+
+lemma Cantor_nf_unique_aux:
+  assumes "Ord \<alpha>"
+    and \<alpha>sON: "List.set \<alpha>s \<subseteq> ON"
+    and \<beta>sON: "List.set \<beta>s \<subseteq> ON"
+    and ms: "list.set ms \<subseteq> {0<..}"
+    and ns: "list.set ns \<subseteq> {0<..}"
+    and mseq: "length \<alpha>s = length ms"
+    and nseq: "length \<beta>s = length ns"
+    and \<alpha>sdec: "Cantor_dec \<alpha>s"
+    and \<beta>sdec: "Cantor_dec \<beta>s"
+    and \<alpha>seq: "\<alpha> = Cantor_sum \<alpha>s ms"
+    and \<beta>seq: "\<alpha> = Cantor_sum \<beta>s ns"
+  shows "\<alpha>s = \<beta>s \<and> ms = ns"
+  using assms
+proof (induction \<alpha> arbitrary: \<alpha>s ms \<beta>s ns rule: Ord_induct)
+  case (step \<alpha>)
+  show ?case
+  proof (cases "\<alpha> = 0")
+    case True
+    then show ?thesis
+      using step.prems by (metis Cantor_sum_0E length_0_conv)
+  next
+    case False
+    then obtain \<alpha>0 \<alpha>s' \<beta>0 \<beta>s' where \<alpha>s: "\<alpha>s = \<alpha>0 # \<alpha>s'" and \<beta>s: "\<beta>s = \<beta>0 # \<beta>s'"
+      by (metis Cantor_sum.simps(1) min_list.cases step.prems(9,10))
+    then have ON: "Ord \<alpha>0" "list.set \<alpha>s' \<subseteq> ON" "Ord \<beta>0" "list.set \<beta>s' \<subseteq> ON"
+      using \<alpha>s \<beta>s step.prems(1,2) by auto
+    then obtain m0 ms' n0 ns' where ms: "ms = m0 # ms'" and ns: "ns = n0 # ns'"
+      by (metis \<alpha>s \<beta>s length_0_conv list.distinct(1) list.exhaust step.prems(5,6))
+    then have nz: "m0 \<noteq> 0" "list.set ms' \<subseteq> {0<..}" "n0 \<noteq> 0" "list.set ns' \<subseteq> {0<..}"
+      using ms ns step.prems(3,4) by auto
+    have False if "\<beta>0 < \<alpha>0"
+    proof -
+      have Ordc: "Ord (Cantor_sum \<beta>s ns)" "Ord (\<omega>\<up>\<alpha>0)"
+        using Ord_oexp \<open>Ord \<alpha>0\<close>  step.hyps step.prems(10) by blast+
+      have *: "Cantor_sum \<beta>s ns < \<omega>\<up>\<alpha>0"
+        using step.prems(2-6) \<open>Ord \<alpha>0\<close> \<open>Cantor_dec \<beta>s\<close> that \<beta>s cnf_2
+        by (metis Cantor_dec_Cons_iff insert_subset list.set(2) mem_Collect_eq)
+      then show False
+        by (metis Cantor_sum_Cons Ord_mem_iff_lt Ord_ord_of_nat Ordc \<alpha>s \<open>m0 \<noteq> 0\<close> * le_mult ms not_add_mem_right ord_of_eq_0 step.prems(9,10) vsubsetD)
+    qed
+    moreover
+    have False if "\<alpha>0 < \<beta>0"
+    proof -
+      have Ordc: "Ord (Cantor_sum \<alpha>s ms)" "Ord (\<omega>\<up>\<beta>0)"
+        using Ord_oexp \<open>Ord \<beta>0\<close>  step.hyps step.prems(9) by blast+
+      have *: "Cantor_sum \<alpha>s ms < \<omega>\<up>\<beta>0"
+        using step.prems(1-5) \<open>Ord \<beta>0\<close> \<open>Cantor_dec \<alpha>s\<close> that \<alpha>s cnf_2
+        by (metis Cantor_dec_Cons_iff \<beta>s insert_subset list.set(2))
+      then show False
+        by (metis Cantor_sum_Cons Ord_mem_iff_lt Ord_ord_of_nat Ordc \<beta>s \<open>n0 \<noteq> 0\<close> * le_mult not_add_mem_right ns ord_of_eq_0 step.prems(9,10) vsubsetD)
+    qed
+    ultimately have 1: "\<alpha>0 = \<beta>0"
+      using Ord_linear_lt \<open>Ord \<alpha>0\<close> \<open>Ord \<beta>0\<close> by blast
+    have False if "m0 < n0"
+    proof -
+      have "\<omega>\<up>\<alpha>0 > Cantor_sum \<alpha>s' ms'"
+        using \<alpha>s \<open>list.set ms' \<subseteq> {0<..}\<close> cnf_2 ms step.prems(1,5,7) by auto
+      then have "\<alpha> < \<omega>\<up>\<alpha>0 * ord_of_nat m0 + \<omega>\<up>\<alpha>0"
+        by (simp add: \<alpha>s ms step.prems(9))
+      also have "\<dots> = \<omega>\<up>\<alpha>0 * ord_of_nat (Suc m0)"
+        by (simp add: mult_succ)
+      also have "\<dots> \<le> \<omega>\<up>\<alpha>0 * ord_of_nat n0"
+        by (meson Ord_\<omega> Ord_oexp Ord_ord_of_nat Suc_leI \<open>Ord \<alpha>0\<close> mult_cancel_le_iff ord_of_nat_mono_iff that)
+      also have "\<dots> \<le> \<alpha>"
+        by (metis Cantor_sum_Cons add_le_cancel_left \<beta>s \<open>\<alpha>0 = \<beta>0\<close> add.right_neutral le_0 ns step.prems(10))
+      finally show False
+        by blast
+    qed
+    moreover have False if "n0 < m0"
+    proof -
+      have "\<omega>\<up>\<beta>0 > Cantor_sum \<beta>s' ns'"
+        using \<beta>s \<open>list.set ns' \<subseteq> {0<..}\<close> cnf_2 ns step.prems(2,6,8) by auto
+      then have "\<alpha> < \<omega>\<up>\<beta>0 * ord_of_nat n0 + \<omega>\<up>\<beta>0"
+        by (simp add: \<beta>s ns step.prems(10))
+      also have "\<dots> = \<omega>\<up>\<beta>0 * ord_of_nat (Suc n0)"
+        by (simp add: mult_succ)
+      also have "\<dots> \<le> \<omega>\<up>\<beta>0 * ord_of_nat m0"
+        by (meson Ord_\<omega> Ord_oexp Ord_ord_of_nat Suc_leI \<open>Ord \<beta>0\<close> mult_cancel_le_iff ord_of_nat_mono_iff that)
+      also have "\<dots> \<le> \<alpha>"
+        by (metis Cantor_sum_Cons add_le_cancel_left \<alpha>s \<open>\<alpha>0 = \<beta>0\<close> add.right_neutral le_0 ms step.prems(9))
+      finally show False
+        by blast
+    qed
+    ultimately have 2: "m0 = n0"
+      using nat_neq_iff by blast
+    have "\<alpha>s' = \<beta>s' \<and> ms' = ns'"
+    proof (rule step.IH)
+      have "Cantor_sum \<alpha>s' ms' < \<omega>\<up>\<alpha>0"
+        using \<alpha>s cnf_2 ms nz(2) step.prems(1) step.prems(5) step.prems(7) by auto
+      also have "\<dots> \<le> Cantor_sum \<alpha>s ms"
+        apply (simp add: \<alpha>s \<beta>s ms ns)
+        by (metis Cantor_sum_Cons add_less_cancel_left ON(1) Ord_\<omega> Ord_linear2 Ord_oexp Ord_ord_of_nat \<alpha>s add.right_neutral dual_order.strict_trans1 le_mult ms not_less_0 nz(1) ord_of_eq_0 step.hyps step.prems(9))
+      finally show "Cantor_sum \<alpha>s' ms' \<in> elts \<alpha>"
+        using ON(2) Ord_Cantor_sum Ord_mem_iff_lt step.hyps step.prems(9) by blast
+      show "length \<alpha>s' = length ms'" "length \<beta>s' = length ns'"
+        using \<alpha>s ms \<beta>s ns step.prems by auto
+      show "Cantor_dec \<alpha>s'" "Cantor_dec \<beta>s'"
+        using \<alpha>s \<beta>s step.prems(7,8) by auto
+      have "Cantor_sum \<alpha>s ms = Cantor_sum \<beta>s ns"
+        using step.prems(9,10) by auto
+      then show "Cantor_sum \<alpha>s' ms' = Cantor_sum \<beta>s' ns'"
+        using 1 2 by (simp add: \<alpha>s \<beta>s ms ns)
+    qed (use ON nz in auto)
+    then show ?thesis
+      using 1 2 by (simp add: \<alpha>s \<beta>s ms ns)
+  qed
+qed
+
+
+proposition Cantor_nf_unique:
+  assumes "Cantor_sum \<alpha>s ms = Cantor_sum \<beta>s ns"
+    and \<alpha>sON: "List.set \<alpha>s \<subseteq> ON"
+    and \<beta>sON: "List.set \<beta>s \<subseteq> ON"
+    and ms: "list.set ms \<subseteq> {0<..}"
+    and ns: "list.set ns \<subseteq> {0<..}"
+    and mseq: "length \<alpha>s = length ms"
+    and nseq: "length \<beta>s = length ns"
+    and \<alpha>sdec: "Cantor_dec \<alpha>s"
+    and \<beta>sdec: "Cantor_dec \<beta>s"
+  shows "\<alpha>s = \<beta>s \<and> ms = ns"
+  using Cantor_nf_unique_aux Ord_Cantor_sum assms  by auto
+
+
+lemma less_\<omega>_power:
+  assumes "Ord \<alpha>1" "Ord \<beta>"
+    and \<alpha>2: "\<alpha>2 \<in> elts \<alpha>1" and \<beta>: "\<beta> < \<omega>\<up>\<alpha>2"
+    and "m1 > 0" "m2 > 0"
+  shows "\<omega>\<up>\<alpha>2 * ord_of_nat m2 + \<beta> < \<omega>\<up>\<alpha>1 * ord_of_nat m1 + (\<omega>\<up>\<alpha>2 * ord_of_nat m2 + \<beta>)"
+        (is "?lhs < ?rhs")
+proof -
+  obtain oo: "Ord (\<omega>\<up>\<alpha>1)" "Ord (\<omega>\<up>\<alpha>2)"
+    using Ord_in_Ord Ord_oexp assms by blast
+  moreover obtain "ord_of_nat m2 \<noteq> 0"
+    using assms ord_of_eq_0 by blast
+  ultimately have "\<beta> < \<omega>\<up>\<alpha>2 * ord_of_nat m2"
+    by (meson Ord_ord_of_nat \<beta> dual_order.strict_trans1 le_mult)
+  with oo assms have "?lhs \<noteq> ?rhs"
+    by (metis Ord_mult Ord_ord_of_nat add_strict_mono add.assoc cnf_1 not_add_less_right oo)
+  then show ?thesis
+    by (simp add: add_le_left \<open>Ord \<beta>\<close> less_V_def oo)
+qed
+
+lemma Cantor_sum_ge:
+  assumes "List.set (\<alpha>#\<alpha>s) \<subseteq> ON" "list.set ms \<subseteq> {0<..}" "length ms > 0"
+  shows "\<omega> \<up> \<alpha> \<le> Cantor_sum (\<alpha>#\<alpha>s) ms"
+proof -
+  obtain m ns where ms: "ms = Cons m ns"
+    using assms(3) strict_sorted.cases by auto
+  then have "\<omega> \<up> \<alpha> \<le> \<omega> \<up> \<alpha> * ord_of_nat m"
+    using assms(2) le_mult by auto
+  then show ?thesis
+    using dual_order.trans ms by auto
+qed
+
+subsection \<open>Simplified Cantor normal form\<close>
+
+text \<open>No coefficients, and the exponents decreasing non-strictly\<close>
+
+fun \<omega>_sum  where
+  \<omega>_sum_Nil: "\<omega>_sum [] = 0"
+| \<omega>_sum_Cons: "\<omega>_sum (\<alpha>#\<alpha>s) = (\<omega>\<up>\<alpha>) + \<omega>_sum \<alpha>s"
+
+abbreviation \<omega>_dec :: "V list \<Rightarrow> bool" where
+  "\<omega>_dec \<equiv> sorted_wrt (\<ge>)"
+
+lemma Ord_\<omega>_sum [simp]: "List.set \<alpha>s \<subseteq> ON \<Longrightarrow> Ord (\<omega>_sum \<alpha>s)"
+  by (induction \<alpha>s) auto
+
+lemma \<omega>_dec_Cons_iff [simp]: "\<omega>_dec (\<alpha>#\<beta>#\<beta>s) \<longleftrightarrow> \<beta> \<le> \<alpha> \<and> \<omega>_dec (\<beta>#\<beta>s)"
+  by auto
+
+lemma \<omega>_sum_0E:
+  assumes "\<omega>_sum \<alpha>s = 0" "List.set \<alpha>s \<subseteq> ON"
+  shows "\<alpha>s = []"
+  using assms
+by (induction \<alpha>s) auto
+
+fun \<omega>_of_Cantor where
+  \<omega>_of_Cantor_Nil: "\<omega>_of_Cantor [] ms = []"
+| \<omega>_of_Cantor_Nil2: "\<omega>_of_Cantor (\<alpha>#\<alpha>s) [] = []"
+| \<omega>_of_Cantor_Cons: "\<omega>_of_Cantor (\<alpha>#\<alpha>s) (m#ms) = replicate m \<alpha> @ \<omega>_of_Cantor \<alpha>s ms"
+
+
+lemma \<omega>_sum_append [simp]: "\<omega>_sum (xs @ ys) = \<omega>_sum xs + \<omega>_sum ys"
+  by (induction xs) (auto simp: add.assoc)
+
+lemma \<omega>_sum_replicate [simp]: "\<omega>_sum (replicate m a) = \<omega> \<up> a * ord_of_nat m"
+  by (induction m) (auto simp: mult_succ simp flip: replicate_append_same)
+
+lemma \<omega>_sum_of_Cantor [simp]: "\<omega>_sum (\<omega>_of_Cantor \<alpha>s ms) = Cantor_sum \<alpha>s ms"
+proof (induction \<alpha>s arbitrary: ms)
+  case (Cons a \<alpha>s ms)
+  then show ?case
+    by (cases ms) auto
+qed auto
+
+lemma \<omega>_of_Cantor_subset: "List.set (\<omega>_of_Cantor \<alpha>s ms) \<subseteq> List.set \<alpha>s"
+proof (induction \<alpha>s arbitrary: ms)
+  case (Cons a \<alpha>s ms)
+  then show ?case
+    by (cases ms) auto
+qed auto
+
+
+lemma \<omega>_dec_replicate: "\<omega>_dec (replicate m \<alpha> @ \<alpha>s) = (if m=0 then \<omega>_dec \<alpha>s else \<omega>_dec (\<alpha>#\<alpha>s))"
+  by (induction m arbitrary: \<alpha>s) (simp_all flip: replicate_append_same)
+
+
+lemma \<omega>_dec_of_Cantor_aux:
+  assumes "Cantor_dec (\<alpha>#\<alpha>s)" "length \<alpha>s = length ms"
+  shows "\<omega>_dec (\<omega>_of_Cantor (\<alpha>#\<alpha>s) (m#ms))"
+  using assms
+proof (induction \<alpha>s arbitrary: ms)
+  case Nil
+  then show ?case
+    using sorted_wrt_iff_nth_less by fastforce
+next
+  case (Cons a \<alpha>s ms)
+  then obtain n ns where ns: "ms = n#ns"
+    by (metis length_Suc_conv)
+  then have "a \<le> \<alpha>"
+    using Cons.prems(1) order.strict_implies_order by auto
+  moreover have "\<forall>x\<in>list.set (\<omega>_of_Cantor \<alpha>s ns). x \<le> a"
+    using Cons ns \<open>a \<le> \<alpha>\<close>
+    apply (simp add: \<omega>_dec_replicate)
+    by (meson \<omega>_of_Cantor_subset order.strict_implies_order subsetD)
+  ultimately show ?case
+    using Cons ns by (force simp: \<omega>_dec_replicate)
+qed
+
+lemma \<omega>_dec_of_Cantor:
+  assumes "Cantor_dec \<alpha>s" "length \<alpha>s = length ms"
+  shows "\<omega>_dec (\<omega>_of_Cantor \<alpha>s ms)"
+proof (cases \<alpha>s)
+  case Nil
+  then have "ms = []"
+    using assms by auto
+  with Nil show ?thesis
+    by simp
+next
+  case (Cons a list)
+  then show ?thesis
+    by (metis \<omega>_dec_of_Cantor_aux assms length_Suc_conv)
+qed
+
+proposition \<omega>_nf_exists:
+  assumes "Ord \<alpha>"
+  obtains \<alpha>s where "List.set \<alpha>s \<subseteq> ON" and "\<omega>_dec \<alpha>s" and "\<alpha> = \<omega>_sum \<alpha>s"
+proof -
+  obtain \<alpha>s ms where "List.set \<alpha>s \<subseteq> ON" "list.set ms \<subseteq> {0<..}" and length: "length \<alpha>s = length ms"
+    and "Cantor_dec \<alpha>s"
+    and \<alpha>: "\<alpha> = Cantor_sum \<alpha>s ms"
+    using Cantor_nf_exists assms by blast
+  then show thesis
+    by (metis \<omega>_dec_of_Cantor \<omega>_of_Cantor_subset \<omega>_sum_of_Cantor order_trans that)
+qed
+
+lemma \<omega>_sum_take_drop: "\<omega>_sum \<alpha>s = \<omega>_sum (take k \<alpha>s) + \<omega>_sum (drop k \<alpha>s)"
+proof (induction k arbitrary: \<alpha>s)
+  case 0
+  then show ?case
+    by simp
+next
+  case (Suc k)
+  then show ?case
+  proof (cases "\<alpha>s")
+    case Nil
+    then show ?thesis
+      by simp
+  next
+    case (Cons a list)
+    with Suc.prems show ?thesis
+      by (simp add: add.assoc flip: Suc.IH)
+  qed
+qed
+
+lemma in_elts_\<omega>_sum:
+  assumes "\<delta> \<in> elts (\<omega>_sum \<alpha>s)"
+  shows "\<exists>k<length \<alpha>s. \<exists>\<gamma>\<in>elts (\<omega> \<up> (\<alpha>s!k)). \<delta> = \<omega>_sum (take k \<alpha>s) + \<gamma>"
+  using assms
+proof (induction \<alpha>s arbitrary: \<delta>)
+  case (Cons \<alpha> \<alpha>s)
+  then have "\<delta> \<in> elts (\<omega> \<up> \<alpha> + \<omega>_sum \<alpha>s)"
+    by simp
+  then show ?case
+  proof (rule mem_plus_V_E)
+    fix \<eta>
+    assume \<eta>: "\<eta> \<in> elts (\<omega>_sum \<alpha>s)" and \<delta>: "\<delta> = \<omega> \<up> \<alpha> + \<eta>"
+    then obtain k \<gamma> where "k<length \<alpha>s" "\<gamma> \<in> elts (\<omega> \<up> (\<alpha>s!k))" "\<eta> = \<omega>_sum (take k \<alpha>s) + \<gamma>"
+      using Cons.IH by blast
+    then show ?case
+      by (rule_tac x="Suc k" in exI) (simp add: \<delta> add.assoc)
+  qed auto
+qed auto
+
+lemma \<omega>_le_\<omega>_sum: "\<lbrakk>k < length \<alpha>s; List.set \<alpha>s \<subseteq> ON\<rbrakk> \<Longrightarrow> \<omega> \<up> (\<alpha>s!k) \<le> \<omega>_sum \<alpha>s"
+proof (induction \<alpha>s arbitrary: k)
+  case (Cons a \<alpha>s)
+  then obtain "Ord a" "list.set \<alpha>s \<subseteq> ON"
+    by simp
+  with Cons.IH have "\<And>k x. k < length \<alpha>s \<Longrightarrow> \<omega> \<up> \<alpha>s ! k \<le> \<omega> \<up> a + \<omega>_sum \<alpha>s"
+    by (meson Ord_\<omega> Ord_\<omega>_sum Ord_oexp add_le_left order_trans)
+  then show ?case
+    using Cons by (simp add: nth_Cons split: nat.split)
+qed auto
+
+lemma \<omega>_sum_less_self:
+  assumes "List.set (\<alpha>#\<alpha>s) \<subseteq> ON" and "\<omega>_dec (\<alpha>#\<alpha>s)"
+  shows "\<omega>_sum \<alpha>s < \<omega>\<up>\<alpha> + \<omega>_sum \<alpha>s"
+  using assms
+proof (induction \<alpha>s arbitrary: \<alpha>)
+  case Nil
+  then show ?case
+    using ZFC_in_HOL.neq0_conv by fastforce
+next
+  case (Cons \<alpha>1 \<alpha>s)
+  then show ?case
+    by (simp add: add_right_strict_mono oexp_mono_le)
+qed
+
+text \<open>Something like Lemma 5.2 for \<omega>_sum\<close>
+lemma \<omega>_sum_less_\<omega>_power:
+  assumes "\<omega>_dec (\<alpha>#\<alpha>s)" "List.set (\<alpha>#\<alpha>s) \<subseteq> ON"
+  shows "\<omega>_sum \<alpha>s < \<omega>\<up>\<alpha> * \<omega>"
+  using assms
+proof (induction \<alpha>s)
+  case Nil
+  then show ?case
+    by (simp add: \<omega>_gt0)
+next
+  case (Cons \<beta> \<alpha>s)
+  then have "Ord \<alpha>"
+    by auto
+  have "\<omega>_sum \<alpha>s < \<omega>\<up>\<alpha> * \<omega>"
+    using Cons by force
+  then have "\<omega>\<up>\<beta> + \<omega>_sum \<alpha>s < \<omega>\<up>\<alpha> + \<omega>\<up>\<alpha> * \<omega>"
+    using Cons.prems add_right_strict_mono oexp_mono_le by auto
+  also have "\<dots> = \<omega>\<up>\<alpha> * \<omega>"
+    by (metis Kirby.add_mult_distrib mult.right_neutral one_plus_\<omega>_equals_\<omega>)
+  finally show ?case
+    by simp
+qed
+
+
+lemma \<omega>_sum_nf_unique_aux:
+  assumes "Ord \<alpha>"
+    and \<alpha>sON: "List.set \<alpha>s \<subseteq> ON"
+    and \<beta>sON: "List.set \<beta>s \<subseteq> ON"
+    and \<alpha>sdec: "\<omega>_dec \<alpha>s"
+    and \<beta>sdec: "\<omega>_dec \<beta>s"
+    and \<alpha>seq: "\<alpha> = \<omega>_sum \<alpha>s"
+    and \<beta>seq: "\<alpha> = \<omega>_sum \<beta>s"
+  shows "\<alpha>s = \<beta>s"
+  using assms
+proof (induction \<alpha> arbitrary: \<alpha>s \<beta>s rule: Ord_induct)
+  case (step \<alpha>)
+  show ?case
+  proof (cases "\<alpha> = 0")
+    case True
+    then show ?thesis
+      using step.prems by (metis \<omega>_sum_0E)
+  next
+    case False
+    then obtain \<alpha>0 \<alpha>s' \<beta>0 \<beta>s' where \<alpha>s: "\<alpha>s = \<alpha>0 # \<alpha>s'" and \<beta>s: "\<beta>s = \<beta>0 # \<beta>s'"
+      by (metis \<omega>_sum.elims step.prems(5,6))
+    then have ON: "Ord \<alpha>0" "list.set \<alpha>s' \<subseteq> ON" "Ord \<beta>0" "list.set \<beta>s' \<subseteq> ON"
+      using \<alpha>s \<beta>s step.prems(1,2) by auto
+    have False if "\<beta>0 < \<alpha>0"
+    proof -
+      have Ordc: "Ord (\<omega>_sum \<beta>s)" "Ord (\<omega>\<up>\<alpha>0)"
+        using Ord_oexp \<open>Ord \<alpha>0\<close>  step.hyps step.prems(6) by blast+
+      have "\<omega>_sum \<beta>s < \<omega>\<up>\<beta>0 * \<omega>"
+        by (rule \<omega>_sum_less_\<omega>_power) (use \<beta>s step.prems ON in auto)
+      also have "\<dots> \<le> \<omega>\<up>\<alpha>0"
+        using ON by (metis Ord_\<omega> Ord_succ oexp_mono_le oexp_succ omega_nonzero succ_le_iff that)
+      finally show False
+        using \<alpha>s leD step.prems(5,6) by auto
+    qed
+    moreover
+    have False if "\<alpha>0 < \<beta>0"
+    proof -
+      have Ordc: "Ord (\<omega>_sum \<alpha>s)" "Ord (\<omega>\<up>\<beta>0)"
+        using Ord_oexp \<open>Ord \<beta>0\<close>  step.hyps step.prems(5) by blast+
+      have "\<omega>_sum \<alpha>s < \<omega>\<up>\<alpha>0 * \<omega>"
+        by (rule \<omega>_sum_less_\<omega>_power) (use \<alpha>s step.prems ON in auto)
+      also have "\<dots> \<le> \<omega>\<up>\<beta>0"
+        using ON by (metis Ord_\<omega> Ord_succ oexp_mono_le oexp_succ omega_nonzero succ_le_iff that)
+      finally show False
+        using \<beta>s leD step.prems(5,6)
+        by (simp add: \<open>\<alpha> = \<omega>_sum \<alpha>s\<close> leD)
+    qed
+    ultimately have \<dagger>: "\<alpha>0 = \<beta>0"
+      using Ord_linear_lt \<open>Ord \<alpha>0\<close> \<open>Ord \<beta>0\<close> by blast
+    moreover have "\<alpha>s' = \<beta>s'"
+    proof (rule step.IH)
+      show "\<omega>_sum \<alpha>s' \<in> elts \<alpha>"
+        using step.prems \<alpha>s
+        by (simp add: Ord_mem_iff_lt \<omega>_sum_less_self)
+      show "\<omega>_dec \<alpha>s'" "\<omega>_dec \<beta>s'"
+        using \<alpha>s \<beta>s step.prems(3,4) by auto
+      have "\<omega>_sum \<alpha>s = \<omega>_sum \<beta>s"
+        using step.prems(5,6) by auto
+      then show "\<omega>_sum \<alpha>s' = \<omega>_sum \<beta>s'"
+        by (simp add: \<dagger> \<alpha>s \<beta>s)
+    qed (use ON in auto)
+    ultimately show ?thesis
+      by (simp add: \<alpha>s \<beta>s)
+  qed
+qed
+
+
+subsection \<open>Indecomposable ordinals\<close>
+
+text \<open>Cf exercise 5 on page 43 of Kunen\<close>
+
+definition indecomposable
+  where "indecomposable \<alpha> \<equiv> Ord \<alpha> \<and> (\<forall>\<beta> \<in> elts \<alpha>. \<forall>\<gamma> \<in> elts \<alpha>. \<beta>+\<gamma> \<in> elts \<alpha>)"
+
+lemma indecomposableD:
+  "\<lbrakk>indecomposable \<alpha>; \<beta> < \<alpha>; \<gamma> < \<alpha>; Ord \<beta>; Ord \<gamma>\<rbrakk> \<Longrightarrow> \<beta>+\<gamma> < \<alpha>"
+  by (meson Ord_mem_iff_lt OrdmemD indecomposable_def)
+
+lemma indecomposable_imp_Ord:
+  "indecomposable \<alpha> \<Longrightarrow> Ord \<alpha>"
+  using indecomposable_def by blast
+
+lemma indecomposable_1: "indecomposable 1"
+  by (auto simp: indecomposable_def)
+
+lemma indecomposable_0: "indecomposable 0"
+  by (auto simp: indecomposable_def)
+
+lemma indecomposable_succ [simp]: "indecomposable (succ \<alpha>) \<longleftrightarrow> \<alpha> = 0"
+  using not_add_mem_right
+  apply (auto simp: indecomposable_def)
+  apply (metis add_right_cancel add.right_neutral)
+  done
+
+lemma indecomposable_alt:
+  assumes ord: "Ord \<alpha>" "Ord \<beta>" and \<beta>: "\<beta> < \<alpha>" and minor: "\<And>\<beta> \<gamma>. \<lbrakk>\<beta> < \<alpha>; \<gamma> < \<alpha>; Ord \<gamma>\<rbrakk> \<Longrightarrow> \<beta>+\<gamma> < \<alpha>"
+  shows "\<beta>+\<alpha> = \<alpha>"
+proof -
+  have "\<not> \<beta>+\<alpha> < \<alpha>"
+    by (simp add: add_le_left ord leD)
+  moreover have "\<not> \<alpha> < \<beta>+\<alpha>"
+    by (metis assms le_Ord_diff less_V_def)
+  ultimately show ?thesis
+    by (simp add: add_le_left less_V_def ord)
+qed
+
+lemma indecomposable_imp_eq:
+  assumes "indecomposable \<alpha>" "Ord \<beta>" "\<beta> < \<alpha>"
+  shows "\<beta>+\<alpha> = \<alpha>"
+  by (metis assms indecomposableD indecomposable_def le_Ord_diff less_V_def less_irrefl)
+
+lemma indecomposable2:
+  assumes y: "y < x" and z: "z < x" and minor: "\<And>y::V. y < x \<Longrightarrow> y+x = x"
+  shows "y+z < x"
+  by (metis add_less_cancel_left y z minor)
+
+lemma indecomposable_imp_Limit:
+  assumes indec: "indecomposable \<alpha>" and "\<alpha> > 1"
+  shows "Limit \<alpha>"
+  using indecomposable_imp_Ord [OF indec]
+proof (cases rule: Ord_cases)
+  case (succ \<beta>)
+  then show ?thesis
+    using assms one_V_def by auto
+qed (use assms in auto)
+
+lemma eq_imp_indecomposable:
+  assumes "Ord \<alpha>" "\<And>\<beta>::V. \<beta> \<in> elts \<alpha> \<Longrightarrow> \<beta>+\<alpha> = \<alpha>"
+  shows "indecomposable \<alpha>"
+  by (metis add_mem_right_cancel assms indecomposable_def)
+
+lemma indecomposable_\<omega>_power:
+  assumes "Ord \<delta>"
+  shows "indecomposable (\<omega>\<up>\<delta>)"
+  unfolding indecomposable_def
+proof (intro conjI ballI)
+  show "Ord (\<omega>\<up>\<delta>)"
+    by (simp add: \<open>Ord \<delta>\<close>)
+next
+  fix \<beta> \<gamma>
+  assume asm: "\<beta> \<in> elts (\<omega>\<up>\<delta>)" "\<gamma> \<in> elts (\<omega>\<up>\<delta>)"
+  then obtain ord: "Ord \<beta>" "Ord \<gamma>" and \<beta>: "\<beta> < \<omega>\<up>\<delta>" and \<gamma>: "\<gamma> < \<omega>\<up>\<delta>"
+    by (meson Ord_\<omega> Ord_in_Ord Ord_oexp OrdmemD \<open>Ord \<delta>\<close>)
+  show "\<beta> + \<gamma> \<in> elts (\<omega>\<up>\<delta>)"
+    using \<open>Ord \<delta>\<close>
+  proof (cases \<delta> rule: Ord_cases)
+    case 0
+    then show ?thesis
+      using \<open>Ord \<delta>\<close> asm by auto
+  next
+    case (succ l)
+    have "\<exists>x\<in>elts \<omega>. \<beta> + \<gamma> \<in> elts (\<omega>\<up>l * x)"
+      if x: "x \<in> elts \<omega>" "\<beta> \<in> elts (\<omega>\<up>l * x)" and y: "y \<in> elts \<omega>" "\<gamma> \<in> elts (\<omega>\<up>l * y)"
+      for x y
+    proof -
+      obtain "Ord x" "Ord y" "Ord (\<omega>\<up>l * x)" "Ord (\<omega>\<up>l * y)"
+        using Ord_\<omega> Ord_mult Ord_oexp x y nat_into_Ord succ(1) by presburger
+      then have "\<beta> + \<gamma> \<in> elts (\<omega>\<up>l * (x+y))"
+        using add_mult_distrib Ord_add Ord_mem_iff_lt add_strict_mono ord x y by presburger
+      then show ?thesis
+        using x y by blast
+    qed
+    then show ?thesis
+      using \<open>Ord \<delta>\<close> succ ord \<beta> \<gamma> by (auto simp: mult_Limit simp flip: Ord_mem_iff_lt)
+  next
+    case limit
+    have "Ord (\<omega>\<up>\<delta>)"
+      by (simp add: \<open>Ord \<delta>\<close>)
+    then obtain x y where x: "x \<in> elts \<delta>" "Ord x" "\<beta> \<in> elts (\<omega>\<up>x)"
+      and y: "y \<in> elts \<delta>" "Ord y" "\<gamma> \<in> elts (\<omega>\<up>y)"
+      using \<open>Ord \<delta>\<close> limit ord \<beta> \<gamma> oexp_Limit
+      by (auto simp flip: Ord_mem_iff_lt intro: Ord_in_Ord)
+    then have "succ (x \<squnion> y) \<in> elts \<delta>"
+      by (metis Limit_def Ord_linear_le limit sup.absorb2 sup.orderE)
+    moreover have "\<beta> + \<gamma> \<in> elts (\<omega>\<up>succ (x \<squnion> y))"
+    proof -
+      have oxy: "Ord (x \<squnion> y)"
+        using Ord_sup x y by blast
+      then obtain "\<omega>\<up>x \<le> \<omega>\<up>(x \<squnion> y)" "\<omega>\<up>y \<le> \<omega>\<up>(x \<squnion> y)"
+        by (metis Ord_\<omega> Ord_linear_le Ord_mem_iff_less_TC Ord_mem_iff_lt le_TC_def less_le_not_le oexp_mono omega_nonzero sup.absorb2 sup.orderE x(2) y(2))
+      then have "\<beta> \<in> elts (\<omega>\<up>(x \<squnion> y))" "\<gamma> \<in> elts (\<omega>\<up>(x \<squnion> y))"
+        using x y by blast+
+      then have "\<beta> + \<gamma> \<in> elts (\<omega>\<up>(x \<squnion> y) * succ (succ 0))"
+        by (metis Ord_\<omega> Ord_add Ord_mem_iff_lt Ord_oexp Ord_sup add_strict_mono mult.right_neutral mult_succ ord one_V_def x(2) y(2))
+      then show ?thesis
+        apply (simp add: oxy)
+        using Ord_\<omega> Ord_mult Ord_oexp Ord_trans mem_0_Ord mult_add_mem_0 oexp_eq_0_iff omega_nonzero oxy succ_in_omega by presburger
+    qed
+    ultimately show ?thesis
+      using ord \<open>Ord (\<omega>\<up>\<delta>)\<close> limit oexp_Limit by auto
+  qed
+qed
+
+lemma \<omega>_power_imp_eq:
+  assumes "\<beta> < \<omega>\<up>\<delta>" "Ord \<beta>" "Ord \<delta>" "\<delta> \<noteq> 0"
+  shows "\<beta> + \<omega>\<up>\<delta> = \<omega>\<up>\<delta>"
+  by (simp add: assms indecomposable_\<omega>_power indecomposable_imp_eq)
+
+lemma type_imp_indecomposable:
+  assumes \<alpha>: "Ord \<alpha>"
+    and minor: "\<And>X. X \<subseteq> elts \<alpha> \<Longrightarrow> ordertype X VWF = \<alpha> \<or> ordertype (elts \<alpha> - X) VWF = \<alpha>"
+  shows "indecomposable \<alpha>"
+  unfolding indecomposable_def
+proof (intro conjI ballI)
+  fix \<beta> \<gamma>
+  assume \<beta>: "\<beta> \<in> elts \<alpha>" and \<gamma>: "\<gamma> \<in> elts \<alpha>"
+  then obtain \<beta>\<gamma>: "elts \<beta> \<subseteq> elts \<alpha>" "elts \<gamma> \<subseteq> elts \<alpha>" "Ord \<beta>" "Ord \<gamma>"
+    using \<alpha> Ord_in_Ord Ord_trans by blast
+ then have oeq: "ordertype (elts \<beta>) VWF = \<beta>"
+    by auto
+  show "\<beta> + \<gamma> \<in> elts \<alpha>"
+  proof (rule ccontr)
+    assume "\<beta> + \<gamma> \<notin> elts \<alpha>"
+    then obtain \<delta> where \<delta>: "Ord \<delta>" "\<beta> + \<delta> = \<alpha>"
+      by (metis Ord_ordertype \<beta>\<gamma>(1) le_Ord_diff less_eq_V_def minor oeq)
+    then have "\<delta> \<in> elts \<alpha>"
+      using Ord_linear \<beta>\<gamma> \<gamma> \<open>\<beta> + \<gamma> \<notin> elts \<alpha>\<close> by blast
+    then have "ordertype (elts \<alpha> - elts \<beta>) VWF = \<delta>"
+      using \<delta> ordertype_diff Limit_def \<alpha> \<open>Ord \<beta>\<close> by blast
+    then show False
+      by (metis \<beta> \<open>\<delta> \<in> elts \<alpha>\<close> \<open>elts \<beta> \<subseteq> elts \<alpha>\<close> oeq mem_not_refl minor)
+  qed
+qed (use assms in auto)
+
+
+text \<open>This proof uses Cantor normal form_split, yet still is rather long\<close>
+proposition indecomposable_is_\<omega>_power:
+  assumes inc: "indecomposable \<mu>"
+  obtains "\<mu> = 0" | \<delta> where "Ord \<delta>" "\<mu> = \<omega>\<up>\<delta>"
+proof (cases "\<mu> = 0")
+  case True
+  then show thesis
+    by (simp add: that)
+next
+  case False
+  obtain "Ord \<mu>"
+    using Limit_def assms indecomposable_def by blast
+  then obtain \<alpha>s ms where Cantor: "List.set \<alpha>s \<subseteq> ON" "list.set ms \<subseteq> {0<..}"
+                                "length \<alpha>s = length ms" "Cantor_dec \<alpha>s"
+    and \<mu>: "\<mu> = Cantor_sum \<alpha>s ms"
+    using Cantor_nf_exists by blast
+  consider (0) "length \<alpha>s = 0" | (1) "length \<alpha>s = 1" | (2) "length \<alpha>s \<ge> 2"
+    by linarith
+  then show thesis
+  proof cases
+    case 0
+    then show ?thesis
+      using \<mu> assms False indecomposable_def by auto
+  next
+    case 1
+    then obtain \<alpha> m where \<alpha>m: "\<alpha>s = [\<alpha>]" "ms = [m]"
+      by (metis One_nat_def \<open>length \<alpha>s = length ms\<close> length_0_conv length_Suc_conv)
+    then obtain "Ord \<alpha>" "m \<noteq> 0" "Ord (\<omega>\<up>\<alpha>)"
+      using \<open>list.set \<alpha>s \<subseteq> ON\<close> \<open>list.set ms \<subseteq> {0<..}\<close> by auto
+    have \<mu>: "\<mu> = \<omega>\<up>\<alpha> * ord_of_nat m"
+      using \<alpha>m by (simp add: \<mu>)
+    moreover have "m = 1"
+    proof (rule ccontr)
+      assume "m \<noteq> 1"
+      then have 2: "m \<ge> 2"
+        using \<open>m \<noteq> 0\<close> by linarith
+      then have "m = Suc 0 + Suc 0 + (m-2)"
+        by simp
+      then have "ord_of_nat m = 1 + 1 + ord_of_nat (m-2)"
+        by (metis add.left_neutral mult.left_neutral mult_succ ord_of_nat.simps ord_of_nat_add)
+      then have \<mu>eq: "\<mu> = \<omega>\<up>\<alpha> + \<omega>\<up>\<alpha> + \<omega>\<up>\<alpha> * ord_of_nat (m-2)"
+        using \<mu> by (simp add: add_mult_distrib)
+      moreover have less: "\<omega>\<up>\<alpha> < \<mu>"
+        by (metis Ord_\<omega> OrdmemD \<mu>eq \<open>Ord \<alpha>\<close> add_le_cancel_left0 add_less_cancel_left0 le_less_trans less_V_def oexp_gt_0_iff zero_in_omega)
+      moreover have "\<omega>\<up>\<alpha> + \<omega>\<up>\<alpha> * ord_of_nat (m-2) < \<mu>"
+        using "2" "\<mu>" \<open>Ord \<alpha>\<close> assms less indecomposableD less_V_def by auto
+      ultimately show False
+        using indecomposableD [OF inc, of "\<omega>\<up>\<alpha>" "\<omega>\<up>\<alpha> + \<omega>\<up>\<alpha> * ord_of_nat (m-2)"]
+        by (simp add: \<open>Ord (\<omega>\<up>\<alpha>)\<close> add.assoc)
+    qed
+    moreover have "Ord \<alpha>"
+      using \<open>List.set \<alpha>s \<subseteq> ON\<close> by (simp add: \<open>\<alpha>s = [\<alpha>]\<close>)
+    ultimately show ?thesis
+      by (metis One_nat_def mult.right_neutral ord_of_nat.simps one_V_def that(2))
+  next
+    case 2
+    then obtain \<alpha>1 \<alpha>2 \<alpha>s' m1 m2 ms' where \<alpha>m: "\<alpha>s = \<alpha>1#\<alpha>2#\<alpha>s'" "ms = m1#m2#ms'"
+      by (metis Cantor(3) One_nat_def Suc_1 impossible_Cons length_Cons list.size(3) not_numeral_le_zero remdups_adj.cases)
+    then obtain "Ord \<alpha>1" "Ord \<alpha>2" "m1 \<noteq> 0" "m2 \<noteq> 0" "Ord (\<omega>\<up>\<alpha>1)" "Ord (\<omega>\<up>\<alpha>2)"
+                "list.set \<alpha>s' \<subseteq> ON" "list.set ms' \<subseteq> {0<..}"
+      using \<open>list.set \<alpha>s \<subseteq> ON\<close> \<open>list.set ms \<subseteq> {0<..}\<close> by auto
+    have oCs: "Ord (Cantor_sum \<alpha>s' ms')"
+      by (simp add: Ord_Cantor_sum \<open>list.set \<alpha>s' \<subseteq> ON\<close>)
+    have \<alpha>21: "\<alpha>2 \<in> elts \<alpha>1"
+      using Cantor_dec_Cons_iff \<alpha>m(1) \<open>Cantor_dec \<alpha>s\<close>
+      by (simp add: Ord_mem_iff_lt \<open>Ord \<alpha>1\<close> \<open>Ord \<alpha>2\<close>)
+    have "\<omega>\<up>\<alpha>2 \<noteq> 0"
+      by (simp add: \<open>Ord \<alpha>2\<close>)
+    then have *: "(\<omega>\<up>\<alpha>2 * ord_of_nat m2 + Cantor_sum \<alpha>s' ms') > 0"
+      by (simp add: OrdmemD \<open>Ord (\<omega>\<up>\<alpha>2)\<close> \<open>m2 \<noteq> 0\<close> mem_0_Ord oCs)
+    have \<mu>: "\<mu> = \<omega>\<up>\<alpha>1 * ord_of_nat m1 + (\<omega>\<up>\<alpha>2 * ord_of_nat m2 + Cantor_sum \<alpha>s' ms')"
+      (is "\<mu> = ?\<alpha> + ?\<beta>")
+      using \<alpha>m by (simp add: \<mu>)
+    moreover
+    have "\<omega>\<up>\<alpha>2 * ord_of_nat m2 + Cantor_sum \<alpha>s' ms' < \<omega>\<up>\<alpha>1 * ord_of_nat m1 + (\<omega>\<up>\<alpha>2 * ord_of_nat m2 + Cantor_sum \<alpha>s' ms')"
+      if "\<alpha>2 \<in> elts \<alpha>1"
+    proof (rule less_\<omega>_power)
+      show "Cantor_sum \<alpha>s' ms' < \<omega>\<up>\<alpha>2"
+        using \<alpha>m Cantor cnf_2 by auto
+    qed (use oCs \<open>Ord \<alpha>1\<close> \<open>m1 \<noteq> 0\<close> \<open>m2 \<noteq> 0\<close> that in auto)
+    then have "?\<beta> < \<mu>"
+      using \<alpha>21 by (simp add: \<mu> \<alpha>m)
+    moreover have less: "?\<alpha> < \<mu>"
+      using oCs by (metis \<mu> "*" add_less_cancel_left add.right_neutral)
+    ultimately have False
+      using indecomposableD [OF inc, of "?\<alpha>" "?\<beta>"]
+      by (simp add: \<open>Ord (\<omega>\<up>\<alpha>1)\<close> \<open>Ord (\<omega>\<up>\<alpha>2)\<close> oCs)
+    then show ?thesis ..
+  qed
+qed
+
+corollary indecomposable_iff_\<omega>_power:
+   "indecomposable \<mu> \<longleftrightarrow> \<mu> = 0 \<or> (\<exists>\<delta>. \<mu> = \<omega>\<up>\<delta> \<and> Ord \<delta>)"
+  by (meson indecomposable_0 indecomposable_\<omega>_power indecomposable_is_\<omega>_power)
+
+theorem indecomposable_imp_type:
+  fixes X :: "bool \<Rightarrow> V set"
+  assumes \<gamma>: "indecomposable \<gamma>"
+    and "\<And>b. ordertype (X b) VWF \<le> \<gamma>" "\<And>b. small (X b)" "\<And>b. X b \<subseteq> ON"
+    and "elts \<gamma> \<subseteq> (UN b. X b)"
+  shows "\<exists>b. ordertype (X b) VWF = \<gamma>"
+  using \<gamma> [THEN indecomposable_imp_Ord] assms
+proof (induction arbitrary: X)
+  case (succ \<beta>)
+  show ?case
+  proof (cases "\<beta> = 0")
+    case True
+    then have "\<exists>b. 0 \<in> X b"
+      using succ.prems(5) by blast
+    then have "\<exists>b. ordertype (X b) VWF \<noteq> 0"
+      using succ.prems(3) by auto
+    then have "\<exists>b. ordertype (X b) VWF \<ge> succ 0"
+      by (meson Ord_0 Ord_linear2 Ord_ordertype less_eq_V_0_iff succ_le_iff)
+    then show ?thesis
+      using True succ.prems(2) by blast
+  next
+    case False
+    then show ?thesis
+      using succ.prems by auto
+  qed
+next
+  case (Limit \<gamma>)
+  then obtain \<delta> where \<delta>: "\<gamma> = \<omega>\<up>\<delta>" and "\<delta> \<noteq> 0" "Ord \<delta>"
+    by (metis Limit_eq_Sup_self image_ident indecomposable_is_\<omega>_power not_succ_Limit oexp_0_right one_V_def zero_not_Limit)
+  show ?case
+  proof (cases "Limit \<delta>")
+    case True
+    have ot: "\<exists>b. ordertype (X b \<inter> elts (\<omega>\<up>\<alpha>)) VWF = \<omega>\<up>\<alpha>"
+      if "\<alpha> \<in> elts \<delta>" for \<alpha>
+    proof (rule Limit.IH)
+      have "Ord \<alpha>"
+        using Ord_in_Ord \<open>Ord \<delta>\<close> that by blast
+      then show "\<omega>\<up>\<alpha> \<in> elts \<gamma>"
+        by (simp add: Ord_mem_iff_lt \<delta> \<omega>_gt1 \<open>Ord \<delta>\<close> oexp_less that)
+      show "indecomposable (\<omega>\<up>\<alpha>)"
+        using \<open>Ord \<alpha>\<close> indecomposable_1 indecomposable_\<omega>_power by fastforce
+      show "small (X b \<inter> elts (\<omega>\<up>\<alpha>))" for b
+        by (meson down inf_le2)
+      show "ordertype (X b \<inter> elts (\<omega> \<up> \<alpha>)) VWF \<le> \<omega> \<up> \<alpha>" for b
+        by (simp add: \<open>Ord \<alpha>\<close> ordertype_le_Ord)
+      show "X b \<inter> elts (\<omega> \<up> \<alpha>) \<subseteq> ON" for b
+        by (simp add: Limit.prems inf.coboundedI1)
+      show "elts (\<omega> \<up> \<alpha>) \<subseteq> (\<Union>b. X b \<inter> elts (\<omega> \<up> \<alpha>))"
+        using Limit.prems Limit.hyps \<open>\<omega> \<up> \<alpha> \<in> elts \<gamma>\<close>
+        by clarsimp (metis Ord_trans UN_E indecomposable_imp_Ord subset_eq)
+    qed
+    define A where "A \<equiv> \<lambda>b. {\<alpha> \<in> elts \<delta>. ordertype (X b \<inter> elts (\<omega>\<up>\<alpha>)) VWF \<ge> \<omega>\<up>\<alpha>}"
+    have Asmall: "small (A b)" for b
+      by (simp add: A_def)
+    have AON: "A b \<subseteq> ON" for b
+      using A_def \<open>Ord \<delta>\<close> elts_subset_ON by blast
+    have eq: "elts \<delta> = (\<Union> b. A b)"
+      by (auto simp: A_def) (metis ot eq_refl)
+    then obtain b where b: "Sup (A b) = \<delta>"
+      using \<open>Limit \<delta>\<close>
+      apply (auto simp: UN_bool_eq)
+      by (metis AON ON_imp_Ord Ord_Sup Ord_linear_le Limit_eq_Sup_self Sup_Un_distrib Asmall sup.absorb2 sup.orderE)
+    have "\<omega>\<up>\<alpha> \<le> ordertype (X b) VWF" if "\<alpha> \<in> A b" for \<alpha>
+    proof -
+      have "(\<omega>\<up>\<alpha>) = ordertype ((X b) \<inter> elts (\<omega>\<up>\<alpha>)) VWF"
+        using \<open>Ord \<delta>\<close> that by (simp add: A_def Ord_in_Ord dual_order.antisym ordertype_le_Ord)
+      also have "\<dots> \<le> ordertype (X b) VWF"
+        by (simp add: Limit.prems ordertype_VWF_mono)
+      finally show ?thesis .
+    qed
+    then have "ordertype (X b) VWF \<ge> Sup ((\<lambda>\<alpha>. \<omega>\<up>\<alpha>) ` A b)"
+      by blast
+    moreover have "Sup ((\<lambda>\<alpha>. \<omega>\<up>\<alpha>) ` A b) = \<omega> \<up> Sup (A b)"
+      by (metis b Ord_\<omega> ZFC_in_HOL.Sup_empty AON \<open>\<delta> \<noteq> 0\<close> Asmall oexp_Sup omega_nonzero)
+    ultimately show ?thesis
+      using Limit.hyps Limit.prems \<delta> b by auto
+  next
+    case False
+    then obtain \<beta> where \<beta>: "\<delta> = succ \<beta>" "Ord \<beta>"
+      using Ord_cases \<open>\<delta> \<noteq> 0\<close> \<open>Ord \<delta>\<close> by auto
+    then have Ord\<omega>\<beta>: "Ord (\<omega>\<up>\<beta>)"
+      using Ord_oexp by blast
+    have subX12: "elts (\<omega>\<up>\<beta> * \<omega>) \<subseteq> (\<Union>b. X b)"
+      using Limit \<beta> \<delta> by auto
+    define E where "E \<equiv> \<lambda>n. {\<omega>\<up>\<beta> * ord_of_nat n ..< \<omega>\<up>\<beta> * ord_of_nat (Suc n)} \<inter> ON"
+    have EON: "E n \<subseteq> ON" for n
+      using E_def by blast
+    have E_imp_less: "x < y" if "i < j" "x \<in> E i" "y \<in> E j" for x y i j
+    proof -
+      have "succ (i) \<le> ord_of_nat j"
+        using that(1) by force
+      then have "\<not> y \<le> x"
+        using that
+        apply (auto simp: E_def)
+        by (metis Ord\<omega>\<beta> Ord_ord_of_nat leD mult_cancel_le_iff ord_of_nat.simps(2) order_trans)
+      with that show ?thesis
+        by (meson EON ON_imp_Ord Ord_linear2)
+    qed
+    then have djE: "disjnt (E i) (E j)" if "i \<noteq> j" for i j
+      using that nat_neq_iff unfolding disjnt_def by auto
+    have less_imp_E: "i \<le> j" if "x < y" "x \<in> E i" "y \<in> E j" for x y i j
+      using that E_imp_less [OF _ \<open>y \<in> E j\<close> \<open>x \<in> E i\<close>] leI less_asym by blast
+    have inc: "indecomposable (\<omega>\<up>\<beta>)"
+      using \<beta> indecomposable_1 indecomposable_\<omega>_power by fastforce
+    have in_En: "\<omega>\<up>\<beta> * ord_of_nat n + x \<in> E n" if "x \<in> elts (\<omega>\<up>\<beta>)" for x n
+      using that Ord\<omega>\<beta> Ord_in_Ord [OF Ord\<omega>\<beta>] by (auto simp: E_def Ord\<omega>\<beta> OrdmemD mult_succ)
+    have *: "elts \<gamma> = \<Union>(range E)"
+    proof
+      have "\<exists>m. \<omega>\<up>\<beta> * m \<le> x \<and> x < \<omega>\<up>\<beta> * succ (ord_of_nat m)"
+        if "x \<in> elts (\<omega>\<up>\<beta> * ord_of_nat n)" for x n
+        using that
+        apply (clarsimp simp add: mult [of _ "ord_of_nat n"] lift_def)
+        by (metis add_less_cancel_left OrdmemD inc indecomposable_imp_Ord mult_succ plus sup_ge1)
+      moreover have "Ord x" if "x \<in> elts (\<omega>\<up>\<beta> * ord_of_nat n)" for x n
+        by (meson Ord\<omega>\<beta> Ord_in_Ord Ord_mult Ord_ord_of_nat that)
+      ultimately show "elts \<gamma> \<subseteq> \<Union>(range E)"
+        by (auto simp: \<delta> \<beta> E_def mult_Limit elts_\<omega>)
+      have "x \<in> elts (\<omega>\<up>\<beta> * succ(ord_of_nat n))"
+        if "Ord x" "x < \<omega>\<up>\<beta> * succ (n)" for x n
+        by (metis that Ord_mem_iff_lt Ord_mult Ord_ord_of_nat inc indecomposable_imp_Ord ord_of_nat.simps(2))
+      then show "\<Union>(range E) \<subseteq> elts \<gamma>"
+        by (force simp: \<delta> \<beta> E_def Limit.prems mult_Limit)
+    qed
+    have smE: "small (E n)" for n
+      by (metis "*" complete_lattice_class.Sup_upper down rangeI)
+    have otE: "ordertype (E n) VWF = \<omega>\<up>\<beta>" for n
+      by (simp add: E_def inc indecomposable_imp_Ord mult_succ ordertype_interval_eq)
+
+    define cut where "cut \<equiv> \<lambda>n x. odiff x (\<omega>\<up>\<beta> * ord_of_nat n)"
+    have cutON: "cut n ` X \<subseteq> ON" if "X \<subseteq> ON" for n X
+      using that by (simp add: image_subset_iff cut_def ON_imp_Ord Ord\<omega>\<beta> Ord_odiff)
+    have cut [simp]: "cut n (\<omega> \<up> \<beta> * ord_of_nat n + x) = x" for x n
+      by (auto simp: cut_def)
+    have cuteq: "x \<in> cut n ` (X \<inter> E n) \<longleftrightarrow> \<omega>\<up>\<beta> * ord_of_nat n + x \<in> X"
+      if x: "x \<in> elts (\<omega>\<up>\<beta>)" for x X n
+    proof
+      show "\<omega>\<up>\<beta> * ord_of_nat n + x \<in> X" if "x \<in> cut n ` (X \<inter> E n)"
+        using E_def Ord\<omega>\<beta> Ord_odiff_eq image_iff local.cut_def that by auto
+      show "x \<in> cut n ` (X \<inter> E n)"
+        if "\<omega>\<up>\<beta> * ord_of_nat n + x \<in> X"
+        by (metis (full_types) IntI cut image_iff in_En that x)
+    qed
+    have ot_cuteq: "ordertype (cut n ` (X \<inter> E n)) VWF = ordertype (X \<inter> E n) VWF" for n X
+    proof (rule ordertype_VWF_inc_eq)
+      show "X \<inter> E n \<subseteq> ON"
+        using E_def by blast
+      then show "cut n ` (X \<inter> E n) \<subseteq> ON"
+        by (simp add: cutON)
+      show "small (X \<inter> E n)"
+        by (meson Int_lower2 smE smaller_than_small)
+      show "cut n x < cut n y"
+        if "x \<in> X \<inter> E n" "y \<in> X \<inter> E n" "x < y" for x y
+        using that \<open>X \<inter> E n \<subseteq> ON\<close> by(simp add: E_def Ord\<omega>\<beta> Ord_odiff_less_odiff local.cut_def)
+    qed
+
+    define N where "N \<equiv> \<lambda>b. {n. ordertype (X b \<inter> E n) VWF = \<omega>\<up>\<beta>}"
+    have "\<exists>b. infinite (N b)"
+    proof (rule ccontr)
+      assume "\<nexists>b. infinite (N b)"
+      then obtain n where "\<And>b. n \<notin> N b"
+        apply (simp add: ex_bool_eq)
+        by (metis (full_types) finite_nat_set_iff_bounded not_less_iff_gr_or_eq)
+      moreover
+      have "\<exists>b. ordertype (cut n ` (X b \<inter> E n)) VWF = \<omega>\<up>\<beta>"
+      proof (rule Limit.IH)
+        show "\<omega>\<up>\<beta> \<in> elts \<gamma>"
+          by (metis Limit.hyps Limit_def Limit_omega Ord_mem_iff_less_TC \<beta> \<delta> mult_le2 not_succ_Limit oexp_succ omega_nonzero one_V_def)
+        show "indecomposable (\<omega>\<up>\<beta>)"
+          by (simp add: inc)
+        show "ordertype (cut n ` (X b \<inter> E n)) VWF \<le> \<omega>\<up>\<beta>" for b
+          by (metis "otE" inf_le2 ordertype_VWF_mono ot_cuteq smE)
+        show "small (cut n ` (X b \<inter> E n))" for b
+          using smE subset_iff_less_eq_V
+          by (meson inf_le2 replacement)
+        show "cut n ` (X b \<inter> E n) \<subseteq> ON" for b
+          using E_def cutON by auto
+        have "elts (\<omega>\<up>\<beta> * succ n) \<subseteq> \<Union>(range X)"
+          by (metis Ord\<omega>\<beta> Ord_\<omega> Ord_ord_of_nat less_eq_V_def mult_cancel_le_iff ord_of_nat.simps(2) ord_of_nat_le_omega order_trans subX12)
+        then show "elts (\<omega>\<up>\<beta>) \<subseteq> (\<Union>b. cut n ` (X b \<inter> E n))"
+          by (auto simp: mult_succ mult_Limit UN_subset_iff cuteq UN_bool_eq)
+      qed
+      then have "\<exists>b. ordertype (X b \<inter> E n) VWF = \<omega>\<up>\<beta>"
+        by (simp add: ot_cuteq)
+      ultimately show False
+        by (simp add: N_def)
+    qed
+    then obtain b where b: "infinite (N b)"
+      by blast
+      then obtain \<phi> :: "nat \<Rightarrow> nat" where \<phi>: "bij_betw \<phi> UNIV (N b)" and mono: "strict_mono \<phi>"
+        by (meson bij_enumerate enumerate_mono strict_mono_def)
+      then have "ordertype (X b \<inter> E (\<phi> n)) VWF = \<omega>\<up>\<beta>" for n
+        using N_def bij_betw_imp_surj_on by blast
+      moreover have "small (X b \<inter> E (\<phi> n))" for n
+        by (meson inf_le2 smE subset_iff_less_eq_V)
+      ultimately have "\<exists>f. bij_betw f (X b \<inter> E (\<phi> n)) (elts (\<omega>\<up>\<beta>)) \<and> (\<forall>x \<in> X b \<inter> E (\<phi> n). \<forall>y \<in> X b \<inter> E (\<phi> n). f x < f y \<longleftrightarrow> (x,y) \<in> VWF)"
+        for n by (metis Ord_ordertype ordertype_VWF_eq_iff)
+      then obtain F where bijF: "\<And>n. bij_betw (F n) (X b \<inter> E (\<phi> n)) (elts (\<omega>\<up>\<beta>))"
+              and F: "\<And>n. \<forall>x \<in> X b \<inter> E (\<phi> n). \<forall>y \<in> X b \<inter> E (\<phi> n). F n x < F n y \<longleftrightarrow> (x,y) \<in> VWF"
+        by metis
+      then have F_bound: "\<And>n. \<forall>x \<in> X b \<inter> E (\<phi> n). F n x < \<omega>\<up>\<beta>"
+        by (metis Ord_\<omega> Ord_oexp OrdmemD \<beta>(2) bij_betw_imp_surj_on image_eqI)
+      have F_Ord: "\<And>n. \<forall>x \<in> X b \<inter> E (\<phi> n). Ord (F n x)"
+        by (metis otE ON_imp_Ord Ord_ordertype bijF bij_betw_def elts_subset_ON imageI)
+
+      have inc: "\<phi> n \<ge> n" for n
+        by (simp add: mono strict_mono_imp_increasing)
+
+      have dj\<phi>: "disjnt (E (\<phi> i)) (E (\<phi> j))" if "i \<noteq> j" for i j
+        by (rule djE) (use \<phi> that in \<open>auto simp: bij_betw_def inj_def\<close>)
+      define Y where "Y \<equiv> (\<Union>n. E (\<phi> n))"
+      have "\<exists>n. y \<in> E (\<phi> n)" if "y \<in> Y" for y
+        using Y_def that by blast
+      then obtain \<iota> where \<iota>: "\<And>y. y \<in> Y \<Longrightarrow> y \<in> E (\<phi> (\<iota> y))"
+        by metis
+      have "Y \<subseteq> ON"
+        by (auto simp: Y_def E_def)
+      have \<iota>le: "\<iota> x \<le> \<iota> y" if "x < y" "x \<in> Y" "y \<in> Y" for x y
+        using less_imp_E strict_mono_less_eq that \<iota> [OF \<open>x \<in> Y\<close>] \<iota> [OF \<open>y \<in> Y\<close>] mono
+        unfolding Y_def by blast
+      have eq\<iota>: "x \<in> E (\<phi> k) \<Longrightarrow> \<iota> x = k" for x k
+        using \<iota> unfolding Y_def
+        by (meson UN_I disjnt_iff dj\<phi> iso_tuple_UNIV_I)
+
+      have upper: "\<omega>\<up>\<beta> * ord_of_nat (\<iota> x) \<le> x" if "x \<in> Y" for x
+        using that
+      proof (clarsimp simp add: Y_def eq\<iota>)
+        fix u v
+        assume u: "u \<in> elts (\<omega>\<up>\<beta> * ord_of_nat v)" and v: "x \<in> E (\<phi> v)"
+        then have "u < \<omega>\<up>\<beta> * ord_of_nat v"
+          by (simp add: OrdmemD \<beta>(2))
+        also have "\<dots> \<le> \<omega>\<up>\<beta> * ord_of_nat (\<phi> v)"
+          by (simp add: \<beta>(2) inc)
+        also have "\<dots> \<le> x"
+          using v by (simp add: E_def)
+        finally show "u \<in> elts x"
+          using \<open>Y \<subseteq> ON\<close>
+          by (meson ON_imp_Ord Ord_\<omega> Ord_in_Ord Ord_mem_iff_lt Ord_mult Ord_oexp Ord_ord_of_nat \<beta>(2) that u)
+      qed
+
+      define G where "G \<equiv> \<lambda>x. \<omega>\<up>\<beta> * ord_of_nat (\<iota> x) + F (\<iota> x) x"
+      have G_strict_mono: "G x < G y" if "x < y" "x \<in> X b \<inter> Y" "y \<in> X b \<inter> Y" for x y
+      proof (cases "\<iota> x = \<iota> y")
+        case True
+        then show ?thesis
+          using that unfolding G_def
+          by (metis F Int_iff add_less_cancel_left Limit.prems(4) ON_imp_Ord VWF_iff_Ord_less \<iota>)
+      next
+        case False
+        then have "\<iota> x < \<iota> y"
+          by (meson IntE \<iota>le le_less that)
+        then show ?thesis
+          using that by (simp add: G_def F_Ord F_bound Ord\<omega>\<beta> \<iota> mult_nat_less_add_less)
+      qed
+
+      have "ordertype (X b \<inter> Y) VWF = (\<omega>\<up>\<beta>) * \<omega>"
+      proof (rule ordertype_VWF_eq_iff [THEN iffD2])
+        show "Ord (\<omega>\<up>\<beta> * \<omega>)"
+          by (simp add: \<beta>)
+        show "small (X b \<inter> Y)"
+          by (meson Limit.prems(3) inf_le1 subset_iff_less_eq_V)
+        have "bij_betw G (X b \<inter> Y) (elts (\<omega>\<up>\<beta> * \<omega>))"
+        proof (rule bij_betw_imageI)
+          show "inj_on G (X b \<inter> Y)"
+          proof (rule linorder_inj_onI)
+            fix x y
+            assume xy: "x < y" "x \<in> (X b \<inter> Y)" "y \<in> (X b \<inter> Y)"
+            show "G x \<noteq> G y"
+              using G_strict_mono xy by force
+          next
+            show "x \<le> y \<or> y \<le> x"
+              if "x \<in> (X b \<inter> Y)" "y \<in> (X b \<inter> Y)" for x y
+              using that \<open>X b \<subseteq> ON\<close> by (clarsimp simp: Y_def) (metis ON_imp_Ord Ord_linear Ord_trans)
+          qed
+          show "G ` (X b \<inter> Y) = elts (\<omega>\<up>\<beta> * \<omega>)"
+          proof
+            show "G ` (X b \<inter> Y) \<subseteq> elts (\<omega>\<up>\<beta> * \<omega>)"
+              using \<open>X b \<subseteq> ON\<close>
+              apply (clarsimp simp: G_def mult_Limit Y_def eq\<iota>)
+              by (metis IntI add_mem_right_cancel bijF bij_betw_imp_surj_on image_eqI mult_succ ord_of_nat_\<omega> succ_in_omega)
+            show "elts (\<omega>\<up>\<beta> * \<omega>) \<subseteq> G ` (X b \<inter> Y)"
+            proof
+              fix x
+              assume x: "x \<in> elts (\<omega>\<up>\<beta> * \<omega>)"
+              then obtain k where n: "x \<in> elts (\<omega>\<up>\<beta> * ord_of_nat (Suc k))"
+                          and minim: "\<And>m. m < Suc k \<Longrightarrow> x \<notin> elts (\<omega>\<up>\<beta> * ord_of_nat m)"
+                using elts_mult_\<omega>E
+                by (metis old.nat.exhaust)
+              then obtain y where y: "y \<in> elts (\<omega>\<up>\<beta>)" and xeq: "x = \<omega>\<up>\<beta> * ord_of_nat k + y"
+                using x by (auto simp: mult_succ elim: mem_plus_V_E)
+              then have 1: "inv_into (X b \<inter> E (\<phi> k)) (F k) y \<in> (X b \<inter> E (\<phi> k))"
+                by (metis bijF bij_betw_def inv_into_into)
+              then have "(inv_into (X b \<inter> E (\<phi> k)) (F k) y) \<in> X b \<inter> Y"
+                by (force simp: Y_def)
+              moreover have "G (inv_into (X b \<inter> E (\<phi> k)) (F k) y) = x"
+                by (metis "1" G_def Int_iff bijF bij_betw_inv_into_right eq\<iota> xeq y)
+                ultimately show "x \<in> G ` (X b \<inter> Y)"
+                  by blast
+            qed
+          qed
+        qed
+        moreover have "(x,y) \<in> VWF"
+          if "x \<in> X b" "x \<in> Y" "y \<in> X b" "y \<in> Y" "G x < G y" for x y
+        proof -
+          have "x < y"
+            using that by (metis G_strict_mono Int_iff Limit.prems(4) ON_imp_Ord Ord_linear_lt less_asym)
+          then show ?thesis
+            using ON_imp_Ord \<open>Y \<subseteq> ON\<close> that by auto
+        qed
+        moreover have "G x < G y"
+          if "x \<in> X b" "x \<in> Y" "y \<in> X b" "y \<in> Y" "(x, y) \<in> VWF" for x y
+        proof -
+          have "x < y"
+            using that ON_imp_Ord \<open>Y \<subseteq> ON\<close> by auto
+          then show ?thesis
+            by (simp add: G_strict_mono that)
+        qed
+        ultimately show "\<exists>f. bij_betw f (X b \<inter> Y) (elts (\<omega>\<up>\<beta> * \<omega>)) \<and> (\<forall>x\<in>(X b \<inter> Y). \<forall>y\<in>(X b \<inter> Y). f x < f y \<longleftrightarrow> ((x, y) \<in> VWF))"
+          by blast
+      qed
+      moreover have "ordertype (\<Union>n. X b \<inter> E (\<phi> n)) VWF \<le> ordertype (X b) VWF"
+        using Limit.prems(3) ordertype_VWF_mono by auto
+      ultimately have "ordertype (X b) VWF = (\<omega>\<up>\<beta>) * \<omega>"
+        using Limit.hyps Limit.prems(2) \<beta> \<delta>
+        using Y_def by auto
+      then show ?thesis
+        using Limit.hyps \<beta> \<delta> by auto
+    qed
+qed auto
+
+corollary indecomposable_imp_type2:
+  assumes \<alpha>: "indecomposable \<gamma>" "X \<subseteq> elts \<gamma>"
+  shows "ordertype X VWF = \<gamma> \<or> ordertype (elts \<gamma> - X) VWF = \<gamma>"
+proof -
+  have "Ord \<gamma>"
+    using assms indecomposable_imp_Ord by blast
+  have "\<exists>b. ordertype (if b then X else elts \<gamma> - X) VWF = \<gamma>"
+  proof (rule indecomposable_imp_type)
+    show "ordertype (if b then X else elts \<gamma> - X) VWF \<le> \<gamma>" for b
+      by (simp add: \<open>Ord \<gamma>\<close> assms ordertype_le_Ord)
+    show "(if b then X else elts \<gamma> - X) \<subseteq> ON" for b
+      using \<open>Ord \<gamma>\<close> assms elts_subset_ON by auto
+  qed (use assms down in auto)
+  then show ?thesis
+    by (metis (full_types))
+qed
+
+subsection \<open>From ordinals to order types\<close>
+
+lemma indecomposable_ordertype_eq:
+  assumes indec: "indecomposable \<alpha>" and \<alpha>: "ordertype A VWF = \<alpha>" and A: "B \<subseteq> A" "small A"
+  shows "ordertype B VWF = \<alpha> \<or> ordertype (A-B) VWF = \<alpha>"
+proof (rule ccontr)
+  assume "\<not> (ordertype B VWF = \<alpha> \<or> ordertype (A - B) VWF = \<alpha>)"
+  moreover have "ordertype (ordermap A VWF ` B) VWF = ordertype B VWF"
+    using \<open>B \<subseteq> A\<close> by (auto intro: ordertype_image_ordermap [OF \<open>small A\<close>])
+  moreover have "ordertype (elts \<alpha> - ordermap A VWF ` B) VWF = ordertype (A - B) VWF"
+    by (metis ordertype_map_image \<alpha> A elts_of_set ordertype_def replacement)
+  moreover have "ordermap A VWF ` B \<subseteq> elts \<alpha>"
+    using \<alpha> A by blast
+  ultimately show False
+    using indecomposable_imp_type2 [OF \<open>indecomposable \<alpha>\<close>]  \<open>small A\<close> by metis
+qed
+
+lemma indecomposable_ordertype_ge:
+  assumes indec: "indecomposable \<alpha>" and \<alpha>: "ordertype A VWF \<ge> \<alpha>" and small: "small A" "small B"
+  shows "ordertype B VWF \<ge> \<alpha> \<or> ordertype (A-B) VWF \<ge> \<alpha>"
+proof -
+  obtain A' where "A' \<subseteq> A" "ordertype A' VWF = \<alpha>"
+    by (meson \<alpha> \<open>small A\<close> indec indecomposable_def le_ordertype_obtains_subset)
+  then have "ordertype (B \<inter> A') VWF = \<alpha> \<or> ordertype (A'-B) VWF = \<alpha>"
+    by (metis Diff_Diff_Int Diff_subset Int_commute \<open>small A\<close> indecomposable_ordertype_eq indec smaller_than_small)
+  moreover have "ordertype (B \<inter> A') VWF \<le> ordertype B VWF"
+    by (meson Int_lower1 small ordertype_VWF_mono smaller_than_small)
+  moreover have "ordertype (A'-B) VWF \<le> ordertype (A-B) VWF"
+    by (meson Diff_mono Diff_subset \<open>A' \<subseteq> A\<close> \<open>small A\<close> order_refl ordertype_VWF_mono smaller_than_small)
+  ultimately show ?thesis
+    by blast
+qed
+
+text \<open>now for finite partitions\<close>
+lemma indecomposable_ordertype_finite_eq:
+  assumes "indecomposable \<alpha>"
+    and \<A>: "finite \<A>" "pairwise disjnt \<A>" "\<Union>\<A> = A" "\<A> \<noteq> {}" "ordertype A VWF = \<alpha>" "small A"
+  shows "\<exists>X \<in> \<A>. ordertype X VWF = \<alpha>"
+  using \<A>
+proof (induction arbitrary: A)
+  case (insert X \<A>)
+  show ?case
+  proof (cases "\<A> = {}")
+    case True
+    then show ?thesis
+      using insert.prems by blast
+  next
+    case False
+    have smA: "small (\<Union>\<A>)"
+      using insert.prems by auto
+    show ?thesis
+    proof (cases "\<exists>X \<in> \<A>. ordertype X VWF = \<alpha>")
+      case True
+      then show ?thesis
+        using insert.prems by blast
+    next
+      case False
+      have "X = A - \<Union>\<A>"
+        using insert.hyps insert.prems by (auto simp: pairwise_insert disjnt_iff)
+      then have "ordertype X VWF = \<alpha>"
+        using indecomposable_ordertype_eq assms insert False
+        by (metis Union_mono cSup_singleton pairwise_insert smA subset_insertI)
+      then show ?thesis
+        using insert.prems by blast
+    qed
+  qed
+qed auto
+
+lemma indecomposable_ordertype_finite_ge:
+  assumes indec: "indecomposable \<alpha>"
+    and \<A>: "finite \<A>" "A \<subseteq> \<Union>\<A>" "\<A> \<noteq> {}" "ordertype A VWF \<ge> \<alpha>" "small (\<Union>\<A>)"
+  shows "\<exists>X \<in> \<A>. ordertype X VWF \<ge> \<alpha>"
+  using \<A>
+proof (induction arbitrary: A)
+  case (insert X \<A>)
+  show ?case
+  proof (cases "\<A> = {}")
+    case True
+    then have "\<alpha> \<le> ordertype X VWF"
+      using insert.prems
+      by (simp add: order.trans ordertype_VWF_mono)
+    then show ?thesis
+      using insert.prems by blast
+  next
+    case False
+    show ?thesis
+    proof (cases "\<exists>X \<in> \<A>. ordertype X VWF \<ge> \<alpha>")
+      case True
+      then show ?thesis
+        using insert.prems by blast
+    next
+      case False
+      moreover have "small (X \<union> \<Union>\<A>)"
+        using insert.prems by auto
+      moreover have "ordertype (\<Union>(insert X \<A>)) VWF \<ge> \<alpha>"
+        using insert.prems ordertype_VWF_mono by blast
+      ultimately have "ordertype X VWF \<ge> \<alpha>"
+        using indecomposable_ordertype_ge [OF indec]
+        by (metis Diff_subset_conv Sup_insert cSup_singleton insert.IH small_sup_iff subset_refl)
+      then show ?thesis
+        using insert.prems by blast
+    qed
+  qed
+qed auto
+
+end
diff --git a/thys/ZFC_in_HOL/ROOT b/thys/ZFC_in_HOL/ROOT
--- a/thys/ZFC_in_HOL/ROOT
+++ b/thys/ZFC_in_HOL/ROOT
@@ -1,13 +1,13 @@
 chapter AFP
 
 session ZFC_in_HOL (AFP) = HOL +
   options [timeout = 600]
   sessions
     "HOL-Library"
     "HOL-Cardinals"
   theories
-    Ordinal_Exp 
+    Cantor_NF
     ZFC_Typeclasses
   document_files
     "root.tex"
     "root.bib"
diff --git a/thys/ZFC_in_HOL/document/root.tex b/thys/ZFC_in_HOL/document/root.tex
--- a/thys/ZFC_in_HOL/document/root.tex
+++ b/thys/ZFC_in_HOL/document/root.tex
@@ -1,61 +1,61 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 
 \usepackage{amssymb}
 \usepackage{stmaryrd}
 
 % this should be the last package used
 \usepackage{pdfsetup}
 
 % urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
 \isabellestyle{it}
 
 % for uniform font size
 %\renewcommand{\isastyle}{\isastyleminor}
 
 
 \begin{document}
 
 \title{Zermelo Fraenkel Set Theory in Higher-Order Logic}
 \author{Lawrence C. Paulson\\ Computer Laboratory\\ University of Cambridge}
 
 \maketitle
 
 \begin{abstract}
 This entry is a new formalisation of ZFC set theory in Isabelle/HOL\@.
 It is logically equivalent to Obua's HOLZF~\cite{obua-partizan-games}; the point is to have the closest possible integration
 with the rest of Isabelle/HOL, minimising the amount of new notations and exploiting type classes.
 
 There is a type \isa{V} of sets and a function 
 \isa{elts :: V\ {\isasymRightarrow}\ V\ set} mapping a set to its elements.
 Classes simply have type \isa{V\ set}, and the predicate \isa{small} identifies those classes that correspond to actual sets.
 Type classes connected with orders and lattices are used to minimise the amount of new notation
 for concepts such as the subset relation, union and intersection.
-Basic concepts --- Cartesian products, disjoint sums, natural numbers, functions, etc. --- are formalised.
+Basic concepts are formalised: Cartesian products, disjoint sums, natural numbers, functions, etc.
 
 More advanced set-theoretic concepts, such as transfinite induction, ordinals, cardinals
 and the transitive closure of a set, are also provided.
 The definition of addition and multiplication for general sets (not just ordinals) follows Kirby \cite{kirby-addition}.
-The development includes essential results about cardinal arithmetic.
+The development includes essential results about cardinal arithmetic. It also develops ordinal exponentiation, Cantor normal form and the concept of indecomposable ordinals. There are numerous results about order types.
 
 The theory provides two type classes with the aim of
 facilitating developments that combine \isa{V} with other Isabelle/HOL types:
 \isa{embeddable}, the class of types that can be injected into~\isa{V} (including \isa{V} itself as well as \isa{V*V}, \isa{V\ list}, etc.), and
 \isa{small}, the class of types that correspond to some ZF set.
 \end{abstract}
 
 \newpage
 \tableofcontents
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
 \newpage
 \input{session}
 
 \bibliographystyle{abbrv}
 \bibliography{root.bib}
 
 \end{document}