PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
mem
select
1
2
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
(u.v)[(i+1)] = t
By:
Unfold `select` 0
THEN
RecUnfold `nth_tl` 0
THEN
SplitOnConclITE
Generated subgoal:
1
10.
0 < i+1
hd(nth_tl(i+1-1;tl((u.v)))) = t
About:
hd(nth_tl(i+1-1;tl((u.v)))) = t
(
i:
||v||. v[i] = t)||v|| (u.v)[(i+1)] = t hd(nth_tl(i+1-1;tl((u.v)))) = t
