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

At: closed rel args 1 1 2 1 2 1
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(v[(i-1)]) = nil
By: BackThruSomeHyp
Generated subgoals:

None

About:
listnilintnatural_numberaddsubtractless_thanlambdaequalimpliesall

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