Nuprl Definition : bpermr

as ≡b bs ==  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: 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: a remove1: as a

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