Nuprl Lemma : decidable__cs-inning-committable

[V:Type]
  ((∀v,v':V.  Dec(v v' ∈ V))
   (∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List. ∀s:ConsensusState. ∀i:ℤ. ∀v:V.
        Dec(in state s, inning could commit )))


Proof




Definitions occuring in Statement :  cs-inning-committable: in state s, inning could commit  consensus-state4: ConsensusState Id: Id l_member: (x ∈ l) list: List decidable: Dec(P) uall: [x:A]. B[x] all: x:A. B[x] implies:  Q set: {x:A| B[x]}  int: universe: Type equal: t ∈ T
Lemmas :  decidable_functionality exists_wf l_member_wf all_wf or_wf cs-archived_wf cs-not-completed_wf l_exists_wf l_exists_iff decidable__l_exists_better-extract decidable__all-list decidable__equal_Id decidable__implies decidable__l_member decidable__equal_set set_wf decidable__or decidable__cs-archived decidable__cs-not-completed consensus-state4_wf list_wf Id_wf decidable_wf equal_wf
\mforall{}[V:Type]
    ((\mforall{}v,v':V.    Dec(v  =  v'))
    {}\mRightarrow{}  (\mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.  \mforall{}s:ConsensusState.  \mforall{}i:\mBbbZ{}.  \mforall{}v:V.
                Dec(in  state  s,  inning  i  could  commit  v  )))



Date html generated: 2015_07_17-AM-11_28_21
Last ObjectModification: 2015_01_28-AM-01_36_16

Home Index