diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz
index 1341ea63765389c209fe268c185289f84666526c..d49c48d3553d1fffce76a592b328f9b419d399ff 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz differ
diff --git a/content/http..mathhub.info/LoViVo/gearbox/gb2.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/gb2.omdoc.xz
index 7f416c6aead594fad584456104d1195c93a2c16c..debafb33bca360d222942c21fcf8689d70c71f62 100644
Binary files a/content/http..mathhub.info/LoViVo/gearbox/gb2.omdoc.xz and b/content/http..mathhub.info/LoViVo/gearbox/gb2.omdoc.xz differ
diff --git a/content/http..mathhub.info/LoViVo/gearbox/gb3.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/gb3.omdoc.xz
index fc8667a1833e2db7d8620e35a7fe1399ebc4b702..671b5fa992b92326bbc8b579c8427779c1700366 100644
Binary files a/content/http..mathhub.info/LoViVo/gearbox/gb3.omdoc.xz and b/content/http..mathhub.info/LoViVo/gearbox/gb3.omdoc.xz differ
diff --git a/errors/mmt-omdoc/Library/gearbox.mmt.err b/errors/mmt-omdoc/Library/gearbox.mmt.err
index 7aceb8167d547b4be4bb249111feb530e3173c43..8ad7b1b757ad5adda70fbda94f0729762b081ce9 100644
--- a/errors/mmt-omdoc/Library/gearbox.mmt.err
+++ b/errors/mmt-omdoc/Library/gearbox.mmt.err
@@ -56,11 +56,11 @@
<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>FastREPL.handleLine(REPL.scala:68)</element>
- <element>FastREPL.run(REPL.scala:48)</element>
- <element>REPL$.doFirst(REPL.scala:34)</element>
- <element>Test.main(preamble.scala:55)</element>
- <element>REPL.main(REPL.scala)</element>
+ <element>FastREPLExtension.handleLine(REPL.scala:70)</element>
+ <element>FastREPLExtension.run(REPL.scala:49)</element>
+ <element>FastREPL$.run(REPL.scala:38)</element>
+ <element>Test.main(preamble.scala:68)</element>
+ <element>FastREPL.main(REPL.scala)</element>
</stacktrace>
</error>
<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦y.radius≠0" level="1">
@@ -121,11 +121,11 @@
<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>FastREPL.handleLine(REPL.scala:68)</element>
- <element>FastREPL.run(REPL.scala:48)</element>
- <element>REPL$.doFirst(REPL.scala:34)</element>
- <element>Test.main(preamble.scala:55)</element>
- <element>REPL.main(REPL.scala)</element>
+ <element>FastREPLExtension.handleLine(REPL.scala:70)</element>
+ <element>FastREPLExtension.run(REPL.scala:49)</element>
+ <element>FastREPL$.run(REPL.scala:38)</element>
+ <element>Test.main(preamble.scala:68)</element>
+ <element>FastREPL.main(REPL.scala)</element>
</stacktrace>
</error>
<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦x.radius≠0" level="1">
@@ -186,11 +186,11 @@
<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>FastREPL.handleLine(REPL.scala:68)</element>
- <element>FastREPL.run(REPL.scala:48)</element>
- <element>REPL$.doFirst(REPL.scala:34)</element>
- <element>Test.main(preamble.scala:55)</element>
- <element>REPL.main(REPL.scala)</element>
+ <element>FastREPLExtension.handleLine(REPL.scala:70)</element>
+ <element>FastREPLExtension.run(REPL.scala:49)</element>
+ <element>FastREPL$.run(REPL.scala:38)</element>
+ <element>Test.main(preamble.scala:68)</element>
+ <element>FastREPL.main(REPL.scala)</element>
</stacktrace>
</error>
<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦RC.radius≠0" level="1">
@@ -250,151 +250,11 @@
<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>FastREPL.handleLine(REPL.scala:68)</element>
- <element>FastREPL.run(REPL.scala:48)</element>
- <element>REPL$.doFirst(REPL.scala:34)</element>
- <element>Test.main(preamble.scala:55)</element>
- <element>REPL.main(REPL.scala)</element>
- </stacktrace>
-</error>
-<error
-type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gb2?c1?definition: Judgment |- ['center=⟨0,0⟩,radius=1,numteeth=10,angle=0,angular_velocity=1'] : rotating_cogwheel" level="2">
- <stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</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.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</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>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.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.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.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>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.apply(StructureParser.scala:93)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:102)</element>
- <element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:53)</element>
- <element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
- <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>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>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>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle(ActionHandling.scala:69)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle$(ActionHandling.scala:67)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.tryHandle(Controller.scala:74)</element>
- <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>FastREPL.handleLine(REPL.scala:68)</element>
- <element>FastREPL.run(REPL.scala:48)</element>
- <element>REPL$.doFirst(REPL.scala:34)</element>
- <element>Test.main(preamble.scala:55)</element>
- <element>REPL.main(REPL.scala)</element>
- </stacktrace>
-</error>
-
-<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?definition: Judgment |- eq_refl c1.radius+c2.radius : ⊦interlocking c1 c2" level="2">
- <stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</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.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</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>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.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.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.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>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.apply(StructureParser.scala:93)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:102)</element>
- <element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:53)</element>
- <element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
- <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>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>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>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle(ActionHandling.scala:69)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle$(ActionHandling.scala:67)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.tryHandle(Controller.scala:74)</element>
- <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>FastREPL.handleLine(REPL.scala:68)</element>
- <element>FastREPL.run(REPL.scala:48)</element>
- <element>REPL$.doFirst(REPL.scala:34)</element>
- <element>Test.main(preamble.scala:55)</element>
- <element>REPL.main(REPL.scala)</element>
+ <element>FastREPLExtension.handleLine(REPL.scala:70)</element>
+ <element>FastREPLExtension.run(REPL.scala:49)</element>
+ <element>FastREPL$.run(REPL.scala:38)</element>
+ <element>Test.main(preamble.scala:68)</element>
+ <element>FastREPL.main(REPL.scala)</element>
</stacktrace>
</error>
</errors>
diff --git a/narration/Library/gearbox.omdoc b/narration/Library/gearbox.omdoc
index 5f1c1c71e5f16db759fc319a7f6041bbb035c60b..7a6448a9a110ca2ff454c48804a7b60861877e74 100644
--- a/narration/Library/gearbox.omdoc
+++ b/narration/Library/gearbox.omdoc
@@ -1,2 +1,2 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#0.0.0:2550.72.68"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/LoViVo/gearbox"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import arith http://mathhub.info/MitM/core/arithmetics"/><instruction text="fixmeta http://mathhub.info/MitM/Foundation?Logic"/><mref name="[http://mathhub.info/LoViVo/gearbox?temp]" target="http://mathhub.info/LoViVo/gearbox?temp"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#178.6.0:188.6.10"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?cogwheels]" target="http://mathhub.info/LoViVo/gearbox?cogwheels"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#359.13.0:374.13.15"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gearbox]" target="http://mathhub.info/LoViVo/gearbox?gearbox"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#839.31.0:852.31.13"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gb2]" target="http://mathhub.info/LoViVo/gearbox?gb2"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#1897.53.0:1906.53.9"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gb3]" target="http://mathhub.info/LoViVo/gearbox?gb3"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#2448.67.0:2457.67.9"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#0.0.0:2736.75.68"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/LoViVo/gearbox"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import arith http://mathhub.info/MitM/core/arithmetics"/><instruction text="fixmeta http://mathhub.info/MitM/Foundation?Logic"/><mref name="[http://mathhub.info/LoViVo/gearbox?temp]" target="http://mathhub.info/LoViVo/gearbox?temp"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#178.6.0:188.6.10"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?cogwheels]" target="http://mathhub.info/LoViVo/gearbox?cogwheels"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#359.13.0:374.13.15"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gearbox]" target="http://mathhub.info/LoViVo/gearbox?gearbox"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#839.31.0:852.31.13"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/Scrolls/TriangleScrolls.omdoc b/narration/Scrolls/TriangleScrolls.omdoc
index fd782e55a48ed1a6e910faba34463623afc98eac..e0ac541b23462f017eddf8ee8713500624a21773 100644
--- a/narration/Scrolls/TriangleScrolls.omdoc
+++ b/narration/Scrolls/TriangleScrolls.omdoc
@@ -1,5 +1,5 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:4945.141.3"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:47.0.47"/></metadata>Modular scrolls having to do with triangles</opaque><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#128.5.0:322.14.0"/></metadata>A blueprint problem theory for triangle scrolls
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:4919.141.3"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:47.0.47"/></metadata>Modular scrolls having to do with triangles</opaque><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#128.5.0:322.14.0"/></metadata>A blueprint problem theory for triangle scrolls
B
/|
/ |
diff --git a/relational/Library/gearbox.rel b/relational/Library/gearbox.rel
index 29e4c7b829b756e46cecece6292f4d363e32ae4a..84743762a9b597ef0a7d459c9f95c8b95c8a4696 100644
--- a/relational/Library/gearbox.rel
+++ b/relational/Library/gearbox.rel
@@ -2,5 +2,3 @@ document http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc
Declares http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc http://mathhub.info/LoViVo/gearbox?temp
Declares http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc http://mathhub.info/LoViVo/gearbox?cogwheels
Declares http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc http://mathhub.info/LoViVo/gearbox?gearbox
-Declares http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc http://mathhub.info/LoViVo/gearbox?gb2
-Declares http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc http://mathhub.info/LoViVo/gearbox?gb3
diff --git a/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel b/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel
index ee58104abfa6e6176a7d8aa8ac9c944767d2b1b2..8f75ff9a069ea4e7328975f76c41839cc50653fe 100644
--- a/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel
+++ b/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel
@@ -1,16 +1,10 @@
-dataconstructor http://mathhub.info/LoViVo/gearbox?gb2?c1
dataconstructor http://mathhub.info/LoViVo/gearbox?gb2?c2
-dataconstructor http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking
dataconstructor http://mathhub.info/LoViVo/gearbox?gb2?c2av
dataconstructor http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat
theory http://mathhub.info/LoViVo/gearbox?gb2
HasMeta http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gearbox
Includes http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/MitM/Foundation?NaturalDeduction
-Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?c1
-constant http://mathhub.info/LoViVo/gearbox?gb2?c1
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c1?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c1?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition
Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?c2
constant http://mathhub.info/LoViVo/gearbox?gb2?c2
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
@@ -20,41 +14,9 @@ DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://cds.omdoc.
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://mathhub.info/MitM/Foundation?NatLiterals?pos_lit?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition
-Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking
-constant http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gb2?c1?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gb2?c2?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gb2?c1?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gb2?c2?definition
Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?c2av
constant http://mathhub.info/LoViVo/gearbox?gb2?c2av
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?gb2?c2?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?gb2?c1?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat
constant http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?gb2?c2?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?gb2?c1?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
diff --git a/source/Library/gearbox.mmt b/source/Library/gearbox.mmt
index 3c1edb35fc6a1c57f4d0c207e428f6acfd1c577f..ada38b454cd7bfa3de77d5a2f477109a8062f429 100644
--- a/source/Library/gearbox.mmt
+++ b/source/Library/gearbox.mmt
@@ -51,13 +51,17 @@ coaxial_cogwheels : ⊦ ∀[x] ∀[y] coaxial x y ⇒ x.angular_velocity ≠y.
// a particular gear box with two cogwheels, one with undefined angular velocity âš
-theory gb2 =
+// doesn't fully typecheck (probably because some computation rules, like for sqrt, are missing, overall non-critical errors âš
+// theory gb2 =
include ?gearbox â™
include ☞base:?NaturalDeduction â™
+
+ // vvv doesn't typecheck â™
c1 : rotating_cogwheel ☠= [' center := (⟨0 , 0⟩), radius:=1, numteeth:=10, angle := 0, angular_velocity:=1 '] â™
c2 : cogwheel ☠= [' center := (⟨0 , 2⟩), radius:=1, numteeth:=10, angle := 0.05 '] â™
- // should work: â™
+ // should work, but doesn't typecheck: â™
proof_interlocking : ⊦ interlocking c1 c2 ☠= eq_refl ((c1.radius) + (c2.radius)) â™
+
// ...but needs computation rule for sqrt â™
c2av : ℠☠= compute_av c1 c2 proof_interlocking â™
@@ -65,9 +69,8 @@ theory gb2 =
c2avcheat : ℠☠= avc c1 c2 â™
âš
-theory gb3 =
+// theory gb3 =
include ?gb2 â™
-
âš
// we want to compute an update rule for the angular velocity of c2 âš
diff --git a/source/Scrolls/TriangleScrolls.mmt b/source/Scrolls/TriangleScrolls.mmt
index ba7b636411aaf27fd1d87ccc9942931a336fe81f..80086b517a915a123398675787fb4ef304570e82 100644
--- a/source/Scrolls/TriangleScrolls.mmt
+++ b/source/Scrolls/TriangleScrolls.mmt
@@ -103,7 +103,7 @@ theory OppositeLen =
// the description verbalizes deducedLineCA, hence must come after its declaration â™
meta ?MetaAnnotations?label "OppositeLen" â™
- meta ?MetaAnnotations?description s"Given a triangle â–³${lverb A B C} right-angled at ⊾${lverb C}, the distance ${lverb deducedLineCA} can be computed from the angle at ${lverb angleB} and the distance ${lverb B C}." â™
+ meta ?MetaAnnotations?description s"Given a triangle â–³${lverb A B C} right-angled at ⊾${lverb C}, the opposide side has length ${lverb deducedLineCA} = tan(${lverb angleB}) â‹… ${lverb B C}." â™
âš
âš