PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: lshort mem 4 1
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;LShort(v)) mem_f(St;s;v)

u = s mem_f(St;s;LShort(v) \ u) u = s mem_f(St;s;v)
By: RWH (LemmaC Thm* l:St*, s:St, eq:(StSt), sx:St. mem_f(St;sx;l \ s) if eq(s,sx) False else mem_f(St;sx;l) fi) 0
Generated subgoal:

1 u = s if eq(u,s) False else mem_f(St;s;LShort(v)) fi u = s mem_f(St;s;v)

About:
impliesorequaluniverselistfunction
boolallassertapplyifthenelsefalse