diff --git a/source/Scrolls/BouncingScroll.mmt b/source/Scrolls/BouncingScroll.mmt
index 331f8a052ac5f65cf385a9723d02a33afc819ea2..9f136cc8e1d95a862d40bd7607169cc45a9c18ed 100644
--- a/source/Scrolls/BouncingScroll.mmt
+++ b/source/Scrolls/BouncingScroll.mmt
@@ -10,14 +10,14 @@ theory BouncingScroll =
     meta ?MetaAnnotations?solutionTheory ?BouncingScroll/Solution ❙
     include ?StepUntil ❙
     theory funcs =
-        //get_ht : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
+        get_ht : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
             [z,zv,g] times_real_lit (minus_real_lit (plus_real_lit zv (sqrt (plus_real_lit (times_real_lit zv zv) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) z)))))) (inv_real_lit g) ❙
-        //new_ht : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
+        new_ht : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
             [zv,g,ht,bo] times_real_lit (times_real_lit (minus_real_lit 2.0) (times_real_lit (minus_real_lit bo) (plus_real_lit (times_real_lit g ht) zv))) (inv_real_lit g) ❙
-        //prep : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ❘ =
+        prep : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ❘ =
             [x,y,z,xv,yv,zv,g,bo] ⟨⟨x, y, z⟩, ⟨xv, yv, zv⟩, ⟨g, get_ht z zv g, bo⟩⟩ ❙
         //vals order: (x,y,z),(xv,yv,zv),(g,ht,bo) ❙
-        //edit : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ❘ =
+        edit : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ❘ =
             [vals] ⟨⟨plus_real_lit (πl (πl vals)) (times_real_lit (πl (πr (πr (πr vals)))) (πl (πl (πr vals)))),
                     plus_real_lit (Ï€l (Ï€r (Ï€l vals))) (times_real_lit (Ï€l (Ï€r (Ï€r (Ï€r vals)))) (Ï€l (Ï€r (Ï€l (Ï€r vals))))),
                     0.0⟩,
@@ -27,26 +27,16 @@ theory BouncingScroll =
                     ⟨(πl (πr (πr vals))),
                     new_ht (Ï€r (Ï€r (Ï€l (Ï€r vals)))) (Ï€l (Ï€r (Ï€r vals))) (Ï€l (Ï€r (Ï€r (Ï€r vals)))) (Ï€r (Ï€r (Ï€r (Ï€r vals)))),
                     (πr (πr (πr (πr vals))))⟩⟩ ❙
-        //fun0 : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ =
-            [vals] cons vals nil ❙
-        //fun1 : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ =
-            [vals] cons vals (fun0 (edit vals)) ❙
-        //fun2 : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ =
-            [vals] cons vals (fun1 (edit vals)) ❙
-        //fun3 : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ =
-            [vals] cons vals (fun2 (edit vals)) ❙
-        //red_ht_helper : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ ℝ ❘ =
+        red_ht_helper : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ ℝ ❘ =
             [cele] πl (πr (πr (πr cele))) ❙
-        //red_ht : List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ⟶ List[ℝ] ❘ =
+        red_ht : List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ⟶ List[ℝ] ❘ =
             [clsele] clsele map ([xele] red_ht_helper xele) ❙
-        //red_vals_helper : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ❘ =
-            [cel] ⟨πl cel, πl (πr cel)⟩ ❙
-        //red_vals : List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ⟶ List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ =
-            [cls] (cls map ([x1] red_vals_helper x1)) ++ nil ❙
-        //get_pos_fun: ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (ℝ ⟶ (ℝ × ℝ × ℝ)) ❘ =
+        get_pos_fun: ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (ℝ ⟶ (ℝ × ℝ × ℝ)) ❘ =
             [x,y,z,xv,yv,zv,g] ([t] ⟨plus_real_lit x (times_real_lit xv t), plus_real_lit y (times_real_lit yv t), plus_real_lit (times_real_lit (times_real_lit 0.5 g) (times_real_lit t t)) (plus_real_lit z (times_real_lit zv t))⟩ ) ❙
-        //red_funcs : List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ⟶ List[ℝ ⟶ (ℝ × ℝ × ℝ)] ❘ =
-            [cls] (cls map ([x] get_pos_fun (πl (πl vals)) (πl (πr (πl vals))) (πr (πr (πl vals)))  (πl (πl (πr vals))) (πl (πr (πl (πr vals)))) (πr (πr (πl (πr vals)))) (πl (πr (πr vals))))) ++ nil ❙
+        red_funcs : List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ⟶ List[ℝ ⟶ (ℝ × ℝ × ℝ)] ❘ =
+            [cls] (cls map ([vals] get_pos_fun (πl (πl vals)) (πl (πr (πl vals))) (πr (πr (πl vals)))  (πl (πl (πr vals))) (πl (πr (πl (πr vals)))) (πr (πr (πl (πr vals)))) (πl (πr (πr vals))))) ++ nil ❙
+        end_cond : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ bool ❘ =
+            [vals] leq_real_lit (πl (πr (πr (πr vals)))) 0.1 ❙
     ❚
     // start position and velocity ❙
     theory Problem =
@@ -64,15 +54,11 @@ theory BouncingScroll =
     // the output of the scroll ❙
     theory Solution =
         include ?BouncingScroll/Problem ❙
-        //full_list: List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ =
-            fun3 (prep xposition yposition zposition xvelocity yvelocity zvelocity g_base bounce) ❙
+        full_list: List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ = stepUntil ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) (prep xposition yposition zposition xvelocity yvelocity zvelocity g_base bounce) edit end_cond ❙
+        ht_list_test: List[ℝ] ❘ = red_ht (cons (prep xposition yposition zposition xvelocity yvelocity zvelocity g_base bounce) nil) ❙
+        fun_list_test : List[ℝ ⟶ (ℝ × ℝ × ℝ)] ❘ = red_funcs (cons (prep xposition yposition zposition xvelocity yvelocity zvelocity g_base bounce) nil) ❙
         //ht_list: List[ℝ] ❘ = red_ht full_list ❙
-        //val_list: List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ = red_vals full_list ❙
-        test_func : ℝ ⟶ ℝ ❘ =
-            [x] plus_real_lit x 1.0 ❙
-        test_bool : ℝ ⟶ bool ❘ =
-            [x] leq_real_lit 10.0 x ❙
-        out_list: List[ℝ] ❘ = stepUntil ℝ 0.0 test_func test_bool ❙
+        //fun_list : List[ℝ ⟶ (ℝ × ℝ × ℝ)] ❘ = red_funcs full_list ❙
         meta ?MetaAnnotations?label "BouncingScroll" ❙
         meta ?MetaAnnotations?description s"Bouncing " ❙
     ❚