diff --git a/source/Scrolls/T3DBouncingScroll.mmt b/source/Scrolls/T3DBouncingScroll.mmt
index 2c858cc8b3897ce6b8527e35b4b743a54a63bf38..01fe9052d3190b474bfce2d71d9f0d42715ec2fd 100644
--- a/source/Scrolls/T3DBouncingScroll.mmt
+++ b/source/Scrolls/T3DBouncingScroll.mmt
@@ -42,12 +42,26 @@ theory T3DBouncingScroll =
             [rht, rp, rv, rg] ⟨plus_real_lit (plus_real_lit (rp _x) (times_real_lit (rv _x) rht)) (times_real_lit (times_real_lit 0.5 (rg _x)) (times_real_lit rht rht)),
                                plus_real_lit (plus_real_lit (rp _y) (times_real_lit (rv _y) rht)) (times_real_lit (times_real_lit 0.5 (rg _y)) (times_real_lit rht rht)),
                                plus_real_lit (plus_real_lit (rp _z) (times_real_lit (rv _z) rht)) (times_real_lit (times_real_lit 0.5 (rg _z)) (times_real_lit rht rht))⟩ ❙
-        check_hit : (ℝ × wall) ⟶ point ⟶ point ⟶ point  ⟶ bool ❘ = 
-            [rw, rp, rv, rg] ([np : point] (bool) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((Ï€r rw).point3) ((Ï€r rw).point2)) (point_subtractI np ((Ï€r rw).point2))) (vec_cross (point_subtractI ((Ï€r rw).point3) ((Ï€r rw).point2)) (point_subtractI ((Ï€r rw).point1) ((Ï€r rw).point2)))))
-                                                  thenx ((bool) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((Ï€r rw).point3) ((Ï€r rw).point1)) (point_subtractI np ((Ï€r rw).point1))) (vec_cross (point_subtractI ((Ï€r rw).point3) ((Ï€r rw).point1)) (point_subtractI ((Ï€r rw).point2) ((Ï€r rw).point1)))))
-                                                                thenx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((Ï€r rw).point2) ((Ï€r rw).point1)) (point_subtractI np ((Ï€r rw).point1))) (vec_cross (point_subtractI ((Ï€r rw).point2) ((Ï€r rw).point1)) (point_subtractI ((Ï€r rw).point3) ((Ï€r rw).point1)))))
-                                                                elsex false)
-                                                  elsex false) (get_pt (πl rw) rp rv rg) ❙
+        check_hit1 : point ⟶ point ⟶ point ⟶ ((ℝ × ℝ × wall) ⟶ (ℝ × ℝ × wall)) ❘ = 
+            [rp, rv, rg] ([rw: ℝ × ℝ × wall] ([np : point] (ℝ × ℝ × wall) ifx (leq_real_lit (πl rw) 0.000001)
+                thenx (⟨-1.0, πl (πr rw), πr (πr rw)⟩)
+                elsex ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point2)) (point_subtractI np ((πr (πr rw)).point2))) (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point2)) (point_subtractI ((πr (πr rw)).point1) ((πr (πr rw)).point2)))))
+                    thenx ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)) (point_subtractI np ((πr (πr rw)).point1))) (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)) (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)))))
+                        thenx ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)) (point_subtractI np ((πr (πr rw)).point1))) (vec_cross (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)) (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)))))
+                            thenx (rw)
+                            elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))
+                        elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))
+                    elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))) (get_pt (πl rw) rp rv rg)) ❙
+        check_hit2 : point ⟶ point ⟶ point ⟶ ((ℝ × ℝ × wall) ⟶ (ℝ × ℝ × wall)) ❘ = 
+            [rp, rv, rg] ([rw: ℝ × ℝ × wall] ([np : point] (ℝ × ℝ × wall) ifx (leq_real_lit (πl (πr rw)) 0.000001)
+                thenx (⟨πl rw, -1.0, πr (πr rw)⟩)
+                elsex ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point2)) (point_subtractI np ((πr (πr rw)).point2))) (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point2)) (point_subtractI ((πr (πr rw)).point1) ((πr (πr rw)).point2)))))
+                    thenx ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)) (point_subtractI np ((πr (πr rw)).point1))) (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)) (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)))))
+                        thenx ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)) (point_subtractI np ((πr (πr rw)).point1))) (vec_cross (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)) (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)))))
+                            thenx (rw)
+                            elsex (⟨πl rw, -1.0, πr (πr rw)⟩))
+                        elsex (⟨πl rw, -1.0, πr (πr rw)⟩))
+                    elsex (⟨πl rw, -1.0, πr (πr rw)⟩))) (get_pt (πl (πr rw)) rp rv rg)) ❙
         fold_func : (ℝ × wall) ⟶ (point × ℝ) ⟶ (point × ℝ) ❘ = 
             [cur][acc] (point × ℝ) ifx (leq_real_lit (πl cur) (πr acc)) thenx (⟨(πr cur).norm_vec, (πl cur)⟩) elsex acc ❙
         calc_new_vals : (point × point × (point × ℝ) × ℝ) ⟶ (point × ℝ) ⟶ (point × point × ℝ) ❘ =
@@ -71,9 +85,9 @@ theory T3DBouncingScroll =
                                                                  thenx (⟨πl wsi, πr (πr wsi)⟩)
                                                                  elsex (⟨πl (πr wsi), πr (πr wsi)⟩))) ❙
         get_next_vals : List[wall] ⟶ (point × ℝ) ⟶ ((point × point × (point × ℝ) × ℝ) ⟶ (point × point × (point × ℝ) × ℝ)) ❘ =
-            [aw, abv] ([v : point × point × (point × ℝ) × ℝ] ([x : point × point × ℝ] ⟨πl x, πl (πr x), ((((((get_abcs aw (πl x) (πl (πr x)) (πl abv)) map mget_hts) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) filter ([wsk : ℝ × wall] check_hit wsk (πl x) (πl (πr x)) (πl abv))) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func), πr (πr x)⟩) (calc_new_vals v abv)) ❙
+            [aw, abv] ([v : point × point × (point × ℝ) × ℝ] ([x : point × point × ℝ] ⟨πl x, πl (πr x), (((((((get_abcs aw (πl x) (πl (πr x)) (πl abv)) map mget_hts) map (check_hit1 (πl x) (πl (πr x)) (πl abv))) map (check_hit2 (πl x) (πl (πr x)) (πl abv))) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func), πr (πr x)⟩) (calc_new_vals v abv)) ❙
         prep : List[wall] ⟶ point ⟶ point ⟶ point ⟶ (point × point × (point × ℝ) × ℝ) ❘ =
-		    [awi, p, v, g]  ⟨p, v, ((((((get_abcs awi p v g) map mget_hts) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) filter ([wsk : ℝ × wall] check_hit wsk p v g)) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func), 0.0⟩ ❙
+		    [awi, p, v, g]  ⟨p, v, (((((((get_abcs awi p v g) map mget_hts) map (check_hit1 p v g)) map (check_hit2 p v g)) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func), 0.0⟩ ❙
         get_pos_fun: point ⟶ point ⟶ point ⟶ (ℝ ⟶ point) ❘ =
             [p, v, g] ([t] ⟨plus_real_lit (times_real_lit (times_real_lit 0.5 (g _x)) (times_real_lit t t)) (plus_real_lit (p _x) (times_real_lit (v _x) t)), plus_real_lit (times_real_lit (times_real_lit 0.5 (g _y)) (times_real_lit t t)) (plus_real_lit (p _y) (times_real_lit (v _y) t)), plus_real_lit (times_real_lit (times_real_lit 0.5 (g _z)) (times_real_lit t t)) (plus_real_lit (p _z) (times_real_lit (v _z) t))⟩) ❙
         red_ht : (point × point × (point × ℝ)) ⟶ ℝ ❘ =
diff --git a/source/Scrolls/W3DBouncingScroll.mmt b/source/Scrolls/W3DBouncingScroll.mmt
index 6915a782c8688fe0756e16e3a08484b97175a040..0a2aa4ea311a13c724e3c631c7f6631b51941917 100644
--- a/source/Scrolls/W3DBouncingScroll.mmt
+++ b/source/Scrolls/W3DBouncingScroll.mmt
@@ -42,14 +42,30 @@ theory W3DBouncingScroll =
             [rht, rp, rv, rg] ⟨plus_real_lit (plus_real_lit (rp _x) (times_real_lit (rv _x) rht)) (times_real_lit (times_real_lit 0.5 (rg _x)) (times_real_lit rht rht)),
                                plus_real_lit (plus_real_lit (rp _y) (times_real_lit (rv _y) rht)) (times_real_lit (times_real_lit 0.5 (rg _y)) (times_real_lit rht rht)),
                                plus_real_lit (plus_real_lit (rp _z) (times_real_lit (rv _z) rht)) (times_real_lit (times_real_lit 0.5 (rg _z)) (times_real_lit rht rht))⟩ ❙
-        check_hit : (ℝ × wall) ⟶ point ⟶ point ⟶ point  ⟶ bool ❘ = 
-            [rw, rp, rv, rg] ([np : point] (bool) ifx (leq_real_lit (scalar_productI ((Ï€r rw).point1) ((Ï€r rw).u)) (scalar_productI np ((Ï€r rw).u)))
-                                                  thenx ((bool) ifx (leq_real_lit (scalar_productI np ((Ï€r rw).u)) (scalar_productI ((Ï€r rw).point2) ((Ï€r rw).u)))
-                                                                thenx ((bool) ifx (leq_real_lit (scalar_productI ((Ï€r rw).point1) (point_subtractI ((Ï€r rw).point4) ((Ï€r rw).point1))) (scalar_productI np (point_subtractI ((Ï€r rw).point4) ((Ï€r rw).point1))))
-                                                                              thenx (leq_real_lit (scalar_productI np (point_subtractI ((Ï€r rw).point4) ((Ï€r rw).point1))) (scalar_productI ((Ï€r rw).point4) (point_subtractI ((Ï€r rw).point4) ((Ï€r rw).point1))))
-                                                                              elsex false)
-                                                                elsex false)
-                                                  elsex false) (get_pt (πl rw) rp rv rg) ❙
+        check_hit1 : point ⟶ point ⟶ point ⟶ ((ℝ × ℝ × wall) ⟶ (ℝ × ℝ × wall)) ❘ = 
+            [rp, rv, rg] ([rw: ℝ × ℝ × wall] ([np : point] (ℝ × ℝ × wall) ifx (leq_real_lit (πl rw) 0.000001)
+                thenx (⟨-1.0, πl (πr rw), πr (πr rw)⟩)
+                elsex ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI ((πr (πr rw)).point1) ((πr (πr rw)).u)) (scalar_productI np ((πr (πr rw)).u)))
+                    thenx ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI np ((πr (πr rw)).u)) (scalar_productI ((πr (πr rw)).point2) ((πr (πr rw)).u)))
+                        thenx ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI ((πr (πr rw)).point1) (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))) (scalar_productI np (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))))
+                            thenx ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI np (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))) (scalar_productI ((πr (πr rw)).point4) (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))))
+                                thenx (rw)
+                                elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))
+                            elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))
+                        elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))
+                    elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))) (get_pt (πl rw) rp rv rg)) ❙
+        check_hit2 : point ⟶ point ⟶ point ⟶ ((ℝ × ℝ × wall) ⟶ (ℝ × ℝ × wall)) ❘ = 
+            [rp, rv, rg] ([rw: ℝ × ℝ × wall] ([np : point] (ℝ × ℝ × wall) ifx (leq_real_lit (πl (πr rw)) 0.000001)
+                thenx (⟨πl rw, -1.0, πr (πr rw)⟩)
+                elsex ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI ((πr (πr rw)).point1) ((πr (πr rw)).u)) (scalar_productI np ((πr (πr rw)).u)))
+                    thenx ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI np ((πr (πr rw)).u)) (scalar_productI ((πr (πr rw)).point2) ((πr (πr rw)).u)))
+                        thenx ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI ((πr (πr rw)).point1) (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))) (scalar_productI np (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))))
+                            thenx ((ℝ × ℝ × wall) ifx (leq_real_lit (scalar_productI np (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))) (scalar_productI ((πr (πr rw)).point4) (point_subtractI ((πr (πr rw)).point4) ((πr (πr rw)).point1))))
+                                thenx (rw)
+                                elsex (⟨πl rw, -1.0, πr (πr rw)⟩))
+                            elsex (⟨πl rw, -1.0, πr (πr rw)⟩))
+                        elsex (⟨πl rw, -1.0, πr (πr rw)⟩))
+                    elsex (⟨πl rw, -1.0, πr (πr rw)⟩))) (get_pt (πl (πr rw)) rp rv rg)) ❙
         fold_func : (ℝ × wall) ⟶ (point × ℝ) ⟶ (point × ℝ) ❘ = 
             [cur][acc] (point × ℝ) ifx (leq_real_lit (πl cur) (πr acc)) thenx (⟨(πr cur).norm_vec, (πl cur)⟩) elsex acc ❙
         calc_new_vals : (point × point × (point × ℝ) × ℝ) ⟶ (point × ℝ) ⟶ (point × point × ℝ) ❘ =
@@ -73,9 +89,9 @@ theory W3DBouncingScroll =
                                                                  thenx (⟨πl wsi, πr (πr wsi)⟩)
                                                                  elsex (⟨πl (πr wsi), πr (πr wsi)⟩))) ❙
         get_next_vals : List[wall] ⟶ (point × ℝ) ⟶ ((point × point × (point × ℝ) × ℝ) ⟶ (point × point × (point × ℝ) × ℝ)) ❘ =
-            [aw, abv] ([v : point × point × (point × ℝ) × ℝ] ([x : point × point × ℝ] ⟨πl x, πl (πr x), ((((((get_abcs aw (πl x) (πl (πr x)) (πl abv)) map mget_hts) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) filter ([wsk : ℝ × wall] check_hit wsk (πl x) (πl (πr x)) (πl abv))) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func), πr (πr x)⟩) (calc_new_vals v abv)) ❙
+            [aw, abv] ([v : point × point × (point × ℝ) × ℝ] ([x : point × point × ℝ] ⟨πl x, πl (πr x), (((((((get_abcs aw (πl x) (πl (πr x)) (πl abv)) map mget_hts) map (check_hit1 (πl x) (πl (πr x)) (πl abv))) map (check_hit2 (πl x) (πl (πr x)) (πl abv))) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func), πr (πr x)⟩) (calc_new_vals v abv)) ❙
         prep : List[wall] ⟶ point ⟶ point ⟶ point ⟶ (point × point × (point × ℝ) × ℝ) ❘ =
-		    [awi, p, v, g]  ⟨p, v, ((((((get_abcs awi p v g) map mget_hts) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) filter ([wsk : ℝ × wall] check_hit wsk p v g)) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func), 0.0⟩ ❙
+		    [awi, p, v, g]  ⟨p, v, (((((((get_abcs awi p v g) map mget_hts) map (check_hit1 p v g)) map (check_hit2 p v g)) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func), 0.0⟩ ❙
         get_pos_fun: point ⟶ point ⟶ point ⟶ (ℝ ⟶ point) ❘ =
             [p, v, g] ([t] ⟨plus_real_lit (times_real_lit (times_real_lit 0.5 (g _x)) (times_real_lit t t)) (plus_real_lit (p _x) (times_real_lit (v _x) t)), plus_real_lit (times_real_lit (times_real_lit 0.5 (g _y)) (times_real_lit t t)) (plus_real_lit (p _y) (times_real_lit (v _y) t)), plus_real_lit (times_real_lit (times_real_lit 0.5 (g _z)) (times_real_lit t t)) (plus_real_lit (p _z) (times_real_lit (v _z) t))⟩) ❙
         red_ht : (point × point × (point × ℝ)) ⟶ ℝ ❘ =