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

At: member rel vars 1

1. x: Label
2. name: relname()
3. r1: Term List
4. (x nil)

i:. i < 0 & (x term_vars(nil[i]))

By:
Unfold `l_member` -1
THEN
ExRepD
THEN
All Reduce


Generated subgoals:

None

About:
listnilnatural_numberless_thanexists

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