Nuprl Definition : num-eq-constraints
num-eq-constraints(p) == case p of inl(q) => ||fst(q)|| | inr(_) => 0
Definitions occuring in Statement :
length: ||as||,
pi1: fst(t),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
natural_number: $n
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
length: ||as||,
pi1: fst(t),
natural_number: $n
FDL editor aliases :
num-eq-constraints
Latex:
num-eq-constraints(p) == case p of inl(q) => ||fst(q)|| | inr($_{}$) => 0
Date html generated:
2016_05_14-AM-07_17_31
Last ObjectModification:
2015_09_22-PM-05_53_43
Theory : omega
Home
Index