diff --git a/HOTG/Arithmetics/HOTG_Addition.thy b/HOTG/Arithmetics/HOTG_Addition.thy
index 361737c..954dd85 100644
--- a/HOTG/Arithmetics/HOTG_Addition.thy
+++ b/HOTG/Arithmetics/HOTG_Addition.thy
@@ -3,7 +3,6 @@
 subsection \<open>Generalised Addition\<close>
 theory HOTG_Addition
   imports
-    HOTG_Less_Than
     HOTG_Ordinals_Base
     HOTG_Transfinite_Recursion
 begin
@@ -17,7 +16,7 @@ text \<open>Translation of generalised set addition from \<^cite>\<open>kirby_se
 \<^cite>\<open>ZFC_in_HOL_AFP\<close>. Note that general set addition is associative and
 monotone and injective in the second argument, but it is not commutative (not proven here).\<close>
 
-definition "add X \<equiv> transrec (\<lambda>addX Y. X \<union> image addX Y)"
+definition "add X \<equiv> transfrec (\<lambda>addX Y. X \<union> image addX Y)"
 
 bundle hotg_add_syntax begin notation add (infixl "+" 65) end
 bundle no_hotg_add_syntax begin no_notation add (infixl "+" 65) end
@@ -26,7 +25,7 @@ unbundle
   no_HOL_ascii_syntax
 
 lemma add_eq_bin_union_repl_add: "X + Y = X \<union> {X + y | y \<in> Y}"
-  unfolding add_def supply transrec_eq[uhint] by (urule refl)
+  unfolding add_def supply transfrec_eq[uhint] by (urule refl)
 
 text \<open>The lift operation from \<^cite>\<open>kirby_set_arithemtics\<close>.\<close>
 
diff --git a/HOTG/Arithmetics/HOTG_Arithmetics_Cardinal_Arithmetics.thy b/HOTG/Arithmetics/HOTG_Arithmetics_Cardinal_Arithmetics.thy
index 90346c4..2d5c357 100644
--- a/HOTG/Arithmetics/HOTG_Arithmetics_Cardinal_Arithmetics.thy
+++ b/HOTG/Arithmetics/HOTG_Arithmetics_Cardinal_Arithmetics.thy
@@ -6,6 +6,7 @@ theory HOTG_Arithmetics_Cardinal_Arithmetics
     HOTG_Cardinals_Addition
     HOTG_Cardinals_Multiplication
     HOTG_Addition
+    HOTG_Functions_Injective
     HOTG_Multiplication
 begin
 
@@ -23,53 +24,36 @@ qed
 
 text\<open>The next theorem shows that set addition is compatible with cardinality addition.\<close>
 
+(*TODO: cardinalities on rhs can be removed*)
 theorem cardinality_add_eq_cardinal_add_cardinality: "|X + Y| = |X| \<oplus> |Y|"
   using disjoint_lift_self_right by (auto simp add:
   cardinality_bin_union_eq_cardinal_add_cardinality_if_disjoint add_eq_bin_union_lift)
 
-text\<open>A similar theorem shows that set multiplication is compatible with cardinality multiplication.\<close>
+text\<open>The next theorems show that set multiplication is compatible with cardinality multiplication.\<close>
 
-lemma bijection_onto_image_if_injective_on:
-  assumes "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> f x = f x' \<Longrightarrow> x = x'"
-  shows "\<exists>g. (bijection_on X (image f X) f g)"
-proof
-  define P where "P y x \<longleftrightarrow> x \<in> X \<and> f x = y" for y x
-  let ?g = "\<lambda>y. THE x. P y x"
-  have inv: "?g y \<in> X \<and> f (?g y) = y" if "y \<in> image f X" for y
-  proof -
-    from that obtain x where hx: "P y x" using P_def image_def by auto
-    moreover from this have "x = x'" if "P y x'" for x' using P_def that assms by auto
-    ultimately have "P y (?g y)" using theI[of "P y"] by blast
-    then show ?thesis using P_def by auto
-  qed 
-  have inv': "?g (f x) = x" if "x \<in> X" for x
-  proof -
-    have "?g (f x) \<in> X \<and> f (?g (f x)) = f x" using that inv image_def by auto
-    then show ?thesis using assms that by auto
-  qed
-  show "bijection_on X (image f X) f ?g" by (urule bijection_onI) (auto simp: inv')
-qed
-
-theorem cardinality_mul_eq_cardinal_mul_cardinality: "|X * Y| = |X| \<otimes> |Y|"
+theorem cardinality_mul_eq_cardinal_pair: "|X * Y| = |X \<times> Y|"
 proof -
-  define f :: "set \<Rightarrow> set" where "f = (\<lambda>\<langle>x, y\<rangle>. X * y + x)"
-  have "p\<^sub>1 = p\<^sub>2" if "p\<^sub>1 \<in> X \<times> Y" "p\<^sub>2 \<in> X \<times> Y" "f p\<^sub>1 = f p\<^sub>2" for p\<^sub>1 p\<^sub>2
-  proof -
-    from that obtain x\<^sub>1 y\<^sub>1 where "x\<^sub>1 \<in> X" "y\<^sub>1 \<in> Y" "p\<^sub>1 = \<langle>x\<^sub>1, y\<^sub>1\<rangle>" by auto
-    moreover from that obtain x\<^sub>2 y\<^sub>2 where "x\<^sub>2 \<in> X" "y\<^sub>2 \<in> Y" "p\<^sub>2 = \<langle>x\<^sub>2, y\<^sub>2\<rangle>" by auto 
+  define f :: "set \<Rightarrow> set" where "f \<equiv> \<lambda>\<langle>x, y\<rangle>. X * y + x"
+  have "injective_on (X \<times> Y :: set) f"
+  proof (urule injective_onI)
+    fix p\<^sub>1 p\<^sub>2 presume asms: "p\<^sub>1 \<in> X \<times> Y" "p\<^sub>2 \<in> X \<times> Y" "f p\<^sub>1 = f p\<^sub>2"
+    then obtain x\<^sub>1 y\<^sub>1 where "x\<^sub>1 \<in> X" "y\<^sub>1 \<in> Y" "p\<^sub>1 = \<langle>x\<^sub>1, y\<^sub>1\<rangle>" by auto
+    moreover from asms obtain x\<^sub>2 y\<^sub>2 where "x\<^sub>2 \<in> X" "y\<^sub>2 \<in> Y" "p\<^sub>2 = \<langle>x\<^sub>2, y\<^sub>2\<rangle>" by auto
     ultimately have "X * y\<^sub>1 + x\<^sub>1 = X * y\<^sub>2 + x\<^sub>2" using f_def \<open>f p\<^sub>1 = f p\<^sub>2\<close> by auto
     moreover have "x\<^sub>1 < X \<and> x\<^sub>2 < X" using \<open>x\<^sub>1 \<in> X\<close> \<open>x\<^sub>2 \<in> X\<close> lt_if_mem by auto
     ultimately have "x\<^sub>1 = x\<^sub>2 \<and> y\<^sub>1 = y\<^sub>2" using eq_if_mul_add_eq_mul_add_if_lt by blast
-    then show ?thesis using \<open>p\<^sub>1 = \<langle>x\<^sub>1, y\<^sub>1\<rangle>\<close> \<open>p\<^sub>2 = \<langle>x\<^sub>2, y\<^sub>2\<rangle>\<close> by auto
-  qed
-  then have "\<exists>g. (bijection_on (X \<times> Y) (image f (X \<times> Y)) f g)"
-    using bijection_onto_image_if_injective_on by blast
+    then show "p\<^sub>1 = p\<^sub>2" using \<open>p\<^sub>1 = \<langle>x\<^sub>1, y\<^sub>1\<rangle>\<close> \<open>p\<^sub>2 = \<langle>x\<^sub>2, y\<^sub>2\<rangle>\<close> by auto
+  qed auto
+  then obtain g where "bijection_on (X \<times> Y) (image f (X \<times> Y)) f g"
+    using bijection_on_image_if_injective_on by blast
   then have "X \<times> Y \<approx> image f (X \<times> Y)" using equipollentI by blast
-  moreover have "image f (X \<times> Y) = X * Y" 
+  moreover have "image f (X \<times> Y) = X * Y"
     unfolding mul_eq_idx_union_repl_mul_add[of X Y] f_def by force
-  ultimately have "|X \<times> Y| = |X * Y|" using cardinality_eq_if_equipollent by auto
-  then show ?thesis using cardinality_mul_cardinality_eq_cardinality_cartprod by auto
+  ultimately show ?thesis using cardinality_eq_if_equipollent by auto
 qed
 
+theorem cardinality_mul_eq_cardinal_mul: "|X * Y| = X \<otimes> Y"
+  using cardinality_mul_eq_cardinal_pair cardinal_mul_eq_cardinality_pair by simp
+
 end
 
diff --git a/HOTG/Arithmetics/HOTG_Multiplication.thy b/HOTG/Arithmetics/HOTG_Multiplication.thy
index 18a6c3a..bdaf440 100644
--- a/HOTG/Arithmetics/HOTG_Multiplication.thy
+++ b/HOTG/Arithmetics/HOTG_Multiplication.thy
@@ -5,8 +5,8 @@ theory HOTG_Multiplication
   imports
     HOTG_Addition
     HOTG_Additively_Divides
-    HOTG_Ranks
     HOTG_Ordinals_Max
+    HOTG_Ranks
 begin
 
 unbundle no_HOL_groups_syntax
@@ -16,14 +16,14 @@ text \<open>Translation of generalised set multiplication for sets from \<^cite>
 and \<^cite>\<open>ZFC_in_HOL_AFP\<close>. Note that general set multiplication is associative,
 but it is not commutative (not proven here).\<close>
 
-definition "mul X \<equiv> transrec (\<lambda>mulX Y. \<Union>(image (\<lambda>y. lift (mulX y) X) Y))"
+definition "mul X \<equiv> transfrec (\<lambda>mulX Y. \<Union>(image (\<lambda>y. lift (mulX y) X) Y))"
 
 bundle hotg_mul_syntax begin notation mul (infixl "*" 70) end
 bundle no_hotg_mul_syntax begin no_notation mul (infixl "*" 70) end
 unbundle hotg_mul_syntax
 
 lemma mul_eq_idx_union_lift_mul: "X * Y = (\<Union>y \<in> Y. lift (X * y) X)"
-  unfolding mul_def by (urule transrec_eq)
+  unfolding mul_def by (urule transfrec_eq)
 
 corollary mul_eq_idx_union_repl_mul_add: "X * Y = (\<Union>y \<in> Y. {X * y + x | x \<in> X})"
   using mul_eq_idx_union_lift_mul[of X Y] lift_eq_repl_add by simp
@@ -233,14 +233,10 @@ qed
 
 paragraph\<open>Lemma 4.7 from \<^cite>\<open>kirby_set_arithemtics\<close>\<close>
 
-text\<open>For the next missing proofs, see
-\<^url>\<open>https://foss.heptapod.net/isa-afp/afp-devel/-/blob/06458dfa40c7b4aaaeb855a37ae77993cb4c8c18/thys/ZFC_in_HOL/Kirby.thy#L1166\<close>.\<close>
-
 lemma eq_if_mul_add_eq_mul_add_if_lt_aux:
   assumes "A * X + R = A * Y + S" "R < A" "S < A"
   assumes IH:
-    "\<And>x y r s. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> r < A \<Longrightarrow> s < A \<Longrightarrow> 
-    A * x + r = A * y + s \<Longrightarrow> x = y"
+    "\<And>x y r s. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> r < A \<Longrightarrow> s < A \<Longrightarrow> A * x + r = A * y + s \<Longrightarrow> x = y"
   shows "X \<subseteq> Y"
 proof
   fix u assume "u \<in> X"
@@ -257,7 +253,7 @@ proof
     then show "False" using \<open>S < A\<close> not_subset_if_lt by blast
   qed
   from \<open>R < A\<close> obtain R' where "R' \<in> A" "R \<le> R'" by (auto elim: lt_mem_leE)
-  have "A * u + R' \<in> A * X" 
+  have "A * u + R' \<in> A * X"
     using mul_eq_idx_union_repl_mul_add[of A X] \<open>R' \<in> A\<close> \<open>u \<in> X\<close> by auto
   moreover have "A * X \<subseteq> A * Y \<union> lift (A * Y) S"
     using \<open>A * X + R = A * Y + S\<close> add_eq_bin_union_lift by auto
@@ -290,7 +286,7 @@ proof
     qed
   next
     case 2
-    then obtain v e where "v \<in> Y" "e \<in> A" "A * u + R' = A * v + e" 
+    then obtain v e where "v \<in> Y" "e \<in> A" "A * u + R' = A * v + e"
       using mul_eq_idx_union_repl_mul_add[of A Y] by auto
     then have "u = v" using IH \<open>u \<in> X\<close> \<open>R' \<in> A\<close> lt_if_mem by blast
     then show ?thesis using \<open>v \<in> Y\<close> by blast
@@ -303,30 +299,28 @@ lemma eq_if_mul_add_eq_mul_add_if_lt:
   shows "X = Y \<and> R = S"
 proof -
   let ?\<alpha> = "max_ordinal (rank X) (rank Y)"
-  have "X = Y \<and> R = S" if "ordinal \<alpha>" "rank X \<le> \<alpha>" "rank Y \<le> \<alpha>" for \<alpha> 
-    using that assms
+  have "X = Y \<and> R = S" if "ordinal \<alpha>" "rank X \<le> \<alpha>" "rank Y \<le> \<alpha>" for \<alpha>
+  using that assms
   proof (induction \<alpha> arbitrary: X Y R S rule: ordinal_mem_induct)
     case (step \<alpha>)
     have "\<exists>\<beta>. \<beta> \<in> \<alpha> \<and> rank x \<le> \<beta> \<and> rank y \<le> \<beta>" if "x \<in> X" "y \<in> Y" for x y
     proof
       define \<beta> :: set where "\<beta> = max_ordinal (rank x) (rank y)"
-      have "rank x < \<alpha>" 
+      have "rank x < \<alpha>"
         using \<open>x \<in> X\<close> lt_if_mem rank_lt_rank_if_lt \<open>rank X \<le> \<alpha>\<close> lt_if_lt_if_le by fastforce
       moreover have "rank y < \<alpha>"
         using \<open>y \<in> Y\<close> lt_if_mem rank_lt_rank_if_lt \<open>rank Y \<le> \<alpha>\<close> lt_if_lt_if_le by fastforce
       ultimately have "\<beta> < \<alpha>" using \<beta>_def max_ordinal_lt_if_lt_if_lt by auto
-      then have "\<beta> \<in> \<alpha>" using \<open>ordinal \<alpha>\<close> 
+      then have "\<beta> \<in> \<alpha>" using \<open>ordinal \<alpha>\<close>
         using mem_if_lt_if_mem_trans_closed ordinal_mem_trans_closedE  by auto
-      then show "\<beta> \<in> \<alpha> \<and> rank x \<le> \<beta> \<and> rank y \<le> \<beta>" using \<beta>_def ordinal_rank 
-        le_max_ordinal_left_if_ordinal_if_ordinal le_max_ordinal_right_if_ordinal_if_ordinal by auto 
+      then show "\<beta> \<in> \<alpha> \<and> rank x \<le> \<beta> \<and> rank y \<le> \<beta>" using \<beta>_def ordinal_rank
+        le_max_ordinal_left_if_ordinal_if_ordinal le_max_ordinal_right_if_ordinal_if_ordinal by auto
     qed
-    then have IH': 
-        "\<And>x y r s. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> r < A \<Longrightarrow> s < A \<Longrightarrow> 
-        A * x + r = A * y + s \<Longrightarrow> x = y \<and> r = s"
+    then have IH':
+      "\<And>x y r s. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> r < A \<Longrightarrow> s < A \<Longrightarrow> A * x + r = A * y + s \<Longrightarrow> x = y \<and> r = s"
       using step.IH by blast
-    then have "X \<subseteq> Y" 
-      using eq_if_mul_add_eq_mul_add_if_lt_aux step.prems by auto
-    moreover have "Y \<subseteq> X" 
+    then have "X \<subseteq> Y" using eq_if_mul_add_eq_mul_add_if_lt_aux step.prems by auto
+    moreover have "Y \<subseteq> X"
       using eq_if_mul_add_eq_mul_add_if_lt_aux[OF \<open>A * X + R = A * Y + S\<close>[symmetric]]
       using \<open>S < A\<close> \<open>R < A\<close> IH' by force
     ultimately have "X = Y" by auto
@@ -339,8 +333,9 @@ proof -
   ultimately show ?thesis by auto
 qed
 
-corollary eq_if_mul_eq_mul_if_nz:
-  assumes nz: "A \<noteq> 0" and eq: "A * X = A * Y"
+corollary eq_if_mul_eq_mul_if_ne_zero:
+  assumes nz: "A \<noteq> 0"
+  and eq: "A * X = A * Y"
   shows "X = Y"
 proof -
   from eq have "A * X + 0 = A * Y + 0" by auto
diff --git a/HOTG/Binary_Relations/Binary_Relations_Transitive_Closure.thy b/HOTG/Binary_Relations/Binary_Relations_Transitive_Closure.thy
new file mode 100644
index 0000000..9e07750
--- /dev/null
+++ b/HOTG/Binary_Relations/Binary_Relations_Transitive_Closure.thy
@@ -0,0 +1,118 @@
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+\<^marker>\<open>creator "Niklas Krofta"\<close>
+subsection \<open>Transitive Closure\<close>
+theory Binary_Relations_Transitive_Closure
+  imports
+    HOTG_Ordinals_Base
+    HOTG_Binary_Relations_Pow
+begin
+
+unbundle no_HOL_order_syntax
+
+(*TODO: could already be defined differently without sets in HOL_Basics library*)
+definition "trans_closure R x y \<equiv> (\<exists>n. rel_pow R n x y)"
+
+lemma trans_closureI [intro]:
+  assumes "rel_pow R n x y"
+  shows "trans_closure R x y"
+  using assms unfolding trans_closure_def by auto
+
+lemma trans_closureE [elim]:
+  assumes "trans_closure R x y"
+  obtains n where "rel_pow R n x y"
+  using assms unfolding trans_closure_def by auto
+
+lemma transitive_trans_closure: "transitive (trans_closure R)"
+proof -
+  have "trans_closure R x z" if "trans_closure R x y" "rel_pow R n y z" for n x y z using that
+  proof (induction n arbitrary: y z rule: mem_induction)
+    case (mem n)
+    consider "R y z" | m u where "m \<in> n" "rel_pow R m y u" "R u z"
+      using \<open>rel_pow R n y z\<close> by (blast elim: rel_powE)
+    then show ?case
+    proof cases
+      case 1
+      from \<open>trans_closure R x y\<close> obtain k where "rel_pow R k x y" by auto
+      from \<open>R y z\<close> have "rel_pow R (succ k) x z"
+        using rel_pow_iff[of R] \<open>rel_pow R k x y\<close> succ_eq_insert_self by blast
+      then show ?thesis by blast
+    next
+      case 2
+      from mem.IH have "trans_closure R x u"
+        using \<open>m \<in> n\<close> \<open>trans_closure R x y\<close> \<open>rel_pow R m y u\<close> by blast
+      then obtain k where "rel_pow R k x u" by auto
+      then have "rel_pow R (succ k) x z"
+        using \<open>R u z\<close> rel_pow_iff[of R] succ_eq_insert_self by blast
+      then show ?thesis by blast
+    qed
+  qed
+  then have "trans_closure R x z" if "trans_closure R x y" "trans_closure R y z" for x y z
+    using that by blast
+  then show ?thesis by fast
+qed
+
+lemma trans_closure_if_rel: "R x y \<Longrightarrow> trans_closure R x y"
+  using rel_pow_if_rel[of R] by fast
+
+lemma trans_closure_cases:
+  assumes "trans_closure R x y"
+  obtains (rel) "R x y" | (step) z where "trans_closure R x z" "R z y"
+  using assms rel_powE[of R] by blast
+
+lemma rel_if_rel_pow_if_le_if_transitive:
+  includes HOL_order_syntax no_hotg_le_syntax
+  assumes "transitive S"
+  and "R \<le> S"
+  and "rel_pow R n x y"
+  shows "S x y"
+using \<open>rel_pow R n x y\<close>
+proof (induction n arbitrary: y rule: mem_induction)
+  case (mem n)
+  show ?case using \<open>rel_pow R n x y\<close>
+  proof (cases rule: rel_powE)
+    case rel
+    then show ?thesis using \<open>R \<le> S\<close> by blast
+  next
+    case (step m z)
+    with mem.IH have "S x z" by blast
+    then show ?thesis using \<open>R z y\<close> \<open>R \<le> S\<close> \<open>transitive S\<close> by blast
+  qed
+qed
+
+corollary rel_if_trans_closure_if_le_if_transitive:
+  includes HOL_order_syntax no_hotg_le_syntax
+  assumes "transitive S"
+  and "R \<le> S"
+  and "trans_closure R x y"
+  shows "S x y"
+  using assms rel_if_rel_pow_if_le_if_transitive by (elim trans_closureE)
+
+text \<open>Note: together,
+@{thm transitive_trans_closure trans_closure_if_rel rel_if_trans_closure_if_le_if_transitive}
+show that @{term "trans_closure R"} satisfies the universal property:
+it is the smallest transitive relation containing @{term R}.\<close>
+
+lemma trans_closure_mem_eq_lt: "trans_closure (\<in>) = (<)"
+proof -
+  have "trans_closure (\<in>) x y \<Longrightarrow> x < y" for x y
+    by (rule rel_if_trans_closure_if_le_if_transitive[where ?R="(\<in>)"])
+    (use transitive_lt lt_if_mem in auto)
+  moreover have "x < y \<Longrightarrow> trans_closure (\<in>) x y" for x y
+  proof (induction y rule: mem_induction)
+    case (mem y)
+    from \<open>x < y\<close> obtain z where "x \<le> z" "z \<in> y" using lt_mem_leE by blast
+    then show ?case
+    proof (cases rule: leE)
+      case lt
+      with \<open>z \<in> y\<close> mem.IH have "trans_closure (\<in>) x z" by blast
+      then show ?thesis using \<open>z \<in> y\<close> transitive_trans_closure[of "(\<in>)"]
+      by (blast dest: trans_closure_if_rel)
+    next
+      case eq
+      then show ?thesis using \<open>z \<in> y\<close> trans_closure_if_rel by auto
+    qed
+  qed
+  ultimately show ?thesis by fastforce
+qed
+
+end
\ No newline at end of file
diff --git a/HOTG/Binary_Relations/HOTG_Binary_Relations.thy b/HOTG/Binary_Relations/HOTG_Binary_Relations.thy
index 6cc7780..c09f1a7 100644
--- a/HOTG/Binary_Relations/HOTG_Binary_Relations.thy
+++ b/HOTG/Binary_Relations/HOTG_Binary_Relations.thy
@@ -2,10 +2,14 @@
 theory HOTG_Binary_Relations
   imports
     HOTG_Binary_Relation_Properties
+    HOTG_Transfinite_Recursion
+    Wellfounded_Recursion
+    Binary_Relations_Transitive_Closure
     HOTG_Binary_Relation_Functions
     HOTG_Binary_Relations_Agree
     HOTG_Binary_Relations_Base
     HOTG_Binary_Relations_Extend
+    HOTG_Binary_Relations_Pow
 begin
 
 
diff --git a/HOTG/Binary_Relations/HOTG_Binary_Relations_Pow.thy b/HOTG/Binary_Relations/HOTG_Binary_Relations_Pow.thy
new file mode 100644
index 0000000..0a4afd6
--- /dev/null
+++ b/HOTG/Binary_Relations/HOTG_Binary_Relations_Pow.thy
@@ -0,0 +1,34 @@
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+\<^marker>\<open>creator "Niklas Krofta"\<close>
+subsection \<open>Power of Relations\<close>
+theory HOTG_Binary_Relations_Pow
+  imports HOTG_Transfinite_Recursion
+begin
+
+paragraph \<open>Summary\<close>
+text \<open>The n-th composition of a relation with itself:\<close>
+
+definition "rel_pow R = transfrec (\<lambda>r_pow n x y. R x y \<or> (\<exists>m : n. \<exists>z. r_pow m x z \<and> R z y))"
+
+lemma rel_pow_iff: "rel_pow R n x y \<longleftrightarrow> R x y \<or> (\<exists>m : n. \<exists>z. rel_pow R m x z \<and> R z y)"
+  using transfrec_eq[of "\<lambda>r_pow n x y. R x y \<or> (\<exists>m : n. \<exists>z. r_pow m x z \<and> R z y)" n]
+  unfolding rel_pow_def by auto
+
+lemma rel_pow_if_rel:
+  assumes "R x y"
+  shows "rel_pow R n x y"
+  using assms rel_pow_iff by fast
+
+lemma rel_pow_if_rel_if_mem_if_rel_pow:
+  assumes "rel_pow R m x z"
+  and "m \<in> n"
+  and "R z y"
+  shows "rel_pow R n x y"
+  using assms rel_pow_iff by fast
+
+lemma rel_powE:
+  assumes "rel_pow R n x y"
+  obtains (rel) "R x y" | (step) m z where "m \<in> n" "rel_pow R m x z" "R z y"
+  using assms unfolding rel_pow_iff[where ?n=n] by blast
+
+end
\ No newline at end of file
diff --git a/HOTG/Binary_Relations/Recursions/HOTG_Transfinite_Recursion.thy b/HOTG/Binary_Relations/Recursions/HOTG_Transfinite_Recursion.thy
new file mode 100644
index 0000000..67f126d
--- /dev/null
+++ b/HOTG/Binary_Relations/Recursions/HOTG_Transfinite_Recursion.thy
@@ -0,0 +1,36 @@
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+\<^marker>\<open>creator "Niklas Krofta"\<close>
+section \<open>Transfinite Recursion\<close>
+theory HOTG_Transfinite_Recursion
+  imports
+    HOTG_Less_Than
+    HOTG_Functions_Restrict
+    Transport.Wellfounded_Transitive_Recursion
+begin
+
+unbundle no_HOL_order_syntax
+
+lemma wellfounded_lt: "wellfounded (<)"
+  by (auto intro!: wellfoundedI elim: lt_minimal_set_witnessE)
+
+context
+  includes fun_restrict_syntax no_rel_restrict_syntax
+begin
+
+definition transfrec :: "((set \<Rightarrow> 'a) \<Rightarrow> set \<Rightarrow> 'a) \<Rightarrow> set \<Rightarrow> 'a" where
+  "transfrec step = wftrec (<) (\<lambda>f X. step f\<restriction>\<^bsub>X\<^esub> X)"
+
+corollary transfrec_eq: "transfrec step X = step (transfrec step)\<restriction>\<^bsub>X\<^esub> X"
+proof -
+  have fun_rel_restrict_eq: "(fun_rel_restrict f (<) X)\<restriction>\<^bsub>X\<^esub> = f\<restriction>\<^bsub>X\<^esub>" for f
+    using lt_if_mem by (auto simp: fun_restrict_eq_if)
+  then have "transfrec step X = step ((fun_rel_restrict (transfrec step) (<) X)\<restriction>\<^bsub>X\<^esub>) X"
+    using wellfounded_lt transitive_lt
+    by (simp_all only: wfrec_step_eq wftrec_eq_wfrec_stepI transfrec_def)
+  then show ?thesis unfolding fun_rel_restrict_eq by simp
+qed
+
+end
+
+
+end
\ No newline at end of file
diff --git a/HOTG/Binary_Relations/Recursions/Wellfounded_Recursion.thy b/HOTG/Binary_Relations/Recursions/Wellfounded_Recursion.thy
new file mode 100644
index 0000000..0d4b64f
--- /dev/null
+++ b/HOTG/Binary_Relations/Recursions/Wellfounded_Recursion.thy
@@ -0,0 +1,58 @@
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+\<^marker>\<open>creator "Niklas Krofta"\<close>
+section \<open>Well-Founded Recursion\<close>
+theory Wellfounded_Recursion
+  imports
+    Binary_Relations_Transitive_Closure
+begin
+
+paragraph \<open>Summary\<close>
+text \<open>We use @{term wftrec} to define well-founded recursion on non-transitive, well-founded
+relations. The fact that the transitive closure of a well-founded relation is itself well-founded
+can be used to remove the transitivity assumption of @{thm wftrec_eq_wfrec_stepI}.\<close>
+
+lemma wellfounded_trans_closure_if_wellfounded:
+  assumes "wellfounded R"
+  shows "wellfounded (trans_closure R)"
+proof (rule ccontr)
+  assume "\<not>(wellfounded (trans_closure R))"
+  then obtain P X where "P X" and no_minimal: "\<And>Y. P Y \<Longrightarrow> (\<exists>y. trans_closure R y Y \<and> P y)"
+    unfolding wellfounded_def by auto
+  from assms have "\<not>(P Y) \<and> (\<forall>y. trans_closure R y Y \<longrightarrow> \<not>(P y))" for Y
+  proof (induction Y rule: wellfounded_induct)
+    case (step Y)
+    show ?case
+    proof (rule ccontr)
+      assume "\<not>(\<not>(P Y) \<and> (\<forall>y. trans_closure R y Y \<longrightarrow> \<not>(P y)))"
+      then consider "P Y" | y where "trans_closure R y Y" "P y" by blast
+      then show "False"
+      proof cases
+        case 1
+        then obtain y where "trans_closure R y Y" "P y" using no_minimal by blast
+        then show "False" using trans_closure_cases step.IH by force
+      next
+        case 2
+        then show "False" using trans_closure_cases step.IH by force
+      qed
+    qed
+  qed
+  then show "False" using \<open>P X\<close> by blast
+qed
+
+definition "wfrec R step = wftrec (trans_closure R) (\<lambda>f. wfrec_step R step (\<lambda>_. f))"
+
+theorem wfrec_eq_wfrec_stepI:
+  assumes "wellfounded R"
+  shows "wfrec R step X = wfrec_step R step (\<lambda>_. wfrec R step) X"
+proof -
+  have fun_rel_restrict_eq:
+    "fun_rel_restrict (fun_rel_restrict f (trans_closure R) X) R X x = fun_rel_restrict f R X x"
+    for f x by (cases "R x X") (auto dest: trans_closure_if_rel)
+  have "wfrec R step X = wfrec_step R step (fun_rel_restrict (wfrec R step) (trans_closure R)) X"
+    using wellfounded_trans_closure_if_wellfounded[OF assms] transitive_trans_closure[of R]
+    wftrec_eq_wfrec_stepI[where ?step="\<lambda>f. wfrec_step R step (\<lambda>_. f)"]
+    by (simp add: wfrec_step_eq wfrec_def)
+  then show ?thesis unfolding wfrec_step_eq fun_rel_restrict_eq by simp
+qed
+
+end
\ No newline at end of file
diff --git a/HOTG/Cardinals/HOTG_Cardinals.thy b/HOTG/Cardinals/HOTG_Cardinals.thy
index 25155ad..1dcdf49 100644
--- a/HOTG/Cardinals/HOTG_Cardinals.thy
+++ b/HOTG/Cardinals/HOTG_Cardinals.thy
@@ -1,5 +1,6 @@
 \<^marker>\<open>creator "Linghan Fang"\<close>
 \<^marker>\<open>creator "Kevin Kappelmann"\<close>
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
 section \<open>Cardinals\<close>
 theory HOTG_Cardinals
   imports
diff --git a/HOTG/Cardinals/HOTG_Cardinals_Addition.thy b/HOTG/Cardinals/HOTG_Cardinals_Addition.thy
index 91d9b37..9d1bef6 100644
--- a/HOTG/Cardinals/HOTG_Cardinals_Addition.thy
+++ b/HOTG/Cardinals/HOTG_Cardinals_Addition.thy
@@ -102,7 +102,7 @@ proof -
     by (blast dest: symmetricD)
   finally have "X \<union> Y \<approx> |X| \<Coprod> |Y|" .
   with cardinality_eq_if_equipollent have "|X \<union> Y| = ||X| \<Coprod> |Y||" by auto
-  with cardinal_add_eq_cardinality_coprod show ?thesis by simp
+  with cardinal_add_eq_cardinality_coprod show ?thesis by auto
 qed
 
 end
diff --git a/HOTG/Cardinals/HOTG_Cardinals_Multiplication.thy b/HOTG/Cardinals/HOTG_Cardinals_Multiplication.thy
index 30418b8..5782a77 100644
--- a/HOTG/Cardinals/HOTG_Cardinals_Multiplication.thy
+++ b/HOTG/Cardinals/HOTG_Cardinals_Multiplication.thy
@@ -4,17 +4,16 @@ begin
 
 unbundle no_HOL_groups_syntax
 
-definition cardinal_mul :: "set \<Rightarrow> set \<Rightarrow> set" where
-"cardinal_mul \<kappa> \<mu> \<equiv> |\<kappa> \<times> \<mu>|"
+definition "cardinal_mul \<kappa> \<mu> \<equiv> |\<kappa> \<times> \<mu>|"
 
 bundle hotg_cardinal_mul_syntax begin notation cardinal_mul (infixl "\<otimes>" 65) end
 bundle no_hotg_cardinal_mul_syntax begin no_notation cardinal_mul (infixl "\<otimes>" 65) end
 unbundle hotg_cardinal_mul_syntax
 
-lemma cardinal_mul_eq_cardinality_cartprod: "X \<otimes> Y = |X \<times> Y|"
+lemma cardinal_mul_eq_cardinality_pair: "X \<otimes> Y = |X \<times> Y|"
   unfolding cardinal_mul_def ..
 
-lemma cartprod_equipollent_if_equipollent:
+lemma pair_equipollent_if_equipollent:
   assumes "X \<approx> X'" and "Y \<approx> Y'"
   shows "X \<times> Y \<approx> X' \<times> Y'"
 proof -
@@ -22,20 +21,21 @@ proof -
     "bijection_on X X' (fX :: set \<Rightarrow> set) (gX :: set \<Rightarrow> set)"
     "bijection_on Y Y' (fY :: set \<Rightarrow> set) (gY :: set \<Rightarrow> set)"
     by (elim equipollentE)
-  let ?f = "\<lambda>\<langle>x,y\<rangle>. \<langle>fX x, fY y\<rangle>"
-  let ?g = "\<lambda>\<langle>x,y\<rangle>. \<langle>gX x, gY y\<rangle>"
+  let ?f = "\<lambda>\<langle>x, y\<rangle>. \<langle>fX x, fY y\<rangle>"
+  let ?g = "\<lambda>\<langle>x, y\<rangle>. \<langle>gX x, gY y\<rangle>"
   have "bijection_on (X \<times> Y :: set) (X' \<times> Y') ?f ?g"
     by (urule (rr) bijection_onI mono_wrt_predI inverse_onI)
     (use bijections in \<open>auto 0 4 simp: bijection_on_left_right_eq_self
       dest: bijection_on_right_left_if_bijection_on_left_right\<close>)
-  then show ?thesis by auto 
+  then show ?thesis by auto
 qed
 
-corollary cartprod_cardinalities_equipollent_cartprod: "|X| \<times> |Y| \<approx> X \<times> Y"
-  using cartprod_equipollent_if_equipollent by auto
+corollary cardinality_pair_cardinality_equipollent_pair: "|X| \<times> |Y| \<approx> X \<times> Y"
+  using pair_equipollent_if_equipollent by auto
 
-corollary cardinality_mul_cardinality_eq_cardinality_cartprod: "|X| \<otimes> |Y| = |X \<times> Y|"
-  using cardinal_mul_eq_cardinality_cartprod cartprod_cardinalities_equipollent_cartprod 
-  using cardinality_eq_if_equipollent by auto
+corollary cardinality_cardinal_mul_eq_cardinality_pair: "|X| \<otimes> |Y| = |X \<times> Y|"
+  using cardinal_mul_eq_cardinality_pair cardinality_pair_cardinality_equipollent_pair
+    cardinality_eq_if_equipollent
+  by auto
 
 end
\ No newline at end of file
diff --git a/HOTG/Functions/Properties/HOTG_Functions_Bijection.thy b/HOTG/Functions/Properties/HOTG_Functions_Bijection.thy
index 25049cf..ab2b272 100644
--- a/HOTG/Functions/Properties/HOTG_Functions_Bijection.thy
+++ b/HOTG/Functions/Properties/HOTG_Functions_Bijection.thy
@@ -3,6 +3,7 @@ subsection \<open>Bijections\<close>
 theory HOTG_Functions_Bijection
   imports
     HOTG_Functions_Evaluation
+    HOTG_Functions_Injective
     Transport.Functions_Bijection
 begin
 
@@ -59,5 +60,27 @@ lemma set_bijection_on_set_iff_set_bijection_on_pred [iff]:
   "bijection_on A B (f :: set) (g :: set) \<longleftrightarrow> bijection_on (mem_of A) (mem_of B) f g"
   by simp
 
+lemma bijection_on_image_if_injective_on:
+  assumes "injective_on X f"
+  obtains g where "bijection_on X (image f X) f g"
+proof
+  define P where "P y x \<longleftrightarrow> x \<in> X \<and> f x = y" for y x
+  let ?g = "\<lambda>y. THE x. P y x"
+  have inv: "?g y \<in> X \<and> f (?g y) = y" if "y \<in> image f X" for y
+  proof -
+    from that obtain x where hx: "P y x" using P_def by auto
+    moreover then have "x = x'" if "P y x'" for x' using P_def that assms
+      by (auto dest: injective_onD)
+    ultimately have "P y (?g y)" using theI[of "P y"] by blast
+    then show ?thesis using P_def by auto
+  qed
+  moreover have "?g (f x) = x" if "x \<in> X" for x
+  proof -
+    have "?g (f x) \<in> X \<and> f (?g (f x)) = f x" using that inv by auto
+    then show ?thesis using assms that by (auto dest: injective_onD)
+  qed
+  ultimately show "bijection_on X (image f X) f ?g"
+    by (urule bijection_onI where chained = insert) auto
+qed
 
 end
\ No newline at end of file
diff --git a/HOTG/HOTG_Transfinite_Recursion.thy b/HOTG/HOTG_Transfinite_Recursion.thy
deleted file mode 100644
index b6199ea..0000000
--- a/HOTG/HOTG_Transfinite_Recursion.thy
+++ /dev/null
@@ -1,353 +0,0 @@
-\<^marker>\<open>creator "Kevin Kappelmann"\<close>
-\<^marker>\<open>creator "Linghan Fang"\<close>
-section \<open>Transfinite Recursion\<close>
-theory HOTG_Transfinite_Recursion
-  imports
-    HOTG_Less_Than 
-    HOTG_Ordinals_Base
-    HOTG_Functions_Restrict
-    Transport.Functions_Restrict
-    Transport.Binary_Relations_Transitive
-begin
-
-unbundle no_HOL_order_syntax
-
-paragraph \<open>Summary\<close>
-text \<open>We take the axiomatization of transfinite recursion from \<^cite>\<open>ZFC_in_HOL_AFP\<close>,
-\<^url>\<open>https://foss.heptapod.net/isa-afp/afp-devel/-/blob/06458dfa40c7b4aaaeb855a37ae77993cb4c8c18/thys/ZFC_in_HOL/ZFC_in_HOL.thy#L1151\<close>.\<close>
-
-definition "wellfounded r \<longleftrightarrow> (\<forall>P x. P x \<longrightarrow> (\<exists>m. P m \<and> (\<forall>y. r y m \<longrightarrow> \<not> P y)))"
-
-lemma wellfoundedI:
-  assumes "\<And>P x. P x \<Longrightarrow> (\<exists>m. P m \<and> (\<forall>y. r y m \<longrightarrow> \<not> P y))"
-  shows "wellfounded r"
-  using assms unfolding wellfounded_def by blast
-
-lemma wellfoundedE:
-  assumes "wellfounded r" "P x"
-  obtains m where "P m" "\<And>y. r y m \<Longrightarrow> \<not> P y"
-  using assms unfolding wellfounded_def by blast
-
-lemma wellfounded_induct:
-  assumes wf: "wellfounded r" 
-  assumes step: "\<And>x. (\<And>y. r y x \<Longrightarrow> P y) \<Longrightarrow> P x"
-  shows "P x"
-proof (rule ccontr)
-  assume "\<not> P x"
-  then obtain m where "\<not> P m" "\<And>y. r y m \<longrightarrow> P y" 
-    using wf wellfoundedE[where P="\<lambda>x. \<not> P x"] by auto
-  then show "False" using step by auto
-qed
-
-locale wellfounded_rel =
-  fixes r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
-  assumes wellfounded: "wellfounded (\<prec>)"
-begin
-
-lemma r_induct [case_names step]:
-  assumes "\<And>x. (\<And>y. y \<prec> x \<Longrightarrow> P y) \<Longrightarrow> P x"
-  shows "P x"
-  using wellfounded_induct[OF wellfounded] assms by blast
-
-definition "ord_restrict f x = (\<lambda>y. if y \<prec> x then f y else undefined)"
-
-lemma ord_restrict_eq_if: "ord_restrict f x y = (if y \<prec> x then f y else undefined)"
-  unfolding ord_restrict_def by auto
-
-lemma ord_restrict_eq:
-  assumes "y \<prec> x"
-  shows "ord_restrict f x y = f y"
-  using assms unfolding ord_restrict_def by auto
-
-lemma ord_restrict_eq_if_not:
-  assumes "\<not> y \<prec> x"
-  shows "ord_restrict f x y = undefined"
-  using assms unfolding ord_restrict_def by auto
-
-lemma ord_restrict_eq_ord_restrict:
-  assumes "\<forall>y. y \<prec> x \<longrightarrow> f y = g y"
-  shows "ord_restrict f x = ord_restrict g x"
-  using assms unfolding ord_restrict_def by auto
-
-end
-
-locale wellfounded_trans_rel = wellfounded_rel +
-  assumes trans: "transitive (\<prec>)"
-begin
-
-definition "is_recfun X R f \<longleftrightarrow> (\<forall>x. f x = (if x \<prec> X then R (ord_restrict f x) x else undefined))"
-
-definition "the_recfun X R = (THE f. is_recfun X R f)"
-
-definition "wftrec R X = R (ord_restrict (the_recfun X R) X) X"
-
-lemma is_recfunE:
-  assumes "is_recfun X R f"
-  shows "\<And>x. x \<prec> X \<Longrightarrow> f x = R (ord_restrict f x) x" "\<And>x. \<not> x \<prec> X \<Longrightarrow> f x = undefined"
-  using assms unfolding is_recfun_def by auto
-
-lemma recfuns_agree_over_intersection:
-  assumes "is_recfun X R f" "is_recfun Y R g" "Z \<prec> X" "Z \<prec> Y"
-  shows "f Z = g Z"
-  using \<open>Z \<prec> X\<close> \<open>Z \<prec> Y\<close>
-proof (induction Z rule: r_induct)
-  case (step Z)
-  have "f z = g z" if "z \<prec> Z" for z using step.IH that trans step.prems by blast
-  then have "ord_restrict f Z = ord_restrict g Z" using ord_restrict_eq_ord_restrict by auto
-  moreover have "f Z = R (ord_restrict f Z) Z" "g Z = R (ord_restrict g Z) Z" 
-    using assms step.prems is_recfunE by auto
-  ultimately show ?case by auto
-qed
-
-corollary recfun_unique:
-  assumes "is_recfun X R f" "is_recfun X R g"
-  shows "f = g"
-  using assms recfuns_agree_over_intersection[OF assms] unfolding is_recfun_def by auto
-
-corollary is_recfun_the_recfun_if_is_recfun:
-  assumes "is_recfun X R f"
-  shows "is_recfun X R (the_recfun X R)"
-proof -
-  have "\<exists>!g. is_recfun X R g" using assms recfun_unique by auto
-  from theI'[OF this] show ?thesis unfolding the_recfun_def by auto
-qed
-
-corollary recfun_restrict_eq_recfun_restrict_if_mem:
-  assumes recfuns: "is_recfun x R f" "is_recfun X R g" and "x \<prec> X"
-  shows "ord_restrict f x = ord_restrict g x"
-proof -
-  have "f y = g y" if "y \<prec> x" for y
-    using recfuns_agree_over_intersection[OF recfuns] \<open>y \<prec> x\<close> \<open>x \<prec> X\<close> trans by blast
-  then show ?thesis using ord_restrict_eq_ord_restrict by auto
-qed
-
-lemma recfun_exists: "\<exists>f. is_recfun X R f"
-proof (induction X rule: r_induct)
-  case (step X)
-  have is_recfun: "is_recfun x R (the_recfun x R)" if "x \<prec> X" for x
-    using is_recfun_the_recfun_if_is_recfun step.IH that by blast
-  define f where "f x = (if x \<prec> X then R (ord_restrict (the_recfun x R) x) x else undefined)" for x
-  have "ord_restrict f x = ord_restrict (the_recfun x R) x" if "x \<prec> X" for x
-  proof -
-    have "f y = (the_recfun x R) y" if "y \<prec> x" for y
-    proof -
-      have "is_recfun y R (the_recfun y R)" "is_recfun x R (the_recfun x R)" 
-        using is_recfun \<open>x \<prec> X\<close> \<open>y \<prec> x\<close> trans by auto
-      from recfun_restrict_eq_recfun_restrict_if_mem[OF this]
-      have "ord_restrict (the_recfun y R) y = ord_restrict (the_recfun x R) y"
-        using \<open>y \<prec> x\<close> by auto
-      moreover have "f y = R (ord_restrict (the_recfun y R) y) y" 
-        using f_def \<open>y \<prec> x\<close> \<open>x \<prec> X\<close> trans by auto
-      moreover have "R (ord_restrict (the_recfun x R) y) y = (the_recfun x R) y" 
-        using is_recfunE(1) \<open>y \<prec> x\<close> is_recfun \<open>x \<prec> X\<close> by force
-      ultimately show ?thesis by auto
-    qed
-    then show ?thesis using ord_restrict_eq_ord_restrict by auto
-  qed
-  then have "is_recfun X R f" using is_recfun_def f_def by force
-  then show ?case by auto
-qed
-
-corollary is_recfun_the_recfun: "is_recfun X R (the_recfun X R)"
-  using is_recfun_the_recfun_if_is_recfun recfun_exists by blast
-
-theorem wftrec_eq: "wftrec R X = R (ord_restrict (wftrec R) X) X"
-proof -
-  have "(the_recfun X R) x = wftrec R x" if "x \<prec> X" for x
-  proof -
-    have "(the_recfun X R) x = R (ord_restrict (the_recfun X R) x) x"
-      using is_recfunE(1) is_recfun_the_recfun \<open>x \<prec> X\<close> by blast
-    moreover have "ord_restrict (the_recfun x R ) x = ord_restrict (the_recfun X R) x"
-      using recfun_restrict_eq_recfun_restrict_if_mem[OF is_recfun_the_recfun is_recfun_the_recfun] 
-      using \<open>x \<prec> X\<close> by auto
-    ultimately show ?thesis unfolding wftrec_def by auto
-  qed
-  then have "ord_restrict (the_recfun X R) X = ord_restrict (wftrec R) X"
-    using ord_restrict_eq_ord_restrict by auto
-  then show ?thesis using wftrec_def[of R X] by auto
-qed
-
-end
-
-lemma wellfounded_lt: "wellfounded (<)"
-  by (auto intro!: wellfoundedI elim: lt_minimal_set_witnessE)
-
-context 
-begin
-
-interpretation wellfounded_trans_rel "(<)"
-  using wellfounded_lt transitive_lt by unfold_locales auto
-
-definition transrec :: "((set \<Rightarrow> 'a) \<Rightarrow> set \<Rightarrow> 'a) \<Rightarrow> set \<Rightarrow> 'a" where
-"transrec R = wftrec (\<lambda>f X. R (fun_restrict f X) X)"
-
-corollary transrec_eq: "transrec R X = R (fun_restrict (transrec R) X) X"
-proof -
-  have fun_restrict_ord_restrict: "fun_restrict (ord_restrict f X) X = fun_restrict f X" for f
-    unfolding fun_restrict_set_eq_fun_restrict_pred fun_restrict_eq_if ord_restrict_eq_if
-    using lt_if_mem by auto
-  have "transrec R X = R (fun_restrict (ord_restrict (transrec R) X) X) X"
-    using wftrec_eq[of "\<lambda>f X. R (fun_restrict f X) X"] transrec_def[of R, symmetric] by auto
-  then show ?thesis unfolding fun_restrict_ord_restrict by simp
-qed
-
-end
-
-(*
-  We use transrec to define the transitive closure of a general relation (\<prec>). The fact that the 
-  transitive closure of a wellfounded relation is itsself wellfounded can be used to remove the
-  transitivity assumption of wftrec. See wfrec
-*)
-
-(* Composition of a relation with itsself. The parameter n should be thought of as a natural number. *)
-definition "rel_pow r = transrec (\<lambda>r_pow n x y. r x y \<or> (\<exists>m u. m \<in> n \<and> r_pow m x u \<and> r u y))"
-
-lemma rel_pow_iff: "rel_pow r n x y \<longleftrightarrow> r x y \<or> (\<exists>m u. m \<in> n \<and> rel_pow r m x u \<and> r u y)"
-  using transrec_eq[of "\<lambda>r_pow n x y. r x y \<or> (\<exists>m u. m \<in> n \<and> r_pow m x u \<and> r u y)" n] 
-  unfolding rel_pow_def[symmetric] by auto
-
-lemma rel_powE:
-  assumes "rel_pow r n x y"
-  obtains (rel) "r x y" | (trans) m u where "m \<in> n" "rel_pow r m x u" "r u y"
-  using assms unfolding rel_pow_iff[of r n x y] by blast
-
-definition "trans_closure r x y \<longleftrightarrow> (\<exists>n. rel_pow r n x y)"
-
-lemma transitive_trans_closure: "transitive (trans_closure r)"
-proof -
-  have "trans_closure r x z" if "trans_closure r x y" "rel_pow r n y z" for n x y z using that
-  proof (induction n arbitrary: y z rule: mem_induction)
-    case (mem n)
-    consider "r y z" | m u where "m \<in> n" "rel_pow r m y u" "r u z"
-      using \<open>rel_pow r n y z\<close> by (blast elim: rel_powE)
-    then show ?case
-    proof cases
-      case 1
-      from \<open>trans_closure r x y\<close> obtain k where "rel_pow r k x y" unfolding trans_closure_def by auto
-      from \<open>r y z\<close> have "rel_pow r (succ k) x z"
-        using rel_pow_iff[of r _ x z] \<open>rel_pow r k x y\<close> succ_eq_insert_self by blast
-      then show ?thesis unfolding trans_closure_def by blast
-    next
-      case 2
-      have "trans_closure r x u"
-        using mem.IH \<open>m \<in> n\<close> \<open>trans_closure r x y\<close> \<open>rel_pow r m y u\<close> by blast
-      then obtain k where "rel_pow r k x u" unfolding trans_closure_def by auto
-      then have "rel_pow r (succ k) x z" 
-        using \<open>r u z\<close> rel_pow_iff[of r _ x z] succ_eq_insert_self by blast
-      then show ?thesis unfolding trans_closure_def by blast
-    qed
-  qed
-  then have "trans_closure r x z" if "trans_closure r x y" "trans_closure r y z" for x y z
-    using that unfolding trans_closure_def[of r y z] by blast
-  then show ?thesis by auto
-qed
-
-lemma trans_closure_if_rel: "r x y \<Longrightarrow> trans_closure r x y"
-  unfolding trans_closure_def rel_pow_iff[of r _ x y] by blast
-
-lemma trans_closure_cases:
-  assumes "trans_closure r x y"
-  obtains "r x y" | u where "trans_closure r x u" "r u y"
-  using assms unfolding trans_closure_def rel_pow_iff[of r _ x y] 
-  using trans_closure_def that by fast
-
-lemma trans_closure_imp_if_rel_imp_if_transitive:
-  fixes r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
-  fixes s :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<lesssim>" 50)
-  assumes "transitive (\<lesssim>)"
-  assumes rel_imp: "\<And>x y. x \<prec> y \<Longrightarrow> x \<lesssim> y"
-  shows "trans_closure (\<prec>) x y \<Longrightarrow> x \<lesssim> y"
-proof -
-  assume hxy: "trans_closure (\<prec>) x y"
-  have "rel_pow (\<prec>) n x y \<Longrightarrow> x \<lesssim> y" for n
-  proof (induction n arbitrary: y rule: mem_induction)
-    case (mem n)
-    show ?case using rel_powE \<open>rel_pow (\<prec>) n x y\<close>
-    proof cases
-      case rel
-      then show ?thesis using rel_imp by blast
-    next
-      case (trans m u)
-      have "x \<lesssim> u" using \<open>m \<in> n\<close> \<open>rel_pow (\<prec>) m x u\<close> mem.IH by blast
-      then show ?thesis using \<open>u \<prec> y\<close> rel_imp \<open>transitive (\<lesssim>)\<close> by blast
-    qed
-  qed
-  then show ?thesis using hxy trans_closure_def by fast
-qed
-
-(* 
-  Note: Together, transitive_trans_closure, trans_closure_if_rel and 
-  trans_closure_imp_if_rel_imp_if_transitive show trans_closure (\<prec>) satisfies the universal
-  property of the transtive closure of (\<prec>): It is the smallest transitive relation bigger than
-  (\<prec>).
-*)
-
-lemma trans_closure_mem_eq_lt: "trans_closure (\<in>) = (<)"
-proof -
-  have "trans_closure (\<in>) x y \<Longrightarrow> x < y" for x y
-    using trans_closure_imp_if_rel_imp_if_transitive transitive_lt lt_if_mem by fastforce
-  moreover have "x < y \<Longrightarrow> trans_closure (\<in>) x y" for x y
-  proof (induction y rule: mem_induction)
-    case (mem y)
-    from \<open>x < y\<close> obtain u where "x \<le> u" "u \<in> y" using lt_mem_leE by blast
-    then show ?case
-    proof (cases rule: leE)
-      case lt
-      then have "trans_closure (\<in>) x u" using \<open>u \<in> y\<close> mem.IH by blast
-      then show ?thesis using \<open>u \<in> y\<close> trans_closure_if_rel transitive_trans_closure by fast
-    next
-      case eq
-      then show ?thesis using \<open>u \<in> y\<close> trans_closure_if_rel by auto
-    qed
-  qed
-  ultimately show ?thesis by blast
-qed
-
-context wellfounded_rel
-begin
-
-lemma wellfounded_trans_closure: "wellfounded (trans_closure (\<prec>))"
-proof (rule ccontr)
-  assume "\<not> wellfounded (trans_closure (\<prec>))"
-  then obtain P X where "P X" and no_minimal: "\<And>Y. P Y \<Longrightarrow> (\<exists>y. trans_closure (\<prec>) y Y \<and> P y)"
-    unfolding wellfounded_def by auto
-  have "\<not> P Y \<and> (\<forall>y. trans_closure (\<prec>) y Y \<longrightarrow> \<not> P y)" for Y
-  proof (induction Y rule: r_induct)
-    case (step Y)
-    show ?case
-    proof (rule ccontr)
-      assume "\<not> (\<not> P Y \<and> (\<forall>y. trans_closure (\<prec>) y Y \<longrightarrow> \<not> P y))"
-      then consider "P Y" | y where "trans_closure (\<prec>) y Y" "P y" by blast
-      then show "False"
-      proof cases
-        case 1
-        then obtain y where "trans_closure (\<prec>) y Y" "P y" using no_minimal by blast
-        then show "False" using trans_closure_cases step.IH by force
-      next
-        case 2
-        then show "False" using trans_closure_cases step.IH by force
-      qed
-    qed
-  qed
-  then show "False" using \<open>P X\<close> by blast
-qed
-
-interpretation trancl: wellfounded_trans_rel "trans_closure (\<prec>)"
-  using transitive_trans_closure wellfounded_trans_closure by unfold_locales blast
-
-definition "wfrec R = trancl.wftrec (\<lambda>f X. R (ord_restrict f X) X)"
-
-theorem wfrec_eq: "wfrec R X = R (ord_restrict (wfrec R) X) X"
-proof -
-  have fun_restrict_ord_restrict: "ord_restrict (trancl.ord_restrict f X) X = ord_restrict f X" for f
-    unfolding fun_restrict_set_eq_fun_restrict_pred fun_restrict_eq_if 
-    unfolding ord_restrict_eq_if trancl.ord_restrict_eq_if
-    using trans_closure_if_rel by force
-  have "wfrec R X = R (ord_restrict (trancl.ord_restrict (wfrec R) X) X) X"
-    using trancl.wftrec_eq[of "\<lambda>f X. R (ord_restrict f X) X"] wfrec_def[of R, symmetric] by auto
-  then show ?thesis unfolding fun_restrict_ord_restrict by simp
-qed
-
-end
-
-end
\ No newline at end of file
diff --git a/HOTG/Mem_Transitive_Closure/HOTG_Mem_Transitive_Closure.thy b/HOTG/Mem_Transitive_Closure/HOTG_Mem_Transitive_Closure.thy
index 0124496..f39ed03 100644
--- a/HOTG/Mem_Transitive_Closure/HOTG_Mem_Transitive_Closure.thy
+++ b/HOTG/Mem_Transitive_Closure/HOTG_Mem_Transitive_Closure.thy
@@ -12,11 +12,10 @@ text \<open>The transitive closure of a set @{term "X ::set"} is the set that co
 all sets that are transitively contained in @{term "X ::set"}.
 In particular, each such set is transitively closed.
 
-We follow the approach from \<^cite>\<open>ZFC_in_HOL_AFP\<close>,
-\<^url>\<open>https://foss.heptapod.net/isa-afp/afp-devel/-/blob/06458dfa40c7b4aaaeb855a37ae77993cb4c8c18/thys/ZFC_in_HOL/ZFC_Cardinals.thy#L410\<close>.\<close>
+We follow the approach from \<^cite>\<open>ZFC_in_HOL_AFP\<close>.\<close>
 
-definition "is_mem_trans_closure_of X T 
-  \<longleftrightarrow> (mem_trans_closed T \<and> X \<subseteq> T \<and> (\<forall>Y : mem_trans_closed. X \<subseteq> Y \<longrightarrow> T \<subseteq> Y))"
+definition "is_mem_trans_closure_of X T
+  \<equiv> mem_trans_closed T \<and> X \<subseteq> T \<and> (\<forall>Y : mem_trans_closed. X \<subseteq> Y \<longrightarrow> T \<subseteq> Y)"
 
 definition "mem_trans_closure X = (THE T. is_mem_trans_closure_of X T)"
 
@@ -62,13 +61,12 @@ proof (intro is_mem_trans_closure_ofI)
       then show ?thesis using \<open>z \<in> X\<close> T_def by auto
     next
       case trans
-      then have "z \<subseteq> mem_trans_closure x" 
+      then have "z \<subseteq> mem_trans_closure x"
         using trans_closure_elems is_mem_trans_closure_ofE mem_trans_closedD by auto
       then show ?thesis using \<open>x \<in> X\<close> T_def by auto
     qed
   qed
-next
-  show "X \<subseteq> T" using T_def by auto
+next show "X \<subseteq> T" unfolding T_def by auto
 next
   fix Y assume hY: "mem_trans_closed Y" "X \<subseteq> Y"
   show "T \<subseteq> Y"
@@ -81,14 +79,14 @@ next
       then show ?thesis using \<open>X \<subseteq> Y\<close> by auto
     next
       case trans
-      then have "mem_trans_closure x \<subseteq> Y" 
+      then have "mem_trans_closure x \<subseteq> Y"
         using trans_closure_elems is_mem_trans_closure_ofE hY by blast
       then show ?thesis using trans by auto
     qed
   qed
 qed
 
-theorem is_mem_trans_closure_of_mem_trans_closure: 
+theorem is_mem_trans_closure_of_mem_trans_closure:
   shows "is_mem_trans_closure_of X (mem_trans_closure X)"
 proof (induction X rule: mem_induction)
   case (mem X)
diff --git a/HOTG/Ordinals/HOTG_Ranks.thy b/HOTG/Ordinals/HOTG_Ranks.thy
index ad54674..cc0bf98 100644
--- a/HOTG/Ordinals/HOTG_Ranks.thy
+++ b/HOTG/Ordinals/HOTG_Ranks.thy
@@ -1,15 +1,18 @@
 \<^marker>\<open>creator "Niklas Krofta"\<close>
 theory HOTG_Ranks
-  imports HOTG_Ordinals_Base HOTG_Less_Than HOTG_Transfinite_Recursion
+  imports
+    HOTG_Ordinals_Base
+    HOTG_Less_Than
+    HOTG_Transfinite_Recursion
 begin
 
 unbundle no_HOL_order_syntax
 
 definition rank :: "set \<Rightarrow> set" where
-  "rank = transrec (\<lambda>rank X. (\<Union>x \<in> X. succ (rank x)))"
+  "rank = transfrec (\<lambda>rank X. (\<Union>x \<in> X. succ (rank x)))"
 
 lemma rank_eq_idx_union_succ_rank: "rank X = (\<Union>x \<in> X. succ (rank x))"
-  unfolding rank_def by (urule transrec_eq)
+  unfolding rank_def by (urule transfrec_eq)
 
 lemma ordinal_rank: "ordinal (rank X)"
 proof (induction X rule: mem_induction)
diff --git a/HOTG/ROOT b/HOTG/ROOT
index d9db976..7992f77 100644
--- a/HOTG/ROOT
+++ b/HOTG/ROOT
@@ -14,6 +14,7 @@ session HOTG = Transport +
     Arithmetics
     Binary_Relations
     "Binary_Relations/Properties"
+    "Binary_Relations/Recursions"
     Cardinals
     Functions
     "Functions/Properties"
@@ -46,7 +47,6 @@ session HOTG = Transport +
     HOTG_Replacement_Predicates
     HOTG_Set_Difference
     HOTG_Subset
-    HOTG_Transfinite_Recursion
     HOTG_Union_Intersection
     HOTG_Universes
     HOTG_Unordered_Pairs