Nuprl Lemma : decidable__cs-committed-change

`∀[V:Type]`
`  ((∃v,v':V. (¬(v = v' ∈ V)))`
`  `` (∀v,v':V.  Dec(v = v' ∈ V))`
`  `` (∀L:V List. Dec(∃v:V. (¬(v ∈ L))))`
`  `` (∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List.`
`        (one-intersection(A;W)`
`        `` (∀i:ℤ. ∀x,y:ConsensusState.`
`              Dec(∃v:V. (in state x, inning i could commit v  ∧ (¬in state y, inning i could commit v )))))))`

Proof

Definitions occuring in Statement :  one-intersection: `one-intersection(A;W)` cs-inning-committable: `in state s, inning i could commit v ` consensus-state4: `ConsensusState` Id: `Id` l_member: `(x ∈ l)` list: `T List` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Lemmas :  cs-inning-committable-some2 consensus-state4_wf one-intersection_wf list_wf Id_wf l_member_wf all_wf decidable_wf exists_wf not_wf equal_wf cs-inning-committable_wf l_exists_iff cs-not-completed_wf set_wf decidable__l_exists_better-extract decidable__cand decidable__cs-inning-committable decidable__not decidable__all-list decidable__equal_Id decidable__implies_better decidable__l_member decidable__equal_set decidable__cs-not-completed decidable_functionality or_wf l_exists_wf iff_wf
\mforall{}[V:Type]
((\mexists{}v,v':V.  (\mneg{}(v  =  v')))
{}\mRightarrow{}  (\mforall{}v,v':V.    Dec(v  =  v'))
{}\mRightarrow{}  (\mforall{}L:V  List.  Dec(\mexists{}v:V.  (\mneg{}(v  \mmember{}  L))))
{}\mRightarrow{}  (\mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.
(one-intersection(A;W)
{}\mRightarrow{}  (\mforall{}i:\mBbbZ{}.  \mforall{}x,y:ConsensusState.
Dec(\mexists{}v:V
(in  state  x,  inning  i  could  commit  v
\mwedge{}  (\mneg{}in  state  y,  inning  i  could  commit  v  )))))))

Date html generated: 2015_07_17-AM-11_35_39
Last ObjectModification: 2015_07_16-AM-10_14_52

Home Index