(15steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

At: rel mentions iff 1 1 1
1. r: rel()
2. x: Label
3. l: Term List
4. (x nil)

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

None

About:
listnilnatural_numberless_thanexists

(15steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc