PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: lshort mem 4 1 1 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;LShort(v)) mem_f(St;s;v)
9. eq(u,s)
10. u = s mem_f(St;s;LShort(v))

u = s mem_f(St;s;v)
By:
Analyze -1
THEN
ProveProp
Generated subgoals:

None

About:
orequaluniverselistfunction
boolallimpliesassertapply