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*

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

By: SplitOnConclITE

Generated subgoals:

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

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

About:

1	8. `eq(s,sx)` `(mem_f(St;sx;v \ s) False) mem_f(St;sx;if eq(s,u) v \ s else u.(v \ s) fi) False`
2	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)`