---

Step * of Lemma int_consensus_accum_wf

∀[n:ℤ]
  (int_consensus_accum(n) ∈ (𝔹 × ℤ × Id List × ℤ List × ℤ) ─→ (ℤ + (Id × ℤ × ℤ)) ─→ (𝔹 × ℤ × Id List × ℤ List × ℤ))
BY
{ ((RepeatFor 2 (ProveWfLemma) THEN Reduce 0)
   THEN (RepeatFor 4 (D -2) THEN D -1)
   THEN Reduce 0
   THEN Auto
   THEN (RepeatFor 2 (D -1) THEN Reduce 0)
   THEN Auto) }

---

Latex:


\mforall{}[n:\mBbbZ{}]
    (int\_consensus\_accum(n)  \mmember{}  (\mBbbB{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Id  List  \mtimes{}  \mBbbZ{}  List  \mtimes{}  \mBbbZ{})
      {}\mrightarrow{}  (\mBbbZ{}  +  (Id  \mtimes{}  \mBbbZ{}  \mtimes{}  \mBbbZ{}))
      {}\mrightarrow{}  (\mBbbB{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Id  List  \mtimes{}  \mBbbZ{}  List  \mtimes{}  \mBbbZ{}))


By

((RepeatFor  2  (ProveWfLemma)  THEN  Reduce  0)
  THEN  (RepeatFor  4  (D  -2)  THEN  D  -1)
  THEN  Reduce  0
  THEN  Auto
  THEN  (RepeatFor  2  (D  -1)  THEN  Reduce  0)
  THEN  Auto)

---

Home Index