Nuprl Definition : deq-sub-bag
deq-sub-bag(eq;as;bs) ==
case TERMOF{decidable__sub-bag:o, 1:l, 1:l} deq-witness(eq) as bs of inl(x) => tt | inr(x) => ff
Definitions occuring in Statement :
deq-witness: deq-witness(eq),
bfalse: ff,
btrue: tt,
apply: f a,
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],
apply: f a,
deq-witness: deq-witness(eq),
btrue: tt,
bfalse: ff
TermOfs occuring in Definition :
decidable__sub-bag
FDL editor aliases :
deq-sub-bag
Latex:
deq-sub-bag(eq;as;bs) ==
case TERMOF\{decidable\_\_sub-bag:o, 1:l, 1:l\} deq-witness(eq) as bs of inl(x) => tt | inr(x) => ff
Date html generated:
2016_05_15-PM-08_09_08
Last ObjectModification:
2015_09_23-AM-08_20_57
Theory : bags_2
Home
Index