---

Step * of Lemma three-cs-no-repeated-votes

∀V:Type. ∀A:Id List. ∀t:ℕ+. ∀f:(V List) ─→ V. ∀s:ts-reachable(three-consensus-ts(V;A;t;f)). ∀a:{a:Id| (a ∈ A)} .
  no_repeats(consensus-rcv(V;A);filter(λx.rcv-vote?(x);s a))
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN (BLemma `ts-reachable-induction`
         THENA (Auto THEN DVar `s' THEN AllHyps h.(RepUR ``ts-type three-consensus-ts`` h THEN Auto) )
         )
   ) }

1
1. V : Type@i'
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ─→ V@i
⊢ ∀s:ts-reachable(three-consensus-ts(V;A;t;f))
    SqStable(∀a:{a:Id| (a ∈ A)} . no_repeats(consensus-rcv(V;A);filter(λx.rcv-vote?(x);s a)))

2
1. V : Type@i'
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ─→ V@i
⊢ ∀a:{a:Id| (a ∈ A)} . no_repeats(consensus-rcv(V;A);filter(λx.rcv-vote?(x);ts-init(three-consensus-ts(V;A;t;f)) a))

3
1. V : Type@i'
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ─→ V@i
⊢ ∀s,y:ts-reachable(three-consensus-ts(V;A;t;f)).
    ((∀a:{a:Id| (a ∈ A)} . no_repeats(consensus-rcv(V;A);filter(λx.rcv-vote?(x);s a)))
    ⇒ (s ts-rel(three-consensus-ts(V;A;t;f)) y)
    ⇒ (∀a:{a:Id| (a ∈ A)} . no_repeats(consensus-rcv(V;A);filter(λx.rcv-vote?(x);y a))))

---

Latex:


\mforall{}V:Type.  \mforall{}A:Id  List.  \mforall{}t:\mBbbN{}\msupplus{}.  \mforall{}f:(V  List)  {}\mrightarrow{}  V.  \mforall{}s:ts-reachable(three-consensus-ts(V;A;t;f)).
\mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .
    no\_repeats(consensus-rcv(V;A);filter(\mlambda{}x.rcv-vote?(x);s  a))


By

(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  (BLemma  `ts-reachable-induction`
              THENA  (Auto  THEN  DVar  `s'  THEN  AllHyps  h.(RepUR  ``ts-type  three-consensus-ts``  h  THEN  Auto)  )
              )
  )

---

Home Index