From 9901c813aa2850af2b18751ec273559d8215c1ea Mon Sep 17 00:00:00 2001
From: Paul-Walcher <paulwalcher12@gmail.com>
Date: Wed, 12 Jun 2024 19:14:29 +0200
Subject: [PATCH] Changed Rectangle and Cuboid Fact

---
 source/Scrolls/CuboidScroll.mmt    | 17 ++---------------
 source/Scrolls/CuboidType.mmt      | 11 +++++------
 source/Scrolls/RectangleScroll.mmt |  1 -
 source/Scrolls/RectangleType.mmt   |  7 -------
 4 files changed, 7 insertions(+), 29 deletions(-)

diff --git a/source/Scrolls/CuboidScroll.mmt b/source/Scrolls/CuboidScroll.mmt
index c54adba..645630d 100644
--- a/source/Scrolls/CuboidScroll.mmt
+++ b/source/Scrolls/CuboidScroll.mmt
@@ -10,6 +10,7 @@ theory CuboidScroll =
     meta ?MetaAnnotations?problemTheory  ?CuboidScroll/Problem ❙
     meta ?MetaAnnotations?solutionTheory ?CuboidScroll/Solution ❙
     theory Problem =
+
         R: Rectangle
          ❘ meta ?MetaAnnotations?label "R"
          ❘ meta ?MetaAnnotations?description "The given rectangle"
@@ -19,20 +20,6 @@ theory CuboidScroll =
          ❘ meta ?MetaAnnotations?description "The point above the centerpoint of the rectangle"
         ❙
 
-        rTBA: ⊦ (∠ T,(R _getB),(R _getA)) ≐ 90.0
-         ❘ meta ?MetaAnnotations?label "rTBA"
-         ❘ meta ?MetaAnnotations?description "A right angle between TBA, where B is the point enclosed by T and A"
-        ❙
-
-        rTBC: ⊦ (∠ T,(R _getB),(R _getC)) ≐ 90.0
-         ❘ meta ?MetaAnnotations?label "rTBC"
-         ❘ meta ?MetaAnnotations?description "A right angle between TBC, where B is the point enclosed by T and C"
-        ❙
-
-
-
-
-    ❙
         
     ❚
     theory Solution =
@@ -41,7 +28,7 @@ theory CuboidScroll =
         meta ?MetaAnnotations?description s"Given a rectangle and a top point that lies above the point in the center of the right-angle formed by the squarepoints
                                             this scroll constructs a cuboid. Additionally you need a proof that there are two right angles between TBC and TBA" ❙
         ConstructedCuboid : Cuboid
-                ❘ = CuboidCons R T
+                ❘ = ( CuboidCons R T )
                 ❘ meta ?MetaAnnotations?label s"Cuboid"
                 ❘ meta ?MetaAnnotations?description s"The constructed Cuboid."
         ❙
diff --git a/source/Scrolls/CuboidType.mmt b/source/Scrolls/CuboidType.mmt
index eec43f5..8f5f066 100644
--- a/source/Scrolls/CuboidType.mmt
+++ b/source/Scrolls/CuboidType.mmt
@@ -2,11 +2,10 @@ namespace http://mathhub.info/FrameIT/frameworld ❚
 fixmeta ur:?LF ❚
 
 theory CuboidType =
-  
-  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
-  include ?FrameITBasics ❙
+    include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+    include ?FrameITBasics ❙
+    include ?RectangleType ❙
 
-  cuboidType : type ❘ # Cuboid ❙
-  cuboidCons : Rectangle ⟶ point  ⟶ Cuboid  ❘ # CuboidCons 1 2 ❙
-  
+    cuboidType : type ❘ # Cuboid ❙
+    cuboidCons : Rectangle ⟶ point ⟶ Cuboid ❘ # CuboidCons 1 2 ❙
 ❚
\ No newline at end of file
diff --git a/source/Scrolls/RectangleScroll.mmt b/source/Scrolls/RectangleScroll.mmt
index 06e2ce1..d26f55b 100644
--- a/source/Scrolls/RectangleScroll.mmt
+++ b/source/Scrolls/RectangleScroll.mmt
@@ -39,7 +39,6 @@ theory RectangleScroll =
         ❙
 
 
-    ❙
         
     ❚
     theory Solution =
diff --git a/source/Scrolls/RectangleType.mmt b/source/Scrolls/RectangleType.mmt
index cf15cc6..becda19 100644
--- a/source/Scrolls/RectangleType.mmt
+++ b/source/Scrolls/RectangleType.mmt
@@ -9,11 +9,4 @@ theory RectangleType =
   rectangleType : type ❘ # Rectangle ❙
   rectangleCons : point ⟶ point ⟶ point  ⟶ Rectangle  ❘ # RectangleCons 1 2 3 ❙
   
-  getA : Rectangle ⟶ point ❘ # 1 _getA ❙
-  getB : Rectangle ⟶ point ❘ # 1 _getB ❙
-  getC : Rectangle ⟶ point ❘ # 1 _getC ❙
-
-  axiomgetA : {R: Rectangle} ⊦ (RectangleCons A B C) ≐ A ❙
-  axiomgetB : {R: Rectangle} ⊦ (RectangleCons A B C) ≐ B ❙
-  axiomgetC : {R: Rectangle} ⊦ (RectangleCons A B C) ≐ C ❙
 ❚
\ No newline at end of file
-- 
GitLab