PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: lremove mem 1 2
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:
RecUnfold `lremove` 0
THEN
Reduce 0
THEN
MoveToConcl -1
Generated subgoal:

1 (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

About:
impliesconsifthenelseapplyfalseuniverse
listfunctionboolorequal