1#lang racket
2(require redex)
3
4(define-language grammar
5  (B t
6     f
7     (B * B)))
8
9(define r
10  (reduction-relation
11   grammar
12   (--> (f * B_1) B_1 false) ; [a]
13   (--> (t * B_1) t true))) ; [b]
14
15(define ->r (compatible-closure r grammar B))
16
17(traces ->r '((f * f) * (t * f)))
18