Nuprl Definition : sd_ordered
sd_ordered(as) == Y (λ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: f 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: f a
Latex:
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