times work with no binding

sandbox/cert_f/rat.lp

@@ -11,10 +11,22 @@ symbol frac : Term nat ⇒ Term N.nznat ⇒ Term rat
 symbol times : @Term Type rat ⇒ @Term Type rat ⇒ @Term Type rat
 
 rule times (frac &a &b) (frac &c &d) →
-  let bv ≔ @fst nat N.not_zero &b in
-  let bpr ≔ @snd nat N.not_zero &b in
-  let dv ≔ @fst nat N.not_zero &d in
-  let dpr ≔ @snd nat N.not_zero &d in
   frac
    (N.times &a &c)
-   (N.nznatc (N.times bv dv) (N.prod_not_zero bv dv bpr dpr))
+   (N.nznatc
+    (N.times (fst N.not_zero &b) (fst N.not_zero &d))
+    (N.prod_not_zero
+     (fst N.not_zero &b)
+     (fst N.not_zero &d)
+     (snd N.not_zero &b)
+     (snd N.not_zero &d)))
+
+
+// rule times (frac &a &b) (frac &c &d) →
+//   let bv  ≔ @fst nat N.not_zero &b in
+//   let bpr ≔ @snd nat N.not_zero &b in
+//   let dv  ≔ @fst nat N.not_zero &d in
+//   let dpr ≔ @snd nat N.not_zero &d in
+//   frac
+//    (N.times &a &c)
+//    (N.nznatc (N.times bv dv) (N.prod_not_zero bv dv bpr dpr))