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