---

{ [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) 
    supposing ((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: ,  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],  product: x:A  B[x],  universe: Type,  list_accum: list_accum(x,a.f[x; a];y;l)
Definitions :  es-interface-at: X@i,  es-local-pred: last(P),  es-rec-class: es-rec-class,  es-interface-val: val(X,e),  intensional-universe: IType,  fpf: a:A fp-> B[a],  strong-subtype: strong-subtype(A;B),  list: type List,  le: A  B,  ge: i  j ,  less_than: a < b,  uiff: uiff(P;Q),  es-prior-interface-vals: X(<e),  false: False,  true: True,  guard: {T},  btrue: tt,  sq_type: SQType(T),  isl: isl(x),  can-apply: can-apply(f;x),  es-prior-interval-vals: X(e1, e2),  eclass-val: X(e),  list_accum: list_accum(x,a.f[x; a];y;l),  infix_ap: x f y,  es-causl: (e < e'),  set: {x:A| B[x]} ,  void: Void,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  in-eclass: e  X,  cand: A c B,  prop: ,  es-threshold: Threshold(init;f;test;nxt;X),  es-E-interface: E(X),  es-locl: (e <loc e'),  not: A,  implies: P  Q,  assert: b,  exists: x:A. B[x],  and: P  Q,  or: P  Q,  uimplies: b supposing a,  product: x:A  B[x],  bool: ,  union: left + right,  subtype: S  T,  subtype_rel: A r B,  atom: Atom,  apply: f a,  top: Top,  token: "$token",  ifthenelse: if b then t else f fi ,  record-select: r.x,  event_ordering: EO,  es-E: E,  lambda: x.A[x],  so_lambda: x y.t[x; y],  eclass: EClass(A[eo; e]),  dep-isect: Error :dep-isect,  eq_atom: x =a y,  eq_atom: eq_atom$n(x;y),  record+: record+,  all: x:A. B[x],  function: x:A  B[x],  isect: x:A. B[x],  uall: [x:A]. B[x],  universe: Type,  member: t  T,  event-ordering+: EO+(Info),  equal: s = t,  tactic: Error :tactic,  is_list_splitting: is_list_splitting(T;L;LL;L2;f),  is_accum_splitting: is_accum_splitting(T;A;L;LL;L2;f;g;x),  req: x = y,  rnonneg: rnonneg(r),  rleq: x  y,  i-member: r  I,  partitions: partitions(I;p),  modulus-of-ccontinuity: modulus-of-ccontinuity(omega;I;f),  fpf-sub: f  g,  squash: T,  sq_stable: SqStable(P),  tag-by: zT,  rev_implies: P  Q,  iff: P  Q,  record: record(x.T[x]),  fset: FSet{T},  isect2: T1  T2,  b-union: A  B,  fpf-cap: f(x)?z,  imax-class: (maximum f[v]  lb with v from X),  es-filter-image: f[X],  map-class: (f[v] where v from X),  es-loc: loc(e),  Id: Id,  pair: <a, b>,  null: null(as),  so_apply: x[s],  eq_knd: a = b,  l_member: (x  l),  fpf-dom: x  dom(f),  es-prior-interface: prior(X),  MaAuto: Error :MaAuto,  Complete: Error :Complete,  CollapseTHEN: Error :CollapseTHEN,  it: ,  ExRepD: Error :ExRepD,  D: Error :D,  RepeatFor: Error :RepeatFor
Lemmas :  implies-is-threshold1,  uiff_inversion,  member-interface-at,  es-interface-at_wf,  sq_stable__assert,  event-ordering+_inc,  subtype_rel_self,  es-E_wf,  es-locl_wf,  event-ordering+_wf,  top_wf,  subtype_rel_wf,  es-threshold_wf,  es-interface-subtype_rel2,  es-interface-top,  member_wf,  eclass_wf,  es-E-interface_wf,  in-eclass_wf,  assert_wf,  not_wf,  bool_wf,  es-prior-interval-vals_wf,  list_accum_wf,  eclass-val_wf,  subtype_base_sq,  bool_subtype_base,  assert_elim,  es-prior-interface-vals_wf,  false_wf,  ifthenelse_wf,  true_wf,  intensional-universe_wf,  assert_witness

---

\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) 
    supposing  ((\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_12_58
Last ObjectModification: 2011_06_20-AM-01_14_07

Home Index