Added a Bouncing Example RiverScroll

source/Scrolls/RiverScroll.mmt

+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 RiverScroll =
+    meta ?MetaAnnotations?problemTheory ?RiverScroll/Problem ❙
+    meta ?MetaAnnotations?solutionTheory ?RiverScroll/Solution ❙
+	include ?IfThenElseX ❙
+
+	theory funcs =
+        get_abs : ℝ ⟶ ℝ ❘ = [val : ℝ] (ℝ) ifx (leq_real_lit 0.0 val) thenx val elsex (minus_real_lit val) ❙
+        get_height : point ⟶ point ⟶ point ⟶ ℝ ❘ = [g, d, c] get_abs (times_real_lit (plus_real_lit (minus_real_lit (scalar_productI g d)) (scalar_productI g c)) (inv_real_lit (sqrt (scalar_productI g g)))) ❙
+        get_ground_distance : point ⟶ point ⟶ point ⟶ ℝ ❘ = [g, d, c] sqrt (plus_real_lit (scalar_productI (point_subtractI d c) (point_subtractI d c)) (minus_real_lit (times_real_lit (get_height g d c) (get_height g d c)))) ❙
+        get_abs_v : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ = [g, d, h, alpha] ([const : ℝ] sqrt (times_real_lit (times_real_lit const const) (inv_real_lit (times_real_lit (-2.0) (plus_real_lit (times_real_lit const (sin alpha)) (times_real_lit g h)))))) (times_real_lit (times_real_lit d g) (inv_real_lit (cos alpha))) ❙
+        get_v : point ⟶ point ⟶ ℝ ⟶ point ❘ = [c, a, vabs] ([const : point] vec_multI (times_real_lit vabs (inv_real_lit (sqrt (scalar_productI const const)))) const) (point_subtractI c a) ❙
+    ❚
+    // start position and velocity ❙
+    theory Problem =
+	    include ?RiverScroll/funcs ❙
+        A: point ❘ meta ?MetaAnnotations?label "A" ❙
+        B: point ❘ meta ?MetaAnnotations?label "B" ❙
+        C: point ❘ meta ?MetaAnnotations?label "C" ❙
+        D: point ❘ meta ?MetaAnnotations?label "D" ❙
+        G: point ❘ meta ?MetaAnnotations?label "G" ❙
+        angleA : Σ α: ℝ. ⊦ ( ∠ B,A,C ) ≐ α ❘
+            meta ?MetaAnnotations?label s"∠${lverb B A C}" ❘
+            meta ?MetaAnnotations?description s"Angle at ${lverb A} as enclosed by legs ${lverb A B} and ${lverb A C}" ❙
+    ❚
+
+    // the output of the scroll ❙
+
+    theory Solution =
+        include ?RiverScroll/Problem ❙
+        v: point ❘ = get_v C A (get_abs_v (minus_real_lit (sqrt (scalar_productI G G))) (get_ground_distance G D C) (get_height G D C) (πl angleA)) ❙
+        meta ?MetaAnnotations?label "RiverScroll" ❙
+        meta ?MetaAnnotations?description s"River " ❙
+    ❚
+❚
\ No newline at end of file