### Nuprl Lemma : consensus-ts4-ref-map1

`∀[V:Type]`
`  ((∃v,v':V. (¬(v = v' ∈ V)))`
`  `` (∀v,v':V.  Dec(v = v' ∈ V))`
`  `` (∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List.`
`        (two-intersection(A;W)`
`        `` {∀s:ConsensusState. ∀i:ℤ.`
`              ∃x:consensus-state3(V)`
`               ((x = INITIAL ∈ consensus-state3(V)`
`                `⇐⇒` ∃v,v':V`
`                     ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v  ∧ in state s, inning i could commit v' ))`
`               ∧ (x = WITHDRAWN ∈ consensus-state3(V) `⇐⇒` ¬(∃v:V. in state s, inning i could commit v ))`
`               ∧ (∀v:V`
`                    ((x = COMMITED[v] ∈ consensus-state3(V) `⇐⇒` in state s, inning i has committed v)`
`                    ∧ (x = CONSIDERING[v] ∈ consensus-state3(V)`
`                      `⇐⇒` in state s, inning i could commit v `
`                          ∧ (¬in state s, inning i has committed v)`
`                          ∧ (∀v':V. (in state s, inning i could commit v'  `` (v' = v ∈ V)))))))})))`

Proof

Definitions occuring in Statement :  two-intersection: `two-intersection(A;W)` cs-inning-committable: `in state s, inning i could commit v ` cs-inning-committed: `in state s, inning i has committed v` consensus-state4: `ConsensusState` cs-commited: `COMMITED[v]` cs-considering: `CONSIDERING[v]` cs-withdrawn: `WITHDRAWN` cs-initial: `INITIAL` consensus-state3: `consensus-state3(T)` Id: `Id` l_member: `(x ∈ l)` list: `T List` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` guard: `{T}` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` not: `¬A` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Lemmas :  l_member_wf Id_wf select_wf list_wf sq_stable__le int_seg_wf length_wf two-intersection_wf all_wf decidable_wf equal_wf exists_wf not_wf decidable__cs-inning-two-committable decidable__cs-inning-committed decidable__cs-inning-committable-some consensus-state4_wf consensus-state3-unequal cs-commited_wf equal-wf-T-base consensus-state3_wf cs-inning-committable_wf cs-inning-committed_wf cs-considering_wf iff_wf cs-inning-committed-single and_wf equal-wf-base-T equal-wf-base cs-initial_wf btrue_neq_bfalse bool_wf isl_wf bfalse_wf btrue_wf assert_wf outl_wf cs-withdrawn_wf cs-archived_wf or_wf set_wf cs-not-completed_wf
\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.
(two-intersection(A;W)
{}\mRightarrow{}  \{\mforall{}s:ConsensusState.  \mforall{}i:\mBbbZ{}.
\mexists{}x:consensus-state3(V)
((x  =  INITIAL
\mLeftarrow{}{}\mRightarrow{}  \mexists{}v,v':V
((\mneg{}(v  =  v'))
\mwedge{}  in  state  s,  inning  i  could  commit  v
\mwedge{}  in  state  s,  inning  i  could  commit  v'  ))
\mwedge{}  (x  =  WITHDRAWN  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(\mexists{}v:V.  in  state  s,  inning  i  could  commit  v  ))
\mwedge{}  (\mforall{}v:V
((x  =  COMMITED[v]  \mLeftarrow{}{}\mRightarrow{}  in  state  s,  inning  i  has  committed  v)
\mwedge{}  (x  =  CONSIDERING[v]
\mLeftarrow{}{}\mRightarrow{}  in  state  s,  inning  i  could  commit  v
\mwedge{}  (\mneg{}in  state  s,  inning  i  has  committed  v)
\mwedge{}  (\mforall{}v':V.  (in  state  s,  inning  i  could  commit  v'    {}\mRightarrow{}  (v'  =  v)))))))\})))

Date html generated: 2015_07_17-AM-11_32_03
Last ObjectModification: 2015_07_16-AM-09_48_02

Home Index