PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: mem select 1 2 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. mem_f(T;t;v)
8. i: ||v||
9. v[i] = t
10. i1: (||v||+1)

i1 < ||u.v||

By: Reduce 0

Generated subgoals:

None


About:
less_thanconsuniverselistimplies
existsnatural_numberequaladd