---

abbr34(f;1b) ==
  Collect(f + 1 vs's from 1b  with maximum fst(snd(vs)) such that tt
           return <fst(snd(vs)),n,vs> with n = maximum case snd(snd(vs))
          of inl(p) => fst(p)
           | inr(x) => -1)

---

Definitions :  natural_number: $n,  minus: -n,  pi1: fst(t),  pi2: snd(t),  decide: case b of inl(x) => s[x] | inr(y) => t[y],  btrue: tt,  add: n + m,  es-collect-filter-max: es-collect-filter-max
FDL editor aliases :  abbr34

---

abbr34(f;1b)  ==
    Collect(f  +  1  vs's  from  1b    with  maximum  fst(snd(vs))  such  that  tt
                      return  <fst(snd(vs)),n,vs>  with  n  =  maximum  case  snd(snd(vs))
                    of  inl(p)  =>  fst(p)
                      |  inr(x)  =>  -1)


Date html generated: 2010_08_28-PM-01_41_42
Last ObjectModification: 2010_08_06-PM-01_34_01

Home Index