Nuprl Definition : sd_ordered

sd_ordered(as) ==  sd_ordered,as. case as of [] => tt a::bs => before(a;bs) ∧b (sd_ordered bs) esac) as

Definitions occuring in Statement :  before: before(u;ps) list_ind: list_ind band: p ∧b q btrue: tt ycomb: Y apply: a lambda: λx.A[x]
Definitions occuring in definition :  ycomb: Y lambda: λx.A[x] list_ind: list_ind btrue: tt band: p ∧b q before: before(u;ps) apply: a

sd\_ordered(as)  ==
    Y  (\mlambda{}sd$_{ordered}$,as.  case  as  of  []  =>  tt  |  a::bs  =>  before(a;bs)  \mwedge{}\msubb{}  (sd$\000C_{ordered}$  bs)  esac)  as

Date html generated: 2016_05_16-AM-08_15_00
Last ObjectModification: 2015_09_23-AM-09_52_48

Theory : polynom_2

Home Index