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