Add #:satisfying to redex-check.

This adds the ability to generate terms satisfying
judgment-forms and metafunctions to redex-check.

pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl

@@ -1837,8 +1837,13 @@ repeating as necessary. The optional keyword argument @racket[retries-expr]
 @racket[exn:fail:redex:generation-failure?].
 }
 
-@defform/subs[(redex-check language @#,ttpattern property-expr kw-arg ...)
+@defform/subs[(redex-check template property-expr kw-arg ...)
-              ([kw-arg (code:line #:attempts attempts-expr)
+              ([template (code:line language @#,ttpattern)
+                         (code:line language #:satisfying
+                            (judgment-form-id @#,ttpattern ...))
+                         (code:line language #:satisfying 
+                            (metafunction-id @#,ttpattern ...) = @#,ttpattern)]
+              [kw-arg (code:line #:attempts attempts-expr)
                        (code:line #:source metafunction)
                        (code:line #:source relation-expr)
                        (code:line #:retries retries-expr)
@@ -1854,11 +1859,24 @@ repeating as necessary. The optional keyword argument @racket[retries-expr]
                            [prepare-expr (-> any/c any/c)])]{
 Searches for a counterexample to @racket[property-expr], interpreted
 as a predicate universally quantified over the pattern variables
-bound by @racket[pattern]. @racket[redex-check] constructs and tests 
+bound by the @racket[pattern](s) in @racket[template].
-a candidate counterexample by choosing a random term @math{t} that 
+@racket[redex-check] constructs and tests 
-matches @racket[pattern] then evaluating @racket[property-expr]
+a candidate counterexample by choosing a random term @math{t} based 
+on @racket[template] and then evaluating @racket[property-expr]
 using the @racket[match-bindings] produced by @racket[match]ing
-@math{t} against @racket[pattern].
+@math{t} against @racket[pattern]. The form of @racket[template] controls
+how @math{t} is generated:
+@itemlist[
+          @item{@racket[language @#,ttpattern]:
+                 In this case, redex-check generates terms that match
+                 @racket[pattern].}
+          @item{@racket[language #:satisfying (judgment-form-id @#,ttpattern ...)]:
+                  Generates terms that match @racket[pattern] and satisfy 
+                  the judgment form.}
+          @item{@racket[language #:satisfying (metafunction-id @#,ttpattern ...) = @#,ttpattern]:
+                  Generates terms matching the two @racket[pattern]s, such that
+                  if the first is the argument to the metafunction, the
+                  second will be the result.}]
 
 @racket[redex-check] generates at most @racket[attempts-expr] (default @racket[(default-check-attempts)])
 random terms in its search. The size and complexity of these terms tend to increase 
@@ -1882,14 +1900,19 @@ generated example before @racket[redex-check] checks @racket[property-expr].
 This keyword may be useful when @racket[property-expr] takes the form
 of a conditional, and a term chosen freely from the grammar is unlikely to
 satisfy the conditional's hypothesis. In some such cases, the @racket[prepare] 
-keyword  can be used to increase the probability that an example satifies the
+keyword  can be used to increase the probability that an example satisfies the
 hypothesis.
 
+The @racket[#:retries] keyword behaves identically as in @racket[generate-term],
+controlling the number of times the generation of any pattern will be
+reattempted. It can't be used together with @racket[#:satisfying].
+
 When passed a metafunction or reduction relation via the optional @racket[#:source]
 argument, @racket[redex-check] distributes its attempts across the left-hand sides
 of that metafunction/relation by using those patterns, rather than @racket[pattern],
 as the basis of its generation. It is an error if any left-hand side generates a
-term that does not match @racket[pattern].}
+term that does not match @racket[pattern]. @racket[#:source] cannot be used
+with @racket[#:satisfying].}
 
 @examples[
 #:eval redex-eval
@@ -1939,7 +1962,28 @@ term that does not match @racket[pattern].}
         #:prepare (λ (n)
                     (printf "preparing ~s; " n)
                     (add1 (abs n)))
-        #:attempts 3)]
+        #:attempts 3)
+                     
+       (define-language L
+         (nat ::= Z (S nat)))
+       (define-judgment-form L
+         #:mode (sum I I O)
+         [---------------
+          (sum Z nat nat)]
+         [(sum nat_1 nat_2 nat_3)
+          -------------------------------
+          (sum (S nat_1) nat_2 (S nat_3))])
+       (redex-check L
+                    #:satisfying
+                    (sum nat_1 nat_2 nat_3)
+                    (equal? (judgment-holds
+                             (sum nat_1 nat_2 nat_4) nat_4)
+                            (term (nat_3)))
+                    #:attempts 100)
+       (redex-check L
+                    #:satisfying
+                    (sum nat_1 nat_2 nat_3)
+                    (equal? (term nat_1) (term nat_2)))]
 
 @defform/subs[(redex-generator language-id satisfying size-expr)
               ([satisfying (judgment-form-id @#,ttpattern ...)

pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt

@@ -15,6 +15,7 @@
          racket/match
          racket/pretty
          (for-syntax racket/base
+                     racket/set
                      syntax/stx
                      setup/path-to-relative
                      "rewrite-side-conditions.rkt"
@@ -82,38 +83,136 @@
         (list (if lists? #'(-> list? list?) #'(-> any/c any/c)) 
               "#:prepare argument")))
 
+(define-for-syntax satisfying-disallowed-kws
+  (set '#:source '#:retries))
+
 (define-syntax (redex-check stx)
-  (syntax-case stx ()
+  (define valid-kws 
-    [(form lang pat property . kw-args)
+    (cons '#:satisfying (map car (list attempts-keyword
-     (with-syntax ([(syncheck-exp pattern (name ...) (name/ellipses ...))
-                    (rewrite-side-conditions/check-errs 
-                     #'lang
-                     'redex-check #t #'pat)]
-                   [show (show-message stx)])
-     (let-values ([(attempts-stx source-stx retries-stx print?-stx size-stx fix-stx)
-                   (apply values
-                          (parse-kw-args (list attempts-keyword
                                        source-keyword
                                        retries-keyword
                                        print?-keyword
                                        attempt-size-keyword
-                                               (prepare-keyword #f))
+                                       (prepare-keyword #f)))))
-                                         (syntax kw-args)
+  (define used-kws
-                                         stx
+    (for/fold ([kws (set)])
-                                         (syntax-e #'form)))])
+              ([maybe-kw-stx (in-list (syntax->list stx))])
-         (with-syntax ([property (syntax
+      (define maybe-kw (syntax-e maybe-kw-stx))
-                                  (bind-prop
+      (cond 
+        [(keyword? maybe-kw)
+         (unless (member maybe-kw valid-kws)
+           (raise-syntax-error 'redex-check "unknown keyword" stx maybe-kw-stx))
+         (set-add kws maybe-kw)]
+        [else kws])))
+  (define bad-kws (set-intersect used-kws satisfying-disallowed-kws))
+  (syntax-case stx (=)
+    [(form lang #:satisfying (mf-id . args) = res property . kw-args)
+     (unless (set-empty? bad-kws)
+       (raise-syntax-error 'redex-check (format "~s cannot be used with #:satisfying" (car (set->list bad-kws))) stx))
+     (redex-check/mf stx #'form #'lang #'mf-id #'args #'res #'property #'kw-args)]
+    [(form lang #:satisfying (jform-id . pats) property . kw-args)
+     (unless (set-empty? bad-kws)
+       (raise-syntax-error 'redex-check (format "~s cannot be used with #:satisfying" (car (set->list bad-kws))) stx))
+     (redex-check/jf stx #'form #'lang #'jform-id #'pats #'property #'kw-args)]
+    [(form lang #:satisfying . rest)
+     (raise-syntax-error 'redex-check "#:satisfying expected judgment form or metafunction syntax followed by a property" stx #'rest)]
+    [(form lang pat property . kw-args)
+     (redex-check/pat stx #'form #'lang #'pat #'property #'kw-args)]))
+
+(define-struct gen-fail ())
+
+(define-for-syntax (redex-check/jf orig-stx form lang jf-id pats property kw-args)
+  (define-values (attempts-stx source-stx retries-stx print?-stx size-stx fix-stx)
+    (parse-redex-check-kw-args kw-args orig-stx form))
+  (define nts (definition-nts lang orig-stx 'redex-check))
+  (unless (judgment-form-id? jf-id)
+    (raise-syntax-error 'redex-check "expected a judgment-form" jf-id))
+  (define j-f (lookup-judgment-form-id jf-id))
+  (define clauses (judgment-form-gen-clauses j-f))
+  (define relation? (judgment-form-relation? j-f))
+  (define args-stx (if relation?
+                       (syntax/loc #'args #`(#,pats))
+                       pats))
+  (with-syntax* ([(syncheck-exp pattern (names ...) (names/ellipses ...))
+                  (rewrite-side-conditions/check-errs lang 'redex-check #t args-stx)]
+                 [show (show-message orig-stx)]
+                 [res-term-stx #`(#,jf-id #,@args-stx)]
+                 [property #`(bind-prop
+                               (λ (bindings)
+                                 (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
+                                           #,property)))])
+                (quasisyntax/loc orig-stx
+                  (let ([term-match (λ (generated)
+                                      (cond [(test-match #,lang res-term-stx generated) => values]
+                                            [else (redex-error 'redex-check "~s does not match ~s" generated 'res-term-stx)]))])
+                    syncheck-exp
+                    (let ([default-attempt-size (λ (s) (add1 (default-attempt-size s)))])
+                      (parameterize ([attempt->size #,size-stx])
+                        (check-one
+                         (λ (size _1 _2)
+                           (values
+                            (match ((make-jf-gen/proc '#,jf-id #,clauses #,lang 'pattern size))
+                              [(and res (? values)) res]
+                              [else (gen-fail)])
+                            #f))
+                         property #,attempts-stx 0 (and #,print?-stx show) #,fix-stx term-match)))))))
+
+(define-for-syntax (redex-check/mf orig-stx form lang mf-id args-stx res-stx property kw-args)
+  (define-values (attempts-stx source-stx retries-stx print?-stx size-stx fix-stx)
+    (parse-redex-check-kw-args kw-args orig-stx form))
+  (define nts (definition-nts lang orig-stx 'redex-check))
+  (define m (metafunc mf-id))
+  (unless m (raise-syntax-error 'generate-term "expected a metafuction" mf-id))
+  (define mf (syntax-local-value mf-id (λ () #f)))
+  (with-syntax* ([(lhs-syncheck-exp lhs-pat (lhs-names ...) (lhs-names/ellipses ...))
+                  (rewrite-side-conditions/check-errs lang 'redex-check #t args-stx)]
+                 [(rhs-syncheck-exp rhs-pat (rhs-names ...) (rhs-names/ellipses ...))
+                  (rewrite-side-conditions/check-errs lang 'redex-check #t res-stx)]
+                 [res-term-stx #`((#,mf-id #,@args-stx) = #,res-stx)]
+                 [mf-id (term-fn-get-id mf)]
+                 [show (show-message orig-stx)]
+                 [property #`(bind-prop
+                               (λ (bindings)
+                                 (term-let ([lhs-names/ellipses (lookup-binding bindings 'lhs-names)] ...
+                                            [rhs-names/ellipses (lookup-binding bindings 'rhs-names)] ...)
+                                           #,property)))])
+                (quasisyntax/loc orig-stx
+                  (let ([term-match (λ (generated)
+                                      (cond [(test-match #,lang res-term-stx generated) => values]
+                                            [else (redex-error 'redex-check "~s does not match ~s" generated 'res-term-stx)]))])
+                    lhs-syncheck-exp
+                    rhs-syncheck-exp
+                    (let ([default-attempt-size (λ (s) (add1 (default-attempt-size s)))])
+                      (parameterize ([attempt->size #,size-stx])
+                        (check-one
+                         (λ (size _1 _2)
+                           (values
+                            (match ((make-mf-gen/proc 'mf-id mf-id #,lang 'lhs-pat 'rhs-pat size))
+                              [(and res (? values)) res]
+                              [else (gen-fail)])
+                            #f))
+                         property #,attempts-stx 0 (and #,print?-stx show) #,fix-stx term-match)))))))
+
+(define-for-syntax (redex-check/pat orig-stx form lang pat property kw-args)
+  (with-syntax ([(syncheck-exp pattern (name ...) (name/ellipses ...))
+                 (rewrite-side-conditions/check-errs 
+                  lang
+                  'redex-check #t pat)]
+                [show (show-message orig-stx)])
+    (define-values (attempts-stx source-stx retries-stx print?-stx size-stx fix-stx)
+      (parse-redex-check-kw-args kw-args orig-stx form)) 
+    (with-syntax ([property #`(bind-prop
                                (λ (bindings)
                                  (term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
-                                               property))))])
+                                           #,property)))])
-           (quasisyntax/loc stx
+      (quasisyntax/loc orig-stx
         (let ([att #,attempts-stx]
               [ret #,retries-stx]
               [print? #,print?-stx]
               [fix #,fix-stx]
               [term-match (λ (generated)
-                                 (cond [(test-match lang pat generated) => values]
+                            (cond [(test-match #,lang #,pat generated) => values]
-                                       [else (redex-error 'redex-check "~s does not match ~s" generated 'pat)]))])
+                                  [else (redex-error 'redex-check "~s does not match ~s" generated '#,pat)]))])
           syncheck-exp
           (parameterize ([attempt->size #,size-stx])
             #,(if source-stx
@@ -122,10 +221,10 @@
                                            => (λ (x) #`(values #,x (length (metafunc-proc-cases #,x))))]
                                           [else
                                            #`(let ([r #,(apply-contract #'reduction-relation? source-stx 
-                                                                           "#:source argument" (syntax-e #'form))])
+                                                                        "#:source argument" (syntax-e form))])
                                                (values r (length (reduction-relation-make-procs r))))])])
                       (check-lhs-pats
-                          lang
+                       #,lang
                        metafunc/red-rel
                        property
                        (max 1 (floor (/ att num-cases)))
@@ -135,22 +234,36 @@
                        fix
                        #:term-match term-match))
                   #`(check-one
-                        #,(term-generator #'lang #'pattern 'redex-check)
+                     #,(term-generator lang #'pattern 'redex-check)
-                        property att ret (and print? show) fix (and fix term-match)))))))))]))
+                     property att ret (and print? show) fix (and fix term-match)))))))))
+
+(define-for-syntax (parse-redex-check-kw-args kw-args orig-stx form-name)
+  (apply values
+         (parse-kw-args (list attempts-keyword
+                              source-keyword
+                              retries-keyword
+                              print?-keyword
+                              attempt-size-keyword
+                              (prepare-keyword #f))
+                        kw-args
+                        orig-stx
+                        (syntax-e form-name))))
 
 (define (format-attempts a)
   (format "~a attempt~a" a (if (= 1 a) "" "s")))
 
 (define (check-one generator property attempts retries show term-fix term-match) 
-  (let ([c (check generator property attempts retries show 
+  (define c (check generator property attempts retries show 
                    #:term-fix term-fix
-                  #:term-match term-match)])
+                   #:term-match term-match))
-    (if (counterexample? c)
+  (cond 
-        (unless show c) ; check printed it
+    [(counterexample? c)
-        (if show
+     (unless show c)] ; check printed it
+    [show
      (show (format "no counterexamples in ~a\n"
-                          (format-attempts attempts)))
+                   (format-attempts attempts)))]
-            #t))))
+    [else
+     #t]))
 
 (define-struct (exn:fail:redex:test exn:fail:redex) (source term))
 (define-struct counterexample (term) #:transparent)
@@ -164,14 +277,20 @@
                #:term-match [term-match #f]
                #:skip-term? [skip-term? (λ (x) #f)])
   (let loop ([remaining attempts])
-    (if (zero? remaining)
+    (cond 
-        #t
+      [(zero? remaining)
-        (let ([attempt (add1 (- attempts remaining))])
+       #t]
-          (let-values ([(term bindings) (generator ((attempt->size) attempt) attempt retries)]
+      [else
-                       [(handler) 
+       (define attempt (add1 (- attempts remaining)))
+       (define-values (raw-term bindings) (generator ((attempt->size) attempt) attempt retries))
+       (cond
+         [(gen-fail? raw-term)
+          (loop (sub1 remaining))]
+         [else
+          (define handler 
             (λ (action term)
               (λ (exn)
-                            (let ([msg (format "~a ~s raises an exception" action term)])
+                (define msg (format "~a ~s raises an exception" action term))
                 (when show (show (format "~a\n" msg)))
                 (raise 
                  (if show
@@ -180,13 +299,12 @@
                       (format "~a:\n~a" msg (exn-message exn))
                       (current-continuation-marks)
                       exn
-                                    term))))))])
+                      term))))))
-            (let ([term (with-handlers ([exn:fail? (handler "fixing" term)])
+          (define term (with-handlers ([exn:fail? (handler "fixing" raw-term)])
-                          (if term-fix (term-fix term) term))])
+                         (if term-fix (term-fix raw-term) raw-term)))
           (cond
             [(skip-term? term) (loop (- remaining 1))]
-                [else
+            [(if term-match
-                 (if (if term-match
                  (let ([bindings (make-bindings 
                                   (match-bindings
                                    (pick-from-list (term-match term))))])
@@ -198,15 +316,15 @@
                    (match (cons property term-fix)
                      [(cons (term-prop pred) _) (pred term)]
                      [(cons (bind-prop pred) #f) (pred bindings)])))
-                     (loop (sub1 remaining))
+             (loop (sub1 remaining))]
-                     (begin
+            [else
              (when show
                (show
                 (format "counterexample found after ~a~a:\n"
                         (format-attempts attempt)
                         (if source (format " with ~a" source) "")))
                (pretty-write term (current-output-port)))
-                       (make-counterexample term)))])))))))
+             (make-counterexample term)])])])))
 
 (define (check-lhs-pats lang mf/rr prop attempts retries what show term-fix
                         #:term-match [term-match #f])

pkgs/redex-pkgs/redex-test/redex/tests/gen-test.rkt

@@ -15,6 +15,11 @@
 (define-syntax-rule (is-false e)
   (test e #f))
 
+(define-syntax-rule (no-counterexample e)
+  (test
+   (counterexample? e)
+   #f))
+
 (define-language L0)
 
 (let ()
@@ -87,7 +92,7 @@
   (test (generate-term nats #:satisfying (sum z z (s z)) 5)
               #f)
   
-  (for ([_ 100])
+  (for ([_ 50])
     (match (generate-term nats #:satisfying (sum n_1 n_2 n_3) 5)
       [`(sum ,l ,r ,res)
        (test (judgment-holds (sum ,l ,r n) n)
@@ -95,7 +100,26 @@
     (match (generate-term nats #:satisfying (r-sum n_1 n_2 n_3) 5)
       [`(r-sum ,l ,r ,res)
        (test (term (r-sum ,l ,r ,res))
-                   #t)])))
+                   #t)]))
+  (no-counterexample
+   (redex-check nats
+                #:satisfying
+                (sum n_1 n_2 n_3)
+                (equal? (car (judgment-holds
+                              (sum n_1 n_2 n_4) n_4))
+                        (term n_3))
+                #:attempts 50
+                #:print? #f))
+  
+  (no-counterexample
+   (redex-check nats
+                #:satisfying
+                (r-sum n_1 n_2 n_3)
+                (judgment-holds
+                 (sum n_1 n_2 n_3))
+                #:attempts 50
+                #:print? #f))
+  )
 
 (let ()
   
@@ -131,14 +155,24 @@
    (not (generate-term lists #:satisfying (not-in a (b (c (d (e (f ())))))) +inf.0))
    #f)
   
-  (for/and ([_ 100])
+  (for/and ([_ 50])
     (match (generate-term lists #:satisfying (not-in a l) 5)
       [`(not-in a ,l)
        (unless (judgment-holds (not-in a ,l)) (printf "l: ~s\n" l))
        (test (judgment-holds (not-in a ,l))
                    #t)]
       [#f
-       (void)])))
+       (void)]))
+  
+  (no-counterexample
+   (redex-check lists
+                #:satisfying
+                (not-in x l)
+                (judgment-holds (not-in x l))
+                #:attempts 50
+                #:print? #f))
+                
+  )
 
 (let ()
   
@@ -174,7 +208,7 @@
     [(double (+ e_1 e_2) e_3)
      (where e_3 (+ (+ e_1 e_1) (+ e_2 e_2)))])
   
-  (for ([_ 100])
+  (for ([_ 50])
     (define t (generate-term simple #:satisfying (double e_1 e_2) +inf.0))
     (match t
       [`(double ,e1 ,e2)
@@ -183,6 +217,15 @@
       [#f
        (void)]))
   
+  (no-counterexample
+   (redex-check simple
+                #:satisfying
+                (double e_1 e_2)
+                (judgment-holds
+                 (double e_1 e_2))
+                #:attempts 50
+                #:print? #f))
+  
   (define-metafunction simple
     [(duplicate e_1 e_1)
      (+ e_1 e_1 e_1)]
@@ -220,14 +263,25 @@
   (test (judgment-holds (double2 (+ 2 2) (+ 2 2 2)))
               #t)
   
-  (for ([_ 100])
+  (for ([_ 50])
     (define t (generate-term simple #:satisfying (double2 e_1 e_2) +inf.0))
     (match t
       [`(double2 ,e1 ,e2)
        (test (judgment-holds (double2 ,e1 ,e2))
                    #t)]
       [#f
-       (void)])))
+       (void)]))
+  
+  (no-counterexample
+   (redex-check simple
+                #:satisfying
+                (double2 e_1 e_2)
+                (judgment-holds 
+                 (double2 e_1 e_2))
+                #:attempts 50
+                #:print? #f))
+  
+  )
 
 (let ()
   (define-language STLC
@@ -283,7 +337,7 @@
   (test (judgment-holds (typeof ([x_2 int] ([x_1 (int → int)] •)) (x_1 5) int))
               #t)
   
-  (for ([_ 100])
+  (for ([_ 50])
     (define term (generate-term STLC #:satisfying (typeof Γ e τ) 6))
     (match term
       [`(typeof ,g ,e ,t)
@@ -292,7 +346,17 @@
       [#f
        (void)]))
   
-  (for ([_ 100])
+  (no-counterexample
+   (redex-check STLC
+                #:satisfying
+                (typeof Γ e τ)
+                (equal? (car (judgment-holds
+                              (typeof Γ e τ_2) τ_2))
+                        (term τ))
+                #:attempts 50
+                #:print? #f))
+  
+  (for ([_ 50])
     (define term (generate-term if-l #:satisfying (typ-if Γ e τ) 5))
     (match term
       [`(typ-if ,g ,e ,t)
@@ -301,8 +365,18 @@
       [#f
        (void)]))
   
+  (no-counterexample
+   (redex-check STLC
+                #:satisfying
+                (typ-if Γ e τ)
+                (equal? (car (judgment-holds
+                              (typ-if Γ e τ_2) τ_2))
+                        (term τ))
+                #:attempts 50
+                #:print? #f))
+  
   (define g (redex-generator STLC (typeof • e τ) 5))
-  (define terms (filter values (for/list ([_ 400]) (g))))
+  (define terms (filter values (for/list ([_ 100]) (g))))
   (test (length terms)
               (length (remove-duplicates terms)))
   (map (match-lambda
@@ -337,7 +411,7 @@
   (test (generate-term l #:satisfying (filtered (1 (2 (3 (4 •)))) 5 (1 (2 (4 •)))) +inf.0)
               #f)
   
-  (for ([_ 50])
+  (for ([_ 25])
     (define term (generate-term l #:satisfying (filtered e_1 n e_2) 5))
     (match term
       [`(filtered ,e1 ,n ,e2)
@@ -346,7 +420,17 @@
       [#f
        (void)]))
   
-  (for ([_ 50])
+  (no-counterexample
+   (redex-check l
+                #:satisfying
+                (filtered e_1 n e_2)
+                (equal? (car (judgment-holds
+                              (filtered e_1 n e_3) e_3))
+                        (term e_2))
+                #:attempts 25
+                #:print? #f))
+  
+  (for ([_ 25])
     (define t (generate-term l #:satisfying (fltr n e) = e_1 5))
     (match t
       [`((fltr ,n ,e) = ,e1)
@@ -354,6 +438,14 @@
       [#f
        (void)]))
   
+  (no-counterexample
+   (redex-check l 
+                #:satisfying 
+                (fltr n e) = e_1
+                (equal? (term (fltr n e)) (term e_1))
+                #:attempts 25
+                #:print? #f))
+  
   (define g (redex-generator l (fltr n e_1) = e_2 5))
   (define terms (filter values (for/list ([_ 50]) (g))))
   (test (length terms)
@@ -550,7 +642,17 @@
   (test (generate-term l #:satisfying (t 6 7) = 2 +inf.0)
               #f)
   (test (generate-term l #:satisfying (t 6 7) = 1 +inf.0)
-              #f))
+              #f)
+  
+  (no-counterexample
+   (redex-check l 
+                #:satisfying 
+                (t n_1 n_2) = n_3
+                (equal? (term (t n_1 n_2)) (term n_3))
+                #:attempts 50
+                #:print? #f))
+  
+  )
 
 (let ()
   (define-judgment-form L0