list 3 jlc Sections Support(jlc) Doc

Def remove(eq;x;L) == (letrec remove eq x L = (Case of L; nil nil ; h.t if eq(x,h) t else h.remove(eq,x,t) fi) ) (eq,x,L)

is mentioned by

Thm* eq:{T}, u:T, L:T List, v:T. v(eq) remove(eq;u;L) v(eq) L[remove_is_member_lemma]
Thm* eq:{T=}, x,y:T, L:T List. x(eq) L eq(x,y) x(eq) remove(eq;y;L)[not_is_member_remove_lemma]
Thm* eq:{T=}, L:T List, x:T. x(eq) L (M,N:T List. L = (M @ (x.N)) & remove(eq;x;L) = (M @ N))[is_member_remove_lemma]
Thm* eq:{T}, x,y:T, L:T List. x(eq) remove(eq;y;L) x(eq) L[remove_is_member]


list 3 jlc Sections Support(jlc) Doc