From a2e6a7c3164ebf32be0e8cd277247af99115d4c2 Mon Sep 17 00:00:00 2001
From: Lucas <lucas.heublein@t-online.de>
Date: Fri, 18 Aug 2023 16:38:06 +0200
Subject: [PATCH] Added the 2D wall Bouncing Scroll (WBouncingScroll) and a new
 StepUntil Function that also takes constant values

---
 .../kwarc/mmt/frameit/rules/StepUntilX.scala  | 65 +++++++++++++++
 source/DefaultSituationSpace.mmt              |  1 +
 source/IntegrationTests/DynamicsDebug.mmt     | 65 ++++++++++++++-
 source/Scrolls/WBouncingScroll.mmt            | 83 +++++++++++++++++++
 source/dynamics.mmt                           |  6 +-
 5 files changed, 218 insertions(+), 2 deletions(-)
 create mode 100644 scala/info/kwarc/mmt/frameit/rules/StepUntilX.scala
 create mode 100644 source/Scrolls/WBouncingScroll.mmt

diff --git a/scala/info/kwarc/mmt/frameit/rules/StepUntilX.scala b/scala/info/kwarc/mmt/frameit/rules/StepUntilX.scala
new file mode 100644
index 0000000..5f9208c
--- /dev/null
+++ b/scala/info/kwarc/mmt/frameit/rules/StepUntilX.scala
@@ -0,0 +1,65 @@
+package info.kwarc.mmt.frameit.rules
+
+import info.kwarc.mmt.api.checking._
+import info.kwarc.mmt.api.{DPath, GlobalName, LocalName, ParametricRule, Rule, RuleSet}
+import info.kwarc.mmt.api.frontend.Controller
+import info.kwarc.mmt.api.objects._
+import Conversions._
+import info.kwarc.mmt.api.uom.{Simplifiability, Simplify}
+import info.kwarc.mmt.lf.{Apply, ApplySpine, Arrow, OfType, Pi}
+import info.kwarc.mmt.LFX.datatypes.{Listtype, Ls}
+import info.kwarc.mmt.api.utils.URI
+
+import scala.collection.mutable
+
+object StepUntilX {
+  val ns: DPath = DPath(URI.http colon "mathhub.info") / "FrameIT" / "frameworld"
+  val path: GlobalName = ns ? "StepUntilX" ? "stepUntilX"
+  val rawhead: OMID = OMS(path)
+  def apply(tpA: Term, tpB: Term, tpC: Term, vB: Term, vC: Term, vA: Term, f: Term, tC: Term): Term =
+    ApplySpine(this.rawhead, tpA, tpB, tpC, vB, vC, vA, f, tC)
+  def unapply(tm : Term) : Option[(Term, Term, Term, Term, Term, Term, Term, Term)] = tm match {
+    case ApplySpine(this.rawhead, List(tpA, tpB, tpC, vB, vC, vA, f, tC)) => Some((tpA, tpB, tpC, vB, vC, vA, f, tC))
+    case _ => None
+  }
+}
+
+object StepUntilXRule extends ParametricRule {
+  // todo: document
+  private val DEBUG_MAX_ITER_COUNT = 100
+
+  override def apply(controller: Controller, home: Term, args: List[Term]): Rule = args match {
+    case List(truetm) =>
+      RuleSet(StepUntilXComp(truetm))
+    case _ =>
+      ???
+  }
+
+  case class StepUntilXComp(truetm: Term) extends ComputationRule(StepUntilX.path) {
+    override def applicable(t: Term): Boolean = t match {
+      case StepUntilX(_, _, _, _, _, _, _, _) => true
+      case _ => false
+    }
+    override def apply(check: CheckingCallback)(tm: Term, covered: Boolean)(implicit stack: Stack, history: History): Simplifiability = tm match {
+      case StepUntilX(_, _, _, vB, vC, vA, f, tC) =>
+        val values = mutable.ListBuffer[Term]()
+        val valB = check.simplify(vB)
+        val valC = check.simplify(vC)
+        var iter = 0
+        var cur = check.simplify(vA)
+        while (iter < DEBUG_MAX_ITER_COUNT) {
+          iter += 1
+          check.tryToCheckWithoutDelay(Equality(stack, Apply(tC, cur), truetm, None)) match {
+            case Some(true) =>
+              return Simplify(Ls(values.toSeq : _*))
+            case Some(false) | None =>
+              values += cur
+              cur = check.simplify(ApplySpine(f, valB, valC, cur))
+          }
+        }
+        // todo: try to log something via stack, history, check, or this
+        Simplify(Ls(values.toSeq : _*))
+      case _ => Simplifiability.NoRecurse
+    }
+  }
+}
\ No newline at end of file
diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt
index 4bad740..2c66635 100644
--- a/source/DefaultSituationSpace.mmt
+++ b/source/DefaultSituationSpace.mmt
@@ -16,6 +16,7 @@ theory DefaultSituationSpace =
         include ?Midpoint ❙
         include ?CircleScroll ❙
 		include ?BouncingScroll ❙
+        include ?WBouncingScroll ❙
       //  include ?SinOppositeLeg ❙
         include ?CircleLineAngleScroll ❙
         include ?CircleAreaScroll ❙
diff --git a/source/IntegrationTests/DynamicsDebug.mmt b/source/IntegrationTests/DynamicsDebug.mmt
index 50266db..b75c102 100644
--- a/source/IntegrationTests/DynamicsDebug.mmt
+++ b/source/IntegrationTests/DynamicsDebug.mmt
@@ -2,12 +2,13 @@ namespace http://mathhub.info/FrameIT/frameworld/integrationtests/dynamicsdebug
 
 rule scala://parser.api.mmt.kwarc.info?MMTURILexer ❚
 
+import rules scala://datatypes.LFX.mmt.kwarc.info ❚
 import frameworld http://mathhub.info/FrameIT/frameworld ❚
 fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta ❚
 
 theory IfElseDebug =
     include ☞http://mathhub.info/FrameIT/frameworld?IfThenElseX ❙
-    c: ℝ ❘ = ifx (leq_real_lit 20.0 10.0) thenx 1.0 elsex 0.0 ❙
+    c: ℝ ❘ = ℝ ifx (leq_real_lit 20.0 10.0) thenx 1.0 elsex 0.0 ❙
 ❚
 
 theory StepUntilDebug =
@@ -16,3 +17,65 @@ theory StepUntilDebug =
     my_list: List[ℝ] ❘ = stepUntil ℝ 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
     //my_list: ℝ ❘ = stepUntil ℝ 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
 ❚
+
+theory StepUntilXDebug =
+    include ☞http://mathhub.info/FrameIT/frameworld?StepUntilX ❙
+    //my_list: List[ℝ] ❘ = (cons 0.0 (cons 2.0 nil)) map ([x: ℝ] plus_real_lit x 1.0) ❙
+    my_list: List[ℝ] ❘ = stepUntilX ℝ List[ℝ] (ℝ × ℝ) (cons 1.0 nil) ⟨2.0, 1.0⟩ 0.0 ([x: List[ℝ], y: ℝ × ℝ, z: ℝ] times_real_lit (plus_real_lit (x fold 0.0 ([curr: ℝ][acc: ℝ] plus_real_lit curr acc)) z) (πl y)) ([x: ℝ] leq_real_lit 50.0 x) ❙
+    //my_list: ℝ ❘ = stepUntil ℝ 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
+❚
+theory StepUntilX2Debug =
+    include ☞http://mathhub.info/FrameIT/frameworld?StepUntilX ❙
+    include ☞http://mathhub.info/FrameIT/frameworld?IfThenElseX ❙
+    rule rules?FilterRule (true) ❙
+    calc_new_vals : (ℝ × ℝ) ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ((ℝ × ℝ) × (ℝ × ℝ)) ❘ =
+		[bv, v] ⟨⟨plus_real_lit (πl (πl v)) (times_real_lit (πl (πl (πr v))) (πl (πr (πr v)))), plus_real_lit (plus_real_lit (πr (πl v)) (times_real_lit (πr (πl (πr v))) (πl (πr (πr v))))) (times_real_lit (times_real_lit 0.5 (πl bv)) (times_real_lit (πl (πr (πr v))) (πl (πr (πr v)))))⟩, ⟨ times_real_lit (πr bv) (plus_real_lit (πl (πl (πr v))) (times_real_lit (times_real_lit (times_real_lit 2.0 (πr (πr (πr v)))) (plus_real_lit (πr (πl (πr v))) (minus_real_lit (times_real_lit (πr (πr (πr v))) (πl (πl (πr v))))))) (inv_real_lit (plus_real_lit 1.0 (times_real_lit (πr (πr (πr v))) (πr (πr (πr v)))))))), times_real_lit (πr bv) (plus_real_lit (plus_real_lit (πr (πl (πr v))) (times_real_lit (πl bv) (πl (πr (πr v))))) (minus_real_lit (times_real_lit (times_real_lit 2.0 (plus_real_lit (plus_real_lit (πr (πl (πr v))) (times_real_lit (πl bv) (πl (πr (πr v))))) (minus_real_lit (times_real_lit (πr (πr (πr v))) (πl (πl (πr v))))))) (inv_real_lit (plus_real_lit 1.0 (times_real_lit (πr (πr (πr v))) (πr (πr (πr v)))))))))⟩⟩ ❙
+    fold_func : (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ⟶ (ℝ × ℝ) ⟶ (ℝ × ℝ) ❘ =
+        [cur][acc] (ℝ × ℝ) ifx (leq_real_lit (πl acc) (πr (πl (πl cur)))) thenx acc elsex ⟨πr (πl (πl cur)), πr cur⟩ ❙
+    check_hit : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
+        [p] leq_real_lit 0.000001 (πr (πl p)) ❙
+    check_hit2 : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
+        [p] leq_real_lit (πl (πr p)) (πl (πl p)) ❙
+    check_hit3 : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
+        [p] leq_real_lit (πl (πl p)) (πr (πr p)) ❙
+    get_hit_time_pos : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ = 
+        [wi, x, y, xv, yv, g] times_real_lit (inv_real_lit g) (plus_real_lit (plus_real_lit (times_real_lit (πl (πl wi)) xv) (minus_real_lit yv)) (sqrt ( plus_real_lit (times_real_lit (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv))) (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv)))) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) (plus_real_lit (plus_real_lit y (minus_real_lit (times_real_lit (πl (πl wi)) x))) (minus_real_lit (πr (πl wi))))))))) ❙
+    get_hit_time_neg : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ = 
+        [wi, x, y, xv, yv, g] times_real_lit (inv_real_lit g) (plus_real_lit (plus_real_lit (times_real_lit (πl (πl wi)) xv) (minus_real_lit yv)) (minus_real_lit (sqrt ( plus_real_lit (times_real_lit (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv))) (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv)))) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) (plus_real_lit (plus_real_lit y (minus_real_lit (times_real_lit (πl (πl wi)) x))) (minus_real_lit (πr (πl wi)))))))))) ❙
+    get_x_ht : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ = [x, xv, ht] plus_real_lit x (times_real_lit xv ht) ❙
+
+    combine_ht_info_pos : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ❘ = 
+        [wi, x, y, xv, yv, g] ⟨⟨⟨get_x_ht x xv (get_hit_time_pos wi x y xv yv g), get_hit_time_pos wi x y xv yv g⟩, ⟨(πl (πr wi)), (πr (πr wi))⟩⟩, (πl (πl wi))⟩ ❙
+    combine_ht_info_neg : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ❘ = 
+        [wi, x, y, xv, yv, g] ⟨⟨⟨get_x_ht x xv (get_hit_time_neg wi x y xv yv g), get_hit_time_neg wi x y xv yv g⟩, ⟨(πl (πr wi)), (πr (πr wi))⟩⟩, (πl (πl wi))⟩ ❙
+
+    get_m : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ❘ = [w] times_real_lit (plus_real_lit (πr (πr w)) (minus_real_lit (πr (πl w)))) (inv_real_lit (plus_real_lit (πl (πr w)) (minus_real_lit (πl (πl w))))) ❙
+    get_c : (ℝ × ℝ) ⟶ ℝ ⟶ ℝ ❘ = [w][m] plus_real_lit (πr w) (minus_real_lit (times_real_lit (πl w) m)) ❙
+    get_mc : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ((ℝ × ℝ) × (ℝ × ℝ)) ❘ = [w] ⟨⟨get_m w, get_c (πl w) (get_m w)⟩, ⟨πl (πl w), πl (πr w)⟩⟩ ❙
+
+    reduce_list_ht_pos : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ List[((ℝ × ℝ) × (ℝ × ℝ)) × ℝ] ❘ =
+        [wsi, x, y, xv, yv, g] (((wsi map ([wi] combine_ht_info_pos wi x y xv yv g)) filter ([wib] check_hit (πl wib))) filter ([wib] check_hit2 (πl wib))) filter ([wib] check_hit3 (πl wib)) ❙
+    reduce_list_ht_neg : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ List[((ℝ × ℝ) × (ℝ × ℝ)) × ℝ] ❘ =
+        [wsi, x, y, xv, yv, g] (((wsi map ([wi] combine_ht_info_neg wi x y xv yv g)) filter ([wib] check_hit (πl wib))) filter ([wib] check_hit2 (πl wib))) filter ([wib] check_hit3 (πl wib)) ❙
+    prep : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ =
+		[wsi, x, y, xv, yv, g]  ⟨⟨x, y⟩, ⟨xv, yv⟩, (reduce_list_ht_pos wsi x y xv yv g) fold ((reduce_list_ht_neg wsi x y xv yv g) fold ⟨99999.9, -1.0⟩ fold_func) fold_func ⟩ ❙
+    get_next_vals : 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 ❙
+    red_ht : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ❘ =
+        [cele] πl (πr (πr cele)) ❙
+    get_pos_fun: ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (ℝ ⟶ (ℝ × ℝ)) ❘ =
+        [x,y,xv,yv,g] ([t] ⟨plus_real_lit x (times_real_lit xv t), plus_real_lit (times_real_lit (times_real_lit 0.5 g) (times_real_lit t t)) (plus_real_lit y (times_real_lit yv t))⟩ ) ❙
+    my_list: List[(ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)] ❘ = stepUntilX ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) List[(ℝ × ℝ) × (ℝ × ℝ)] (ℝ × ℝ) ((cons ⟨⟨-10000.0, 0.0⟩, ⟨10000.0, 0.0⟩⟩ (cons ⟨⟨0.0, -1000.0⟩, ⟨0.1, 1000.0⟩⟩ (cons ⟨⟨50.0, -150.0⟩, ⟨50.1, 150.0⟩⟩ nil))) map get_mc) ⟨-200.0, 0.5⟩ (prep ((cons ⟨⟨-10000.0, 0.0⟩, ⟨10000.0, 0.0⟩⟩ (cons ⟨⟨0.0, -1000.0⟩, ⟨0.1, 1000.0⟩⟩ (cons ⟨⟨50.0, -150.0⟩, ⟨50.1, 150.0⟩⟩ nil))) map get_mc) 200.0 300.0 (-100.0) 100.0 (-200.0)) get_next_vals end_cond ❙
+    //my_list: ℝ ❘ = stepUntil ℝ 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
+    // full_list	
+			: List[ ℝ×ℝ×(ℝ×ℝ)×(ℝ×ℝ)]
+			= stepUntilX (ℝ×ℝ×(ℝ×ℝ)×(ℝ×ℝ)) List[ ℝ×ℝ×(ℝ×ℝ)] (ℝ×ℝ) cons ⟨⟨0.0,0.0⟩,⟨-10000.0,10000.0⟩⟩ nil  ⟨-200.0,0.5⟩ ⟨⟨200.0,300.0⟩,⟨-100.0,100.0⟩,⟨2.302775638,0.0⟩⟩ [wsi,bv,v]([xt:ℝ×ℝ×(ℝ×ℝ)]⟨⟨πl πl xt,πr πl xt⟩,⟨πl πr xt,πr πr xt⟩,(([wsit,x,y,xv,yv,g]wsit map [wi]([wi,x,y,xv,yv,g]⟨⟨⟨([x,xv,ht]x+(xv×ht)) x xv (([wi,x,y,xv,yv,g]g⁻¹×((πl πl wi)×xv)+-yv+-(sqrt (yv+-((πl πl wi)×xv)×yv+-((πl πl wi)×xv))+-(2.0×g×y+-((πl πl wi)×x)+-πr πl wi))) wi x y xv yv g),([wi,x,y,xv,yv,g]g⁻¹×((πl πl wi)×xv)+-yv+-(sqrt (yv+-((πl πl wi)×xv)×yv+-((πl πl wi)×xv))+-(2.0×g×y+-((πl πl wi)×x)+-πr πl wi))) wi x y xv yv g⟩,⟨πl πr wi,πr πr wi⟩⟩,πl πl wi⟩) wi x y xv yv g) wsi (πl πl xt) (πr πl xt) (πl πr xt) (πr πr xt) πl bv) fold ⟨99999.9,-1.0⟩ [cur][acc](ℝ×ℝ) ifx (leq_real_lit (πl acc) πr πl πl cur) thenx acc elsex ⟨πr πl πl cur,πr cur⟩⟩) (([bv,v]⟨⟨(πl πl v)+((πl πl πr v)×πl πr πr v),(πr πl v)+((πr πl πr v)×πl πr πr v)+(0.5×πl bv×((πl πr πr v)×πl πr πr v))⟩,⟨(πr bv)×(πl πl πr v)+(2.0×πr πr πr v×(πr πl πr v)+-((πr πr πr v)×πl πl πr v)×(1.0+((πr πr πr v)×πr πr πr v))⁻¹),(πr bv)×(πr πl πr v)+((πl bv)×πl πr πr v)+-(2.0×(πr πl πr v)+((πl bv)×πl πr πr v)+-((πr πr πr v)×πl πl πr v)×(1.0+((πr πr πr v)×πr πr πr v))⁻¹)⟩⟩) bv v) [vals]leq_real_lit (πl πr πr vals) 0.1 ❙
+
+    //iterated_fun: List[ ℝ×ℝ×(ℝ×ℝ)] ⟶ (ℝ×ℝ) ⟶ (ℝ×ℝ×(ℝ×ℝ)×(ℝ×ℝ)) ⟶ (ℝ×ℝ×(ℝ×ℝ)) ⟶ (ℝ×ℝ×(ℝ×ℝ)×(ℝ×ℝ)) ❘
+    = [wsi,bv,v,xt] ⟨⟨πl πl xt,πr πl xt⟩,⟨πl πr xt,πr πr xt⟩,(([wsit: List[(ℝ × ℝ) × (ℝ × ℝ)],x: ℝ,y: ℝ,xv: ℝ,yv: ℝ,g: ℝ]wsit map [wi: (ℝ × ℝ) × (ℝ × ℝ)]([wi: (ℝ × ℝ) × (ℝ × ℝ), x: ℝ,y: ℝ, xv: ℝ, yv: ℝ, g: ℝ]⟨⟨⟨([x: ℝ,xv: ℝ,ht: ℝ]x+(xv×ht)) x xv (([wi: (ℝ × ℝ) × (ℝ × ℝ), x: ℝ,y: ℝ, xv: ℝ, yv: ℝ, g: ℝ]g⁻¹×((πl πl wi)×xv)+-yv+-(sqrt (yv+-((πl πl wi)×xv)×yv+-((πl πl wi)×xv))+-(2.0×g×y+-((πl πl wi)×x)+-πr πl wi))) wi x y xv yv g),([wi: (ℝ × ℝ) × (ℝ × ℝ), x: ℝ,y: ℝ, xv: ℝ, yv: ℝ, g: ℝ]g⁻¹×((πl πl wi)×xv)+-yv+-(sqrt (yv+-((πl πl wi)×xv)×yv+-((πl πl wi)×xv))+-(2.0×g×y+-((πl πl wi)×x)+-πr πl wi))) wi x y xv yv g⟩,⟨πl πr wi,πr πr wi⟩⟩,πl πl wi⟩) wi x y xv yv g) wsi (πl πl xt) (πr πl xt) (πl πr xt) (πr πr xt) πl bv) fold ⟨99999.9,-1.0⟩ [cur: ((ℝ × ℝ) × (ℝ × ℝ)) × ℝ][acc: ℝ × ℝ](ℝ×ℝ) ifx (leq_real_lit (πl acc) πr πl πl cur) thenx acc elsex ⟨πr πl πl cur,πr cur⟩⟩ ❙ 
+    
+    
+    // (([bv,v]⟨⟨(πl πl v)+((πl πl πr v)×πl πr πr v),(πr πl v)+((πr πl πr v)×πl πr πr v)+(0.5×πl bv×((πl πr πr v)×πl πr πr v))⟩,⟨(πr bv)×(πl πl πr v)+(2.0×πr πr πr v×(πr πl πr v)+-((πr πr πr v)×πl πl πr v)×(1.0+((πr πr πr v)×πr πr πr v))⁻¹),(πr bv)×(πr πl πr v)+((πl bv)×πl πr πr v)+-(2.0×(πr πl πr v)+((πl bv)×πl πr πr v)+-((πr πr πr v)×πl πl πr v)×(1.0+((πr πr πr v)×πr πr πr v))⁻¹)⟩⟩) bv v) ❙
+❚
diff --git a/source/Scrolls/WBouncingScroll.mmt b/source/Scrolls/WBouncingScroll.mmt
new file mode 100644
index 0000000..6c645cd
--- /dev/null
+++ b/source/Scrolls/WBouncingScroll.mmt
@@ -0,0 +1,83 @@
+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 WBouncingScroll =
+    meta ?MetaAnnotations?problemTheory ?WBouncingScroll/Problem ❙
+    meta ?MetaAnnotations?solutionTheory ?WBouncingScroll/Solution ❙
+    rule rules?FilterRule (true) ❙
+	include ?IfThenElseX ❙
+    include ?StepUntilX ❙
+
+	theory funcs =
+	    calc_new_vals : (ℝ × ℝ) ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ((ℝ × ℝ) × (ℝ × ℝ)) ❘ =
+		    [bv, v] ⟨⟨plus_real_lit (πl (πl v)) (times_real_lit (πl (πl (πr v))) (πl (πr (πr v)))), plus_real_lit (plus_real_lit (πr (πl v)) (times_real_lit (πr (πl (πr v))) (πl (πr (πr v))))) (times_real_lit (times_real_lit 0.5 (πl bv)) (times_real_lit (πl (πr (πr v))) (πl (πr (πr v)))))⟩, ⟨ times_real_lit (πr bv) (plus_real_lit (πl (πl (πr v))) (times_real_lit (times_real_lit (times_real_lit 2.0 (πr (πr (πr v)))) (plus_real_lit (plus_real_lit (πr (πl (πr v))) (times_real_lit (πl bv) (πl (πr (πr v))))) (minus_real_lit (times_real_lit (πr (πr (πr v))) (πl (πl (πr v))))))) (inv_real_lit (plus_real_lit 1.0 (times_real_lit (πr (πr (πr v))) (πr (πr (πr v)))))))), times_real_lit (πr bv) (plus_real_lit (plus_real_lit (πr (πl (πr v))) (times_real_lit (πl bv) (πl (πr (πr v))))) (minus_real_lit (times_real_lit (times_real_lit 2.0 (plus_real_lit (plus_real_lit (πr (πl (πr v))) (times_real_lit (πl bv) (πl (πr (πr v))))) (minus_real_lit (times_real_lit (πr (πr (πr v))) (πl (πl (πr v))))))) (inv_real_lit (plus_real_lit 1.0 (times_real_lit (πr (πr (πr v))) (πr (πr (πr v)))))))))⟩⟩ ❙
+        fold_func : (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ⟶ (ℝ × ℝ) ⟶ (ℝ × ℝ) ❘ =
+            [cur][acc] (ℝ × ℝ) ifx (leq_real_lit (πl acc) (πr (πl (πl cur)))) thenx acc elsex ⟨πr (πl (πl cur)), πr cur⟩ ❙
+        check_hit : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
+            [p] leq_real_lit 0.000001 (πr (πl p)) ❙
+        check_hit2 : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
+            [p] leq_real_lit (πl (πr p)) (πl (πl p)) ❙
+        check_hit3 : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
+            [p] leq_real_lit (πl (πl p)) (πr (πr p)) ❙
+        get_hit_time_pos : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ = 
+            [wi, x, y, xv, yv, g] times_real_lit (inv_real_lit g) (plus_real_lit (plus_real_lit (times_real_lit (πl (πl wi)) xv) (minus_real_lit yv)) (sqrt ( plus_real_lit (times_real_lit (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv))) (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv)))) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) (plus_real_lit (plus_real_lit y (minus_real_lit (times_real_lit (πl (πl wi)) x))) (minus_real_lit (πr (πl wi))))))))) ❙
+        get_hit_time_neg : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ = 
+            [wi, x, y, xv, yv, g] times_real_lit (inv_real_lit g) (plus_real_lit (plus_real_lit (times_real_lit (πl (πl wi)) xv) (minus_real_lit yv)) (minus_real_lit (sqrt ( plus_real_lit (times_real_lit (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv))) (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv)))) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) (plus_real_lit (plus_real_lit y (minus_real_lit (times_real_lit (πl (πl wi)) x))) (minus_real_lit (πr (πl wi)))))))))) ❙
+        get_x_ht : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ = [x, xv, ht] plus_real_lit x (times_real_lit xv ht) ❙
+
+        combine_ht_info_pos : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ❘ = 
+            [wi, x, y, xv, yv, g] ⟨⟨⟨get_x_ht x xv (get_hit_time_pos wi x y xv yv g), get_hit_time_pos wi x y xv yv g⟩, ⟨(πl (πr wi)), (πr (πr wi))⟩⟩, (πl (πl wi))⟩ ❙
+        combine_ht_info_neg : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ❘ = 
+            [wi, x, y, xv, yv, g] ⟨⟨⟨get_x_ht x xv (get_hit_time_neg wi x y xv yv g), get_hit_time_neg wi x y xv yv g⟩, ⟨(πl (πr wi)), (πr (πr wi))⟩⟩, (πl (πl wi))⟩ ❙
+
+        get_m : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ❘ = [w] times_real_lit (plus_real_lit (πr (πr w)) (minus_real_lit (πr (πl w)))) (inv_real_lit (plus_real_lit (πl (πr w)) (minus_real_lit (πl (πl w))))) ❙
+        get_c : (ℝ × ℝ) ⟶ ℝ ⟶ ℝ ❘ = [w][m] plus_real_lit (πr w) (minus_real_lit (times_real_lit (πl w) m)) ❙
+        get_mc : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ((ℝ × ℝ) × (ℝ × ℝ)) ❘ = [w] ⟨⟨get_m w, get_c (πl w) (get_m w)⟩, ⟨πl (πl w), πl (πr w)⟩⟩ ❙
+
+        reduce_list_ht_pos : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ List[((ℝ × ℝ) × (ℝ × ℝ)) × ℝ] ❘ =
+            [wsi, x, y, xv, yv, g] (((wsi map ([wi] combine_ht_info_pos wi x y xv yv g)) filter ([wib] check_hit (πl wib))) filter ([wib] check_hit2 (πl wib))) filter ([wib] check_hit3 (πl wib)) ❙
+        reduce_list_ht_neg : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ List[((ℝ × ℝ) × (ℝ × ℝ)) × ℝ] ❘ =
+            [wsi, x, y, xv, yv, g] (((wsi map ([wi] combine_ht_info_neg wi x y xv yv g)) filter ([wib] check_hit (πl wib))) filter ([wib] check_hit2 (πl wib))) filter ([wib] check_hit3 (πl wib)) ❙
+		prep : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ =
+		    [wsi, x, y, xv, yv, g]  ⟨⟨x, y⟩, ⟨xv, yv⟩, (reduce_list_ht_pos wsi x y xv yv g) fold ((reduce_list_ht_neg wsi x y xv yv g) fold ⟨99999.9, -1.0⟩ fold_func) fold_func ⟩ ❙
+        get_next_vals : 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 ❙
+		red_ht : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ❘ =
+            [cele] πl (πr (πr cele)) ❙
+		get_pos_fun: ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (ℝ ⟶ (ℝ × ℝ)) ❘ =
+            [x,y,xv,yv,g] ([t] ⟨plus_real_lit x (times_real_lit xv t), plus_real_lit (times_real_lit (times_real_lit 0.5 g) (times_real_lit t t)) (plus_real_lit y (times_real_lit yv t))⟩ ) ❙
+    ❚
+    // start position and velocity ❙
+    theory Problem =
+	    include ?WBouncingScroll/funcs ❙
+        xposition: ℝ ❘ meta ?MetaAnnotations?label "X" ❙
+        yposition: ℝ ❘ meta ?MetaAnnotations?label "Y" ❙
+        xvelocity: ℝ ❘ meta ?MetaAnnotations?label "XV" ❙
+	    yvelocity: ℝ ❘ meta ?MetaAnnotations?label "YV" ❙
+	    g_base: ℝ ❘ meta ?MetaAnnotations?label "G" ❙
+		bounce: ℝ ❘ meta ?MetaAnnotations?label "BO" ❙
+        walls: List[(ℝ × ℝ) × (ℝ × ℝ)] ❘ meta ?MetaAnnotations?label "Walls" ❙
+    ❚
+
+    // the output of the scroll ❙
+
+    theory Solution =
+        include ?WBouncingScroll/Problem ❙
+        //mcws : List[(ℝ × ℝ) × (ℝ × ℝ)] ❘ = get_mc_list walls ❙
+		//basev : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ = prep (walls map get_mc) xposition yposition xvelocity yvelocity g_base ❙
+		//nextv : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ = get_next_vals (walls map get_mc ) ⟨g_base, bounce⟩ basev ❙
+		//nextv2 : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ = get_next_vals (walls map get_mc ) ⟨g_base, bounce⟩ nextv ❙
+		full_list: List[(ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)] ❘ = stepUntilX ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) List[(ℝ × ℝ) × (ℝ × ℝ)] (ℝ × ℝ) (walls map get_mc) ⟨g_base, bounce⟩ (prep (walls map get_mc) xposition yposition xvelocity yvelocity g_base) get_next_vals end_cond ❙
+		ht_list: List[ℝ] ❘ = full_list map ([xele] red_ht xele) ❙
+		fun_list : List[ℝ ⟶ (ℝ × ℝ)] ❘ = full_list map ([vals] get_pos_fun (πl (πl vals)) (πr (πl vals)) (πl (πl (πr vals))) (πr (πl (πr vals))) g_base) ❙
+        meta ?MetaAnnotations?label "WBouncingScroll" ❙
+        meta ?MetaAnnotations?description s"Bouncing " ❙
+    ❚
+❚
\ No newline at end of file
diff --git a/source/dynamics.mmt b/source/dynamics.mmt
index 31bf8cf..48c12aa 100644
--- a/source/dynamics.mmt
+++ b/source/dynamics.mmt
@@ -10,8 +10,12 @@ theory StepUntil =
     //stepUntil : {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ X ❘ # stepUntil 1 2 3 4 ❙
     rule rules?StepUntilRule (true) ❙
 ❚
+theory StepUntilX =
+    stepUntilX : {A: type}{B: type}{C: type} B ⟶ C ⟶ A ⟶ (B ⟶ C ⟶ A ⟶ A) ⟶ (A ⟶ bool) ⟶ List[A] ❘ # stepUntilX 1 2 3 4 5 6 7 8 ❙
+    rule rules?StepUntilXRule (true) ❙
+❚
 theory IfThenElseX =
     // {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ List[X] ❙
-    ifthenelsex : {X: type} bool ⟶ X ⟶ X ⟶ X ❘ # ifx 2 thenx 3 elsex 4 ❙
+    ifthenelsex : {X: type} bool ⟶ X ⟶ X ⟶ X ❘ # 1 ifx 2 thenx 3 elsex 4 ❙
     rule rules?IfThenElseRuleX (true) (false) ❙
 ❚
-- 
GitLab