Nuprl Lemma : cs-inning-committable-some2

[V:Type]
  ((v,v':V. ((v = v')))
   (v,v':V.  Dec(v = v'))
   (A:Id List. W:{a:Id| (a  A)}  List List.
        (one-intersection(A;W)
         (s:ConsensusState. i:.
              L:V List
               v:V
                 (in state s, inning i could commit v 
                  (in state s, inning i could commit v   (v  L))
                      (wsW. a:{a:Id| (a  A)} . ((a  ws)  in state s, a has not completed inning i)))))))


Proof not projected



Definitions occuring in Statement :  one-intersection: one-intersection(A;W),  cs-inning-committable: in state s, inning i could commit v ,  cs-not-completed: in state s, a has not completed inning i,  consensus-state4: ConsensusState,  Id: Id,  decidable: Dec(P),  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,  set: {x:A| B[x]} ,  list: type List,  int: ,  universe: Type,  equal: s = t,  l_exists: (xL. P[x]),  l_member: (x  l)
Definitions :  uall: [x:A]. B[x],  implies: P  Q,  all: x:A. B[x],  member: t  T,  prop: ,  so_lambda: x.t[x],  true: True,  consensus-state4: ConsensusState,  exists: x:A. B[x],  iff: P  Q,  or: P  Q,  and: P  Q,  l_exists: (xL. P[x]),  rev_implies: P  Q,  cand: A c B,  guard: {T},  cs-inning-committable: in state s, inning i could commit v ,  squash: T,  subtype: S  T,  so_apply: x[s],  uiff: uiff(P;Q),  uimplies: b supposing a,  decidable: Dec(P),  false: False,  not: A,  cs-archived: by state s, a archived v in inning i,  sq_stable: SqStable(P),  fpf-domain: fpf-domain(f)
Lemmas :  consensus-state4_wf,  one-intersection_wf,  Id_wf,  l_member_wf,  all_wf,  decidable_wf,  equal_wf,  exists_wf,  not_wf,  fpf-ap_wf,  assert_wf,  subtype-top,  subtype-fpf2,  subtype_rel_simple_product,  subtype_rel_self,  fpf_wf,  subtype_rel_function,  top_wf,  cs-estimate_wf,  int-deq_wf,  fpf-dom_wf,  list-subtype,  mapfilter_wf,  decidable__cand,  cs-inning-committable_wf,  decidable__cs-inning-committable,  decidable__l_member,  l_exists_wf,  cs-not-completed_wf,  or_wf,  iff_wf,  cs-archived_wf,  member-mapfilter,  subtype_top,  strong-subtype-self,  subtype-fpf3,  subtype_rel_dep_function,  member-fpf-dom,  decidable__equal_Id,  sq_stable_from_decidable,  decidable__cs-archived,  property-from-l_member
\mforall{}[V:Type]
    ((\mexists{}v,v':V.  (\mneg{}(v  =  v')))
    {}\mRightarrow{}  (\mforall{}v,v':V.    Dec(v  =  v'))
    {}\mRightarrow{}  (\mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.
                (one-intersection(A;W)
                {}\mRightarrow{}  (\mforall{}s:ConsensusState.  \mforall{}i:\mBbbZ{}.
                            \mexists{}L:V  List
                              \mforall{}v:V
                                  (in  state  s,  inning  i  could  commit  v 
                                  \mLeftarrow{}{}\mRightarrow{}  (in  state  s,  inning  i  could  commit  v    \mwedge{}  (v  \mmember{}  L))
                                          \mvee{}  (\mexists{}ws\mmember{}W.  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\} 
                                                                  ((a  \mmember{}  ws)  {}\mRightarrow{}  in  state  s,  a  has  not  completed  inning  i)))))))


Date html generated: 2012_01_23-PM-12_04_06
Last ObjectModification: 2011_12_17-PM-04_28_46

Home Index