Nuprl Lemma : filter-interface-predecessors-lower-bound2

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[T:Type]
      ∀X:EClass(T). ∀P:E(X) ─→ 𝔹.
        ∀[R:Id ─→ E(X) ─→ ℙ]
          ∀L:Id List
            ((∀x∈L.∃y:E(X). (R[x;y] ∧ (↑P[y])))
               ⇒ (∃e:{e:E(X)| ↑P[e]} . (||L|| ≤ ||filter(λe.P[e];≤(X)(e))||))) supposing 
               (0 < ||L|| and 
               no_repeats(Id;L)) 
          supposing ∀x1,x2:Id. ∀y:E(X).  (R[x1;y] ⇒ R[x2;y] ⇒ (x1 = x2 ∈ Id)) 
        supposing ∀e1,e2:E(X).  (loc(e1) = loc(e2) ∈ Id) supposing ((↑P[e2]) and (↑P[e1]))


Proof



Definitions occuring in Statement :  es-interface-predecessors: ≤(X)(e),  es-E-interface: E(X),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-loc: loc(e),  Id: Id,  l_all: (∀x∈L.P[x]),  no_repeats: no_repeats(T;l),  filter: filter(P;l),  length: ||as||,  list: T List,  assert: ↑b,  bool: 𝔹,  less_than: a < b,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  prop: ℙ,  so_apply: x[s1;s2],  so_apply: x[s],  le: A ≤ B,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q,  set: {x:A| B[x]} ,  lambda: λx.A[x],  function: x:A ─→ B[x],  natural_number: $n,  universe: Type,  equal: s = t ∈ T
Lemmas :  assert_wf,  es-E-interface_wf,  es-interface-subtype_rel2,  es-E_wf,  event-ordering+_subtype,  event-ordering+_wf,  top_wf,  Id_wf,  no_repeats_witness,  member-less_than,  length_wf,  l_all_exists_injection,  filter-interface-predecessors-lower-bound3,  less_than_wf,  int_seg_wf,  l_all_wf2,  l_member_wf,  exists_wf,  no_repeats_wf,  list_wf,  all_wf,  isect_wf,  equal_wf,  es-loc_wf,  bool_wf,  eclass_wf,  set_wf,  assert_elim,  subtype_base_sq,  bool_subtype_base
Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[T:Type]
            \mforall{}X:EClass(T).  \mforall{}P:E(X)  {}\mrightarrow{}  \mBbbB{}.
                \mforall{}[R:Id  {}\mrightarrow{}  E(X)  {}\mrightarrow{}  \mBbbP{}]
                    \mforall{}L:Id  List
                        ((\mforall{}x\mmember{}L.\mexists{}y:E(X).  (R[x;y]  \mwedge{}  (\muparrow{}P[y])))
                              {}\mRightarrow{}  (\mexists{}e:\{e:E(X)|  \muparrow{}P[e]\}  .  (||L||  \mleq{}  ||filter(\mlambda{}e.P[e];\mleq{}(X)(e))||)))  supposing 
                              (0  <  ||L||  and 
                              no\_repeats(Id;L)) 
                    supposing  \mforall{}x1,x2:Id.  \mforall{}y:E(X).    (R[x1;y]  {}\mRightarrow{}  R[x2;y]  {}\mRightarrow{}  (x1  =  x2)) 
                supposing  \mforall{}e1,e2:E(X).    (loc(e1)  =  loc(e2))  supposing  ((\muparrow{}P[e2])  and  (\muparrow{}P[e1]))


Date html generated: 2015_07_21-PM-03_40_49
Last ObjectModification: 2015_01_27-PM-06_28_46

Home Index