From c98251957b5d682a9fc1ec0d2651cd5d6d31c7b5 Mon Sep 17 00:00:00 2001
From: josd <josderoo@gmail.com>
Date: Mon, 11 Nov 2024 20:40:54 +0100
Subject: [PATCH] refreshing

---
 color/filter/filter-proof.n3 | 49 ++++++++----------------------------
 color/filter/filter-query.n3 | 10 ++------
 2 files changed, 13 insertions(+), 46 deletions(-)

diff --git a/color/filter/filter-proof.n3 b/color/filter/filter-proof.n3
index b8d043ff1..061856e95 100644
--- a/color/filter/filter-proof.n3
+++ b/color/filter/filter-proof.n3
@@ -18,55 +18,28 @@ skolem:lemma1 a r:Inference;
         :result :is ("Huey" "Dewey").
     };
     r:evidence (
-        skolem:lemma2
         [ a r:Fact; r:gives {(_:sk_0 {
             :Let :param _:sk_0.
             _:sk_0 string:lessThan "Louie".
         } ("Huey" "Dewey")) log:collectAllIn ((<https://eyereasoner.github.io/eye/color/filter/filter.n3>) 1)}]
         [ a r:Fact; r:gives {("Huey" "Dewey") list:length 2}]
     );
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ((<https://eyereasoner.github.io/eye/color/filter/filter.n3>) 1)];
     r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo {
-        :Let :param _:sk_0.
-        _:sk_0 string:lessThan "Louie".
-    }];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((<https://eyereasoner.github.io/eye/color/filter/filter.n3>) 1)];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo ("Huey" "Dewey")];
-    r:rule skolem:lemma3.
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo ("Huey" "Dewey")];
+    r:rule skolem:lemma2.
 
-skolem:lemma2 a r:Inference;
+skolem:lemma2 a r:Extraction;
     r:gives {
-        :Let :where (_:sk_0 {
-            :Let :param _:sk_0.
-            _:sk_0 string:lessThan "Louie".
-        }).
-    };
-    r:evidence (
-        [ a r:Fact; r:gives true]
-    );
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]];
-    r:rule skolem:lemma4.
-
-skolem:lemma3 a r:Extraction;
-    r:gives {
-        @forAll var:x_0, var:x_1, var:x_2, var:x_3. {
-            :Let :where (var:x_0 var:x_1).
-            (var:x_0 var:x_1 var:x_2) log:collectAllIn var:x_3.
-            var:x_2 list:length 2.
-        } => {
-            :result :is var:x_2.
-        }.
-    };
-    r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/filter/filter-query.n3>].
-
-skolem:lemma4 a r:Extraction;
-    r:gives {
-        @forSome var:x_0. {
-            :Let :where (var:x_0 {
+        @forAll var:x_0, var:x_1, var:x_2. {
+            (var:x_0 {
                 :Let :param var:x_0.
                 var:x_0 string:lessThan "Louie".
-            }).
-        } <= true.
+            } var:x_1) log:collectAllIn var:x_2.
+            var:x_1 list:length 2.
+        } => {
+            :result :is var:x_1.
+        }.
     };
     r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/color/filter/filter-query.n3>].
 
diff --git a/color/filter/filter-query.n3 b/color/filter/filter-query.n3
index 3966313ad..2456df69a 100644
--- a/color/filter/filter-query.n3
+++ b/color/filter/filter-query.n3
@@ -5,14 +5,8 @@
 
 # query
 {
-    :Let :where (?param ?where).
-    (?param ?where ?filteredParams) log:collectAllIn ?scope.
+    (?param { :Let :param ?param. ?param string:lessThan "Louie" } ?filteredParams) log:collectAllIn ?scope.
     ?filteredParams list:length 2.
-} =^ {
+} => {
     :result :is ?filteredParams.
 }.
-
-:Let :where (?param {
-    :Let :param ?param.
-    ?param string:lessThan "Louie".
-}).