PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: lremove mem 1 2 1 2
1. St: Type
2. l: St*
3. s: St
4. eq: StSt
5. sx: St
6. u: St
7. v: St*
8. eq(s,sx)

(mem_f(St;sx;v \ s) mem_f(St;sx;v)) mem_f(St;sx;if eq(s,u) v \ s else u.(v \ s) fi) u = sx mem_f(St;sx;v)
By:
Analyze 0
THEN
SplitOnConclITE
Generated subgoals:

19. mem_f(St;sx;v \ s) mem_f(St;sx;v)
10. eq(s,u)
mem_f(St;sx;v \ s) u = sx mem_f(St;sx;v)
29. mem_f(St;sx;v \ s) mem_f(St;sx;v)
10. eq(s,u)
mem_f(St;sx;u.(v \ s)) u = sx mem_f(St;sx;v)

About:
impliesifthenelseapplyconsorequal
universelistfunctionboolassert