Nuprl Definition : bl-rev-exists
(∃x∈rev(L).P[x])_b == rec-case(L) of [] => ff | a::as => r.case r of inl(x) => tt | inr(x) => P[a]
Definitions occuring in Statement :
list_ind: list_ind,
bfalse: ff,
btrue: tt,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
list_ind: list_ind,
bfalse: ff,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
btrue: tt
FDL editor aliases :
bl-rev-exists
Latex:
(\mexists{}x\mmember{}rev(L).P[x])\_b == rec-case(L) of [] => ff | a::as => r.case r of inl(x) => tt | inr(x) => P[a]
Date html generated:
2016_05_15-PM-03_48_51
Last ObjectModification:
2015_09_23-AM-07_45_05
Theory : general
Home
Index