Nuprl Definition : mem_f
mem_f(T;a;bs) == Y (λmem_f,bs. case bs of [] => False | b::bs' => (b = a ∈ T) ∨ (mem_f bs') esac) bs
Definitions occuring in Statement :
list_ind: list_ind,
ycomb: Y,
or: P ∨ Q,
false: False,
apply: f a,
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
ycomb: Y,
lambda: λx.A[x],
list_ind: list_ind,
false: False,
or: P ∨ Q,
equal: s = t ∈ T,
apply: f a
Latex:
mem\_f(T;a;bs) == Y (\mlambda{}mem$_{f}$,bs. case bs of [] => False | b::bs' => (b = a) \mvee{}\000C (mem$_{f}$ bs') esac) bs
Date html generated:
2016_05_16-AM-07_34_57
Last ObjectModification:
2015_09_23-AM-09_51_28
Theory : list_2
Home
Index