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

At: member rel primed vars 1
1. x: Label
2. name: relname()
3. r1: Term List
4. (x nil)

i:. i < 0 & (x term_primed_vars(nil[i]))
By:
Unfold `l_member` -1
THEN
ExRepD
THEN
All Reduce
Generated subgoals:

None

About:
listnilnatural_numberless_thanexists

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