---

{ [S,A,B:Type]. [test:S  A  ]. [nxt:S  A  S]. [step:S  A  S].
  [g:S  A  (B?)].
    (threshold_accum(test;
     nxt;
     step;
     g)  S  (B?)  A  (S  (B?))) }

{ Proof }

---

Definitions occuring in Statement :  threshold_accum: threshold_accum,  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,  threshold_accum: threshold_accum,  bfalse: ff,  top: Top,  all: x:A. B[x],  subtype: S  T
Lemmas :  ifthenelse_wf,  pi1_wf_top,  unit_wf,  it_wf,  bool_wf

---

\mforall{}[S,A,B:Type].  \mforall{}[test:S  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[nxt:S  \mtimes{}  A  {}\mrightarrow{}  S].  \mforall{}[step:S  {}\mrightarrow{}  A  {}\mrightarrow{}  S].  \mforall{}[g:S  \mtimes{}  A  {}\mrightarrow{}  (B?)].
    (threshold\_accum(test;
      nxt;
      step;
      g)  \mmember{}  S  \mtimes{}  (B?)  {}\mrightarrow{}  A  {}\mrightarrow{}  (S  \mtimes{}  (B?)))


Date html generated: 2011_08_16-AM-11_03_15
Last ObjectModification: 2011_06_18-AM-09_36_37

Home Index