### 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] = f y[i] ∈ consensus-state3(V)) supposing `
`       ((∀v:V`
`           ((in state x, inning i could commit v  `⇐⇒` in state y, inning i could commit v )`
`           ∧ (in state x, inning i has committed v `⇐⇒` in state y, inning i 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 i could commit v ` cs-inning-committed: `in state s, inning i has committed v` consensus-state4: `ConsensusState` consensus-state3: `consensus-state3(T)` Id: `Id` l_member: `(x ∈ l)` select: `L[n]` length: `||as||` list: `T List` int_seg: `{i..j-}` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ─→ B[x]` natural_number: `\$n` universe: `Type` equal: `s = 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