From 819ecd6ce2bea3cd9199203f947abf88dda2446a Mon Sep 17 00:00:00 2001
From: Paul-Walcher <paulwalcher12@gmail.com>
Date: Tue, 25 Jun 2024 09:06:12 +0200
Subject: [PATCH] expanded CuboidScroll

---
 source/MetaTheories.mmt         |  8 ++++++++
 source/Scrolls/CuboidScroll.mmt | 10 ++++++++++
 2 files changed, 18 insertions(+)

diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index aedd54d..10b4921 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -344,6 +344,14 @@ theory RectangleType =
 
   rectangleType : type ❘ # Rectangle ❙
   rectangleCons : point ⟶ point ⟶ point  ⟶ Rectangle  ❘ # RectangleCons 1 2 3 ❙
+  
+  getA : Rectangle ⟶ point ❘ # getA 1  ❙
+  getB : Rectangle ⟶ point ❘ # getB 1  ❙
+  getC : Rectangle ⟶ point ❘ # getC 1  ❙
+
+  getAAxiom : {A, B, C} ⊦ ( ( getA ( RectangleCons A B C) ) ≐ A ) ❘ role Simplify❙
+  getBAxiom : {A, B, C} ⊦ ( ( getB ( RectangleCons A B C) ) ≐ B ) ❘ role Simplify❙
+  getCAxiom : {A, B, C} ⊦ ( ( getC ( RectangleCons A B C) ) ≐ C ) ❘ role Simplify❙
 ❚
 
 theory CuboidType =
diff --git a/source/Scrolls/CuboidScroll.mmt b/source/Scrolls/CuboidScroll.mmt
index 645630d..f7e6729 100644
--- a/source/Scrolls/CuboidScroll.mmt
+++ b/source/Scrolls/CuboidScroll.mmt
@@ -20,6 +20,16 @@ theory CuboidScroll =
          ❘ meta ?MetaAnnotations?description "The point above the centerpoint of the rectangle"
         ❙
 
+        rTBA: ⊦ (∠ T,(getB R),(getA R)) ≐ 90.0
+         ❘ meta ?MetaAnnotations?label "rTBA"
+         ❘ meta ?MetaAnnotations?description "A right angle between TBA, where B is the point enclosed by T A"
+        ❙
+        
+        rTBC: ⊦ (∠ T,(getB R),(getC R)) ≐ 90.0
+         ❘ meta ?MetaAnnotations?label "rTBC"
+         ❘ meta ?MetaAnnotations?description "A right angle between TBC, where B is the point enclosed by T C"
+        ❙
+
         
     ❚
     theory Solution =
-- 
GitLab