---

{ [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.
              ((e  X)
               (e':E(Threshold(init;f;test;nxt;X))
                  ((e' <loc e)
                   (e'':E(X)
                       ((e' <loc e'')
                        (e'' <loc e)
                        ((test 
                              list_accum(s,v.f s v;
                                         nxt Threshold(init;f;test;nxt;X)(e');
                                         X(e', e'')) 
                              X(e'')))))
                   let s = list_accum(s,v.f s v;
                                       nxt Threshold(init;f;test;nxt;X)(e');
                                       X(e', e)) in
                        ((test s X(e)))
                         (Threshold(init;f;test;nxt;X)(e) = <s, X(e)>))))
               ((e  X)
                 (e':E(X)
                     ((e' <loc e)
                      ((test list_accum(s,v.f s v;init;X(<e')) X(e')))))
                 let s = list_accum(s,v.f s v;init;X(<e)) in
                      ((test s X(e)))
                       (Threshold(init;f;test;nxt;X)(e) = <s, X(e)>)) 
              supposing e  Threshold(init;f;test;nxt;X) }

{ Proof }

---

Definitions occuring in Statement :  es-threshold: Threshold(init;f;test;nxt;X),  es-prior-interval-vals: X(e1, e2),  es-prior-interface-vals: X(<e),  es-E-interface: E(X),  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-locl: (e <loc e'),  es-E: E,  assert: b,  bool: ,  let: let,  uimplies: b supposing a,  uall: [x:A]. B[x],  all: x:A. B[x],  exists: x:A. B[x],  not: A,  implies: P  Q,  or: P  Q,  and: P  Q,  apply: f a,  function: x:A  B[x],  pair: <a, b>,  product: x:A  B[x],  universe: Type,  equal: s = t,  list_accum: list_accum(x,a.f[x; a];y;l)
Definitions :  assert: b,  member: t  T,  top: Top,  all: x:A. B[x],  so_lambda: x y.t[x; y],  or: P  Q,  and: P  Q,  exists: x:A. B[x],  es-E-interface: E(X),  implies: P  Q,  let: let,  ifthenelse: if b then t else f fi ,  prop: ,  cand: A c B,  btrue: tt,  guard: {T},  true: True,  uall: [x:A]. B[x],  uimplies: b supposing a,  so_apply: x[s1;s2],  iff: P  Q,  sq_type: SQType(T),  subtype: S  T
Lemmas :  in-eclass_wf,  es-threshold_wf,  es-interface-subtype_rel2,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  top_wf,  is-threshold,  es-threshold-cases,  assert_wf,  es-locl_wf,  es-E-interface_wf,  es-interface-top,  not_wf,  list_accum_wf,  es-prior-interval-vals_wf,  eclass-val_wf,  es-prior-interface-vals_wf,  subtype_base_sq,  bool_wf,  bool_subtype_base,  assert_elim,  eclass_wf

---

\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.
                        ((\muparrow{}e  \mmember{}\msubb{}  X)
                        \mwedge{}  (\mexists{}e':E(Threshold(init;f;test;nxt;X))
                                ((e'  <loc  e)
                                \mwedge{}  (\mforall{}e'':E(X)
                                          ((e'  <loc  e'')
                                          {}\mRightarrow{}  (e''  <loc  e)
                                          {}\mRightarrow{}  (\mneg{}\muparrow{}(test 
                                                        list\_accum(s,v.f  s  v;nxt  Threshold(init;f;test;nxt;X)(e');X(e',  e'')) 
                                                        X(e'')))))
                                \mwedge{}  let  s  =  list\_accum(s,v.f  s  v;nxt  Threshold(init;f;test;nxt;X)(e');X(e',  e))  in
                                            (\muparrow{}(test  s  X(e)))  \mwedge{}  (Threshold(init;f;test;nxt;X)(e)  =  <s,  X(e)>))))
                        \mvee{}  ((\muparrow{}e  \mmember{}\msubb{}  X)
                            \mwedge{}  (\mforall{}e':E(X).  ((e'  <loc  e)  {}\mRightarrow{}  (\mneg{}\muparrow{}(test  list\_accum(s,v.f  s  v;init;X(<e'))  X(e')))))
                            \mwedge{}  let  s  =  list\_accum(s,v.f  s  v;init;X(<e))  in
                                        (\muparrow{}(test  s  X(e)))  \mwedge{}  (Threshold(init;f;test;nxt;X)(e)  =  <s,  X(e)>)) 
                        supposing  \muparrow{}e  \mmember{}\msubb{}  Threshold(init;f;test;nxt;X)


Date html generated: 2011_08_16-PM-05_12_20
Last ObjectModification: 2011_06_20-AM-01_13_52

Home Index