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

At: closed rel args 1 1 2 1 2
1. r: rel()
2. l: Term List
3. u: Term
4. v: Term List
5. i:. reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil i < ||v|| term_free_vars(v[i]) = nil
6. i:
7. term_free_vars(u) = nil
8. reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil
9. i < ||v||+1
10. i = 0

term_free_vars([u / v][i]) = nil
By: RWW "select_cons_tl" 0
Generated subgoal:

1 term_free_vars(v[(i-1)]) = nil

About:
listconsnilintnatural_numberadd
subtractless_thanlambdaequalimpliesall

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