12. (term_free_vars(u) @ reduce(
t,vs. term_free_vars(t) @ vs;nil;v)) = nil
list_accum(x,t.x
([[t]] 1of(e) s s' a1 tr);X
([[u]] 1of(e) s s' a1 tr);v) ~ list_accum(x,t.x
(...);...;v)
X:Top.
reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil 
(list_accum(x,t.x([[t]] 1of(e) s s' a1 tr);X;v) ~ list_accum(x,t.x([[t]] 1of(e) s s' a2 tr);X;v)) X:Top.
(term_free_vars(u) @ reduce(t,vs. term_free_vars(t) @ vs;nil;v)) = nil
...| 1 | 11. X: Top 12. (term_free_vars(u) @ reduce( t,vs. term_free_vars(t) @ vs;nil;v)) = nil list_accum(x,t.x
([[t]] 1of(e) s s' a1 tr);X
([[u]] 1of(e) s s' a1 tr);v) ~ list_accum(x,t.x
(...);...;v) |
About:
 |  |  |  |  |  |  |  |  |