new scroll labels/descriptions + more modular triangle scrolls

3d961b83 · ComFreek · cb7bbfd6 · 3d961b83 · 3d961b83 · 3d961b83
Commit 3d961b83 authored 4 years ago by ComFreek
--- a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.omdoc.xz
--- a/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err
+++ b/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err
-<errors>
-</errors>
--- a/narration/Scrolls/TriangleScrolls.omdoc
+++ b/narration/Scrolls/TriangleScrolls.omdoc
 <?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:4666.135.3"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:47.0.47"/></metadata>Modular scrolls having to do with triangles</opaque><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#128.5.0:322.14.0"/></metadata>A blueprint problem theory for triangle scrolls
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:4946.141.3"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:47.0.47"/></metadata>Modular scrolls having to do with triangles</opaque><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#128.5.0:322.14.0"/></metadata>A blueprint problem theory for triangle scrolls
       B
      /|
     / |
@@ -7,6 +7,6 @@
   /___|
  A    C

-  (nicer image: https://en.wikipedia.org/wiki/Right_triangle#/media/File:Rtriangle.svg)</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#324.15.0:359.15.35"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#511.21.0:667.23.77"/></metadata>A blueprint problem theory for triangle scrolls that require a right angle
+  (nicer image: https://en.wikipedia.org/wiki/Right_triangle#/media/File:Rtriangle.svg)</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#324.15.0:345.15.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#497.21.0:653.23.77"/></metadata>A blueprint problem theory for triangle scrolls that require a right angle

-   We use ?TriangleScroll_GeneralProblem and demand the angle at C to be 90°</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#669.24.0:708.24.39"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?AngleSum]" target="http://mathhub.info/FrameIT/frameworld?AngleSum"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#941.33.0:955.33.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?OppositeLen]" target="http://mathhub.info/FrameIT/frameworld?OppositeLen"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#2240.68.0:2257.68.17"/></metadata></mref></omdoc>
\ No newline at end of file
+   We use ?TriangleScroll_GeneralProblem and demand the angle at C to be 90°</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC]" target="http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#655.24.0:690.24.35"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA]" target="http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#988.33.0:1018.33.30"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]" target="http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#1277.42.0:1307.42.30"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?AngleSum]" target="http://mathhub.info/FrameIT/frameworld?AngleSum"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#1521.51.0:1535.51.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?OppositeLen]" target="http://mathhub.info/FrameIT/frameworld?OppositeLen"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#2574.77.0:2591.77.17"/></metadata></mref></omdoc>
\ No newline at end of file
--- a/relational/Scrolls/TriangleScrolls.rel
+++ b/relational/Scrolls/TriangleScrolls.rel
 document http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc
-Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem
-Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem
+Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?TriangleProblem
+Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC
+Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA
+Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB
 Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?AngleSum
 Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?OppositeLen
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel
@@ -3,61 +3,39 @@ HasMeta http://mathhub.info/FrameIT/frameworld?AngleSum http://mathhub.info/Fram
 Declares http://mathhub.info/FrameIT/frameworld?AngleSum http://mathhub.info/FrameIT/frameworld?AngleSum?Problem
 theory http://mathhub.info/FrameIT/frameworld?AngleSum/Problem
 HasMeta http://mathhub.info/FrameIT/frameworld?AngleSum/Problem http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Includes http://mathhub.info/FrameIT/frameworld?AngleSum/Problem http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem
-Declares http://mathhub.info/FrameIT/frameworld?AngleSum/Problem http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC
-constant http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-Declares http://mathhub.info/FrameIT/frameworld?AngleSum/Problem http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC
-constant http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+Includes http://mathhub.info/FrameIT/frameworld?AngleSum/Problem http://mathhub.info/FrameIT/frameworld?TriangleProblem
+Includes http://mathhub.info/FrameIT/frameworld?AngleSum/Problem http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA
+Includes http://mathhub.info/FrameIT/frameworld?AngleSum/Problem http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB
 Declares http://mathhub.info/FrameIT/frameworld?AngleSum http://mathhub.info/FrameIT/frameworld?AngleSum?Solution
 theory http://mathhub.info/FrameIT/frameworld?AngleSum/Solution
 HasMeta http://mathhub.info/FrameIT/frameworld?AngleSum/Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta
 Includes http://mathhub.info/FrameIT/frameworld?AngleSum/Solution http://mathhub.info/FrameIT/frameworld?AngleSum/Problem
-Declares http://mathhub.info/FrameIT/frameworld?AngleSum/Solution http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA
-constant http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://cds.omdoc.org/urtheories?Ded?DED?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?subtraction?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://cds.omdoc.org/urtheories?Strings?string?type
+Declares http://mathhub.info/FrameIT/frameworld?AngleSum/Solution http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC
+constant http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://mathhub.info/FrameIT/frameworld?TriangleProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://mathhub.info/FrameIT/frameworld?TriangleProblem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB?angleB?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?subtraction?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA?angleA?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://mathhub.info/FrameIT/frameworld?TriangleProblem?B?type
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel
@@ -3,7 +3,7 @@ HasMeta http://mathhub.info/FrameIT/frameworld?OppositeLen http://mathhub.info/F
 Declares http://mathhub.info/FrameIT/frameworld?OppositeLen http://mathhub.info/FrameIT/frameworld?OppositeLen?Problem
 theory http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem
 HasMeta http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Includes http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem
+Includes http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC
 Declares http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC
 constant http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
@@ -11,22 +11,11 @@ DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?C?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-Declares http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC
-constant http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?B?type
+Includes http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB
 Declares http://mathhub.info/FrameIT/frameworld?OppositeLen http://mathhub.info/FrameIT/frameworld?OppositeLen?Solution
 theory http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution
 HasMeta http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta
@@ -38,15 +27,16 @@ DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLin
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?ded?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?prop?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?C?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?eq?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Trigonometry?tan?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?TriangleProblem?A?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?TriangleProblem?C?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://cds.omdoc.org/urtheories?Ded?DED?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
@@ -55,7 +45,6 @@ DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLin
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB?angleB?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://cds.omdoc.org/urtheories?Strings?string?type
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.rel
+dataconstructor http://mathhub.info/FrameIT/frameworld?TriangleProblem?A
+dataconstructor http://mathhub.info/FrameIT/frameworld?TriangleProblem?B
+dataconstructor http://mathhub.info/FrameIT/frameworld?TriangleProblem?C
+theory http://mathhub.info/FrameIT/frameworld?TriangleProblem
+HasMeta http://mathhub.info/FrameIT/frameworld?TriangleProblem http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Declares http://mathhub.info/FrameIT/frameworld?TriangleProblem http://mathhub.info/FrameIT/frameworld?TriangleProblem?A
+constant http://mathhub.info/FrameIT/frameworld?TriangleProblem?A
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld?TriangleProblem http://mathhub.info/FrameIT/frameworld?TriangleProblem?B
+constant http://mathhub.info/FrameIT/frameworld?TriangleProblem?B
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld?TriangleProblem http://mathhub.info/FrameIT/frameworld?TriangleProblem?C
+constant http://mathhub.info/FrameIT/frameworld?TriangleProblem?C
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.rel
+dataconstructor http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA?angleA
+theory http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA
+HasMeta http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA http://mathhub.info/FrameIT/frameworld?TriangleProblem
+Declares http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA?angleA
+constant http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA?angleA
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA?angleA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA?angleA?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA?angleA?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA?angleA?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA?angleA?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA?angleA?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA?angleA?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA?angleA?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA?angleA?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA?angleA?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?B?type
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.rel
+dataconstructor http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB?angleB
+theory http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB
+HasMeta http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB http://mathhub.info/FrameIT/frameworld?TriangleProblem
+Declares http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB?angleB
+constant http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB?angleB
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB?angleB?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB?angleB?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB?angleB?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB?angleB?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB?angleB?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB?angleB?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB?angleB?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB?angleB?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB?angleB?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB?angleB?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?B?type
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.rel
+dataconstructor http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC?rightAngleC
+theory http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC
+HasMeta http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC http://mathhub.info/FrameIT/frameworld?TriangleProblem
+Declares http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC?rightAngleC
+constant http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC?rightAngleC
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC?rightAngleC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC?rightAngleC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC?rightAngleC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC?rightAngleC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC?rightAngleC?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC?rightAngleC?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC?rightAngleC?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC?rightAngleC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC?rightAngleC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC?rightAngleC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC?rightAngleC?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?B?type
--- a/source/Scrolls/TriangleScrolls.mmt
+++ b/source/Scrolls/TriangleScrolls.mmt
@@ -13,7 +13,7 @@ fixmeta ?FrameworldMeta ❚

  (nicer image: https://en.wikipedia.org/wiki/Right_triangle#/media/File:Rtriangle.svg)
 ❚
-theory TriangleScroll_GeneralProblem =
+theory TriangleProblem =
    A: point ❘ meta ?MetaAnnotations?label "A" ❙
    B: point ❘ meta ?MetaAnnotations?label "B"❙
    C: point ❘ meta ?MetaAnnotations?label "C"❙
@@ -22,47 +22,56 @@ theory TriangleScroll_GeneralProblem =
 /T A blueprint problem theory for triangle scrolls that require a right angle

   We use ?TriangleScroll_GeneralProblem and demand the angle at C to be 90° ❚
-theory TriangleScroll_RightAngledProblem =
-    include ?TriangleScroll_GeneralProblem ❙
-    rightAngleBCA
+theory TriangleProblem_RightAngleAtC =
+    include ?TriangleProblem ❙
+    rightAngleC
        : ⊦ ( ∠ B,C,A ) ≐ 90.0 ❘
-        meta ?MetaAnnotations?label s"∟${lverb C}" ❘
-        meta ?MetaAnnotations?description s"Right angle at ${lverb C}"
+        meta ?MetaAnnotations?label s"⊾${lverb C} (${lverb A C} ⟂ ${lverb B C})" ❘
+        meta ?MetaAnnotations?description s"Right angle at ${lverb C} as enclosed by legs ${lverb A C} and ${lverb B C}."
    ❙
 ❚

+theory TriangleProblem_AngleAtA =
+   include ?TriangleProblem ❙
+   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}"
+   ❙
+❚
+
+theory TriangleProblem_AngleAtB =
+    include ?TriangleProblem ❙
+    angleB
+        : Σ β: ℝ. ⊦ ( ∠ A,B,C ) ≐ β ❘
+        meta ?MetaAnnotations?label s"∠${lverb A B C}" ❘
+        meta ?MetaAnnotations?description s"Angle at ${lverb B}"
+   ❙
+❚
+
 theory AngleSum =
    meta ?MetaAnnotations?problemTheory ?AngleSum/Problem ❙
    meta ?MetaAnnotations?solutionTheory ?AngleSum/Solution ❙

    theory Problem =
-        include ?TriangleScroll_GeneralProblem ❙
-
-        angleBAC
-            : Σ α: ℝ. ⊦ ( ∠ B,A,C ) ≐ α ❘
-            meta ?MetaAnnotations?label s"∠${lverb B A C}" ❘
-            meta ?MetaAnnotations?description s"Angle at ${lverb A}"
-        ❙
-
-        angleABC
-            : Σ β: ℝ. ⊦ ( ∠ A,B,C ) ≐ β ❘
-            meta ?MetaAnnotations?label s"∠${lverb A B C}" ❘
-            meta ?MetaAnnotations?description s"Angle at ${lverb B}"
-        ❙
+        include ?TriangleProblem ❙
+        include ?TriangleProblem_AngleAtA ❙
+        include ?TriangleProblem_AngleAtB ❙
    ❚

    theory Solution =
        include ?AngleSum/Problem ❙

-        meta ?MetaAnnotations?label "AngleSum" ❙
-        meta ?MetaAnnotations?description s"Given a triangle ${lverb A B C} and two known angles, we can deduce the missing angle by the sum of interior angles in triangles always being 180°" ❙
-
-        angleBCA
+        angleC
            : Σ γ: ℝ. ⊦ ( ∠ B,C,A ) ≐ γ ❘
-            = ⟨180.0 - (πl angleBAC) - (πl angleABC), sketch "By sum of interior angles = 180° in triangles"⟩ ❘
+            = ⟨180.0 - (πl angleA) - (πl angleB), sketch "By sum of interior angles = 180° in triangles"⟩ ❘
            meta ?MetaAnnotations?label s"∠${lverb B C A}" ❘
-            meta ?MetaAnnotations?description s"The deduced angle by calculating 180° - ${lverb angleBAC} - ${lverb angleABC}"
+            meta ?MetaAnnotations?description s"The deduced angle by calculating 180° - ${lverb angleA} - ${lverb angleB}"
        ❙
+
+        // the description verbalizes angleC, hence must come after its declaration ❙
+        meta ?MetaAnnotations?label "AngleSum" ❙
+        meta ?MetaAnnotations?description s"Given a triangle △${lverb A B C} and two known angles, we can deduce the missing angle by: ${lverb angleC} = 180° - ${lverb angleA} - ${lverb angleB}." ❙
    ❚
 ❚

@@ -71,33 +80,30 @@ theory OppositeLen =
    meta ?MetaAnnotations?solutionTheory ?OppositeLen/Solution ❙

    theory Problem =
-        include ?TriangleScroll_RightAngledProblem ❙
+        include ?TriangleProblem_RightAngleAtC ❙
    
        distanceBC
            : Σ x:ℝ . ⊦ ( d- B C ) ≐ x ❘
            meta ?MetaAnnotations?label s"${lverb B C}" ❘
            meta ?MetaAnnotations?description s"Length of leg ${lverb B C}"
        ❙
-    
-        angleABC
-            : Σ a:ℝ . ⊦ ( ∠ A,B,C ) ≐ a ❘
-            meta ?MetaAnnotations?label s"∠${lverb A B C}" ❘
-            meta ?MetaAnnotations?description s"Angle at ${lverb B}"
-        ❙
+
+        include ?TriangleProblem_AngleAtB ❙
    ❚
    
    theory Solution =
        include ?OppositeLen/Problem ❙
-
-        meta ?MetaAnnotations?label "OppositeLen" ❙
-        meta ?MetaAnnotations?description s"Given a triangle ${lverb A B C} right angled at ${lverb C}, the distance ${lverb A B} can be computed from the angle at ${lverb B} and the distance ${lverb B C}" ❙
    
        deducedLineCA
            : Σ x:ℝ . ⊦ (d- C A) ≐ x ❘
-            = ⟨(tan (πl angleABC)) ⋅ (πl distanceBC), sketch "OppositeLen Scroll"⟩ ❘
+            = ⟨(tan (πl angleB)) ⋅ (πl distanceBC), sketch "OppositeLen Scroll"⟩ ❘
            meta ?MetaAnnotations?label s"${lverb C A}" ❘
            meta ?MetaAnnotations?description s"The deduced length of the line ${lverb C A}"
        ❙
+
+        // the description verbalizes deducedLineCA, hence must come after its declaration ❙
+        meta ?MetaAnnotations?label "OppositeLen" ❙
+        meta ?MetaAnnotations?description s"Given a triangle △${lverb A B C} right-angled at ⊾${lverb C}, the distance ${lverb deducedLineCA} can be computed from the angle at ${lverb angleB} and the distance ${lverb B C}." ❙
    ❚
 ❚