Nuprl Definition : bpermr
as ≡b bs == Y (λbpermr,as,bs. case as of [] => null(bs) | a::as' => (a ∈b bs) ∧b (bpermr as' (bs \ a)) esac) as bs
Definitions occuring in Statement :
remove1: as \ a,
mem: a ∈b as,
null: null(as),
list_ind: list_ind,
band: p ∧b q,
ycomb: Y,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
ycomb: Y,
lambda: λx.A[x],
list_ind: list_ind,
null: null(as),
band: p ∧b q,
mem: a ∈b as,
apply: f a,
remove1: as \ a
Latex:
as \mequiv{}\msubb{} bs ==
Y (\mlambda{}bpermr,as,bs. case as of [] => null(bs) | a::as' => (a \mmember{}\msubb{} bs) \mwedge{}\msubb{} (bpermr as' (bs \mbackslash{} a)) esac) a\000Cs bs
Date html generated:
2016_05_16-AM-07_39_06
Last ObjectModification:
2015_09_23-AM-09_51_37
Theory : list_2
Home
Index