Nuprl Lemma : cs-ref-map-equal

[V:Type]. ∀[A:Id List]. ∀[W:{a:Id| (a ∈ A)}  List List]. ∀[f:ConsensusState ─→ (consensus-state3(V) List)].
  ∀[x,y:ConsensusState]. ∀[i:ℕ||f x||].
    (f x[i] y[i] ∈ consensus-state3(V)) supposing 
       ((∀v:V
           ((in state x, inning could commit v  ⇐⇒ in state y, inning could commit )
           ∧ (in state x, inning has committed ⇐⇒ in state y, inning has committed v))) and 
       i < ||f y||) 
  supposing cs-ref-map-constraints(V;A;W;f)


Proof




Definitions occuring in Statement :  cs-ref-map-constraints: cs-ref-map-constraints(V;A;W;f) cs-inning-committable: in state s, inning could commit  cs-inning-committed: in state s, inning has committed v consensus-state4: ConsensusState consensus-state3: consensus-state3(T) Id: Id l_member: (x ∈ l) select: L[n] length: ||as|| list: List int_seg: {i..j-} less_than: a < b uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q set: {x:A| B[x]}  apply: a function: x:A ─→ B[x] natural_number: $n universe: Type equal: t ∈ T
Lemmas :  cs-inning-committable_wf cs-inning-committed_wf int_seg_subtype-nat length_wf consensus-state3_wf false_wf all_wf iff_wf less_than_wf int_seg_wf consensus-state4_wf cs-ref-map-constraints_wf list_wf Id_wf l_member_wf exists_wf not_wf equal_wf equal-wf-T-base select_wf sq_stable__le cs-commited_wf cs-considering_wf consensus-state3-cases iff_weakening_equal
\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[W:\{a:Id|  (a  \mmember{}  A)\}    List  List].
\mforall{}[f:ConsensusState  {}\mrightarrow{}  (consensus-state3(V)  List)].
    \mforall{}[x,y:ConsensusState].  \mforall{}[i:\mBbbN{}||f  x||].
        (f  x[i]  =  f  y[i])  supposing 
              ((\mforall{}v:V
                      ((in  state  x,  inning  i  could  commit  v    \mLeftarrow{}{}\mRightarrow{}  in  state  y,  inning  i  could  commit  v  )
                      \mwedge{}  (in  state  x,  inning  i  has  committed  v  \mLeftarrow{}{}\mRightarrow{}  in  state  y,  inning  i  has  committed  v)))  and 
              i  <  ||f  y||) 
    supposing  cs-ref-map-constraints(V;A;W;f)



Date html generated: 2015_07_17-AM-11_32_18
Last ObjectModification: 2015_02_04-PM-04_59_53

Home Index