(12steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

At: member rel vars 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_vars(t) @ vs;nil;v)) (i:. i < ||v|| & (x term_vars(v[i])))
7. (x term_vars(u))

i:. i < ||v||+1 & (x term_vars([u / v][i]))
By:
(InstConcl [0]) THENA (Auto THEN (Reduce 0))
THEN
Analyze 0
Generated subgoal:

18. 0 < ||v||+1
(x term_vars([u / v][0]))

About:
listconsnilnatural_numberaddless_thanlambdaimpliesexists

(12steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc