(6steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

At: rel primed vars rel vars 1 2
1. name: relname()
2. r1: Term List
3. x: Label
4. u: Term
5. v: Term List
6. (x reduce(t,vs. term_primed_vars(t) @ vs;nil;v)) (x reduce(t,vs. term_vars(t) @ vs;nil;v))

(x term_primed_vars(u) @ reduce(t,vs. term_primed_vars(t) @ vs;nil;v)) (x term_vars(u) @ reduce(t,vs. term_vars(t) @ vs;nil;v))
By: RWO "member_append" 0
Generated subgoal:

17. (x term_primed_vars(u)) (x reduce(t,vs. term_primed_vars(t) @ vs;nil;v))
(x term_vars(u)) (x reduce(t,vs. term_vars(t) @ vs;nil;v))

About:
listnillambdaimpliesor

(6steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc