PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: lshort mem 2
1. St: Type
2. l: St*
3. eq: StSt
4. x,y:St. eq(x,y) x = y
5. s: St
6. u: St
7. v: St*
8. mem_f(St;s;v) mem_f(St;s;LShort(v))

mem_f(St;s;u.v) mem_f(St;s;LShort((u.v)))
By:
RecUnfold `mem_f` 0
THEN
RecUnfold `lshort` 0
THEN
Reduce 0
Generated subgoal:

1 u = s mem_f(St;s;v) u = s mem_f(St;s;LShort(v) \ u)

About:
impliesconsuniverselistfunctionbool
allassertapplyequalor