---

{ [A,B,S:Type]. [test:S  A  ]. [nxt:S  A  S]. [step:S  A  S].
  [b:S  A  (B?)]. [init:S].
    (ThresholdComb1(A;B;S;test;nxt;step;b;init)  CombinatorDef) }

{ Proof }

---

Definitions occuring in Statement :  ThresholdComb1: ThresholdComb1(A;B;S;test;nxt;step;b;init),  combinator-def: CombinatorDef,  bool: ,  uall: [x:A]. B[x],  unit: Unit,  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  union: left + right,  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  ThresholdComb1: ThresholdComb1(A;B;S;test;nxt;step;b;init)
Lemmas :  AccumComb_wf,  unit_wf,  it_wf,  threshold_accum_wf,  bool_wf

---

\mforall{}[A,B,S:Type].  \mforall{}[test:S  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[nxt:S  \mtimes{}  A  {}\mrightarrow{}  S].  \mforall{}[step:S  {}\mrightarrow{}  A  {}\mrightarrow{}  S].  \mforall{}[b:S  \mtimes{}  A  {}\mrightarrow{}  (B?)].
\mforall{}[init:S].
    (ThresholdComb1(A;B;S;test;nxt;step;b;init)  \mmember{}  CombinatorDef)


Date html generated: 2011_08_17-PM-06_30_16
Last ObjectModification: 2011_06_18-AM-11_52_43

Home Index