diff --git a/bin/info/kwarc/mmt/frameit/rules/AngleInvertible$.class b/bin/info/kwarc/mmt/frameit/rules/AngleInvertible$.class
index f22c0718e7804efc907afdfd81a56a4fd7e18b42..09006ce7f066e2d90cab7fbfe6dc2faf0cfdb992 100644
Binary files a/bin/info/kwarc/mmt/frameit/rules/AngleInvertible$.class and b/bin/info/kwarc/mmt/frameit/rules/AngleInvertible$.class differ
diff --git a/bin/info/kwarc/mmt/frameit/rules/AngleInvertible.class b/bin/info/kwarc/mmt/frameit/rules/AngleInvertible.class
index 5601b73efe89e541aadd06ec24aeeccca8428974..26061b5129e9e082e3efb0729c4758b7a6c47d37 100644
Binary files a/bin/info/kwarc/mmt/frameit/rules/AngleInvertible.class and b/bin/info/kwarc/mmt/frameit/rules/AngleInvertible.class differ
diff --git a/bin/info/kwarc/mmt/frameit/rules/FrameIT$.class b/bin/info/kwarc/mmt/frameit/rules/FrameIT$.class
index d357bd08b493c55bbe6d6ba9f48c535413e9efac..22f05eba9c7947d37268b5687e95557d8623dbd1 100644
Binary files a/bin/info/kwarc/mmt/frameit/rules/FrameIT$.class and b/bin/info/kwarc/mmt/frameit/rules/FrameIT$.class differ
diff --git a/bin/info/kwarc/mmt/frameit/rules/FrameIT.class b/bin/info/kwarc/mmt/frameit/rules/FrameIT.class
index 7396b0ca7a04915610d6b237af85be3ecd8cbaba..ab219786521b0d985cff923a92f773524942ad96 100644
Binary files a/bin/info/kwarc/mmt/frameit/rules/FrameIT.class and b/bin/info/kwarc/mmt/frameit/rules/FrameIT.class differ
diff --git a/bin/info/kwarc/mmt/frameit/rules/MetricCommutative$.class b/bin/info/kwarc/mmt/frameit/rules/MetricCommutative$.class
index 6384c02c78137b2a910d38fcbbf53fe4b3cea389..333752ef05c182d3f6d4fd188d63db32054cce68 100644
Binary files a/bin/info/kwarc/mmt/frameit/rules/MetricCommutative$.class and b/bin/info/kwarc/mmt/frameit/rules/MetricCommutative$.class differ
diff --git a/bin/info/kwarc/mmt/frameit/rules/MetricCommutative.class b/bin/info/kwarc/mmt/frameit/rules/MetricCommutative.class
index 2aa1c923f95477d7891ab5cf705d91f58fb55383..aaccece7268161e0c6c4b2712c57cbf2a5f54d32 100644
Binary files a/bin/info/kwarc/mmt/frameit/rules/MetricCommutative.class and b/bin/info/kwarc/mmt/frameit/rules/MetricCommutative.class differ
diff --git a/bin/info/kwarc/mmt/frameit/rules/Symbols$.class b/bin/info/kwarc/mmt/frameit/rules/Symbols$.class
index 78a79db3d4e6eaddd66eefa2af433610affb5f88..140f47f69b8fd9810f80ba46a31ad75f13656354 100644
Binary files a/bin/info/kwarc/mmt/frameit/rules/Symbols$.class and b/bin/info/kwarc/mmt/frameit/rules/Symbols$.class differ
diff --git a/bin/info/kwarc/mmt/frameit/rules/Symbols.class b/bin/info/kwarc/mmt/frameit/rules/Symbols.class
index 39d532cc6bb47b1663c4d1daae607fec5385e4a4..d6d5c179f2bf88e652c9bdd65d9183fe97aabcf6 100644
Binary files a/bin/info/kwarc/mmt/frameit/rules/Symbols.class and b/bin/info/kwarc/mmt/frameit/rules/Symbols.class differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz
index 08fcc4295929f4ab4f7c7c73ea60af68ba5e2f24..6dd9b556cac60a7d100d497b8ea00b418c84c696 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz differ
diff --git a/errors/mmt-omdoc/Library/gearbox.mmt.err b/errors/mmt-omdoc/Library/gearbox.mmt.err
index 8ad7b1b757ad5adda70fbda94f0729762b081ce9..7a1dca44bcff2c00514b0d1bf0723ca41f107c85 100644
--- a/errors/mmt-omdoc/Library/gearbox.mmt.err
+++ b/errors/mmt-omdoc/Library/gearbox.mmt.err
@@ -3,27 +3,27 @@
   <stacktrace>
     <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12(RuleBasedChecker.scala:88)</element>
     <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12$adapted(RuleBasedChecker.scala:85)</element>
-    <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+    <element>scala.collection.immutable.List.foreach(List.scala:333)</element>
     <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:85)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element>
-    <element>scala.Option.foreach(Option.scala:407)</element>
+    <element>scala.Option.foreach(Option.scala:437)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
     <element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501)</element>
-    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:692)</element>
+    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:695)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element>
-    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element>
-    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
+    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:775)</element>
+    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
     <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
-    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element>
+    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:775)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:420)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
-    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
+    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
     <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
@@ -35,14 +35,14 @@
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
     <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
-    <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+    <element>scala.collection.immutable.List.foreach(List.scala:333)</element>
     <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
     <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
-    <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+    <element>scala.collection.immutable.List.foreach(List.scala:333)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
     <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
@@ -56,9 +56,14 @@
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
     <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
-    <element>FastREPLExtension.handleLine(REPL.scala:70)</element>
-    <element>FastREPLExtension.run(REPL.scala:49)</element>
-    <element>FastREPL$.run(REPL.scala:38)</element>
+    <element>FastREPLExtension.handleLine(REPL.scala:74)</element>
+    <element>FastREPLExtension.$anonfun$run$3(REPL.scala:53)</element>
+    <element>FastREPLExtension.$anonfun$run$3$adapted(REPL.scala:52)</element>
+    <element>scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)</element>
+    <element>scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)</element>
+    <element>scala.collection.AbstractIterator.foreach(Iterator.scala:1279)</element>
+    <element>FastREPLExtension.run(REPL.scala:52)</element>
+    <element>FastREPL$.run(REPL.scala:44)</element>
     <element>Test.main(preamble.scala:68)</element>
     <element>FastREPL.main(REPL.scala)</element>
   </stacktrace>
@@ -67,28 +72,28 @@
   <stacktrace>
     <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12(RuleBasedChecker.scala:88)</element>
     <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12$adapted(RuleBasedChecker.scala:85)</element>
-    <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+    <element>scala.collection.immutable.List.foreach(List.scala:333)</element>
     <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:85)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:316)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13(MMTStructureChecker.scala:325)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13$adapted(MMTStructureChecker.scala:322)</element>
-    <element>scala.Option.foreach(Option.scala:407)</element>
+    <element>scala.Option.foreach(Option.scala:437)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:322)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
     <element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501)</element>
-    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:692)</element>
+    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:695)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element>
-    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element>
-    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
+    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:775)</element>
+    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
     <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
-    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element>
+    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:775)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:420)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
-    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
+    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
     <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
@@ -100,14 +105,14 @@
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
     <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
-    <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+    <element>scala.collection.immutable.List.foreach(List.scala:333)</element>
     <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
     <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
-    <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+    <element>scala.collection.immutable.List.foreach(List.scala:333)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
     <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
@@ -121,9 +126,14 @@
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
     <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
-    <element>FastREPLExtension.handleLine(REPL.scala:70)</element>
-    <element>FastREPLExtension.run(REPL.scala:49)</element>
-    <element>FastREPL$.run(REPL.scala:38)</element>
+    <element>FastREPLExtension.handleLine(REPL.scala:74)</element>
+    <element>FastREPLExtension.$anonfun$run$3(REPL.scala:53)</element>
+    <element>FastREPLExtension.$anonfun$run$3$adapted(REPL.scala:52)</element>
+    <element>scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)</element>
+    <element>scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)</element>
+    <element>scala.collection.AbstractIterator.foreach(Iterator.scala:1279)</element>
+    <element>FastREPLExtension.run(REPL.scala:52)</element>
+    <element>FastREPL$.run(REPL.scala:44)</element>
     <element>Test.main(preamble.scala:68)</element>
     <element>FastREPL.main(REPL.scala)</element>
   </stacktrace>
@@ -132,28 +142,28 @@
   <stacktrace>
     <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12(RuleBasedChecker.scala:88)</element>
     <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12$adapted(RuleBasedChecker.scala:85)</element>
-    <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+    <element>scala.collection.immutable.List.foreach(List.scala:333)</element>
     <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:85)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:316)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13(MMTStructureChecker.scala:325)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13$adapted(MMTStructureChecker.scala:322)</element>
-    <element>scala.Option.foreach(Option.scala:407)</element>
+    <element>scala.Option.foreach(Option.scala:437)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:322)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
     <element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501)</element>
-    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:692)</element>
+    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:695)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element>
-    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element>
-    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
+    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:775)</element>
+    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
     <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
-    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element>
+    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:775)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:420)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
-    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
+    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
     <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
@@ -165,14 +175,14 @@
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
     <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
-    <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+    <element>scala.collection.immutable.List.foreach(List.scala:333)</element>
     <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
     <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
-    <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+    <element>scala.collection.immutable.List.foreach(List.scala:333)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
     <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
@@ -186,9 +196,14 @@
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
     <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
-    <element>FastREPLExtension.handleLine(REPL.scala:70)</element>
-    <element>FastREPLExtension.run(REPL.scala:49)</element>
-    <element>FastREPL$.run(REPL.scala:38)</element>
+    <element>FastREPLExtension.handleLine(REPL.scala:74)</element>
+    <element>FastREPLExtension.$anonfun$run$3(REPL.scala:53)</element>
+    <element>FastREPLExtension.$anonfun$run$3$adapted(REPL.scala:52)</element>
+    <element>scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)</element>
+    <element>scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)</element>
+    <element>scala.collection.AbstractIterator.foreach(Iterator.scala:1279)</element>
+    <element>FastREPLExtension.run(REPL.scala:52)</element>
+    <element>FastREPL$.run(REPL.scala:44)</element>
     <element>Test.main(preamble.scala:68)</element>
     <element>FastREPL.main(REPL.scala)</element>
   </stacktrace>
@@ -197,27 +212,27 @@
   <stacktrace>
     <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12(RuleBasedChecker.scala:88)</element>
     <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12$adapted(RuleBasedChecker.scala:85)</element>
-    <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+    <element>scala.collection.immutable.List.foreach(List.scala:333)</element>
     <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:85)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element>
-    <element>scala.Option.foreach(Option.scala:407)</element>
+    <element>scala.Option.foreach(Option.scala:437)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</element>
     <element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
     <element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501)</element>
-    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:692)</element>
+    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:695)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element>
-    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element>
-    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
+    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:775)</element>
+    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
     <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
-    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element>
+    <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:775)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:420)</element>
     <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
-    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
+    <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
     <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
     <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
@@ -229,14 +244,14 @@
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
     <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
-    <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+    <element>scala.collection.immutable.List.foreach(List.scala:333)</element>
     <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
     <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
     <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
-    <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
+    <element>scala.collection.immutable.List.foreach(List.scala:333)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
     <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
@@ -250,9 +265,14 @@
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
     <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
-    <element>FastREPLExtension.handleLine(REPL.scala:70)</element>
-    <element>FastREPLExtension.run(REPL.scala:49)</element>
-    <element>FastREPL$.run(REPL.scala:38)</element>
+    <element>FastREPLExtension.handleLine(REPL.scala:74)</element>
+    <element>FastREPLExtension.$anonfun$run$3(REPL.scala:53)</element>
+    <element>FastREPLExtension.$anonfun$run$3$adapted(REPL.scala:52)</element>
+    <element>scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)</element>
+    <element>scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)</element>
+    <element>scala.collection.AbstractIterator.foreach(Iterator.scala:1279)</element>
+    <element>FastREPLExtension.run(REPL.scala:52)</element>
+    <element>FastREPL$.run(REPL.scala:44)</element>
     <element>Test.main(preamble.scala:68)</element>
     <element>FastREPL.main(REPL.scala)</element>
   </stacktrace>
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel
index 8d4c439e751c7aa34b1dc8d97c2a8c50f5e0c138..3fbfd050f300a37b2276d61afe428e0d700c7cef 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel
@@ -12,30 +12,30 @@ HasMeta http://mathhub.info/FrameIT/frameworld?AngleSum/Solution http://mathhub.
 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?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/FrameIT/frameworld?TriangleProblem?B?type
+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?eq?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?Logic?prop?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?definition
 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://cds.omdoc.org/urtheories?Strings?string?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/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/core/geometry?3DGeometry?point?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/FrameIT/frameworld?TriangleProblem_AngleAtA?angleA?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://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://cds.omdoc.org/urtheories?Ded?DED?type
 DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleC?definition http://mathhub.info/FrameIT/frameworld?TriangleProblem?B?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/Foundation?Logic?ded?definition
+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?prop?type
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Midpoint.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Midpoint.rel
index 2f362d918602781d8889765303d713655b579deb..ae2e4798937354af2b438d902b93a3cbb83821e4 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Midpoint.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Midpoint.rel
@@ -5,27 +5,27 @@ theory http://mathhub.info/FrameIT/frameworld?Midpoint/Problem
 HasMeta http://mathhub.info/FrameIT/frameworld?Midpoint/Problem http://mathhub.info/FrameIT/frameworld?FrameworldMeta
 Declares http://mathhub.info/FrameIT/frameworld?Midpoint/Problem http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?P
 constant http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?P
-DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?P?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?P?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?P?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 Declares http://mathhub.info/FrameIT/frameworld?Midpoint/Problem http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?Q
 constant http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?Q
-DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?Q?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?Q?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?Q?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 Declares http://mathhub.info/FrameIT/frameworld?Midpoint http://mathhub.info/FrameIT/frameworld?Midpoint?Solution
 theory http://mathhub.info/FrameIT/frameworld?Midpoint/Solution
 HasMeta http://mathhub.info/FrameIT/frameworld?Midpoint/Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta
 Includes http://mathhub.info/FrameIT/frameworld?Midpoint/Solution http://mathhub.info/FrameIT/frameworld?Midpoint/Problem
 Declares http://mathhub.info/FrameIT/frameworld?Midpoint/Solution http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint
 constant http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint
-DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?addition?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?Q?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?P?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
 DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/FrameIT/frameworld?Midpoint/Problem?P?type
-DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?addition?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Midpoint/Solution?midpoint?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel
index 9b162282b5ddf7103234266253c8715579e725da..cb8d7594ea6d88c127e314e7898771af363c3170 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel
@@ -6,15 +6,15 @@ HasMeta http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem http://mathhu
 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
+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/FrameIT/frameworld?TriangleProblem?B?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-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?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?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?ded?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/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
@@ -22,29 +22,29 @@ HasMeta http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution http://mathh
 Includes http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem
 Declares http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA
 constant http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?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/core/geometry?3DGeometry?point?type
-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?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?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?ded?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?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/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://cds.omdoc.org/urtheories?Strings?string?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?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/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?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://cds.omdoc.org/urtheories?Bool?BOOL?type
-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/FrameIT/frameworld?OppositeLen/Problem?distanceBC?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://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?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://cds.omdoc.org/urtheories?Strings?string?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://cds.omdoc.org/urtheories?Ded?DED?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?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.rel
index 4d92d994ade885b0bde8e5c035e0d84105aad622..491178189fc277657c349d207ae42fc8a0f88d3b 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.rel
@@ -5,97 +5,97 @@ theory http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem
 HasMeta http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?FrameworldMeta
 Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A
 constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B
 constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C
 constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D
 constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?L
 constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?L
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type?type
 Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L
 constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?L?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?onLine?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?onLine?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?L?type
 Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L
 constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?L?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?onLine?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?onLine?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?L?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
 Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L
 constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?L?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?onLine?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?onLine?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?L?type
 Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD
 constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/Foundation?Logic?eq?type
 Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles http://mathhub.info/FrameIT/frameworld?SupplementaryAngles?Solution
 theory http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution
 HasMeta http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta
 Includes http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem
 Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC
 constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?subtraction?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?subtraction?type
 DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.rel
index e83f644f75d14ed169ee9c302a1da421f7862850..49a6bc6283d4b8dc665073beb64920aea23ecee4 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.rel
@@ -5,13 +5,13 @@ 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
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 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
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 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
+DependsOn http://mathhub.info/FrameIT/frameworld?TriangleProblem?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
diff --git 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
index f3e958276d3cf2c4a6fc0d3f16c0e07cecebf47b..c211e287eb02ead16045248e02fb6989562d3bb0 100644
--- 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
@@ -4,13 +4,13 @@ HasMeta http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtA http://m
 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/FrameIT/frameworld?TriangleProblem?B?type
+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?eq?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?Logic?prop?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?definition
 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
diff --git 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
index ecaa41815ed41e4d25e7cf412d05166f25df4298..92e293cec7c43c132abf12959494b6f83248fa0c 100644
--- 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
@@ -4,13 +4,13 @@ HasMeta http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB http://m
 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/FrameIT/frameworld?TriangleProblem?B?type
+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?eq?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?Logic?prop?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?definition
 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
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 637218bc8604654e7ba723577fd7667c23622b82..21db50e3d535a56ae1bba6e3692c50f2df2dd413 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,14 @@ 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/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/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
-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
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.rel
index da8a1a1fae224d3f48f98c6e1a2369ea27d65bd1..a152096e242e496ddf9d8e273b36274539e99f42 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.rel
@@ -13,29 +13,29 @@ DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?definition
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/MitM/Foundation?Logic?prop?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://cds.omdoc.org/urtheories?Strings?string?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://cds.omdoc.org/urtheories?Ded?DED?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?definition
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.rel
index af1b73176e7a5f5a57ce1393445c34617c1e102e..330dd9c59212153e76ece49e43c29e876fcd8856 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.rel
@@ -17,11 +17,11 @@ DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pangleABC_v
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pangleABC_v
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pangleABC_v?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.rel
index d2ccb1493412672d7e8d1c8d32bdb681df786677..be5bedb14941ac4979b429cb83bd7ea51abe67c8 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.rel
@@ -8,16 +8,16 @@ theory http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_
 HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld?FrameworldMeta
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codA
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codA
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codB
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codB
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codB?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codB?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codB?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codC
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codC
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?arcsin
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?arcsin
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?arcsin?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.rel
index d1886288f479323a44b61225f640df5f72c53c0c..767a2e327af9d1fc86bd3e02c279848212526def 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.rel
@@ -6,25 +6,25 @@ theory http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_
 HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain http://mathhub.info/FrameIT/frameworld?FrameworldMeta
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?A
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?A
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?B
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?B
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?C
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?C
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?A?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.rel
index 4f69a9c6fcc6d2a724dd5c8f9f5331bfda1664e8..3b87c537290e5ff18ac2c5438f18563824e97e83 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.rel
@@ -7,122 +7,122 @@ Includes http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituation
 Includes http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld?AngleSum
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Strings?string?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Strings?string?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Strings?string?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Strings?string?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Strings?string?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Strings?string?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Strings?string?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.rel
index 1a4992d2a0ec3dbfa135456dfa9e0b8f950f7d52..f9cf237e56b3d8f66da7cc6a61d471e66c17b80e 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.rel
@@ -8,10 +8,10 @@ Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?b
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?p
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?p
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?p?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?p?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?p?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?p?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?p?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?p?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?v
 HasDomain http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem
 HasCodomain http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory
@@ -28,10 +28,10 @@ Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?c
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?q
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?q
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?q?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?q?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?q?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?q?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?q?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?p?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?q?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?w
 HasDomain http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory/w http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem
 HasCodomain http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory/w http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.rel
index aff1ebd13aa8ecd411b423dd3dc7de0536773612..12622d6c6fa6d8b8b2046b88e043b22ed2f2a885 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.rel
@@ -16,8 +16,8 @@ DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParamete
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist?definition http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?A?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist?definition http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist?definition http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?A?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?TheoryParameterBug?dist?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
diff --git a/relational/http..mathhub.info/LoViVo/gearbox/cogwheels.rel b/relational/http..mathhub.info/LoViVo/gearbox/cogwheels.rel
index 18715a350767df6634ca85bd70e0bd8e1b0146c5..f5acaa932ffecfa26509888bf3e588a7f9c5a24a 100644
--- a/relational/http..mathhub.info/LoViVo/gearbox/cogwheels.rel
+++ b/relational/http..mathhub.info/LoViVo/gearbox/cogwheels.rel
@@ -14,8 +14,8 @@ constant http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory?radius
 DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory?radius?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
 Declares http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory?numteeth
 constant http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory?numteeth
-DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory?numteeth?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
 DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory?numteeth?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory?numteeth?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
 Declares http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory?angle
 constant http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory?angle
 DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory?angle?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
diff --git a/relational/http..mathhub.info/LoViVo/gearbox/gearbox.rel b/relational/http..mathhub.info/LoViVo/gearbox/gearbox.rel
index ab1cc4ea28333b1564238a5e4f20d5123f19a223..385b0297cb650d354fe9f752dc989a195c4c31c2 100644
--- a/relational/http..mathhub.info/LoViVo/gearbox/gearbox.rel
+++ b/relational/http..mathhub.info/LoViVo/gearbox/gearbox.rel
@@ -8,82 +8,82 @@ HasMeta http://mathhub.info/LoViVo/gearbox?gearbox http://mathhub.info/MitM/Foun
 Includes http://mathhub.info/LoViVo/gearbox?gearbox http://mathhub.info/LoViVo/gearbox?cogwheels
 Declares http://mathhub.info/LoViVo/gearbox?gearbox http://mathhub.info/LoViVo/gearbox?gearbox?interlocking
 constant http://mathhub.info/LoViVo/gearbox?gearbox?interlocking
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?addition?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition http://mathhub.info/LoViVo/gearbox?temp?dist?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?addition?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
 Declares http://mathhub.info/LoViVo/gearbox?gearbox http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels
 constant http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?implies?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ImplicitProof?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://cds.omdoc.org/urtheories?NatSymbols?NAT?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?neq?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/core/arithmetics?RealArithmetics?div?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://cds.omdoc.org/urtheories?Bool?BOOL?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ImplicitProof?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?neq?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?neq?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/core/arithmetics?RealArithmetics?div?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?implies?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?prop?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?forall?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://cds.omdoc.org/urtheories?NatSymbols?NAT?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
 Declares http://mathhub.info/LoViVo/gearbox?gearbox http://mathhub.info/LoViVo/gearbox?gearbox?coaxial
 constant http://mathhub.info/LoViVo/gearbox?gearbox?coaxial
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial?definition http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial?definition http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition
 Declares http://mathhub.info/LoViVo/gearbox?gearbox http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels
 constant http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/LoViVo/gearbox?gearbox?coaxial?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?implies?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?prop?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?forall?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?prop?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?eq?type
 Declares http://mathhub.info/LoViVo/gearbox?gearbox http://mathhub.info/LoViVo/gearbox?gearbox?compute_av
 constant http://mathhub.info/LoViVo/gearbox?gearbox?compute_av
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/MitM/Foundation?Logic?ded?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/MitM/Foundation?Logic?ded?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?ImplicitProof?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://cds.omdoc.org/urtheories?NatSymbols?NAT?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?neq?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?neq?definition
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?div?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?ImplicitProof?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?neq?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://cds.omdoc.org/urtheories?NatSymbols?NAT?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit?type
 DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
diff --git a/relational/http..mathhub.info/LoViVo/gearbox/temp.rel b/relational/http..mathhub.info/LoViVo/gearbox/temp.rel
index 7b51cc248325726aa705dc2ef42067ee49ec1439..c657b374be38e65e2db00f7c9ceb00a39e071287 100644
--- a/relational/http..mathhub.info/LoViVo/gearbox/temp.rel
+++ b/relational/http..mathhub.info/LoViVo/gearbox/temp.rel
@@ -6,18 +6,18 @@ Includes http://mathhub.info/LoViVo/gearbox?temp http://mathhub.info/MitM/Founda
 Declares http://mathhub.info/LoViVo/gearbox?temp http://mathhub.info/LoViVo/gearbox?temp?dist
 constant http://mathhub.info/LoViVo/gearbox?temp?dist
 DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?type
-DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?ImplicitProof?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?subtraction?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?exponentiation?type
 DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
 DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?squareRoot?type
-DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?NatLiterals?pos_lit?type
 DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
 DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
-DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?exponentiation?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?type
 DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?ImplicitProof?type
-DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?subtraction?type
 DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?squareRoot?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?NatLiterals?pos_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition