---

Step * of 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)
BY
{ ((Auto THEN (Assert i < ||f x|| BY Auto))
   THEN (Assert ∀v:V. (in state x, inning i could commit v  ⇐⇒ in state y, inning i could commit v ) BY
               Auto)
   THEN (Assert ∀v:V. (in state x, inning i has committed v ⇐⇒ in state y, inning i has committed v) BY
               Auto)
   THEN Thin (-4)
   THEN Unfold `cs-ref-map-constraints` 5
   THEN (InstHyp[⌈x⌉;⌈i⌉] 5⋅ THENA Auto)
   THEN Fold `cs-ref-map-constraints` 5
   THEN (RWO "-2 -3" (-1) THENA Auto)
   THEN (Unfold `cs-ref-map-constraints` 5 THEN (InstHyp[⌈y⌉;⌈i⌉] 5⋅ THENA Auto) THEN Fold `cs-ref-map-constraints` 5)
   THEN Auto
   THEN ThinTrivial
   THEN Auto
   THEN (InstLemma `consensus-state3-cases`[⌈V⌉;⌈f x[i]⌉]⋅ THENA Auto)
   THEN (SplitOrHyps THEN ExRepD THEN SplitOrHyps)
   THEN ThinTrivial
   THEN Auto
   THEN AllHyps h.(SimpleInstHyp ⌈v⌉ h⋅ THENA Complete (Auto)) 
   THEN Auto
   THEN RepeatFor 2 (ThinTrivial)
   THEN Auto) }

---

Latex:


\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)


By

((Auto  THEN  (Assert  i  <  ||f  x||  BY  Auto))
  THEN  (Assert  \mforall{}v:V
                                (in  state  x,  inning  i  could  commit  v    \mLeftarrow{}{}\mRightarrow{}  in  state  y,  inning  i  could  commit  v  )  BY
                          Auto)
  THEN  (Assert  \mforall{}v:V
                                (in  state  x,  inning  i  has  committed  v  \mLeftarrow{}{}\mRightarrow{}  in  state  y,  inning  i  has  committed  v)  BY
                          Auto)
  THEN  Thin  (-4)
  THEN  Unfold  `cs-ref-map-constraints`  5
  THEN  (InstHyp[\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  Fold  `cs-ref-map-constraints`  5
  THEN  (RWO  "-2  -3"  (-1)  THENA  Auto)
  THEN  (Unfold  `cs-ref-map-constraints`  5
              THEN  (InstHyp[\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
              THEN  Fold  `cs-ref-map-constraints`  5)
  THEN  Auto
  THEN  ThinTrivial
  THEN  Auto
  THEN  (InstLemma  `consensus-state3-cases`[\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}f  x[i]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (SplitOrHyps  THEN  ExRepD  THEN  SplitOrHyps)
  THEN  ThinTrivial
  THEN  Auto
  THEN  AllHyps  h.(SimpleInstHyp  \mkleeneopen{}v\mkleeneclose{}  h\mcdot{}  THENA  Complete  (Auto)) 
  THEN  Auto
  THEN  RepeatFor  2  (ThinTrivial)
  THEN  Auto)

---

Home Index