Nuprl - Pf lremove

PrintForm Definitions list 3 autom Sections AutomataTheory Doc

1. St: Type
2. l: St*
3. s: St
4. eq: StSt
5. sx: St
6. u: St
7. v: St*
8. mem_f(St;sx;v \ s) if eq(s,sx) False else mem_f(St;sx;v) fi

mem_f(St;sx;(u.v) \ s) if eq(s,sx) False else mem_f(St;sx;u.v) fi

By: MoveToConcl -1 THEN SplitOnConclITE THEN Analyze 0

Generated subgoals:

1 8. eq(s,sx)
9. mem_f(St;sx;v \ s) False
mem_f(St;sx;(u.v) \ s) False

2 8. eq(s,sx)
9. mem_f(St;sx;v \ s) mem_f(St;sx;v)
mem_f(St;sx;(u.v) \ s) mem_f(St;sx;u.v)

About:

1	8. `eq(s,sx)` 9. `mem_f(St;sx;v \ s) False` `mem_f(St;sx;(u.v) \ s) False`
2	8. `eq(s,sx)` 9. `mem_f(St;sx;v \ s) mem_f(St;sx;v)` `mem_f(St;sx;(u.v) \ s) mem_f(St;sx;u.v)`