x
(a(x));
p 
val(p);
p
q val(p) val(q);
p
q val(p) val(q);
p
q val(p) val(q); )
(F)
| def | valuation | (F under a)
== (letrec val f = case f:
x (a(x));
p val(p);
pq val(p) val(q);
pq val(p) val(q);
pq val(p) val(q); )
(F) |