diff --git a/README.md b/README.md
index f4338bd..1c8ee46 100644
--- a/README.md
+++ b/README.md
@@ -1,3 +1,9 @@
 # IsabelleClub
 
-Repo for Isabelle Club problems
\ No newline at end of file
+Repo for Isabelle Club problems
+
+This repo requires the installation of the Archive of Formal Proofs (AFP) as a component to your isabelle version.
+
+Download can be found here -> https://www.isa-afp.org/download/
+
+Instructions for adding the AFP as a component can be found here -> https://www.isa-afp.org/help/
diff --git a/VerifyThis2024/Fibonacci.thy~ b/VerifyThis2024/Fibonacci.thy~
deleted file mode 100644
index 4502c8a..0000000
--- a/VerifyThis2024/Fibonacci.thy~
+++ /dev/null
@@ -1,64 +0,0 @@
-theory Fibonacci
-imports Main HOL.NthRoot
-begin
-
-fun fib :: \<open>nat \<Rightarrow> nat\<close> where
-\<open>fib 0 = 0\<close>|
-\<open>fib (Suc 0) = Suc 0\<close>|
-\<open>fib (Suc (Suc n)) = fib (Suc n) + fib n\<close>
-
-definition \<open>\<phi> = (1 + sqrt 5)/2\<close>
-definition \<open>\<psi> = (1 - sqrt 5)/2\<close>
-
-definition fib_intvl :: \<open>nat \<Rightarrow> nat set\<close> where
-\<open>fib_intvl n = {fib n..<fib (Suc n)}\<close>
-
-lemma \<phi>_pow_2: \<open>\<phi>^2 = (1 + \<phi>)\<close> unfolding \<phi>_def 
-proof-
-  have *: \<open>(1+sqrt 5)\<^sup>2 = (1 + 2*sqrt 5 + 5)\<close> using power2_sum[of \<open>1\<close> \<open>sqrt 5\<close>] by auto
-  have \<open>((1 + sqrt 5) / 2)\<^sup>2 = (1+sqrt 5)\<^sup>2 / 4\<close>
-    by (simp add: power_divide)
-  hence \<open>... = (1 + 2*sqrt 5 + 5) / 4\<close> using * by auto
-  hence \<open>... = 2*(1 + sqrt 5)/4 + 1\<close> by simp
-  thus \<open>((1 + sqrt 5) / 2)\<^sup>2= 1 + (1 + sqrt 5) / 2\<close>
-  by (smt (z3) "*" field_sum_of_halves four_x_squared)
-qed
-
-lemma \<psi>_pow_2: \<open>\<psi>^2 = (1 + \<psi>)\<close>
-proof-
-  have *: \<open>(1-sqrt 5)\<^sup>2 = (1 - 2*sqrt 5 + 5)\<close> using power2_diff[of \<open>1\<close> \<open>sqrt 5\<close>] by auto
-  hence \<open>(1-sqrt 5)\<^sup>2/4 = (1 - 2*sqrt 5 + 5)/4\<close> by auto
-  hence \<open>... = 2*(1 - sqrt 5)/4 + 1\<close> by simp
-  thus ?thesis
-  by (smt (z3) "*" \<psi>_def field_sum_of_halves four_x_squared)
-qed
-
-lemmas golden_ratios = \<phi>_def \<psi>_def
-
-lemma golden_diff: \<open>(\<phi> - \<psi>) = sqrt 5\<close> unfolding golden_ratios
-  by (smt (z3) field_sum_of_halves)
-
-lemma fib_correct: \<open>fib n = (\<phi>^n - \<psi>^n) / sqrt 5\<close> 
-proof(induction n rule: fib.induct)
-  case 1
-  then show ?case by simp
-next
-  case 2
-  then show ?case
-    by (simp add: golden_diff) 
-next
-  case (3 n)
-  then show ?case
-  proof-
-    have \<open>real (fib (Suc (Suc n))) = real (fib (Suc n)) + real (fib n)\<close> by auto
-    moreover have \<open>... =  (\<phi> ^ Suc n - \<psi> ^ Suc n) / sqrt 5 +  (\<phi> ^  n - \<psi> ^  n) / sqrt 5\<close> using 3 by auto
-    moreover have \<open>... = (\<phi> ^ Suc n  + \<phi>^n - \<psi> ^ Suc n - \<psi> ^ n)/sqrt 5\<close> 
-      by (smt (verit, best) add_divide_distrib)
-    moreover have \<open>... = (\<phi> ^ n * (\<phi> + 1) - \<psi> ^ n * (\<psi> + 1))/ sqrt 5\<close> 
-      by (simp add: distrib_right mult.commute)
-    ultimately show ?case using \<psi>_pow_2 \<phi>_pow_2 
-    by (metis add.commute add_2_eq_Suc power_add)
-  qed
-qed
-
-end
\ No newline at end of file
diff --git a/VerifyThis2024/Ropes.thy~ b/VerifyThis2024/Ropes.thy~
deleted file mode 100644
index 785295a..0000000
--- a/VerifyThis2024/Ropes.thy~
+++ /dev/null
@@ -1,235 +0,0 @@
-theory Ropes
-imports Utils
-begin
-
-section\<open>Challenge 0 from VerifyThis 2024: \<^url>\<open>https://www.pm.inf.ethz.ch/research/verifythis.html\<close>\<close>
-
-subsection\<open>The Rope Data Structure\<close>
-
-text\<open>The task is to implement a "Rope" ( \<^url>\<open>https://en.wikipedia.org/wiki/Rope_(data_structure)\<close> ) 
-originally published by Boehm - \<^url>\<open>https://www.cs.tufts.edu/comp/150FP/archive/hans-boehm/ropes.pdf\<close>
-- a special type of binary tree to represent a string (in honor of Billy who can't be here today).\<close>
-
-text\<open>A Rope stores a string as a tree of where leaves contain a specific sub string and a weight that is equal to the number of characters in the sub string (see example from wiki page). 
-The corresponding parent node stores the sum of left children leaf weights (see example from wiki page).\<close>
-
-subsection\<open>Tasks\<close>
-
-text\<open>Implement a function @{term \<open>valid_rope (r :: Rope) :: bool\<close>} which checks that a rope is well constructed\<close>
-
-lemma mk_leaf_valid: \<open>valid_rope (mk_leaf s)\<close> by simp
-
-value \<open>to_str (Node (Leaf (STR ''Hello '') 6) 6 (Leaf (STR ''World'') 5))\<close>
-
-value \<open>valid_rope (Node (Leaf (STR ''Hello '') 6) 6 (Leaf (STR ''World'') 5))\<close>
-
-text\<open>Implement a function @{term \<open>str_len (r :: Rope)\<close>} that can efficiently compute the length of the string. Further, prove its correctness\<close>
-
-fun str_len :: \<open>Rope \<Rightarrow> nat\<close> where 
-\<open>str_len (Leaf _ N) = N\<close>|
-\<open>str_len (Node l w r) = w + str_len r\<close>
-
-value \<open>size (to_str hello_world_rope)\<close>
-
-lemma sum_weights_eq_size:
-  assumes \<open>valid_rope r\<close> 
-  shows \<open>sum_weights r = size (to_str r)\<close>
-using assms proof(induction r)
-  case (Leaf s w)
-  then show ?case by simp
-next
-  case (Node l w r)
-  have \<open>sum_weights (Node l w r) = sum_weights l + sum_weights r\<close> by simp
-  moreover have \<open>... = size (to_str l) + size (to_str r)\<close> using Node by simp
-  moreover have \<open>... = size (to_str l + to_str r)\<close> using literal_plus_size_eq by simp
-  ultimately show ?case by simp
-qed
-
-lemma str_len_eq_size:
-  assumes \<open>valid_rope r\<close>
-  shows   \<open>str_len r = size (to_str r)\<close>
-using assms proof(induction r)
-  case (Leaf s w)
-  then show ?case by simp
-next
-  case (Node l w r)
-  hence left_valid: \<open>valid_rope l\<close> and right_valid: \<open>valid_rope r\<close> and w_def : \<open>w = sum_weights l\<close> by simp+
-  hence \<open>str_len (Node l w r) = sum_weights l + str_len r\<close> by (simp add: Node)
-  moreover have \<open>... = size (to_str l) + size (to_str r)\<close> by (simp add: sum_weights_eq_size left_valid right_valid Node)
-  moreover have \<open>... = size (to_str l + to_str r)\<close> by (simp add: literal_plus_size_eq)
-  ultimately show ?case by simp
-qed
-
-lemma str_len_sum_weights_eq:
-  assumes \<open>valid_rope r\<close>
-  shows \<open>str_len r = sum_weights r\<close>
-  using str_len_eq_size sum_weights_eq_size assms by auto
-
-text\<open>Implement a function that computes the concatenation of two ropes @{term \<open>rope_concat (l::Rope) (r :: Rope)\<close>}\<close>
-
-definition rope_concat :: \<open>Rope \<Rightarrow> Rope \<Rightarrow> Rope\<close> where
-\<open>rope_concat l r = Node l (str_len l) r\<close>
-
-lemma valid_rope_concat:
-  assumes \<open>valid_rope l\<close> \<open>valid_rope r\<close>
-  shows \<open>valid_rope (rope_concat l r)\<close> by (simp add: assms str_len_sum_weights_eq rope_concat_def)
-
-lemma rope_concat_eq: \<open>to_str (rope_concat l r) = to_str l + to_str r\<close> by (simp add: rope_concat_def)
-
-text\<open>Implement a function @{term \<open>rope_delete (r :: Rope) (i :: nat) (len :: nat)\<close>} that returns a rope where the @{term \<open>len\<close>} 
-characters starting from the position @{term \<open>i\<close>} have been removed.\<close>
-
-
-fun split :: \<open>Rope \<Rightarrow> nat \<Rightarrow> Rope \<times> Rope\<close> where
-\<open>split (Leaf s w) i = (mk_leaf (sub_str s {0..<i}), mk_leaf (sub_str s {i..size s}))\<close>|
-\<open>split (Node l w r) i = (if i < w then 
-                            (let (left, right) = split l i 
-                             in (left, rope_concat right r)) 
-                        else 
-                             (if i > w then 
-                                 (let (left,right) = split r (i - w) 
-                                  in (rope_concat l left, right)) 
-                              else (l,r)))\<close>
-
-value \<open>split (Node (Leaf (STR ''44'') 2) 2 (Leaf (STR ''44'') 2)) 0\<close>
-
-value \<open>split (mk_leaf STR ''a'') 0\<close>
-
-lemma valid_split:
-  assumes \<open>valid_rope rope\<close> 
-  shows \<open>valid_rope (fst (split rope i)) \<and> valid_rope (snd (split rope i))\<close> 
-using assms proof(induction \<open>rope\<close> arbitrary: i)
-  case (Leaf x1 x2)
-  then show ?case by simp
-next
-  case (Node l' w r')
-  hence l'_valid: \<open>valid_rope l'\<close> and r'_valid: \<open>valid_rope r'\<close> by auto
-  hence l'_lsplit_valid: \<open>valid_rope (fst (split l' i))\<close> and l'_rsplit_valid: \<open>valid_rope (snd (split l' i))\<close> 
-            and r'_lsplit_valid: \<open>valid_rope (fst (split r' i))\<close> and r'_rsplit_valid: \<open>valid_rope (snd (split r' i))\<close> 
-  using Node by auto
-  show ?case
-  proof(cases \<open>i < w\<close>)
-    case True
-    then show ?thesis using l'_lsplit_valid l'_rsplit_valid 
-      by (simp add: r'_valid split_beta valid_rope_concat)
-  next
-    case False
-    show ?thesis 
-    proof(cases \<open>i = w\<close>)
-      case True
-      then show ?thesis 
-        by (simp add: l'_valid r'_valid)
-    next
-      case False
-      then show ?thesis 
-        by (simp add: Node.IH(2) l'_lsplit_valid l'_rsplit_valid l'_valid r'_valid split_beta valid_rope_concat)
-    qed
-  qed
-qed
-
-fun short_rope :: \<open>Rope \<Rightarrow> bool\<close> where
-\<open>short_rope r = (str_len r \<le> 1)\<close>
-
-fun is_empty :: \<open>Rope \<Rightarrow> bool\<close> where
-\<open>is_empty r = (str_len r = 0)\<close>
-
-fun smart_rope_concat :: \<open>Rope \<Rightarrow> Rope \<Rightarrow> Rope\<close> where
-\<open>smart_rope_concat (Leaf l w_l) (Leaf r w_r) = (if w_r \<le> 1 then Leaf (l + r) (w_l + w_r) else (Node (Leaf l w_l) w_l (Leaf r w_r)))\<close>|
-\<open>smart_rope_concat (Node l w r) (Leaf r' w') = (if w' \<le> 1 then Node l w (smart_rope_concat r (Leaf r' w')) else (Node (Node l w r) w (Leaf r' w')))\<close>|
-\<open>smart_rope_concat (Leaf l w) (Node l' w' r) = (if w \<le> 1 then Node (smart_rope_concat (Leaf l w) l') (w + w') r else (Node (Leaf l w) w (Node l' w' r)))\<close>|
-\<open>smart_rope_concat (Node l w r) (Node l' w' r') = Node (Node l w r) w (Node l' w' r')\<close>
-
-value \<open>smart_rope_concat (Node (mk_leaf STR ''?'') 1 (mk_leaf STR ''?'')) (mk_leaf STR '''')\<close>
-
-lemma smart_rope_concat_eq: 
-  assumes \<open>valid_rope l\<close> \<open>valid_rope r\<close>
-  shows \<open>to_str (smart_rope_concat l r) = to_str (rope_concat l r)\<close> 
-using assms proof(induction l )
-  case (Leaf l w_l)
-  show ?case 
-  using assms(2) proof(induction \<open>r\<close>)
-    case (Leaf r' w_r)
-    then show ?case
-      by (simp add: rope_concat_eq)
-  next
-    case (Node r_l w_r r')
-    then show ?case
-      by (simp add: add.assoc rope_concat_eq)
-  qed
-next
-  case (Node l1 x2 l2)
-  then show ?case 
-    using assms(2) proof(induction r)
-    case (Leaf x1 x2)
-    then show ?case 
-      by (simp add: add.assoc rope_concat_eq)
-  next
-    case (Node r1 x2 r2)
-    then show ?case
-      by (simp add: rope_concat_def)
-  qed
-qed
-
-lemma smart_concat_lessThanEq_rope_concat:
-  assumes \<open>valid_rope l\<close> \<open>valid_rope r\<close>
-  shows \<open>size (smart_rope_concat l r) \<le> size(rope_concat l r)\<close> 
-  using assms proof(induction l)
-  case (Leaf x1 x2)
-  then show ?case 
-    using assms(2) proof(induction r)
-    case (Leaf x1 x2)
-    then show ?case 
-      by (simp add: rope_concat_def)
-  next
-    case (Node r1 x2 r2)
-    then show ?case by (simp add: rope_concat_def)
-  qed
-next
-  case (Node l1 x2 l2)
-  then show ?case using assms(2) by(induction r, simp_all add: rope_concat_def)
-qed
-
-fun safe_rope_delete :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (Rope \<times> Rope)\<close> where
-\<open>safe_rope_delete rope i len = (let (left,rem) = split rope i; 
-                               (_, right) = split rem len;
-                               return = (if is_empty left then right else if is_empty right then left else rope_concat left right)
-                            in (rem, return))\<close>
-
-definition rope_delete :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> Rope\<close> where
-\<open>rope_delete  r i len = snd (safe_rope_delete r i len)\<close>
-
-definition rope_sub_str :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> Rope\<close> where
-\<open>rope_sub_str r i len = fst (safe_rope_delete r i len)\<close>
-
-
-definition \<open>hello_my_rope \<equiv> rope_concat (Leaf STR ''Hello_'' 6) (Leaf STR ''my_'' 3)\<close>
-
-definition \<open>name_i_rope \<equiv> rope_concat (Leaf STR ''na'' 2) (Leaf STR ''me_i'' 4)\<close>
-
-definition \<open>s_Simon_rope \<equiv> rope_concat (Leaf STR ''s'' 1) (Leaf STR ''_Simon'' 6)\<close>
-
-definition \<open>name_is_Simon_rope \<equiv> rope_concat name_i_rope s_Simon_rope\<close>
-
-definition \<open>hello_my_name_is_Simon_rope \<equiv> rope_concat (rope_concat hello_my_rope name_is_Simon_rope) (Leaf STR '''' 0)\<close>
-
-value \<open>to_str (rope_delete hello_my_name_is_Simon_rope (2) 15)\<close>
-
-text\<open>Implement a function @{term \<open>rope_insert (r :: Rope) (i :: nat) (s :: String.literal)\<close>} that inserts the string @{term s} at position @{term \<open>i\<close>}.\<close>
-
-fun rope_insert :: \<open>Rope \<Rightarrow> nat \<Rightarrow> String.literal \<Rightarrow> Rope\<close> where
-\<open>rope_insert r i s = (let (left, right) = split r i in rope_concat (rope_concat left (mk_leaf s)) right)\<close>
-
-value \<open>to_str (rope_insert hello_my_name_is_Simon_rope  9 STR ''first_'')\<close>
-
-definition \<open>test r i len = rope_insert (rope_delete r i len) i (to_str (rope_sub_str r i len))\<close>
-                                                                    
-value \<open>safe_rope_delete (Node (Leaf STR ''a'' 1) 1 (Leaf STR ''a'' 1)) 1 1 \<close>
-
-lemma \<open>rope_insert (rope_delete r i len) i (to_str (rope_sub_str r i len)) = r\<close> oops
-text\<open>These methods are correct as is, but do not perform the most optimally. Optimize these operations by implementing
- a function @{term \<open>rebalance\<close>} that rebalances the the Rope.\<close>
-
-fun rebalance :: \<open>Rope \<Rightarrow> Rope\<close> where
-\<open>rebalance (Leaf s w) = Leaf s w\<close>|
-\<open>rebalance (Node l w r) = \<close>
-end
\ No newline at end of file
diff --git a/VerifyThis2024/Ropes_Template.thy~ b/VerifyThis2024/Ropes_Template.thy~
deleted file mode 100644
index b6ce564..0000000
--- a/VerifyThis2024/Ropes_Template.thy~
+++ /dev/null
@@ -1,77 +0,0 @@
-theory Ropes_Template
-  imports Utils  
-begin
-
-chapter\<open>Challenge 0 from VerifyThis 2024: \<^url>\<open>https://www.pm.inf.ethz.ch/research/verifythis.html\<close>\<close>
-
-section\<open>The Rope Data Structure\<close>
-
-text\<open>The task is to implement a "Rope" ( \<^url>\<open>https://en.wikipedia.org/wiki/Rope_(data_structure)\<close> ) 
-originally published by Boehm - \<^url>\<open>https://www.cs.tufts.edu/comp/150FP/archive/hans-boehm/ropes.pdf\<close>
-- a special type of binary tree to efficiently store strings (in honor of Billy who can't be here today).\<close>
-
-text\<open>Since the first half of this challenge is quite easy in HOL (termination and non crashing of basic functions),
-we will skip the "trivial components" that can be found in \<^file>\<open>Utils.thy\<close>\<close>
-
-section\<open>Tasks\<close>
-
-text\<open>The following are my play on ADTs using locales. We have three tiers:
- 
-\<bullet> Basic
-\<bullet> Intermediate
-\<bullet> Advanced
-
-\<close>
-subsection\<open>Basic Ropes\<close>
-
-text\<open>
-Basic ropes require the implementation of efficient length calculation,
-inefficient "naive" concatenation and finally splitting a rope into two across an index.
-\<close>
-
-locale Basic_Ropes =
-  fixes str_len :: \<open>Rope \<Rightarrow> nat\<close>
-  and   rope_concat :: \<open>Rope \<Rightarrow> Rope \<Rightarrow> Rope\<close>
-  and   rope_split :: \<open>Rope \<Rightarrow> nat \<Rightarrow> Rope \<times> Rope\<close>
-assumes \<open>\<And>r. valid_rope r \<Longrightarrow> str_len r = size (to_str r)\<close>
-        \<open>\<And>l r. \<lbrakk>valid_rope l; valid_rope r\<rbrakk> \<Longrightarrow> to_str (rope_concat l r) = to_str l + to_str r\<close>
-        \<open>\<And>i r. valid_rope r \<Longrightarrow> valid_rope (fst (rope_split r i)) \<and> valid_rope (snd (rope_split r i))\<close>
-
-subsection\<open>Intermediate Ropes\<close>
-
-text\<open>Intermediate Ropes require the implementation of "efficient" concatenation as similar to Boehm's \<^url>\<open>https://www.cs.tufts.edu/comp/150FP/archive/hans-boehm/ropes.pdf\<close>.
-and a naive implementation of delete, sub string and insert. Naive in the sense that deleting then inserting the same string is not structure preserving. 
-However inserting then deleting the same string should be structure preserving.
-\<close>
-
-locale Intermediate_Ropes = Basic_Ropes + 
-  fixes boehm_concat :: \<open>Rope \<Rightarrow> Rope \<Rightarrow> Rope\<close> 
-  and   rope_delete ::  \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> Rope\<close>
-  and   rope_sub_str :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> Rope\<close>
-  and   rope_insert ::  \<open>Rope \<Rightarrow> nat \<Rightarrow> String.literal \<Rightarrow> Rope\<close>
-assumes \<open>\<And>l r. \<lbrakk>valid_rope l; valid_rope r\<rbrakk> \<Longrightarrow> to_str (boehm_concat l r) = to_str l + to_str r\<close>
-        \<open>\<And>l r. \<lbrakk>valid_rope l; valid_rope r\<rbrakk> \<Longrightarrow> size (boehm_concat l r) \<le> size (rope_concat l r)\<close>
-        \<open>\<And>r i str. valid_rope r \<Longrightarrow> rope_delete (rope_insert r i str) i (size str) = r\<close>
-        \<open>\<And>r i len. valid_rope r \<Longrightarrow> to_str (rope_insert (rope_delete r i len) i (to_str (rope_sub_str r i len))) = to_str r\<close>
-
-subsection\<open>Advanced Ropes\<close>
-
-text\<open>Advanced Ropes are really what makes them useful data structures. 
-Before, all rope functions have been functionally correct, but not efficient due to the lack of rebalancing. 
-These require the implementation of a rebalance function to balance a Rope, and a function mk_rope which constructs a non-trivially balanced Rope from a string.
-Using this rebalance function, implement efficient an efficient insert and delete which preserves the balancing of the tree\<close>
-
-
-locale Advanced_Ropes = Intermediate_Ropes +
-  fixes max_leaf_size :: \<open>nat\<close>
-  and   rebalance :: \<open>Rope \<Rightarrow> Rope\<close>
-  and   mk_Rope ::   \<open>String.literal \<Rightarrow> Rope\<close>
-  and   efficient_delete :: \<open>Rope \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> Rope\<close>
-  and   efficient_insert :: \<open>Rope \<Rightarrow> nat \<Rightarrow> String.literal \<Rightarrow> Rope\<close>
-assumes \<open>\<And>r. \<not> is_balanced r \<and> valid_rope r \<Longrightarrow> is_balanced (rebalance r)\<close>
-        \<open>\<And>s.   is_balanced (mk_Rope s)\<close>
-        \<open>\<And>r i str. is_balanced r \<Longrightarrow> is_balanced (rope_insert r i str) \<and> (\<forall>leaf \<in># all_leaves (rope_insert r i str). str_len leaf \<in> {0<..max_leaf_size})\<close>
-        \<open>\<And>r i len. is_balanced r \<Longrightarrow> is_balanced (efficient_delete r i len)\<close>
-
-
-end
\ No newline at end of file
diff --git a/VerifyThis2024/Utils.thy~ b/VerifyThis2024/Utils.thy~
deleted file mode 100644
index 9d71027..0000000
--- a/VerifyThis2024/Utils.thy~
+++ /dev/null
@@ -1,89 +0,0 @@
-theory Utils
-  imports Main Fibonacci "HOL-Library.Multiset"
-begin
-
-chapter\<open>Helper Lemmas, Functions and Definitions\<close>
-
-section\<open>String Literal helper lemmas for Rope proofs\<close>
-
-lemma literal_plus_size_eq: \<open>size ((l::String.literal) + r) = size l + size r\<close>
-  by (simp add: plus_literal.rep_eq size_literal.rep_eq)
-
-fun sub_str :: \<open>String.literal \<Rightarrow> nat set \<Rightarrow> String.literal\<close> where
-\<open>sub_str s I = String.implode (nths (literal.explode s) I)\<close>
-
-lemma explode_sub_str: \<open>literal.explode (sub_str s I) = nths (literal.explode s) I\<close> 
-  by (metis String.implode_explode_eq implode.rep_eq nths_map sub_str.simps)
-
-lemma size_implode_single: \<open>size (String.implode [x]) = Suc 0\<close> by (simp add: size_literal.rep_eq)
-
-lemma size_implode: \<open>size (String.implode xs) = length xs\<close> 
-proof(induction xs)
-  case Nil
-  then show ?case 
-    by (simp add: size_literal.rep_eq)
-next
-  case (Cons a xs)
-  have \<open>size (String.implode (a # xs)) = (size (String.implode [a] + String.implode xs))\<close> 
-    apply (simp add: String.implode_def)
-    by (metis String.explode_implode_eq add_0 add_Suc implode.abs_eq length_Cons list.simps(8,9)
-        list.size(3) literal_plus_size_eq size_literal.rep_eq)
-  moreover have \<open>... = Suc (size (String.implode xs))\<close> by (simp add: literal_plus_size_eq size_implode_single)
-  moreover have \<open>... = Suc (length xs)\<close> using Cons by blast
-  ultimately show ?case by simp 
-qed
-
-lemma size_sub_str: \<open>size (sub_str s I) = card {i. i < size s \<and> i \<in> I}\<close> 
-  by(simp add: size_implode length_nths size_literal.rep_eq)
-
-lemma atLeastLessThan_eq: \<open>{i..<size s} = {ia. ia < size s \<and> i \<le> ia}\<close> by auto
-
-lemma atLeastAtMost_eq: \<open>(if i < size s then {..i} else {..<size s}) = {ia. ia < size s \<and> ia \<le> i}\<close> by auto
-
-lemma size_sub_str_atLeast: \<open>size (sub_str s {i..}) = size s - i\<close> unfolding size_sub_str[of s \<open>{i..}\<close>]
-  by (simp add: atLeastLessThan_eq[symmetric])
-
-lemma size_sub_str_atMost: \<open>size (sub_str s {..i}) = (if i < size s then Suc i else size s)\<close> unfolding size_sub_str[of s \<open>{..i}\<close>]
-  by (simp add: atLeastAtMost_eq[symmetric])
-
-section\<open>Rope Definitions\<close>
-
-subsection\<open>Basics\<close>
-
-datatype Rope =  Leaf String.literal nat | Node Rope nat Rope 
-
-definition \<open>hello_world_rope \<equiv> Node (Leaf (STR ''Hello '') 6) 6 (Leaf (STR ''World'') 5)\<close> 
-
-fun mk_leaf :: \<open>String.literal \<Rightarrow> Rope\<close> where
-\<open>mk_leaf s = Leaf s (size s)\<close>
-
-fun sum_weights :: \<open>Rope \<Rightarrow> nat\<close> where 
-\<open>sum_weights (Leaf _ s) = s\<close>|
-\<open>sum_weights (Node l w r) = sum_weights l + sum_weights r\<close>
-
-fun valid_rope :: \<open>Rope \<Rightarrow> bool\<close> where
-\<open>valid_rope (Leaf s w) = (size s = w)\<close>|
-\<open>valid_rope (Node l w r) = (valid_rope l \<and> valid_rope r \<and> (w = sum_weights l))\<close>
-
-fun to_str :: \<open>Rope \<Rightarrow> String.literal\<close> where 
-\<open>to_str (Leaf s _) = s\<close>|
-\<open>to_str (Node l _ r) = to_str l + to_str r\<close>
-
-fun all_leaves :: \<open>Rope \<Rightarrow> Rope multiset\<close> where
-\<open>all_leaves (Leaf s w) = {# Leaf s w #}\<close>|
-\<open>all_leaves (Node l _ r) = all_leaves l \<union># all_leaves r\<close>
-
-subsection\<open>Advanced\<close>
-
-text\<open>The following formalises the definition of balanced from Boehm \<^url>\<open>https://www.cs.tufts.edu/comp/150FP/archive/hans-boehm/ropes.pdf\<close>\<close>
-
-definition rope_width :: \<open>Rope \<Rightarrow> nat\<close> where
-\<open>rope_width r = size (all_leaves r)\<close>
-
-definition is_balanced :: \<open>Rope \<Rightarrow> bool\<close> where
-\<open>is_balanced r = (fib (size r + 2) \<le> sum_weights r)\<close>
-
-value \<open>is_balanced hello_world_rope\<close>
-
-value \<open>fib 5\<close>
-end
\ No newline at end of file