Nuprl Definition : min_w_unit_l_tree
min_w_unit_l_tree(u1;u2;f) ==
case u1 of inl(val1) => case u2 of inl(val2) => inl min_w_ord(val1;val2;f) | inr(unitval2) => u1 | inr(unitval1) => u2
Definitions occuring in Statement :
min_w_ord: min_w_ord(t1;t2;f),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inl: inl x
FDL editor aliases :
min_w_unit_l_tree
Latex:
min\_w\_unit\_l\_tree(u1;u2;f) ==
case u1
of inl(val1) =>
case u2 of inl(val2) => inl min\_w\_ord(val1;val2;f) | inr(unitval2) => u1
| inr(unitval1) =>
u2
Date html generated:
2018_05_22-PM-09_39_49
Last ObjectModification:
2012_06_23-AM-09_00_28
Theory : labeled!trees
Home
Index