(13steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc

At: member rel primed vars 2 2 1
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))
7. i:
8. i < ||v||
9. (x term_primed_vars(v[i]))

i+1 < ||v||+1 & (x term_primed_vars([u / v][(i+1)]))
By: Analyze 0
Generated subgoal:

110. i+1 < ||v||+1
(x term_primed_vars([u / v][(i+1)]))

About:
listconsnilnatural_numberaddless_thanlambda

(13steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc