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