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

At: closed rel args 1 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

i:. (term_free_vars(u) @ reduce(t,vs. term_free_vars(t) @ vs;nil;v)) = nil i < ||v||+1 term_free_vars([u / v][i]) = nil
By: (RWW "append_is_nil" 0) THENA (Auto THEN (Reduce 0))
Generated subgoal:

1 i:. term_free_vars(u) = nil & reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil i < ||v||+1 term_free_vars([u / v][i]) = nil

About:
listconsnilnatural_numberaddless_than
lambdaequalimpliesandall

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