diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz
index bf8b1ae0a1bfc8301a9bd7bbbb042d42d8c5b495..1d13cd70a4e13baa37333790a01edf5da8a26309 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz
index 022ad2d27d331f0f24d0e91671e23966210f8b78..7f2de8265273d9eb0d2b8f7bb88d0fb7445196b7 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz
index 4b37bdb1152ec36596733e072ab281d30d430738..f58dd1ac5451c19fd0e55f5fdb1830515be3f6b9 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz
index e11b9e79a43c859c1da4ffeaa6baab5ffa7501db..8d01f7915ad285643da6b2c237c1b3872bf4fd79 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz
index f03c131da820789cf2e3864e0a489ba9804b9cd6..c8354a0f018d32c5ff09aaba8cafea121bf9b92f 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz
index a108280932a641225023c1f20ece77e258252ef7..88635db33d429f083926068770dc8fcf88174a1c 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Pythagoras.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Pythagoras.omdoc.xz
index 220acb5aaf530ad737af2ef4d70c27cecbb7d427..cea1f796dbc9fbc2a0969698d75f1fe6c704ccaf 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Pythagoras.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Pythagoras.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz
index 6c87ea67192b69f18617be0ea0da3e425f4f5c74..7150180157c1ad2a49e77fc721b9cd1d310d1e77 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.omdoc.xz
index 114223d374263e15ccd3d27b4e27aab25ebe3a58..b380d1824ee6ce8c8a4f5faab7a9dd12391b9dfb 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.omdoc.xz differ
diff --git 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
index 08b96e69ececec2468120093ba7bdde8fcc4ccc9..27549ca5bfb7f144e3bfff7c6b3e85b7ac1e01f2 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.omdoc.xz differ
diff --git 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
index a467e2afbf41c1e7dbb81b57dd9bccd9210976d6..7eeb303a9c550409330bf2518636ca6938d2d9ba 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz differ
diff --git 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
index d38587278df425f6c80b39c8203ee3645c79d182..f1c59d444fe2ae82e0b5f84dff6c682e0902e4ae 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.omdoc.xz differ
diff --git a/errors/mmt-omdoc/DefaultSituationSpace.mmt.err b/errors/mmt-omdoc/DefaultSituationSpace.mmt.err
index a003a310ddaac2945e140ceaaaa6d7e3db90d6b4..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/errors/mmt-omdoc/DefaultSituationSpace.mmt.err
+++ b/errors/mmt-omdoc/DefaultSituationSpace.mmt.err
@@ -1,2 +0,0 @@
-<errors>
-</errors>
diff --git a/errors/mmt-omdoc/MetaTheories.mmt.err b/errors/mmt-omdoc/MetaTheories.mmt.err
index a003a310ddaac2945e140ceaaaa6d7e3db90d6b4..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/errors/mmt-omdoc/MetaTheories.mmt.err
+++ b/errors/mmt-omdoc/MetaTheories.mmt.err
@@ -1,2 +0,0 @@
-<errors>
-</errors>
diff --git a/errors/mmt-omdoc/Scrolls/MiscScrolls.mmt.err b/errors/mmt-omdoc/Scrolls/MiscScrolls.mmt.err
index a003a310ddaac2945e140ceaaaa6d7e3db90d6b4..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/errors/mmt-omdoc/Scrolls/MiscScrolls.mmt.err
+++ b/errors/mmt-omdoc/Scrolls/MiscScrolls.mmt.err
@@ -1,2 +0,0 @@
-<errors>
-</errors>
diff --git a/errors/mmt-omdoc/Scrolls/SupplementaryAngles.mmt.err b/errors/mmt-omdoc/Scrolls/SupplementaryAngles.mmt.err
index a003a310ddaac2945e140ceaaaa6d7e3db90d6b4..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/errors/mmt-omdoc/Scrolls/SupplementaryAngles.mmt.err
+++ b/errors/mmt-omdoc/Scrolls/SupplementaryAngles.mmt.err
@@ -1,2 +0,0 @@
-<errors>
-</errors>
diff --git a/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err b/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err
index a003a310ddaac2945e140ceaaaa6d7e3db90d6b4..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err
+++ b/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err
@@ -1,2 +0,0 @@
-<errors>
-</errors>
diff --git a/narration/DefaultSituationSpace.omdoc b/narration/DefaultSituationSpace.omdoc
index 5c9ef7d20d50c9d42d492299f6d1773584d3f1c7..c3da48e6a701cde2bd4486809c4a87a51c5f85f5 100644
--- a/narration/DefaultSituationSpace.omdoc
+++ b/narration/DefaultSituationSpace.omdoc
@@ -1,2 +1,2 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.mmt#0.0.0:300.12.0"/><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><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace]" target="http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.mmt#117.4.0:144.4.27"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.mmt#0.0.0:699.26.0"/><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><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace]" target="http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.mmt#117.4.0:144.4.27"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/MetaTheories.omdoc b/narration/MetaTheories.omdoc
index a75d096ac0d47212c0f5963561f4ffb33343746b..34be72d83c4920796d703191a93355e36eccee11 100644
--- a/narration/MetaTheories.omdoc
+++ b/narration/MetaTheories.omdoc
@@ -1,2 +1,2 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#0.0.0:1074.34.0"/><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><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#70.4.0:198.4.128"/></metadata>MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?MetaAnnotations]" target="http://mathhub.info/FrameIT/frameworld?MetaAnnotations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#200.5.0:221.5.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#628.22.0:723.22.95"/></metadata>The meta theory to use for situation theories, scroll problem, and scroll solution theories</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?FrameworldMeta]" target="http://mathhub.info/FrameIT/frameworld?FrameworldMeta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#725.23.0:745.23.20"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#0.0.0:20521.388.0"/><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><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#125.5.0:253.5.128"/></metadata>MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?MetaAnnotations]" target="http://mathhub.info/FrameIT/frameworld?MetaAnnotations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#255.6.0:276.6.21"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?2DPoints]" target="http://mathhub.info/FrameIT/frameworld?2DPoints"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#685.24.1:699.24.15"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITBasics]" target="http://mathhub.info/FrameIT/frameworld?FrameITBasics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#1094.48.0:1113.48.19"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITRectangles]" target="http://mathhub.info/FrameIT/frameworld?FrameITRectangles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#4340.108.0:4363.108.23"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITTriangles]" target="http://mathhub.info/FrameIT/frameworld?FrameITTriangles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#7437.158.0:7459.158.22"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCircle]" target="http://mathhub.info/FrameIT/frameworld?FrameITCircle"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#10771.202.0:10790.202.19"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCone]" target="http://mathhub.info/FrameIT/frameworld?FrameITCone"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#12754.240.0:12771.240.17"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCylinder]" target="http://mathhub.info/FrameIT/frameworld?FrameITCylinder"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#16111.295.0:16132.295.21"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITTheories]" target="http://mathhub.info/FrameIT/frameworld?FrameITTheories"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#17019.318.0:17040.318.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#19961.370.0:20056.370.95"/></metadata>The meta theory to use for situation theories, scroll problem, and scroll solution theories</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?FrameworldMeta]" target="http://mathhub.info/FrameIT/frameworld?FrameworldMeta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#20058.371.0:20078.371.20"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/Scrolls/MiscScrolls.omdoc b/narration/Scrolls/MiscScrolls.omdoc
index d967130bcf8c7289799ef1b9b055a69f05bdc9db..6e9db13ff5dc36629229b1c61ce6cf5ae10a8b8f 100644
--- a/narration/Scrolls/MiscScrolls.omdoc
+++ b/narration/Scrolls/MiscScrolls.omdoc
@@ -1,2 +1,2 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.mmt#0.0.0:1241.36.0"/><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/MiscScrolls.mmt#0.0.0:84.0.84"/></metadata>Miscellaneous scrolls for playing around/testing that don't have a good home yet</opaque><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld?Midpoint]" target="http://mathhub.info/FrameIT/frameworld?Midpoint"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.mmt#165.5.0:179.5.14"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.mmt#0.0.0:1242.36.0"/><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/MiscScrolls.mmt#0.0.0:85.0.85"/></metadata>Miscellaneous scrolls for playing around/testing that don't have a good home yet</opaque><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld?Midpoint]" target="http://mathhub.info/FrameIT/frameworld?Midpoint"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.mmt#166.5.0:180.5.14"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/Scrolls/SupplementaryAngles.omdoc b/narration/Scrolls/SupplementaryAngles.omdoc
index b5fb88ea673d58f1f1292fc07e06a99e14dcd8e6..de14b366a6daf68b008e8a8819b22c84c92ae7f0 100644
--- a/narration/Scrolls/SupplementaryAngles.omdoc
+++ b/narration/Scrolls/SupplementaryAngles.omdoc
@@ -1,8 +1,8 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.mmt#0.0.0:1623.46.0"/><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><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/SupplementaryAngles.mmt#78.3.0:245.11.0"/></metadata><scope>\
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.mmt#0.0.0:1627.46.0"/><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><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/SupplementaryAngles.mmt#78.3.0:246.11.0"/></metadata><scope>\
\ D
\
________\_________
A B C
-The scroll encodes angle ABD + angle DBC = 180°, or rather, angle DBC = 180° - angle ABD</scope></opaque><mref name="[http://mathhub.info/FrameIT/frameworld?SupplementaryAngles]" target="http://mathhub.info/FrameIT/frameworld?SupplementaryAngles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.mmt#247.12.0:272.12.25"/></metadata></mref></omdoc>
\ No newline at end of file
+The scroll encodes angle ABD + angle DBC = 180°, or rather, angle DBC = 180° - angle ABD</scope></opaque><mref name="[http://mathhub.info/FrameIT/frameworld?SupplementaryAngles]" target="http://mathhub.info/FrameIT/frameworld?SupplementaryAngles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.mmt#248.12.0:273.12.25"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/Scrolls/TriangleScrolls.omdoc b/narration/Scrolls/TriangleScrolls.omdoc
index e0ac541b23462f017eddf8ee8713500624a21773..cdf39a4293079d3a5b1a1e707a4949d45eb7241b 100644
--- a/narration/Scrolls/TriangleScrolls.omdoc
+++ b/narration/Scrolls/TriangleScrolls.omdoc
@@ -1,5 +1,5 @@
<?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:4919.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
+<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:5183.146.0"/><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
/|
/ |
@@ -9,4 +9,4 @@
(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?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#987.33.0:1017.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#1276.42.0:1306.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#1520.51.0:1534.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#2573.77.0:2590.77.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#1019.34.0:1049.34.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#1308.43.0:1338.43.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#1552.52.0:1566.52.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#2605.78.0:2622.78.17"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?Pythagoras]" target="http://mathhub.info/FrameIT/frameworld?Pythagoras"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#3857.111.1:3873.111.17"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/relational/MetaTheories.rel b/relational/MetaTheories.rel
index 8b853ecba0ea1b39e4118c561bf4713db7ca49a7..6b8fa1982acbe47a182d7f0fba9ba416ab6d3a05 100644
--- a/relational/MetaTheories.rel
+++ b/relational/MetaTheories.rel
@@ -1,3 +1,11 @@
document http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc
Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?MetaAnnotations
+Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?2DPoints
+Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?FrameITBasics
+Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?FrameITRectangles
+Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?FrameITTriangles
+Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?FrameITCircle
+Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?FrameITCone
+Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?FrameITCylinder
+Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?FrameITTheories
Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?FrameworldMeta
diff --git a/relational/Scrolls/TriangleScrolls.rel b/relational/Scrolls/TriangleScrolls.rel
index 05c2bf85a4eccdaed220441bbc28c37b4c040424..488dd37d92d59fe9258e73eb559910b74d290cad 100644
--- a/relational/Scrolls/TriangleScrolls.rel
+++ b/relational/Scrolls/TriangleScrolls.rel
@@ -5,3 +5,4 @@ Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc ht
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
+Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?Pythagoras
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel
index f9fa1b075770bb616d2158a68084e3efa8996548..978c253e43588fc065624457d0146af9ac3cf4d0 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel
@@ -3,7 +3,14 @@ HasMeta http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace http://math
Declares http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace?Root
theory http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root
HasMeta http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?SupplementaryAngles
Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?OppositeLen
Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?AngleSum
+Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?CylinderVolumeScroll
+Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?PlaneAngleToAngleScroll
Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?Midpoint
+Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?CircleScroll
+Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?SinOppositeLeg
+Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?PlaneLineAngleScroll
+Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?CircleAreaScroll
+Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?ConeVolumeScroll
+Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?TruncatedConeVolumeScroll
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.rel
index 956f2232a1786c294bb4d54fee225dbd081530c7..8be1a9452b1667d0b88642321a0768fd8fd1260d 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.rel
@@ -1,8 +1,5 @@
theory http://mathhub.info/FrameIT/frameworld?FrameworldMeta
HasMeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta http://cds.omdoc.org/urtheories?LF
Includes http://mathhub.info/FrameIT/frameworld?FrameworldMeta http://mathhub.info/FrameIT/frameworld?MetaAnnotations
-Includes http://mathhub.info/FrameIT/frameworld?FrameworldMeta http://mathhub.info/MitM/Foundation?Strings
-Includes http://mathhub.info/FrameIT/frameworld?FrameworldMeta http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma
+Includes http://mathhub.info/FrameIT/frameworld?FrameworldMeta http://mathhub.info/FrameIT/frameworld?FrameITTheories
Includes http://mathhub.info/FrameIT/frameworld?FrameworldMeta http://mathhub.info/MitM/Foundation?Math
-Includes http://mathhub.info/FrameIT/frameworld?FrameworldMeta http://mathhub.info/MitM/core/geometry?3DGeometry
-Includes http://mathhub.info/FrameIT/frameworld?FrameworldMeta http://mathhub.info/MitM/core/geometry?Planes
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Pythagoras.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Pythagoras.rel
index 8c07a175d2b13c6cfa670a9ab73d466fa7b02d0c..abc155ae771250dcc856794a8b6117e2e3f6e7d6 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Pythagoras.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Pythagoras.rel
@@ -1,68 +1,61 @@
theory http://mathhub.info/FrameIT/frameworld?Pythagoras
HasMeta http://mathhub.info/FrameIT/frameworld?Pythagoras http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Declares http://mathhub.info/FrameIT/frameworld?Pythagoras http://mathhub.info/FrameIT/frameworld?Pythagoras?Pythagoras_Problem
-theory http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem
-HasMeta http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Includes http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem
-Declares http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceAC
-constant http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceAC
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceAC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceAC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceAC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceAC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceAC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceAC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceAC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceAC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceAC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-Declares http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceBC
-constant http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceBC
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceBC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceBC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceBC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceBC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-Declares http://mathhub.info/FrameIT/frameworld?Pythagoras http://mathhub.info/FrameIT/frameworld?Pythagoras?Pythagoras_Solution
-theory http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution
-HasMeta http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Includes http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem
-Declares http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse
-constant http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?addition?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?squareRoot?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://cds.omdoc.org/urtheories?Ded?DED?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?NatLiterals?pos_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?InformalProofs?trivial?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceBC?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?exponentiation?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceAC?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Strings?string?type
+Declares http://mathhub.info/FrameIT/frameworld?Pythagoras http://mathhub.info/FrameIT/frameworld?Pythagoras?Problem
+theory http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem
+HasMeta http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC
+Declares http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceAC
+constant http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceAC
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceAC?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceAC?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceAC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceAC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceAC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceAC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceAC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceAC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceAC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceBC
+constant http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceBC
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceBC?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceBC?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceBC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceBC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld?Pythagoras http://mathhub.info/FrameIT/frameworld?Pythagoras?Solution
+theory http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution
+HasMeta http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem
+Declares http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse
+constant http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceAC?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?TriangleProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?Pythagoras/Problem?distanceBC?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?TriangleProblem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?FrameITBasics?useRoot?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?addition?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
diff --git 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
index 21db50e3d535a56ae1bba6e3692c50f2df2dd413..0fb5bab4ba88223028a566d32fdb430817fd5fb0 100644
--- 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
@@ -4,14 +4,12 @@ HasMeta http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC htt
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/FrameIT/frameworld?FrameITBasics?rightAngle?type
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/FrameIT/frameworld?TriangleProblem?C?type
DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC?rightAngleC?type http://mathhub.info/FrameIT/frameworld?TriangleProblem?B?type
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?eq?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/MitM/core/geometry?Geometry/Common?angle_between?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?ded?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/MitM/Foundation?RealLiterals?real_lit?type
diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt
index 7ad9610d93a4894788dafcc78b4b9e12c577145a..53a79d8f364e475d5f32e82f0cc3f6139da79eca 100644
--- a/source/DefaultSituationSpace.mmt
+++ b/source/DefaultSituationSpace.mmt
@@ -4,9 +4,23 @@ fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta âš
theory DefaultSituationSpace =
theory Root =
- include ?SupplementaryAngles â™
+ // include ?SupplementaryAngles â™
include ?OppositeLen â™
include ?AngleSum â™
+ // include ?ParallelLines â™
+ // include ?InterceptTheorem â™
+ // include ?Pythagorasâ™
+ include ?CylinderVolumeScrollâ™
+ include ?PlaneAngleToAngleScrollâ™
+
include ?Midpoint â™
+ include ?CircleScroll â™
+ include ?SinOppositeLeg â™
+ include ?PlaneLineAngleScroll â™
+ include ?CircleAreaScroll â™
+ include ?ConeVolumeScroll â™
+ include ?TruncatedConeVolumeScroll â™
+
+
âš
âš
diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index 895da273153564f46b2b36d37c20c8333d37afcb..39ae590e5d6432951e2e52ef98b4fa5c8a2e0501 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -1,4 +1,5 @@
namespace http://mathhub.info/FrameIT/frameworld âš
+// import rules scala://rules.frameit.mmt.kwarc.info âš
fixmeta ur:?LF âš
@@ -20,15 +21,368 @@ theory MetaAnnotations =
description_verbalization_of # dverb â™
âš
+
+ theory 2DPoints =
+ include ?FrameITBasics â™
+
+ // simple 2d Point theory. â™
+ Point2D : type ☠# point2d â™
+ Point2Dmk : ℠⟶ ℠⟶ point2d ☠# mkpoint2d 1 2 â™
+
+ XPoint2D : point2d ⟶ ℠☠# p2x 1 â™
+
+ XPoint2DAxiom : {x,y} ⊦ ( p2x (mkpoint2d x y ) ≠x ) ☠role Simplifyâ™
+
+
+ YPoint2D : point2d ⟶ ℠☠# p2y 1 â™
+ YPoint2DAxiom : {x,y} ⊦ ( p2y (mkpoint2d x y ) ) ≠y ☠role Simplify â™
+
+
+
+
+
+ âš
+
+
+
+
+theory FrameITBasics =
+ include ☞http://mathhub.info/MitM/core/geometry?3DGeometry â™
+ include ☞http://mathhub.info/MitM/core/geometry?Planes â™
+
+ // Basics for FrameIT theories â™
+
+ // a lot of Simplify roles, so the scrolls get simplified accordingly â™
+ // com_dist : {p1: point,p2: point} ⊦ ( d- p1 p2 ) ≠( d- p2 p1 ) ☠role Simplify â™
+
+
+
+ axiomBasepoint2 : {p1,p2} ⊦ from (from p1 to p2) ≠p1 ☠role Simplify â™
+ axiomTargetpoint2 : {p1,p2} ⊦ to (from p1 to p2) ≠p2 ☠role Simplify â™
+
+ PlaneBaseAxiom12 : {v, w, b } ⊦ Pbase (Ppara b v w ) ≠b ☠role Simplify â™
+ PlaneBaseAxiomNormal2 : { v, b } ⊦ ( Pbase ( Ppn b v ) ) ≠b ☠role Simplify â™
+
+ normalAxiom12 : { v, w, b } ⊦ ( Pnormal ( Ppara b v w ) ) ≠( normalize ( v Vcross w ) ) ☠role Simplify â™
+ normalAxiom22 : { v, b } ⊦ ( Pnormal ( Ppn b v ) ) ≠( norm ( v ) ) ☠role Simplify â™
+
+ rightAngle : point ⟶ point ⟶ point ⟶ bool ☠# ∠r 1 2 3 â™
+ epsi = 0.000000000004626 â™
+
+ // early on there where problems with those functions. They might not be required anymore â™
+ multiplyPointScalar : ℠⟶ point ⟶ point ☠= [a, P ] ⟨a â‹… ( P _x ) , a â‹… (P _y ), a â‹… (P _z )⟩ ☠# 1 rdotp 2 prec 22 â™
+ addPointPoint : point ⟶ point ⟶ point ☠= [Q,P ] ⟨ ( Q _x ) + ( P _x ) , ( Q _y ) + (P _y ), ( Q _z ) + (P _z )⟩ ☠# 1 p+p 2 prec 12 â™
+ subtractPointPoint : point ⟶ point ⟶ point ☠= [Q,P ] ⟨ ( Q _x ) - ( P _x ) , ( Q _y ) - (P _y ), ( Q _z ) - (P _z )⟩ ☠# 1 p-p 2 prec 12 â™
+
+ directionLine : line ⟶ point ☠= [l] ( to l ) p-p ( from l ) ☠# directionL 1 â™
+
+ // added those, because sometimes you cant use certain operations in scrolls? Maybe this bug is fixed by now? â™
+ useRoot : ℠⟶ ℠☠= [a] √ a ☠# doRoot 1 â™
+ absValue : ℠⟶ ℠☠= [a] √ (real_pow a 2.0 ) ☠# doAbs 1 â™
+
+
+ useDiv : ℠⟶ ℠⟶ ℠☠= [a,b] a / b ☠# doDiv 1 2 â™
+ useInv : ℠⟶ ℠☠= [a] inv a ☠# doInv 1 â™ // trying to make inv work â™
+ useExpo : ℠⟶ ℠⟶ ℠☠= [a,b] real_pow a b ☠# doExpo 1 2 â™
+
+ // projection and distance function for planes â™
+ helperFunctionForProjection : plane ⟶ point ⟶ ℠☠= [e, p] ( < ( Pnormal e ) , ( planeBase e ) > - < ( Pnormal e ) , p > ) / ( < ( Pnormal e ) , ( Pnormal e ) > ) ☠# helperT 1 2 prec 1 â™
+ orthogonalProjectionPointToPlane : plane ⟶ point ⟶ point ☠= [e,p] p p+p ( ( helperT e p ) rdotp( Pnormal e ) ) ☠# orthogProjPointToPlane 1 2 prec 1 â™
+ distancePlanePoint : plane ⟶ point ⟶ ℠☠= [e,p] ( doAbs ( < Pnormal e , p > - < Pnormal e , Pbase e > ) ) / ( | Pnormal e | ) ☠# distPlP 1 2 prec 1 â™
+
+ // functions to calculate the angle between a plane and a line â™
+ anglePlaneLineCalc : point ⟶ point ⟶ ℠☠= [v,w] asin ( < v,w > / (|v| â‹… |w|)) ☠# plcalc 1 2 prec 1 â™
+ anglePlaneLine : plane ⟶ line ⟶ ℠☠= [e,l] plcalc ( Pnormal e ) ( directionL l ) ☠# ∠pl 1 2 prec 1 â™
+ radToDegree : ℠⟶ ℠☠= [r] ( r / pi_num ) â‹… 180.0 ☠# radToDegree 1 prec 1 â™
+
+
+ // obvious proofs that sometimes are required â™
+
+ lineOnProofFrom: {l } ⊦ ( from l ) on l ☠# fromOnProofLine 1 â™
+ lineOnProofTo: {l } ⊦ ( to l ) on l ☠# toOnProofLine 1 â™
+
+
+
+ âš
+
+
+theory FrameITRectangles =
+ include ☞http://mathhub.info/MitM/core/geometry?3DGeometry â™
+ include ☞http://mathhub.info/MitM/core/geometry?Planes â™
+ include ?FrameITBasics â™
+
+ // used for parallelLineTheorem â™
+ isRectangle : point ⟶ point ⟶ point ⟶ point ⟶ bool ☠= [p1, p2 , p3, p4] ( rightAngle p1 p2 p3) ∧ ( rightAngle p2 p3 p4) ∧ ( rightAngle p3 p4 p1) ∧ ( rightAngle p4 p1 p2) ☠# isRect 1 2 3 4 â™
+
+ rectangleProof : {p1,p2,p3,p4} { proof1 : ⊦ rightAngle p1 p2 p3 } { proof2 : ⊦ rightAngle p2 p3 p4 } { proof3 : ⊦ rightAngle p3 p4 p1 } { proof4 : ⊦ rightAngle p4 p1 p2 } ⊦ isRect p1 p2 p3 p4 ☠# isRectProof 5 6 7 8 â™
+
+ axiomRectParallelOne : {p1,p2,p3,p4} { proof1 : ⊦ isRect p1 p2 p3 p4 } ⊦ paraL (from p1 to p2) (from p3 to p4) â™
+
+ axiomRectParallelOneAdjusted : {g1,g2,p1,p2,p3,p4} { proof1 : ⊦ isRect p1 p2 p3 p4 } { proof_p1_on_g1 : ⊦ p1 on g1 } { proof_p2_on_g1 : ⊦ p2 on g1 } { proof_p3_on_g2 : ⊦ p3 on g2 } { proof_p4_on_g2 : ⊦ p4 on g2 } ⊦ paraL g1 g2 ☠# axiomRectParallel 7 8 9 10 11 â™
+
+ axiomRectParallelADBC: {g1: line,g2: line,p1: point,p2: point,p3: point,p4: point} { proof1 : ⊦ isRect p1 p2 p3 p4 } { proof_p1_on_g1 : ⊦ p1 on g1 } { proof_p4_on_g1 : ⊦ p4 on g1 } { proof_p2_on_g2 : ⊦ p2 on g2 } { proof_p3_on_g2 : ⊦ p3 on g2 } ⊦ paraL g1 g2 ☠# axRectParallelADBC 7 8 9 10 11 â™
+
+
+
+ // tried to define a rectangle type â™
+ // TODO maybe delete â™
+
+ rectangle_type : type ☠# rect â™
+
+ mkRectangle : { A: point , B : point, C : point , D : point } ( ⊦ isRect A B C D ) ⟶ rect ☠# mkRect 1 2 3 4 5 â™
+ cornerA : rect ⟶ point ☠# rectA 1 â™
+ cornerB : rect ⟶ point ☠# rectB 1 â™
+ cornerC : rect ⟶ point ☠# rectC 1 â™
+ cornerD : rect ⟶ point ☠# rectD 1 â™
+ rectSideAD : rect ⟶ line ☠# rectAD 1 â™
+ rectSideBC : rect ⟶ line ☠# rectBC 1 â™
+
+
+
+ axiomCornerA : {A,B,C,D,p} ⊦ ( cornerA ( mkRectangle A B C D p ) ≠A ) ☠role Simplify â™
+ axiomCornerB : {A,B,C,D,p} ⊦ ( cornerB ( mkRectangle A B C D p ) ≠B ) ☠role Simplify â™
+ axiomCornerC : {A,B,C,D,p} ⊦ ( cornerC ( mkRectangle A B C D p ) ≠C ) ☠role Simplify â™
+ axiomCornerD : {A,B,C,D,p} ⊦ ( cornerD ( mkRectangle A B C D p ) ≠D ) ☠role Simplify â™
+ axiomSideAD : {A,B,C,D,p} ⊦ ( rectSideAD ( mkRectangle A B C D p ) ≠( from A to D ) ) ☠role Simplify â™
+ axiomSideBC : {A,B,C,D,p} ⊦ ( rectSideBC ( mkRectangle A B C D p ) ≠( from B to C ) ) ☠role Simplify â™
+
+ rectParalleABCD : {r: rect } ⊦ ( paraL ( from ( cornerA r ) to ( cornerB r ) ) ( from ( cornerC r) to ( cornerD r ) ) ) ☠# rParalleABCD 1 â™
+
+ // rect_paralle_AD_BC : {r: rect } ⊦ ( paraL ( from ( corner_A r ) to ( corner_D r ) ) ( from ( corner_B r) to ( corner_C r ) ) ) ☠# r_paralle_AD_BC 1 â™
+ rectParalleADBC : {r: rect } ⊦ ( paraL ( rectSideAD r ) ( rectSideBC r ) ) ☠# rParalleADBC 1 â™
+
+ rectParallADBCProof2 : {r: rect, ad: line, bc: line, p1 : ⊦ ( rectSideAD r ) ≠ad , p2 : ⊦ ( rectSideBC r ) ≠bc } ⊦ paraL ad bc ☠# parallelADBCProofv2 1 2 3 %I4 %I5 â™
+
+ âš
+
+
+theory FrameITTriangles =
+ include ☞http://mathhub.info/MitM/core/geometry?3DGeometry â™
+ include ☞http://mathhub.info/MitM/core/geometry?Planes â™
+ include ?FrameITBasics â™
+
+ // some theories for triangles â™
+ // TODO maybe delete â™
+
+ // triangle rules we need to simplify terms ... â™
+ axiomAtriangle : {a,b,c} ⊦ ( _A ( Δ a b c ) ) ≠a ☠role Simplify â™
+ axiomBtriangle : {a,b,c} ⊦ ( _B ( Δ a b c ) ) ≠b ☠role Simplify â™
+ axiomCtriangle : {a,b,c} ⊦ ( _C ( Δ a b c ) ) ≠c ☠role Simplify â™
+
+
+ triangleToPlane2: triangle ⟶ plane ☠= [t] ( Ppara ( _A t ) ( ( _A t ) p-p ( _B t ) ) ( ( _A t ) p-p ( _C t ) ) ) ☠# Pof2Δ 1 â™
+
+ // additional triangle rules â™
+ // Mittelsenkrechten und deren Schnittpunkt â™
+ trianglePerpendicularBisectorAB3D : triangle ⟶ line ☠= [t] from ( 0.5 rdotp ( ( _A t ) p+p ( _B t ) ) ) to ( ( 0.5 rdotp ( ( _A t ) p+p ( _B t ) ) ) p+p ( ( Pnormal ( Pof2Δ t ) ) Vcross ( ( _B t ) p-p ( _A t ) ) ) ) ☠# bisecTriAB3D 1 â™
+ trianglePerpendicularBisectorBC3D : triangle ⟶ line ☠= [t] from ( 0.5 rdotp ( ( _B t ) p+p ( _C t ) ) ) to ( ( 0.5 rdotp ( ( _B t ) p+p ( _C t ) ) ) p+p ( ( Pnormal ( Pof2Δ t ) ) Vcross ( ( _C t ) p-p ( _B t ) ) ) ) ☠# bisecTriBC3D 1 â™
+ trianglePerpendicularBisectorCA3D : triangle ⟶ line ☠= [t] from ( 0.5 rdotp ( ( _C t ) p+p ( _A t ) ) ) to ( ( 0.5 rdotp ( ( _C t ) p+p ( _A t ) ) ) p+p ( ( Pnormal ( Pof2Δ t ) ) Vcross ( ( _A t ) p-p ( _C t ) ) ) ) ☠# bisecTriCA3D 1 â™
+
+ trianglePerpendicularBisectorIntersectAxiom : { t } ⊦ colL ( bisecTriAB3D t ) ( bisecTriBC3D t) ☠# perpBisIntersectAxiomABBC 1 â™
+ // this cant be the way to calculate it. Because we will not get a point with colV... ff â™
+ // triangle_mid_point : triangle ⟶ point ☠= [t] colLV ( bisec_tri_AB_3d t ) ( bisec_tri_BC_3d t) ( perp_bis_intersect_axiom_AB_BC t ) ☠# mid_triangle_3d 1 â™
+
+
+ cramerRuleIntersection : point ⟶ point ⟶ point ⟶ ℠☠= [c,u,v] ( (-1.0 â‹… ( c _x ) â‹… ( v _y ) ) + ( ( c _y ) â‹… ( v _x ) ) ) / ( epsi + ( (-1.0 â‹… ( u _x ) â‹… ( v _y ) ) + ( ( u _y ) â‹… ( v _x ) )) ) ☠# CramerRuleIntersection 1 2 3 â™
+ // This function shouldn't be necessary. But due to some weird bug, the server will crash without it. â™
+ wrapCramerRuleIntersectionForIntersectingBisectors : line ⟶ line ⟶ ℠☠= [l,h] ( cramerRuleIntersection ( ( from l ) p-p ( from h ) ) ( directionL l ) ( directionL h ) ) ☠# CramerRuleIntersectionLines 1 2 â™
+
+ // wrap_cramer_rule_intersection_for_intersecting_bisectors : {l: line,h: line} ( ⊦ colL l h ) â™
+ intersectionTwoLines : line ⟶ line ⟶ point ☠= [l,h] ( from l ) p+p ( ( CramerRuleIntersectionLines l h ) rdotp ( directionL l ) ) ☠# intersectTwoLinesActualPoint 1 2 â™
+
+ // ( perp_bis_intersect_axiom_AB_BC t )â™
+ triangleMidPoint : triangle ⟶ point ☠= [t] intersectTwoLinesActualPoint ( bisecTriAB3D t ) ( bisecTriBC3D t) ☠# midTriangle3D 1 â™
+
+ triangleMidPointWrapper : point ⟶ point ⟶ point ⟶ point ☠= [p1,p2,p3] midTriangle3D ( Δ A B C ) ☠# midTriangle3DWrap 1 2 3 â™
+ // triangle_perpendicular_bisectors_intersection_3d : triangle ⟶ point ☠= [t] ( ( 0.5 rdotp ( ( _A t ) p+p ( _B t ) ) ) ) ☠# mid_tri_3d 1 â™
+
+
+
+ âš
+
+theory FrameITCircle =
+ include ☞http://mathhub.info/MitM/core/geometry?3DGeometry â™
+ include ☞http://mathhub.info/MitM/core/geometry?Planes â™
+ include ?FrameITBasics â™
+
+
+ circleType3D : type ☠# circle â™
+ // circle constructor taking a plane ( the circle lies in ) a point (middle) and a real number (radius) â™
+ circle3D : plane ⟶ point ⟶ ℠⟶ circle ☠# mkCirc3D 1 2 3 â™
+
+ circleMidPoint : circle ⟶ point ☠# mid 1 â™
+ circleRadius : circle ⟶ ℠☠# radius 1 â™
+ circlePlane : circle ⟶ plane ☠# planeCircle 1 â™
+
+ axiomMidPoint : {e,p,r} ⊦ mid (mkCirc3D e p r) ≠p ☠role Simplify â™
+ axiomPlane : {e,p,r} ⊦ planeCircle (mkCirc3D e p r) ≠e ☠role Simplify â™
+ axiomRadius : {e,p,r} ⊦ radius (mkCirc3D e p r) ≠r ☠role Simplify â™
+
+ pointOnCircle : circle ⟶ point ⟶ bool ☠= [c,p] ( p VonP ( planeCircle c ) ) ∧ ( leq_real_lit ( d-p ( mid c ) ) ( radius c ) ) ☠# 2 VonC 1 â™
+ midAlwaysOnCircle : {c: circle, m: point, p: ⊦ ( mid c ) ≠m } ⊦ m VonC c ☠# midOnC 1 2 %I3 â™
+
+
+ areaCircle : circle ⟶ ℠☠= [c] ( real_pow ( radius c) 2.0 ) â‹… pi_num ☠# areaCirc 1 â™
+ circumCircle : circle ⟶ ℠☠= [c] 2.0 â‹… ( radius c ) â‹… pi_num ☠# circCirc 1 â™
+
+ angleCircleLine : circle ⟶ line ⟶ ℠☠= [c,l] radToDegree ( plcalc ( Pnormal ( planeCircle c ) ) ( directionL l ) ) ☠# ∠cl 1 2 prec 1 â™
+ orthogonalCircleLine : circle ⟶ line ⟶ bool ☠# orthogCL 1 2 â™
+
+ pointsToPlaneNormal : point ⟶ point ⟶ point ⟶ plane ☠= [p1,p2,p3] Ppn p1 ( normalize ( (p2 p-p p1 ) Vcross ( p3 p-p p1) ) ) ☠# pToPlane 1 2 3 â™
+ wrap3EdgePointsToPlaneParametric : point ⟶ point ⟶ point ⟶ plane ☠= [p1,p2,p3 ] Ppara p1 (p2 p-p p1 ) ( p3 p-p p1) ☠# pointsToPlanePara 1 2 3 â™
+
+ parallelCircles: circle ⟶ circle ⟶ bool ☠# paraCirc 1 2 â™
+ proofParallelCircles : {c1: circle, c2:circle, ab: line, p1: ⊦ orthogCL c1 ab , p2: ⊦ orthogCL c2 ab } ⊦ paraCirc c1 c2 ☠# axParaCirc 1 2 3 4 5 â™
+
+
+
+ âš
+
+theory FrameITCone =
+ include ☞http://mathhub.info/MitM/core/geometry?3DGeometry â™
+ include ☞http://mathhub.info/MitM/core/geometry?Planes â™
+ include ?FrameITBasics â™
+ include ?FrameITCircle â™
+
+
+ circleConeType : type ☠# cone â™
+ circleConeOf : circle ⟶ point ⟶ cone ☠# planeC 1 apex 2 â™
+ circleConeApex : cone ⟶ point ☠# coneApex 1 prec 1 â™
+ circleConePlane : cone ⟶ circle ☠# conePl 1 prec 1 â™
+
+ axiomConeApex : {c, p} ⊦ coneApex ( planeC c apex p ) ≠p ☠role Simplify â™
+ axiomConePlane : {c,p} ⊦ conePl ( planeC c apex p ) ≠c ☠role Simplify â™
+
+
+ coneHeightProjection : cone ⟶ point ☠= [c] orthogProjPointToPlane ( planeCircle ( conePl c ) ) ( coneApex c ) ☠# coneHeightOnBaseProj 1 prec 1 â™
+ coneHeightLine : cone ⟶ line ☠= [c] from ( coneApex c) to ( coneHeightOnBaseProj c ) ☠# heightLineC 1 prec 1 â™
+ coneHeightLength : cone ⟶ ℠☠= [c] d- ( coneApex c) ( coneHeightOnBaseProj c ) ☠# heightLengthC 1 prec 1 â™
+
+ // distance_apex_plane : cone ⟶ ℠☠= [c] ( do_abs ( < Pnormal ( circle_plane ( cone_plane c ) ) , cone_apex c > - < Pnormal ( circle_plane ( cone_plane c ) ) , Pbase ( circle_plane ( cone_plane c ) ) > ) ) / ( | Pnormal ( circle_plane ( cone_plane c ) ) | ) ☠# dist_p_s 1 prec 1 â™
+ distApexPlane : cone ⟶ ℠☠= [c] distPlP ( circlePlane ( conePl c ) ) ( coneApex c ) ☠# distPS 1 prec 1 â™
+
+ volumeCone : cone ⟶ ℠☠= [c] ( areaCirc ( conePl c) ) â‹… ( distPS c) / 3.0 ☠# volCone 1 prec 1 â™
+ baseAreaCone : cone ⟶ ℠☠= [c] ( areaCirc ( conePl c ) ) ☠# baseAreaC 1 prec 1 â™
+
+ // truncated cones â™
+
+
+ truncatedConeType : type ☠# tcone â™
+ mkTruncatedCone : {c1: circle, c2: circle} ( ⊦ paraCirc c1 c2 ) ⟶ tcone ☠# mkTcone 1 2 3 â™
+
+ truncatedConeBase : tcone ⟶ circle ☠# tconeBase 1 â™
+ truncatedConeTop : tcone ⟶ circle ☠# tconeTop 1 â™
+
+ axiomTruncatedConeBase : {c1, c2, p} ⊦ tconeBase ( mkTcone c1 c2 p) ≠c1 ☠role Simplify â™
+ axiomTruncatedConeTop : {c1, c2, p} ⊦ tconeTop ( mkTcone c1 c2 p) ≠c2 ☠role Simplify â™
+
+ // truncated_cone_height : tcone ⟶ ℠☠= [tc] d- ( mid ( tcone_base tc ) ) ( mid ( tcone_top tc ) ) ☠# tcone_height 1 â™
+
+ // swapped top and base should be fine thoâ™
+ truncatedConeHeight : tcone ⟶ ℠☠= [tc] distPlP ( circlePlane ( tconeBase tc ) ) ( mid ( tconeTop tc ) ) ☠# tconeHeight 1 â™
+
+ // truncatedConeBaseArea : tcone ⟶ ℠☠= [tc] ( real_pow ( radius ( tconeBase tc ) ) 2.0 ) + ( ( radius ( tconeTop tc ) ) â‹… ( radius ( tconeBase tc ) ) ) + ( real_pow ( radius ( tconeTop tc ) ) 2.0 ) ☠# tconeBaseArea 1 â™
+
+ truncatedConeArea : tcone ⟶ ℠☠= [tc] ( areaCirc ( tconeBase tc ) ) + ( ( ( radius ( tconeTop tc ) ) â‹… ( radius ( tconeBase tc ) ) ) â‹… pi_num ) + ( areaCirc ( tconeTop tc ) ) ☠# tconeArea 1 â™
+
+
+ truncatedConeVolume : tcone ⟶ ℠☠= [tc] ( 1.0 / 3.0 ) â‹… (tconeHeight tc) â‹… ( tconeArea tc ) ☠# tconeVol 1 â™
+
+ // truncatedConeVolume : tcone ⟶ ℠☠= [tc] ( ( ( 1.0 / 3.0 ) â‹… pi_num ) â‹… (tconeHeight tc) ) â‹… ( ( real_pow ( radius ( tconeBase tc ) ) 2.0 ) + ( ( radius ( tconeTop tc ) ) â‹… ( radius ( tconeBase tc ) ) ) + ( real_pow ( radius ( tconeTop tc ) ) 2.0 ) ) ☠# tconeVol 1 â™
+
+
+ âš
+
+theory FrameITCylinder =
+ include ☞http://mathhub.info/MitM/core/geometry?3DGeometry â™
+ include ☞http://mathhub.info/MitM/core/geometry?Planes â™
+ include ?FrameITBasics â™
+ include ?FrameITCircle â™
+
+
+ cylinderType : type ☠# cyl â™
+ mkCylinder : {c1: circle, c2: circle} ( ⊦ paraCirc c1 c2 ) ⟶ cyl ☠# mkCyl 1 2 3 â™
+ cylinderBase : cyl ⟶ circle ☠# cylBase 1 â™
+ cylinderTop : cyl ⟶ circle ☠# cylTop 1 â™
+
+ axCylBase : {c1, c2, p} ⊦ cylBase ( mkCyl c1 c2 p) ≠c1 ☠role Simplify â™
+ axCylTop : {c1, c2, p} ⊦ cylTop ( mkCyl c1 c2 p) ≠c2 ☠role Simplify â™
+
+ cylinderArea : cyl ⟶ ℠☠= [c] areaCirc ( cylBase c) ☠# cylArea 1 prec 1 â™
+ cylinderHeight : cyl ⟶ ℠☠= [c] d- ( mid ( cylBase c) ) ( mid ( cylTop c) ) ☠# cylHeight 1 prec 1 â™
+
+ cylinderVolume : cyl ⟶ ℠☠= [c] (cylHeight c) â‹… ( cylArea c ) ☠# cylVol 1 â™
+
+
+ âš
+
+theory FrameITTheories =
+ include ☞http://mathhub.info/MitM/core/geometry?3DGeometry â™
+ include ☞http://mathhub.info/MitM/core/geometry?Planes â™
+ include ?FrameITTriangles â™
+ include ?FrameITRectangles â™
+ include ?FrameITCircle â™
+ include ?FrameITCone â™
+ include ?FrameITCylinder â™
+
+
+ // intersection_two_lines_test : line ⟶ line ⟶ ℠☠= [l,h] ( cramer_rule_intersection ( ( from l ) p-p (from h) ) ( direction_l l ) ( direction_l h ) ) ☠# intersect_two_lines_actual_point_test 1 2 â™
+ // wrap_intersection_test : line ⟶ line ⟶ point ☠= [l,h] ( ( cramer_rule_intersection ( ( from l ) p-p ( from h ) ) ( direction_l l ) ( direction_l h ) ) rdotp ( direction_l l ) ) ☠# intersect_two_lines_wrap 1 2 â™
+ // wrap_intersection_test2 : line ⟶ line ⟶ ℠☠= [l,h] ( cramer_rule_intersection ( ( from l ) p-p ( from h ) ) ( direction_l l ) ( direction_l h ) ) ☠# intersect_two_lines_wrap2 1 2 â™
+ // wrap_wrap : line ⟶ line ⟶ point ☠= [l,h] ( intersect_two_lines_wrap2 l h ) rdotp ( direction_l l ) ☠# wrap_wrap_losing_mind 1 2 â™
+
+ // wrap_wrapv2 : point ⟶ line ⟶ line ⟶ point ☠= [A,l,h] ( ( do_the_root ( 0.5 ) ) rdotp ( direction_l l ) ) ☠# wrap_wrap_losing_mindv2 1 2 3 â™
+ // fast_equal : ℠⟶ ℠⟶ bool ☠= [a,b] | a p-p b | â™
+ // ☠= [A,B] lineDirection A ∥ lineDirection B â™
+ // parallelo: line ⟶ line ⟶ bool ☠# paraLL 1 2 â™
+ // para_axio : { a: line , b: line } ⊦ paraLL a b ☠# cheat 1 2 â™
+
+
+
+ // defining circle over 2 points. One for the center one for the edgeâ™
+ // circleOf : point ⟶ point ⟶ circle ☠# mid 1 edge 2 â™
+ // midpoint : circle ⟶ point ☠# mid 1 prec 1 â™
+ // edgepoint : circle ⟶ point ☠# edge 1 prec 1 â™
+ // axiom_midpoint : {p1,p2} ⊦ mid (mid p1 edge p2) ≠p1 ☠role ForwardRule â™
+ // axiom_edgepoint : {p1,p2} ⊦ edge (mid p1 edge p2) ≠p2 ☠role ForwardRule â™
+
+ // radius_circle : circle ⟶ ℠☠= [c] d- ( mid c ) (edge c) ☠# radius_circle 1 â™
+ // circum_circle : circle ⟶ ℠☠= [c] ((d- ( mid c ) (edge c)) + (d- ( mid c ) (edge c))) â‹… pi_num ☠# circ_circ 1 â™
+
+ // partial circlce circumference. x should be used in % â™
+ // partial_circum_circle : circle ⟶ ℠⟶ ℠☠= [c,x] ((d- ( mid c ) (edge c)) + (d- ( mid c ) (edge c))) â‹… pi_num â‹… x ☠# partial_circ_circ 1 â™
+
+ // area_circle : circle ⟶ ℠☠= [c] ((d- ( mid c ) (edge c)) â‹… (d- ( mid c ) (edge c))) â‹… pi_num ☠# area_circ 1 â™
+
+ // use_actual_scp : point ⟶ ℠☠= [a] ( < a , a > ) ☠# do_actual_scp 1 â™
+
+
+ makeCircleOf3EdgePoints : point ⟶ point ⟶ point ⟶ circle ☠= [p1,p2,p3 ] mkCirc3D ( Ppara p1 (p2 p-p p1) ( p3 p-p p1) ) ( midTriangle3D ( Δ p1 p2 p3 ) ) ( d- ( midTriangle3D ( Δ p1 p2 p3 ) ) p1 ) ☠# mkCirc3P3D 1 2 3 â™
+
+
+
+
+ âš
+
+
+
+
+
/T The meta theory to use for situation theories, scroll problem, and scroll solution theories âš
theory FrameworldMeta =
include ?MetaAnnotations â™
+ include ?FrameITTheories â™
+ // include ☞http://mathhub.info/MitM/core/arithmetics?RealArithmetics â™
- include ☞http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma â™
- include ☞http://mathhub.info/MitM/Foundation?Strings â™
+ // include ☞http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma â™
+
+// include ☞http://mathhub.info/MitM/Foundation?Strings â™
include ☞http://mathhub.info/MitM/Foundation?Math â™
- include ☞http://mathhub.info/MitM/core/geometry?3DGeometry â™
- include ☞http://mathhub.info/MitM/core/geometry?Planes â™
+// include ☞http://mathhub.info/MitM/core/geometry?3DGeometry â™
+// include ☞http://mathhub.info/MitM/core/geometry?Planes â™
+
+
+
âš
diff --git a/source/Scrolls/MiscScrolls.mmt b/source/Scrolls/MiscScrolls.mmt
index 19a535dc34f0f9cb1cb3e3f655f32d88d9cff829..3e52ad0422a445708f4719ffa72f6bbf66c2dab3 100644
--- a/source/Scrolls/MiscScrolls.mmt
+++ b/source/Scrolls/MiscScrolls.mmt
@@ -1,4 +1,4 @@
-/T Miscellaneous scrolls for playing around/testing that don't have a good home yet âš
+/T Miscellaneous scrolls for playing around/testing that don't have a good home yet âš
namespace http://mathhub.info/FrameIT/frameworld âš
fixmeta ?FrameworldMeta âš
diff --git a/source/Scrolls/SupplementaryAngles.mmt b/source/Scrolls/SupplementaryAngles.mmt
index e6e3184849251d68dbb65f7c42250f505089ccd2..58ccc1813294c28e87fe5bd6bee04dcc3cae30a6 100644
--- a/source/Scrolls/SupplementaryAngles.mmt
+++ b/source/Scrolls/SupplementaryAngles.mmt
@@ -32,8 +32,8 @@ theory SupplementaryAngles =
âš
theory Solution =
- meta ?MetaAnnotations?label "SupplementaryAngles" â™
- meta ?MetaAnnotations?description "Supplementary angles add up to 180 degree " â™
+ meta ?MetaAnnotations?label "SupplementaryAngles" â™
+ meta ?MetaAnnotations?description s"Supplementary angles add up to 180 degree " â™
include ?SupplementaryAngles/Problem â™
diff --git a/source/Scrolls/TriangleScrolls.mmt b/source/Scrolls/TriangleScrolls.mmt
index 253bb55d06688ef39f8a5e1e190d5e83c60eb954..692cd3506a924f69bbc862ac392614271f792a6b 100644
--- a/source/Scrolls/TriangleScrolls.mmt
+++ b/source/Scrolls/TriangleScrolls.mmt
@@ -25,8 +25,9 @@ theory TriangleProblem =
theory TriangleProblem_RightAngleAtC =
include ?TriangleProblem â™
rightAngleC
- : ⊦ ( ∠B,C,A ) ≠90.0 â˜
- meta ?MetaAnnotations?label s"⊾${lverb C}" â˜
+ // : ⊦ ( ∠B,C,A ) ≠90.0 â˜
+ : ⊦ ( ∠r B C A ) â˜
+ meta ?MetaAnnotations?label s"⊾${lverb C}" â˜
meta ?MetaAnnotations?description s"${lverb A C} ⟂ ${lverb B C}: right angle at ${lverb C} as enclosed by legs ${lverb A C} and ${lverb B C}."
â™
âš
@@ -88,7 +89,7 @@ theory OppositeLen =
meta ?MetaAnnotations?description s"Length of leg ${lverb B C}"
â™
- include ?TriangleProblem_AngleAtB â™
+ include ?TriangleProblem_AngleAtB â™
âš
theory Solution =
@@ -107,26 +108,28 @@ theory OppositeLen =
âš
âš
-// Doesn't typecheck, not sure why âš
-// theory Pythagoras =
+ // Doesn't typecheck, not sure why âš
+ theory Pythagoras =
meta ?MetaAnnotations?problemTheory ?Pythagoras/Problem â™
meta ?MetaAnnotations?solutionTheory ?Pythagoras/Solution â™
theory Problem =
- include ?TriangleScroll_RightAngledProblem â™
-
+ // include ?TriangleScroll_RightAngledProblem â™
+ include ?TriangleProblem_RightAngleAtC â™
distanceAC
: Σ x:â„. ⊦ (d- A C) ≠x â˜
+ meta ?MetaAnnotations?label s"${lverb A C}" â˜
meta ?MetaAnnotations?description "Length of leg AC"
â™
distanceBC
: Σ x:â„. ⊦ (d- B C) ≠x â˜
+ meta ?MetaAnnotations?label s"${lverb B C}" â˜
meta ?MetaAnnotations?description "Length of leg BC"
â™
âš
- // theory Solution =
+ theory Solution =
include ?Pythagoras/Problem â™
meta ?MetaAnnotations?label "Pythagoras" â™
@@ -134,9 +137,10 @@ theory OppositeLen =
deducedHypotenuse
: Σ x:â„. ⊦ (d- A B) ≠x â˜
- = ⟨√ ((πl distanceAC) ⋅ (πl distanceAC) + (πl distanceBC) ⋅ (πl distanceBC)),
+ = ⟨ doTheRoot ( (πl distanceAC) ⋅ (πl distanceAC) + (πl distanceBC) ⋅ (πl distanceBC)),
sketch "By Pythagora's theorem"⟩ â˜
+ meta ?MetaAnnotations?label s"${lverb B A}" â˜
meta ?MetaAnnotations?description "Deduced length of hypotenuse AB"
â™
âš
-// âš
+ âš