Nuprl - Pf lshort

PrintForm Definitions list 3 autom Sections AutomataTheory Doc

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))

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

By: Analyze 0 THEN Analyze -1

Generated subgoals:

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

2 9. mem_f(St;s;v)
u = s mem_f(St;s;LShort(v) \ u)

About:

1	9. `u = s` `u = s mem_f(St;s;LShort(v) \ u)`
2	9. `mem_f(St;s;v)` `u = s mem_f(St;s;LShort(v) \ u)`