At:
rel mentions iff
1
2
2
1
1.
r: rel()
2.
x: Label
3.
l: 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:
. i < ||v|| & (x
term_vars(v[i]))) 
(x
reduce(
t,vs. term_vars(t) @ vs;nil;v))
8.
(x
term_vars(u))
i:
. i < ||v||+1 & (x
term_vars([u / v][i]))
By:
InstConcl [0]
THEN
Reduce 0
THEN
Reduce 0
Generated subgoals:
None
About: