x:Label, r:rel(). (x rel_primed_vars(r)) (i:. i < ||r.args|| & (x term_primed_vars(r.args[i])))

1	1. x: Label 2. name: relname() 3. r1: Term List 4. (x nil) i:. i < 0 & (x term_primed_vars(nil[i]))
2	1. x: Label 2. name: relname() 3. r1: Term List 4. u: Term 5. v: Term List 6. (x reduce(t,vs. term_primed_vars(t) @ vs;nil;v)) (i:. i < ||v|| & (x term_primed_vars(v[i]))) 7. (x term_primed_vars(u) @ reduce(t,vs. term_primed_vars(t) @ vs;nil;v)) i:. i < ||v||+1 & (x term_primed_vars([u / v][i]))
3	1. x: Label 2. name: relname() 3. r1: Term List 4. u: Term 5. v: Term List 6. (i:. i < ||v|| & (x term_primed_vars(v[i]))) (x reduce(t,vs. term_primed_vars(t) @ vs;nil;v)) 7. i: 8. i < ||v||+1 9. (x term_primed_vars([u / v][i])) (x term_primed_vars(u) @ reduce(t,vs. term_primed_vars(t) @ vs;nil;v))
4	1. x: Label 2. name: relname() 3. r1: Term List 4. u: Term 5. v: Term List 6. (i:. i < ||v|| & (x term_primed_vars(v[i]))) (x reduce(t,vs. term_primed_vars(t) @ vs;nil;v)) 7. i: 8. i < ||v||+1 i < ||[u / v]||

About: