diff --git a/scala/info/kwarc/mmt/frameit/rules/GetListAtInd.scala b/scala/info/kwarc/mmt/frameit/rules/GetListAtInd.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b459809d3f977fb7e98f6e9925b81aa56969d9d5
--- /dev/null
+++ b/scala/info/kwarc/mmt/frameit/rules/GetListAtInd.scala
@@ -0,0 +1,49 @@
+package info.kwarc.mmt.frameit.rules
+
+import info.kwarc.mmt.api.checking._
+import info.kwarc.mmt.api.{DPath, GlobalName, Path}
+import info.kwarc.mmt.api.frontend.Controller
+import info.kwarc.mmt.api.objects._
+import Conversions._
+import info.kwarc.mmt.api.uom.{RealizedType, Simplifiability, Simplify, StandardInt, StandardPositive}
+import info.kwarc.mmt.lf.ApplySpine
+import info.kwarc.mmt.LFX.datatypes.{Listtype, Ls}
+import info.kwarc.mmt.api.utils.URI
+
+object GetListAtInd {
+  val ns: DPath = DPath(URI.http colon "mathhub.info") / "FrameIT" / "frameworld"
+  val path: GlobalName = ns ? "GetListAtInd" ? "getListAtInd"
+  val rawhead: OMID = OMS(path)
+  def apply(tp1: Term, ls: Term, inde: Term): Term =
+    ApplySpine(this.rawhead, tp1, ls, inde)
+  def unapply(tm : Term) : Option[(Term, Term, Term)] = tm match {
+    case ApplySpine(this.rawhead, List(tp1, ls, inde)) => Some((tp1, ls, inde))
+    case _ => None
+  }
+}
+
+object GetListAtIndComp extends ComputationRule(GetListAtInd.path) {
+  override def applicable(t: Term): Boolean = t match {
+    case GetListAtInd(_, _, _) => true
+    case _ => false
+  }
+  override def apply(check: CheckingCallback)(tm: Term, covered: Boolean)(implicit stack: Stack, history: History): Simplifiability = tm match {
+      case GetListAtInd(_, Ls(lsi), inde) =>
+        val p = Path.parseS("http://mathhub.info/MitM/Foundation?NatLiterals?pos_lit")
+        val indexSimpl = check.simplify(inde)
+        val indexBase = indexSimpl match {
+          case OMLIT(i: BigInt, RealizedType(OMS(`p`), StandardPositive)) => Some(i)
+          case _ => None
+        }
+        indexBase match {
+          case Some(idx) =>
+            val idxInt = idx.toInt
+            if ((idxInt >= lsi.length) || (idxInt < 0)) {
+              return Simplifiability.NoRecurse
+            }
+            Simplify(lsi(idx.toInt))
+          case _ => Simplifiability.NoRecurse
+        }
+      case _ => Simplifiability.NoRecurse
+  }
+}
\ No newline at end of file
diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt
index 5dc2f2aa5d57436b26f47e33a634dc7ec2797eae..03fe76c6bcc82a9747c1702a964c6d76f2ec36ab 100644
--- a/source/DefaultSituationSpace.mmt
+++ b/source/DefaultSituationSpace.mmt
@@ -18,6 +18,7 @@ theory DefaultSituationSpace =
 		include ?BouncingScroll ❙
         include ?WBouncingScroll ❙
         include ?W3DBouncingScroll ❙
+        include ?T3DBouncingScroll ❙
       //  include ?SinOppositeLeg ❙
         include ?CircleLineAngleScroll ❙
         include ?CircleAreaScroll ❙
diff --git a/source/Scrolls/T3DBouncingScroll.mmt b/source/Scrolls/T3DBouncingScroll.mmt
new file mode 100644
index 0000000000000000000000000000000000000000..2c858cc8b3897ce6b8527e35b4b743a54a63bf38
--- /dev/null
+++ b/source/Scrolls/T3DBouncingScroll.mmt
@@ -0,0 +1,105 @@
+namespace http://mathhub.info/FrameIT/frameworld ❚
+
+import base http://mathhub.info/MitM/Foundation ❚
+import arith http://mathhub.info/MitM/core/arithmetics ❚
+import rules scala://datatypes.LFX.mmt.kwarc.info ❚
+
+fixmeta ?FrameworldMeta ❚
+
+theory T3DBouncingScroll =
+    meta ?MetaAnnotations?problemTheory ?T3DBouncingScroll/Problem ❙
+    meta ?MetaAnnotations?solutionTheory ?T3DBouncingScroll/Solution ❙
+    rule rules?FilterRule (true) ❙
+	include ?IfThenElseX ❙
+    include ?StepUntil ❙
+	include ?Triangles ❙
+    //stepUntil : {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ List[X] ❘ # stepUntil 1 2 3 4 ❙
+    //filter2 : List[ℝ × wall] ⟶ ((ℝ × wall) ⟶ bool) ⟶ List[ℝ × wall] ❘ # 1 filter2 2 ❙
+
+	theory funcs =
+        eq_zero : ℝ ⟶ bool ❘ =
+            [val] (bool) ifx (leq_real_lit val 0.000001)
+                         thenx ((bool) ifx (leq_real_lit (minus_real_lit 0.000001) val)
+                                       thenx true
+                                       elsex false)
+                         elsex false ❙
+        get_abcs : List[wall] ⟶ point ⟶ point ⟶ point  ⟶ List[point × wall] ❘ =
+            [w, p, v, g] w map ([wi : wall] ⟨⟨(plus_real_lit (times_real_lit (wi.a) (g _x)) (plus_real_lit (times_real_lit (wi.b) (g _y)) (times_real_lit (wi.c) (g _z)))),
+                                             (plus_real_lit (plus_real_lit (times_real_lit (wi.a) (v _x)) (times_real_lit (wi.b) (v _y))) (times_real_lit (wi.c) (v _z))),
+                                             (plus_real_lit (plus_real_lit (plus_real_lit (times_real_lit (wi.a) (p _x)) (times_real_lit (wi.b) (p _y))) (times_real_lit (wi.c) (p _z))) (minus_real_lit (wi.d)))⟩,
+                                            wi⟩) ❙
+        mget_hts : (point × wall) ⟶ (ℝ × ℝ × wall) ❘ =
+            [cabc] (ℝ × ℝ × wall) ifx (eq_zero ((πl cabc) _x))
+                                  thenx ((ℝ × ℝ × wall) ifx (eq_zero ((πl cabc) _y))
+                                                        thenx (⟨-1.0, -1.0, (πr cabc)⟩)
+                                                        elsex (⟨minus_real_lit (times_real_lit ((πl cabc) _z) (inv_real_lit ((πl cabc) _y))),
+                                                                minus_real_lit (times_real_lit ((πl cabc) _z) (inv_real_lit ((πl cabc) _y))), (πr cabc)⟩))
+                                  elsex ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (plus_real_lit (times_real_lit ((πl cabc) _y) ((πl cabc) _y)) (minus_real_lit (times_real_lit 2.0 (times_real_lit ((πl cabc) _x) ((πl cabc) _z))))))
+                                                        thenx (⟨times_real_lit (plus_real_lit (minus_real_lit ((πl cabc) _y)) (sqrt (plus_real_lit (times_real_lit ((πl cabc) _y) ((πl cabc) _y)) (minus_real_lit (times_real_lit 2.0 (times_real_lit ((πl cabc) _x) ((πl cabc) _z))))))) (inv_real_lit ((πl cabc) _x)),
+                                                                times_real_lit (plus_real_lit (minus_real_lit ((πl cabc) _y)) (minus_real_lit (sqrt (plus_real_lit (times_real_lit ((πl cabc) _y) ((πl cabc) _y)) (minus_real_lit (times_real_lit 2.0 (times_real_lit ((πl cabc) _x) ((πl cabc) _z)))))))) (inv_real_lit ((πl cabc) _x)), (πr cabc)⟩)
+                                                        elsex (⟨-1.0, -1.0, (πr cabc)⟩)) ❙
+	    get_pt : ℝ ⟶ point ⟶ point ⟶ point  ⟶ point ❘ = 
+            [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) ❙
+        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 × ℝ) ❘ =
+            [v, bv] ⟨get_pt (πr (πl (πr (πr v)))) (πl v) (πl (πr v)) (πl bv), ([d : point] vec_multI (πr bv) (point_subtractI d (vec_multI (times_real_lit 2.0 (scalar_productI d (πl (πl (πr (πr v)))))) (πl (πl (πr (πr v))))))) (⟨plus_real_lit ((πl (πr v)) _x) (times_real_lit (πr (πl (πr (πr v)))) ((πl bv) _x)), plus_real_lit ((πl (πr v)) _y) (times_real_lit (πr (πl (πr (πr v)))) ((πl bv) _y)), plus_real_lit ((πl (πr v)) _z) (times_real_lit (πr (πl (πr (πr v)))) ((πl bv) _z))⟩), plus_real_lit (πr (πr (πr v))) (πr (πl (πr (πr v))))⟩ ❙
+        end_cond : (point × point × (point × ℝ) × ℝ) ⟶ bool ❘ =
+            [vals] (bool) ifx (leq_real_lit (Ï€r (Ï€l (Ï€r (Ï€r vals)))) 0.1)
+                          thenx ((bool) ifx (leq_real_lit (sqrt(scalar_productI (Ï€l (Ï€r vals)) (Ï€l (Ï€r vals)))) 10.0)
+                                        thenx (true)
+                                        elsex false)
+                          elsex ((bool) ifx (leq_real_lit 99999.0 (Ï€r (Ï€l (Ï€r (Ï€r vals)))))
+                                        thenx (true)
+                                        elsex false) ❙
+        map_reduce_hts : (ℝ × ℝ × wall) ⟶ (ℝ × wall) ❘ =
+            [wsi] (ℝ × wall) ifx (leq_real_lit (πl wsi) 0.000001)
+                             thenx ((ℝ × wall) ifx (leq_real_lit (πl (πr wsi)) 0.000001)
+                                               thenx (⟨-1.0, πr (πr wsi)⟩)
+                                               elsex (⟨πl (πr wsi), πr (πr wsi)⟩))
+                             elsex ((ℝ × wall) ifx (leq_real_lit (πl (πr wsi)) 0.000001)
+                                               thenx (⟨πl wsi, πr (πr wsi)⟩)
+                                               elsex ((ℝ × wall) ifx (leq_real_lit (πl wsi) (πl (πr wsi)))
+                                                                 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)) ❙
+        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⟩ ❙
+        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 × ℝ)) ⟶ ℝ ❘ =
+            [cele] πr (πr (πr cele)) ❙
+        map_fun_list : (point × point × (point × ℝ) × ℝ) ⟶ point ⟶ ((ℝ × ℝ) × (ℝ ⟶ ℝ) × (ℝ ⟶ point)) ❘ =
+            [vals, g] ⟨⟨πr (πr (πr vals)), plus_real_lit (πr (πr (πr vals))) (πr (πl (πr (πr vals))))⟩, ([ts : ℝ] plus_real_lit ts (minus_real_lit (πr (πr (πr vals))))), get_pos_fun (πl vals) (πl (πr vals)) g⟩ ❙
+    ❚
+    // start position and velocity ❙
+    theory Problem =
+	    include ?T3DBouncingScroll/funcs ❙
+        position: point ❘ meta ?MetaAnnotations?label "Pos" ❙
+        velocity: point ❘ meta ?MetaAnnotations?label "Vel" ❙
+        g_base: point ❘ meta ?MetaAnnotations?label "G" ❙
+		bounce: ℝ ❘ meta ?MetaAnnotations?label "BO" ❙
+        wallsr: List[wall] ❘ meta ?MetaAnnotations?label "WallsR" ❙
+    ❚
+
+    // the output of the scroll ❙
+
+    theory Solution =
+        include ?T3DBouncingScroll/Problem ❙
+        full_list: List[point × point × (point × ℝ) × ℝ] ❘ = stepUntil (point × point × (point × ℝ) × ℝ) (prep wallsr position velocity g_base) (get_next_vals wallsr ⟨g_base, bounce⟩) end_cond ❙
+        fun_list : List[(ℝ × ℝ) × (ℝ ⟶ ℝ) × (ℝ ⟶ point)] ❘ = full_list map ([vals : point × point × (point × ℝ) × ℝ] map_fun_list vals g_base) ❙
+        //ht_list: List[ℝ] ❘ = full_list map red_ht ❙
+		//fun_list : List[ℝ ⟶ point] ❘ = full_list map ([vals] get_pos_fun (πl vals) (πl (πr vals)) g_base) ❙
+        meta ?MetaAnnotations?label "T3DBouncingScroll" ❙
+        meta ?MetaAnnotations?description s"Bouncing " ❙
+    ❚
+❚
\ No newline at end of file
diff --git a/source/Scrolls/W3DBouncingScroll.mmt b/source/Scrolls/W3DBouncingScroll.mmt
index f80d4ee9798dd5100d5609c70e95d601e8bbc483..6915a782c8688fe0756e16e3a08484b97175a040 100644
--- a/source/Scrolls/W3DBouncingScroll.mmt
+++ b/source/Scrolls/W3DBouncingScroll.mmt
@@ -13,6 +13,8 @@ theory W3DBouncingScroll =
 	include ?IfThenElseX ❙
     include ?StepUntil ❙
 	include ?Walls ❙
+    //stepUntil : {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ List[X] ❘ # stepUntil 1 2 3 4 ❙
+    //filter2 : List[ℝ × wall] ⟶ ((ℝ × wall) ⟶ bool) ⟶ List[ℝ × wall] ❘ # 1 filter2 2 ❙
 
 	theory funcs =
         eq_zero : ℝ ⟶ bool ❘ =
@@ -53,7 +55,13 @@ theory W3DBouncingScroll =
         calc_new_vals : (point × point × (point × ℝ) × ℝ) ⟶ (point × ℝ) ⟶ (point × point × ℝ) ❘ =
             [v, bv] ⟨get_pt (πr (πl (πr (πr v)))) (πl v) (πl (πr v)) (πl bv), ([d : point] vec_multI (πr bv) (point_subtractI d (vec_multI (times_real_lit 2.0 (scalar_productI d (πl (πl (πr (πr v)))))) (πl (πl (πr (πr v))))))) (⟨plus_real_lit ((πl (πr v)) _x) (times_real_lit (πr (πl (πr (πr v)))) ((πl bv) _x)), plus_real_lit ((πl (πr v)) _y) (times_real_lit (πr (πl (πr (πr v)))) ((πl bv) _y)), plus_real_lit ((πl (πr v)) _z) (times_real_lit (πr (πl (πr (πr v)))) ((πl bv) _z))⟩), plus_real_lit (πr (πr (πr v))) (πr (πl (πr (πr v))))⟩ ❙
         end_cond : (point × point × (point × ℝ) × ℝ) ⟶ bool ❘ =
-            [vals] leq_real_lit (πr (πl (πr (πr vals)))) 0.1 ❙
+            [vals] (bool) ifx (leq_real_lit (Ï€r (Ï€l (Ï€r (Ï€r vals)))) 0.1)
+                          thenx ((bool) ifx (leq_real_lit (sqrt(scalar_productI (Ï€l (Ï€r vals)) (Ï€l (Ï€r vals)))) 10.0)
+                                        thenx (true)
+                                        elsex false)
+                          elsex ((bool) ifx (leq_real_lit 99999.0 (Ï€r (Ï€l (Ï€r (Ï€r vals)))))
+                                        thenx (true)
+                                        elsex false) ❙
         map_reduce_hts : (ℝ × ℝ × wall) ⟶ (ℝ × wall) ❘ =
             [wsi] (ℝ × wall) ifx (leq_real_lit (πl wsi) 0.000001)
                              thenx ((ℝ × wall) ifx (leq_real_lit (πl (πr wsi)) 0.000001)
@@ -89,8 +97,6 @@ theory W3DBouncingScroll =
 
     theory Solution =
         include ?W3DBouncingScroll/Problem ❙
-        //testw : List[point × point × point × point] ❘ = cons (⟨⟨0.0, 0.0, 0.0⟩, ⟨1.0, 0.0, 0.0⟩, ⟨2.0, 0.0, 0.0⟩, ⟨3.0, 0.0, 0.0⟩⟩) (cons (⟨⟨0.0, 1.0, 0.0⟩, ⟨1.0, 1.0, 0.0⟩, ⟨2.0, 1.0, 0.0⟩, ⟨3.0, 1.0, 0.0⟩⟩) nil) ❙
-        //wallse : List[wall] ❘ = wallsr map ([cw] create_wall (πl cw) (πl (πr cw)) (πl (πr (πr cw))) (πr (πr (πr cw)))) ❙
         full_list: List[point × point × (point × ℝ) × ℝ] ❘ = stepUntil (point × point × (point × ℝ) × ℝ) (prep (wallsr map ([cw] create_wall (πl cw) (πl (πr cw)) (πl (πr (πr cw))) (πr (πr (πr cw))))) position velocity g_base) (get_next_vals (wallsr map ([cw] create_wall (πl cw) (πl (πr cw)) (πl (πr (πr cw))) (πr (πr (πr cw))))) ⟨g_base, bounce⟩) end_cond ❙
         fun_list : List[(ℝ × ℝ) × (ℝ ⟶ ℝ) × (ℝ ⟶ point)] ❘ = full_list map ([vals : point × point × (point × ℝ) × ℝ] map_fun_list vals g_base) ❙
         //ht_list: List[ℝ] ❘ = full_list map red_ht ❙
diff --git a/source/Scrolls/WBouncingScroll.mmt b/source/Scrolls/WBouncingScroll.mmt
index 8e1317bc80ecdd36dc13dd255273ce69dd8c74d1..ea51dd5a1ae326c476e6e910211530c689de9beb 100644
--- a/source/Scrolls/WBouncingScroll.mmt
+++ b/source/Scrolls/WBouncingScroll.mmt
@@ -51,7 +51,13 @@ theory WBouncingScroll =
         get_next_vals_extra : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ (ℝ × ℝ) ⟶ (((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ))) ❘ = 
 		    [wsi, bv] ([v : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ))] ([x : ((ℝ × ℝ) × (ℝ × ℝ))] ⟨⟨πl (πl x), πr (πl x)⟩, ⟨πl (πr x), πr (πr x)⟩, (reduce_list_ht_pos wsi (πl (πl x)) (πr (πl x)) (πl (πr x)) (πr (πr x)) (πl bv)) fold ((reduce_list_ht_neg wsi (πl (πl x)) (πr (πl x)) (πl (πr x)) (πr (πr x)) (πl bv)) fold ⟨99999.9, -1.0⟩ fold_func) fold_func ⟩) (calc_new_vals bv v)) ❙
 		end_cond : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
-            [vals] leq_real_lit (πl (πr (πr vals))) 0.1 ❙
+            [vals] (bool) ifx (leq_real_lit (Ï€l (Ï€r (Ï€r vals))) 0.1)
+                          thenx ((bool) ifx (leq_real_lit (sqrt(plus_real_lit (times_real_lit (Ï€l (Ï€l (Ï€r vals))) (Ï€l (Ï€l (Ï€r vals)))) (times_real_lit (Ï€r (Ï€l (Ï€r vals))) (Ï€r (Ï€l (Ï€r vals)))))) 10.0)
+                                        thenx (true)
+                                        elsex false)
+                          elsex ((bool) ifx (leq_real_lit 99999.0 (Ï€l (Ï€r (Ï€r vals))))
+                                        thenx (true)
+                                        elsex false) ❙
 		red_ht : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ❘ =
             [cele] πl (πr (πr cele)) ❙
 		get_pos_fun: ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (ℝ ⟶ (ℝ × ℝ)) ❘ =
diff --git a/source/dynamics.mmt b/source/dynamics.mmt
index d3dfc0488ba77e334b9fe1d4f192fe7a47398b1b..819fed50685a952ced6c3c509f5af1500f163d35 100644
--- a/source/dynamics.mmt
+++ b/source/dynamics.mmt
@@ -19,22 +19,12 @@ theory IfThenElseX =
     ifthenelsex : {X: type} bool ⟶ X ⟶ X ⟶ X ❘ # 1 ifx 2 thenx 3 elsex 4 ❙
     rule rules?IfThenElseRuleX (true) (false) ❙
 ❚
+theory GetListAtInd =
+    // {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ List[X] ❙
+    getListAtInd : {X: type} List[X] ⟶ ℕ ⟶ X ❘ # 1 getlistatind 2 3 ❙
+    rule rules?GetListAtIndComp ❙
+❚
 theory Walls =
-    //wall : type ❘ = {'
-        point1 : point,
-        point2 : point,
-        point3 : point,
-        point4 : point,
-        u : point := point_subtractI point2 point1,
-        v : point := point_subtractI point3 point1,
-        vc : point := vec_cross u v,
-        a : ℝ := vc _x,
-        b : ℝ := vc _y,
-        c : ℝ := vc _z,
-        d : ℝ := plus_real_lit (plus_real_lit (times_real_lit a (point1 _x)) (times_real_lit b (point1 _y))) (times_real_lit c (point1 _z)),
-        length : ℝ := sqrt (plus_real_lit (plus_real_lit (times_real_lit a a) (times_real_lit b b)) (times_real_lit c c)),
-        norm_vec : point := ⟨times_real_lit a (inv_real_lit length), times_real_lit b (inv_real_lit length), times_real_lit c (inv_real_lit length)⟩
-    '} ❙
     wall : type ❘ = {'
         point1 : point,
         point2 : point,
@@ -60,4 +50,30 @@ theory Walls =
                                                                                                 times_real_lit (vcc _y) (inv_real_lit (sqrt (plus_real_lit (plus_real_lit (times_real_lit (vcc _x) (vcc _x)) (times_real_lit (vcc _y) (vcc _y))) (times_real_lit (vcc _z) (vcc _z))))),
                                                                                                 times_real_lit (vcc _z) (inv_real_lit (sqrt (plus_real_lit (plus_real_lit (times_real_lit (vcc _x) (vcc _x)) (times_real_lit (vcc _y) (vcc _y))) (times_real_lit (vcc _z) (vcc _z)))))⟩) ']
                                                                                 ) (vec_cross (point_subtractI p2 p1) (point_subtractI p3 p1))  ❙
+❚
+theory Triangles =
+    wall : type ❘ = {'
+        point1 : point,
+        point2 : point,
+        point3 : point,
+        u : point,
+        v : point,
+        vc : point,
+        a : ℝ,
+        b : ℝ,
+        c : ℝ,
+        d : ℝ,
+        length : ℝ,
+        norm_vec : point
+    '} ❙
+    create_wall : point ⟶ point ⟶ point ⟶ wall ❘ = [p1, p2, p3] ([vcc : point] ['point1 := p1, point2 := p2, point3 := p3,
+                                                                                      u := point_subtractI p2 p1,
+                                                                                      v := point_subtractI p3 p1,
+                                                                                      vc := vcc, a := vcc _x, b := vcc _y, c := vcc _z,
+                                                                                      d := plus_real_lit (plus_real_lit (times_real_lit (vcc _x) (p1 _x)) (times_real_lit (vcc _y) (p1 _y))) (times_real_lit (vcc _z) (p1 _z)),
+                                                                                      length := sqrt (plus_real_lit (plus_real_lit (times_real_lit (vcc _x) (vcc _x)) (times_real_lit (vcc _y) (vcc _y))) (times_real_lit (vcc _z) (vcc _z))),
+                                                                                      norm_vec := (⟨ times_real_lit (vcc _x) (inv_real_lit (sqrt (plus_real_lit (plus_real_lit (times_real_lit (vcc _x) (vcc _x)) (times_real_lit (vcc _y) (vcc _y))) (times_real_lit (vcc _z) (vcc _z))))),
+                                                                                                    times_real_lit (vcc _y) (inv_real_lit (sqrt (plus_real_lit (plus_real_lit (times_real_lit (vcc _x) (vcc _x)) (times_real_lit (vcc _y) (vcc _y))) (times_real_lit (vcc _z) (vcc _z))))),
+                                                                                                    times_real_lit (vcc _z) (inv_real_lit (sqrt (plus_real_lit (plus_real_lit (times_real_lit (vcc _x) (vcc _x)) (times_real_lit (vcc _y) (vcc _y))) (times_real_lit (vcc _z) (vcc _z)))))⟩) ']
+                                                                                    ) (vec_cross (point_subtractI p2 p1) (point_subtractI p3 p1))  ❙
 ❚
\ No newline at end of file