PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
mem
select
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.
u = t
mem_f(T;t;v)
i:
(||v||+1). (u.v)[i] = t
By:
Analyze -1
Generated subgoals:
1
7.
u = t
i:
(||v||+1). (u.v)[i] = t
2
7.
mem_f(T;t;v)
i:
(||v||+1). (u.v)[i] = t
About:
i:
(||v||+1). (u.v)[i] = t i:(||v||+1). (u.v)[i] = t
(i:||v||. v[i] = t)
mem_f(T;t;v) i:(||v||+1). (u.v)[i] = t i:(||v||+1). (u.v)[i] = t i:(||v||+1). (u.v)[i] = t
