PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: mem select 1 2 1 1 1

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. 0 < i+1

hd(nth_tl(i+1-1;tl((u.v)))) = t

By:
Fold `select` 0
THEN
Reduce 0
THEN
ArithSimp 0


Generated subgoals:

None


About:
equalsubtractaddnatural_numbercons
universelistimpliesexistsless_than