From 82fa06b48416d5f4b832833e349aaa6737165de0 Mon Sep 17 00:00:00 2001 From: MaZiFAU <63099053+MaZiFAU@users.noreply.github.com> Date: Sat, 25 May 2024 16:56:53 +0200 Subject: [PATCH] Toggle for prefatching from Server/Json; Fact naming; updated scrolls.json; Fact pushout now blocking; --- Assets/Scripts/GlobalBehaviour.cs | 145 +- .../FactHandling/Facts/Fact.cs | 18 +- .../FactHandling/Facts/UnsortedFact.cs | 8 +- .../Scripts/InventoryStuff/ScrollDetails.cs | 10 +- .../StreamToPersistentDataPath/scrolls.json | 1697 +++++++++++++++++ Assets/StreamingAssets/scrolls.json | 1697 +++++++++++++++++ 6 files changed, 3508 insertions(+), 67 deletions(-) diff --git a/Assets/Scripts/GlobalBehaviour.cs b/Assets/Scripts/GlobalBehaviour.cs index d01555d4..243cf100 100644 --- a/Assets/Scripts/GlobalBehaviour.cs +++ b/Assets/Scripts/GlobalBehaviour.cs @@ -51,12 +51,18 @@ public static GlobalBehaviour Instance [SerializeField] private float _GadgetPhysicalDistance; #endregion + //TODO: move? + /// <summary> Default Setting for all JSONConvert operations </summary> + public static JsonSerializerSettings JsonConvertDefaultSettings = new() { MaxDepth = 256 }; + private void Awake() { Instance = this; if (Instance != this) return; + JsonConvert.DefaultSettings = () => JsonConvertDefaultSettings; + DontDestroyOnLoad(this); GetScrollsfromServer(); GetContextfromServer(); @@ -67,6 +73,7 @@ private void Awake() public int tryScrollListTimes = 2; static public List<REST_JSON_API.Scroll> AvailableScrolls; public static IEnumerator InitiateScrolls = IEnumeratorExtensions.yield_break; + public static bool AttemptScrollList = true; //false; private void GetScrollsfromServer() { @@ -81,41 +88,48 @@ IEnumerator _GetScrollsfromServer() System.DateTime requestTime = System.DateTime.UtcNow; UnityWebRequest request = null; - for (int i = 0; i < this.tryScrollListTimes; i++) - { - request = UnityWebRequest.Get(CommunicationEvents.ServerAdress + "/scroll/list"); - request.method = UnityWebRequest.kHttpVerbGET; - yield return request.SendWebRequest(); - - if (request.result == UnityWebRequest.Result.ConnectionError - || request.result == UnityWebRequest.Result.ProtocolError) + if (AttemptScrollList) + { + for (int i = 0; i < this.tryScrollListTimes; i++) { - Debug.LogWarning(request.error); - Debug.Log("GET Scroll/list failed. Attempt: " + (i + 1).ToString()); + request = UnityWebRequest.Get(CommunicationEvents.ServerAdress + "/scroll/list"); + request.method = UnityWebRequest.kHttpVerbGET; + + yield return request.SendWebRequest(); + + if (request.result == UnityWebRequest.Result.ConnectionError + || request.result == UnityWebRequest.Result.ProtocolError) + { + Debug.LogWarning(request.error); + Debug.Log("GET Scroll/list failed. Attempt: " + (i + 1).ToString()); + } + else + break; } - else - break; + while (request.result == UnityWebRequest.Result.InProgress) + yield return null; } - while (request.result == UnityWebRequest.Result.InProgress) - yield return null; System.DateTime answerTime = System.DateTime.UtcNow; string jsonString = null; - if (request.result == UnityWebRequest.Result.ConnectionError - || request.result == UnityWebRequest.Result.ProtocolError) - { - Debug.LogWarning(request.error); - } - else + if (AttemptScrollList) { - CommunicationEvents.ServerRunning = true; + if (request.result == UnityWebRequest.Result.ConnectionError + || request.result == UnityWebRequest.Result.ProtocolError) + { + Debug.LogWarning(request.error); + } + else + { + CommunicationEvents.ServerRunning = true; - while (!request.downloadHandler.isDone) - yield return null; - jsonString = request.downloadHandler.text; + while (!request.downloadHandler.isDone) + yield return null; + jsonString = request.downloadHandler.text; + } } if (string.IsNullOrEmpty(jsonString) @@ -127,7 +141,8 @@ IEnumerator _GetScrollsfromServer() System.DateTime parseTime = System.DateTime.UtcNow; List<Scroll> _AvailableScrolls = JsonConvert.DeserializeObject<List<Scroll>>(jsonString); - + + System.DateTime processTime = System.DateTime.UtcNow; AvailableScrolls = new(); foreach (Scroll scroll in _AvailableScrolls) AvailableScrolls.Add(IJSONsavable<Scroll>.postprocess(scroll)); @@ -137,7 +152,8 @@ IEnumerator _GetScrollsfromServer() $"Summ\t{(System.DateTime.UtcNow - requestTime).TotalMilliseconds}ms\n" + $"Server\t{(answerTime - requestTime).TotalMilliseconds}ms\n" + $"Download\t{(parseTime - answerTime).TotalMilliseconds}ms\n" + - $"Parsing\t{(System.DateTime.UtcNow - parseTime).TotalMilliseconds}ms"); + $"JSONParsing\t{(processTime - parseTime).TotalMilliseconds}ms\n" + + $"Processing\t{(System.DateTime.UtcNow - processTime).TotalMilliseconds}ms"); yield break; } @@ -146,6 +162,7 @@ IEnumerator _GetScrollsfromServer() public static FactRecorder Context = new(); public static IEnumerator InitiateContext = IEnumeratorExtensions.yield_break; public static bool ContextLoaded = false; + public static bool AttemptContextLoad = true; //false; private void GetContextfromServer() { @@ -157,41 +174,48 @@ IEnumerator _GetContextfromServer() System.DateTime requestTime = System.DateTime.UtcNow; UnityWebRequest request = null; - for (int i = 0; i < this.tryScrollListTimes; i++) - { - request = UnityWebRequest.Get(CommunicationEvents.ServerAdress + "/fact/list"); - request.method = UnityWebRequest.kHttpVerbGET; - - yield return request.SendWebRequest(); - if (request.result == UnityWebRequest.Result.ConnectionError - || request.result == UnityWebRequest.Result.ProtocolError) + if (AttemptContextLoad) + { + for (int i = 0; i < this.tryScrollListTimes; i++) { - Debug.LogWarning(request.error); - Debug.Log("GET /fact/list failed. Attempt: " + (i + 1).ToString()); + request = UnityWebRequest.Get(CommunicationEvents.ServerAdress + "/fact/list"); + request.method = UnityWebRequest.kHttpVerbGET; + + yield return request.SendWebRequest(); + + if (request.result == UnityWebRequest.Result.ConnectionError + || request.result == UnityWebRequest.Result.ProtocolError) + { + Debug.LogWarning(request.error); + Debug.Log("GET /fact/list failed. Attempt: " + (i + 1).ToString()); + } + else + break; } - else - break; + while (request.result == UnityWebRequest.Result.InProgress) + yield return null; } - while (request.result == UnityWebRequest.Result.InProgress) - yield return null; System.DateTime answerTime = System.DateTime.UtcNow; string jsonString = null; - if (request.result == UnityWebRequest.Result.ConnectionError - || request.result == UnityWebRequest.Result.ProtocolError) - { - Debug.LogWarning(request.error); - } - else + if (AttemptContextLoad) { - CommunicationEvents.ServerRunning = true; + if (request.result == UnityWebRequest.Result.ConnectionError + || request.result == UnityWebRequest.Result.ProtocolError) + { + Debug.LogWarning(request.error); + } + else + { + CommunicationEvents.ServerRunning = true; - while (!request.downloadHandler.isDone) - yield return null; - jsonString = request.downloadHandler.text; + while (!request.downloadHandler.isDone) + yield return null; + jsonString = request.downloadHandler.text; + } } if (string.IsNullOrEmpty(jsonString) @@ -205,8 +229,8 @@ IEnumerator _GetContextfromServer() MMTFact[] context_facts = JsonConvert.DeserializeObject<MMTFact[]>(jsonString); System.DateTime parseEnd = System.DateTime.UtcNow; - System.DateTime justParseTime = default; - System.DateTime justAddinTime = default; + System.TimeSpan justParseTime = default; + System.TimeSpan justAddinTime = default; bool samestep = false; foreach (MMTFact fact in context_facts) @@ -216,9 +240,9 @@ IEnumerator _GetContextfromServer() || fact.GetDefines() == null) // Scala rule? continue; - System.DateTime parse_time = System.DateTime.Now; + System.DateTime parse_time = System.DateTime.UtcNow; List<Fact> new_list = Fact.MMTFactory(fact); // old but IEnumerator: yield return ParsingDictionary.parseFactDictionary[fact.getType()](new_list, fact); - justParseTime += System.DateTime.Now - parse_time; + justParseTime += System.DateTime.UtcNow - parse_time; if (new_list.Count == 0) { @@ -226,16 +250,16 @@ IEnumerator _GetContextfromServer() continue; } - System.DateTime addin_time = System.DateTime.Now; + System.DateTime addin_time = System.DateTime.UtcNow; foreach (Fact new_fact in new_list) { Context.Add(new_fact, out bool exists, samestep, null, null, true, true); if (!exists) samestep = true; - yield return null; + //yield return null; } - justAddinTime += System.DateTime.Now - addin_time; + justAddinTime += System.DateTime.UtcNow - addin_time; } Debug.Log( @@ -243,9 +267,10 @@ IEnumerator _GetContextfromServer() $"Summ\t{(System.DateTime.UtcNow - requestTime).TotalMilliseconds}ms\n" + $"Server\t{(answerTime - requestTime).TotalMilliseconds}ms\n" + $"Download\t{(parseTime - answerTime).TotalMilliseconds}ms\n" + - $"Parsing\t{(parseEnd - parseTime).TotalMilliseconds}ms\n" + - $"FactParsing\t{justParseTime.Millisecond}ms\n" + - $"FactAdding\t{justAddinTime.Millisecond}ms\n" + + $"JSONParsing\t{(parseEnd - parseTime).TotalMilliseconds}ms\n" + + $"FactCreation\t{(System.DateTime.UtcNow - parseEnd).TotalMilliseconds}ms\n" + + $"FactJustParsing\t{justParseTime.Milliseconds}ms\n" + + $"FactJustAdding\t{justAddinTime.Milliseconds}ms\n" + ""); ContextLoaded = true; diff --git a/Assets/Scripts/InteractionEngine/FactHandling/Facts/Fact.cs b/Assets/Scripts/InteractionEngine/FactHandling/Facts/Fact.cs index 69d74d13..f22e9f97 100644 --- a/Assets/Scripts/InteractionEngine/FactHandling/Facts/Fact.cs +++ b/Assets/Scripts/InteractionEngine/FactHandling/Facts/Fact.cs @@ -438,7 +438,19 @@ protected virtual string generateLabel(FactRecorder name_space) name_space.UnusedLabelIds.Remove(LabelId); } - return ((char)(64 + LabelId)).ToString(); + int LabelIdMod, LabelIdRes = LabelId; + string label = ""; + while (true) + { + LabelIdMod = LabelIdRes % 26; + label = (char)(65 + LabelIdMod) + label; + + if (LabelIdRes < 26) + break; + + LabelIdRes /= 26; + } + return "(" + label + ")"; } /// <summary> @@ -648,7 +660,7 @@ public static List<Fact> MMTFactory(MMTFact ingredient) if (ret.Count != 0) return ret; } - catch(Exception ex) + catch (Exception ex) { Debug.LogException(ex); Debug.Log($"Could not statically parse {nameof(MMTFact)} {nameof(ingredient)}. Using dynamic Fallback..."); @@ -794,7 +806,7 @@ public override MMTFact MakeMMTDeclaration() { throw new NotImplementedException(); } - + public override SOMDoc Defines() { throw new NotImplementedException(); diff --git a/Assets/Scripts/InteractionEngine/FactHandling/Facts/UnsortedFact.cs b/Assets/Scripts/InteractionEngine/FactHandling/Facts/UnsortedFact.cs index 29af5a54..54e2fb4e 100644 --- a/Assets/Scripts/InteractionEngine/FactHandling/Facts/UnsortedFact.cs +++ b/Assets/Scripts/InteractionEngine/FactHandling/Facts/UnsortedFact.cs @@ -398,12 +398,14 @@ private void Init(string[] pid_corners) throw new ArgumentException("All Points must lie on the same Plane!"); } - /// \copydoc Fact.parseFact(ScrollFact) public new static IEnumerator parseFact(List<Fact> ret, MMTFact fact) { throw new NotImplementedException(); } + protected override string generateLabel(FactRecorder name_space) + => "[" + String.Join(",", Points.Select(p => p.GetLabel(name_space)).ToArray()) + "]"; + public override MMTFact MakeMMTDeclaration() { SOMDoc tp = new OMS(MMTConstants.Wall); @@ -506,12 +508,14 @@ private void Init(Vector3[] Verticies) Normal = Vector3.Cross(Tangents, AltTangents).normalized; } - /// \copydoc Fact.parseFact(ScrollFact) public new static IEnumerator parseFact(List<Fact> ret, MMTFact fact) { throw new NotImplementedException(); } + //protected override string generateLabel(FactRecorder name_space) + // => "[" + String.Join(",", Points.Select(p => p.GetLabel(name_space)).ToArray()) + "]"; + public override MMTFact MakeMMTDeclaration() => new MMTGeneralFact(_LastLabel, GetMMTType(), Defines()); diff --git a/Assets/Scripts/InventoryStuff/ScrollDetails.cs b/Assets/Scripts/InventoryStuff/ScrollDetails.cs index 91237778..63850233 100644 --- a/Assets/Scripts/InventoryStuff/ScrollDetails.cs +++ b/Assets/Scripts/InventoryStuff/ScrollDetails.cs @@ -146,6 +146,9 @@ public bool SetNextEmptyTo(FactObjectUI activator) public void MagicButtonTrigger() { + if (ActiveScroll == null) + return; + StartCoroutine(_MagicButton()); IEnumerator _MagicButton() @@ -170,7 +173,9 @@ IEnumerator _MagicButton() if (VerboseURI) Debug.Log("Magic answers:\n" + currentMmtAnswer); + System.DateTime serializeTime = System.DateTime.UtcNow; ScrollApplicationInfo pushout = JsonConvert.DeserializeObject<ScrollApplicationInfo>(currentMmtAnswer); + Debug.LogFormat($"Answerd serialized in : {(System.DateTime.UtcNow - serializeTime).TotalMilliseconds}ms"); if (pushout.acquiredFacts.Count == 0 || pushout.errors.Length > 0) @@ -216,10 +221,9 @@ IEnumerator __GeneratePushoutFacts(List<MMTFact> pushoutFacts) // AnimateExistingFactEvent.Invoke(_new, FactWrapper.FactMaterials.Hint); // Automaticly done in FactRecorder old_to_new.Add(new_fact.Id, added.Id); } - } - yield return null; + //yield return null; } Debug.Log($"Facts parsed within {(System.DateTime.UtcNow - parseTime).TotalMilliseconds}ms"); @@ -229,6 +233,8 @@ IEnumerator __GeneratePushoutFacts(List<MMTFact> pushoutFacts) public void NewAssignmentTrigger() { + //return; //if you read this, delete this line! + if (ActiveScroll?.ScrollReference == null || NoDynamicScroll.Contains(ActiveScroll.ScrollReference)) return; diff --git a/Assets/StreamingAssets/StreamToPersistentDataPath/scrolls.json b/Assets/StreamingAssets/StreamToPersistentDataPath/scrolls.json index 544f6e91..759335b8 100644 --- a/Assets/StreamingAssets/StreamToPersistentDataPath/scrolls.json +++ b/Assets/StreamingAssets/StreamToPersistentDataPath/scrolls.json @@ -39250,5 +39250,1702 @@ "kind": "veq" } ] + }, + { + "ref": "http://mathhub.info/FrameIT/frameworld?RiverScroll", + "label": "RiverScroll", + "description": "River ", + "requiredFacts": [ + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_abs" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "kind": "FUNTYPE" + }, + "df": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "val", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + } + ], + "body": { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?IfThenElseX?ifthenelsex", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?leq_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "type": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "value": 0.0, + "kind": "OMLIT<Double>" + }, + { + "name": "val", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "name": "val", + "kind": "VAR" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "name": "val", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + } + }, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_height" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "kind": "FUNTYPE" + }, + "df": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "g", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "d", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "c", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + } + ], + "body": { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_abs", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "g", + "kind": "VAR" + }, + { + "name": "d", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "g", + "kind": "VAR" + }, + { + "name": "c", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "g", + "kind": "VAR" + }, + { + "name": "g", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + } + }, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_ground_distance" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "kind": "FUNTYPE" + }, + "df": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "g", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "d", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "c", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + } + ], + "body": { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "d", + "kind": "VAR" + }, + { + "name": "c", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "d", + "kind": "VAR" + }, + { + "name": "c", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_height", + "kind": "OMS" + }, + "arguments": [ + { + "name": "g", + "kind": "VAR" + }, + { + "name": "d", + "kind": "VAR" + }, + { + "name": "c", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_height", + "kind": "OMS" + }, + "arguments": [ + { + "name": "g", + "kind": "VAR" + }, + { + "name": "d", + "kind": "VAR" + }, + { + "name": "c", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + } + }, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_abs_v" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "kind": "FUNTYPE" + }, + "df": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "g", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + }, + { + "name": "d", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + }, + { + "name": "h", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + }, + { + "name": "alpha", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + } + ], + "body": { + "applicant": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "const", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + } + ], + "body": { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "name": "const", + "kind": "VAR" + }, + { + "name": "const", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "type": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "value": 2.0, + "kind": "OMLIT<Double>" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "name": "const", + "kind": "VAR" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?Trigonometry?sin", + "kind": "OMS" + }, + "arguments": [ + { + "name": "alpha", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "name": "g", + "kind": "VAR" + }, + { + "name": "h", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + } + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "name": "d", + "kind": "VAR" + }, + { + "name": "g", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?Trigonometry?cos", + "kind": "OMS" + }, + "arguments": [ + { + "name": "alpha", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + } + }, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_v" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "kind": "FUNTYPE" + }, + "df": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "c", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "a", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "vabs", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + } + ], + "body": { + "applicant": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "const", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + } + } + ], + "body": { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?vec_multI", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vabs", + "kind": "VAR" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "const", + "kind": "VAR" + }, + { + "name": "const", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "name": "const", + "kind": "VAR" + } + ], + "kind": "OMA" + } + } + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "c", + "kind": "VAR" + }, + { + "name": "a", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + } + }, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A" + }, + "label": "A", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?B" + }, + "label": "B", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C" + }, + "label": "C", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?D" + }, + "label": "D", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G" + }, + "label": "G", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?angleA" + }, + "label": "∠BAC", + "lhs": { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?B", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + "valueTp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "value": null, + "proof": null, + "kind": "veq" + } + ], + "acquiredFacts": [ + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Solution?v" + }, + "label": "<no label>", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Tuple", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_abs_v", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_ground_distance", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?D", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_height", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?D", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Projl", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?angleA", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_abs_v", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_ground_distance", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?D", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_height", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?D", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Projl", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?angleA", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_abs_v", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_ground_distance", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?D", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_height", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?D", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Projl", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?angleA", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + "kind": "general" + } + ] } ] \ No newline at end of file diff --git a/Assets/StreamingAssets/scrolls.json b/Assets/StreamingAssets/scrolls.json index 544f6e91..759335b8 100644 --- a/Assets/StreamingAssets/scrolls.json +++ b/Assets/StreamingAssets/scrolls.json @@ -39250,5 +39250,1702 @@ "kind": "veq" } ] + }, + { + "ref": "http://mathhub.info/FrameIT/frameworld?RiverScroll", + "label": "RiverScroll", + "description": "River ", + "requiredFacts": [ + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_abs" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "kind": "FUNTYPE" + }, + "df": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "val", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + } + ], + "body": { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?IfThenElseX?ifthenelsex", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?leq_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "type": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "value": 0.0, + "kind": "OMLIT<Double>" + }, + { + "name": "val", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "name": "val", + "kind": "VAR" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "name": "val", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + } + }, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_height" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "kind": "FUNTYPE" + }, + "df": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "g", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "d", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "c", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + } + ], + "body": { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_abs", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "g", + "kind": "VAR" + }, + { + "name": "d", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "g", + "kind": "VAR" + }, + { + "name": "c", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "g", + "kind": "VAR" + }, + { + "name": "g", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + } + }, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_ground_distance" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "kind": "FUNTYPE" + }, + "df": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "g", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "d", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "c", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + } + ], + "body": { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "d", + "kind": "VAR" + }, + { + "name": "c", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "d", + "kind": "VAR" + }, + { + "name": "c", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_height", + "kind": "OMS" + }, + "arguments": [ + { + "name": "g", + "kind": "VAR" + }, + { + "name": "d", + "kind": "VAR" + }, + { + "name": "c", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_height", + "kind": "OMS" + }, + "arguments": [ + { + "name": "g", + "kind": "VAR" + }, + { + "name": "d", + "kind": "VAR" + }, + { + "name": "c", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + } + }, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_abs_v" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "kind": "FUNTYPE" + }, + "df": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "g", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + }, + { + "name": "d", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + }, + { + "name": "h", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + }, + { + "name": "alpha", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + } + ], + "body": { + "applicant": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "const", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + } + ], + "body": { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "name": "const", + "kind": "VAR" + }, + { + "name": "const", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "type": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "value": 2.0, + "kind": "OMLIT<Double>" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "name": "const", + "kind": "VAR" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?Trigonometry?sin", + "kind": "OMS" + }, + "arguments": [ + { + "name": "alpha", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "name": "g", + "kind": "VAR" + }, + { + "name": "h", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + } + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "name": "d", + "kind": "VAR" + }, + { + "name": "g", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?Trigonometry?cos", + "kind": "OMS" + }, + "arguments": [ + { + "name": "alpha", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + } + }, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_v" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "kind": "FUNTYPE" + }, + "df": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "c", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "a", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "vabs", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + } + ], + "body": { + "applicant": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "const", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + } + } + ], + "body": { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?vec_multI", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vabs", + "kind": "VAR" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "const", + "kind": "VAR" + }, + { + "name": "const", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "name": "const", + "kind": "VAR" + } + ], + "kind": "OMA" + } + } + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "c", + "kind": "VAR" + }, + { + "name": "a", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + } + }, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A" + }, + "label": "A", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?B" + }, + "label": "B", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C" + }, + "label": "C", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?D" + }, + "label": "D", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G" + }, + "label": "G", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?angleA" + }, + "label": "∠BAC", + "lhs": { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?B", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + "valueTp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "value": null, + "proof": null, + "kind": "veq" + } + ], + "acquiredFacts": [ + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Solution?v" + }, + "label": "<no label>", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Tuple", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_abs_v", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_ground_distance", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?D", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_height", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?D", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Projl", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?angleA", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_abs_v", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_ground_distance", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?D", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_height", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?D", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Projl", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?angleA", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_abs_v", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_ground_distance", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?D", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/funcs?get_height", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?G", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?D", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Projl", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?angleA", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?scalar_productI", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?C", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?RiverScroll/Problem?A", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + "kind": "general" + } + ] } ] \ No newline at end of file -- GitLab