PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: mem select 1 1 2

1. T: Type
2. L: T*
3. t: T
4. u: T
5. v: T*
6. mem_f(T;t;v) (i:||v||. v[i] = t)
7. u = t
8. i: (||v||+1)

i < ||u.v||

By: Reduce 0

Generated subgoals:

None


About:
less_thanconsuniverselistimplies
existsnatural_numberequaladd