(module compatible-closure mzscheme
  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 4))
           (planet "gui.ss" ("robby" "redex.plt" 4)))
  
  (define-language grammar
    (B t
       f
       (B * B)))

  (define r
    (reduction-relation
     grammar
     (--> (f * B_1) B_1 false) ; [a]
     (--> (t * B_1) t true))) ; [b]

  (define ->r (compatible-closure r grammar B))
  
  (traces grammar ->r '((f * f) * (t * f))))