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 of inl(x) => s[x] inr(y) => t[y] inl: inl x
FDL editor aliases :  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



Date html generated: 2015_07_17-AM-07_41_45
Last ObjectModification: 2012_06_23-AM-09_00_26

Home Index