At:
member rel vars4
1.
x: Label
2.
name: relname()
3.
r1: Term List
4.
u: Term
5.
v: Term List
6.
(i:. i < ||v|| & (x term_vars(v[i]))) (x reduce(t,vs. term_vars(t) @ vs;nil;v))
7.
i:
8.
i < ||v||+1
i < ||[u / v]||
By:
Reduce 0
Generated subgoals: