Collect2 ==
Collect(x2 + 1 vs's from x1 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
Collect2 ==
Collect(x2 + 1 vs's from x1 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_30-AM-12_51_10
Last ObjectModification:
2010_08_16-PM-10_57_35
Home
Index