---

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

{ 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: ,  uall: [x:A]. B[x],  all: x:A. B[x],  exists: x:A. B[x],  iff: P  Q,  not: A,  implies: P  Q,  or: P  Q,  and: P  Q,  apply: f a,  function: x:A  B[x],  product: x:A  B[x],  universe: Type,  list_accum: list_accum(x,a.f[x; a];y;l)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  iff: P  Q,  assert: b,  or: P  Q,  and: P  Q,  exists: x:A. B[x],  implies: P  Q,  rev_implies: P  Q,  member: t  T,  cand: A c B,  prop: ,  so_lambda: x y.t[x; y],  guard: {T},  top: Top,  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  es-E-interface: E(X),  uimplies: b supposing a,  let: let,  so_apply: x[s1;s2],  sq_type: SQType(T),  subtype: S  T
Lemmas :  is-threshold2,  es-locl_wf,  not_wf,  assert_wf,  list_accum_wf,  es-prior-interval-vals_wf,  eclass-val_wf,  es-E_wf,  event-ordering+_inc,  es-threshold_wf,  es-prior-interface-vals_wf,  es-E-interface_wf,  es-interface-subtype_rel2,  event-ordering+_wf,  top_wf,  in-eclass_wf,  implies-is-threshold,  subtype_base_sq,  bool_subtype_base,  bool_wf,  eclass_wf,  assert_elim

---

\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{}  Threshold(init;f;test;nxt;X)
                        \mLeftarrow{}{}\mRightarrow{}  ((\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{}  (\muparrow{}(test  list\_accum(s,v.f  s  v;nxt  Threshold(init;f;test;nxt;X)(e');X(e',  e)) 
                                                  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{}  (\muparrow{}(test  list\_accum(s,v.f  s  v;init;X(<e))  X(e)))))


Date html generated: 2011_08_16-PM-05_13_08
Last ObjectModification: 2011_06_20-AM-01_14_15

Home Index