Nuprl Definition : strict-majority-or-first

strict-majority-or-first(eq;L) ==  case strict-majority(eq;L) of inl(x) => x | inr(z) => hd(L)


Definitions occuring in Statement :  strict-majority: strict-majority(eq;L),  hd: hd(l),  decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :  decide: case b of inl(x) => s[x] | inr(y) => t[y],  strict-majority: strict-majority(eq;L),  hd: hd(l)
FDL editor aliases :  strict-majority-or-first
Latex:
strict-majority-or-first(eq;L)  ==    case  strict-majority(eq;L)  of  inl(x)  =>  x  |  inr(z)  =>  hd(L)


Date html generated: 2016_05_14-PM-03_23_48
Last ObjectModification: 2015_09_22-PM-05_59_30

Theory : decidable!equality


Home Index