Nuprl Lemma : es-threshold-val

[Info:Type]. [es:EO+(Info)]. [A:Type]. [X:EClass(A)]. [S:Type]. [init:S]. [f:S  A  S]. [test:S  A  ].
[nxt:S  A  S]. [e:E].
  Threshold(init;f;test;nxt;X)(e)
  = <if e  prior(Threshold(init;f;test;nxt;X))
     then let e' = prior(Threshold(init;f;test;nxt;X))(e) in
              list_accum(s,v.f s v;nxt Threshold(init;f;test;nxt;X)(e');X(e', e))
     else list_accum(s,v.f s v;init;X(<e))
     fi 
    , X(e)
    > 
  supposing e  Threshold(init;f;test;nxt;X)


Proof not projected

Error : references
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[S:Type].  \mforall{}[init:S].  \mforall{}[f:S  {}\mrightarrow{}  A  {}\mrightarrow{}  S].
\mforall{}[test:S  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[nxt:S  \mtimes{}  A  {}\mrightarrow{}  S].  \mforall{}[e:E].
    Threshold(init;f;test;nxt;X)(e)
    =  <if  e  \mmember{}\msubb{}  prior(Threshold(init;f;test;nxt;X))
          then  let  e'  =  prior(Threshold(init;f;test;nxt;X))(e)  in
                            list\_accum(s,v.f  s  v;nxt  Threshold(init;f;test;nxt;X)(e');X(e',  e))
          else  list\_accum(s,v.f  s  v;init;X(<e))
          fi 
        ,  X(e)
        > 
    supposing  \muparrow{}e  \mmember{}\msubb{}  Threshold(init;f;test;nxt;X)


Date html generated: 2012_02_20-PM-07_50_47
Last ObjectModification: 2010_11_10-PM-09_28_41

Home Index