blockVoted : (p  e  ls —[ mm ]→ ls′)  Maybe (Block × Chain)
blockVoted {e = e} = λ where
  (VoteBlock {H = H} {txs = txs} {ch = ch} _ _ _ _ _ _)  just ( H , e , txs  , ch)
  (ProposeBlock {ch = ch} {txs = txs} _ _ _ _)  just ( ch  , e , txs  , ch)
  _  nothing

≡[_▷_] : Pid  Block × Chain  LocalStepProperty
≡[ p  b , ch ] ((p′ , e′ , _)  st)
  = (p  p′)
  × (b .epoch  e′)
  × Any ((b , ch) ≡_) (blockVoted st)

HasVoted˘ : TraceProperty
HasVoted˘ tr@(s , _) =  {p b ch} 
  tr ∋⋯ ≡[ p  b , ch ]
  ──────────────────────────
  p  voteIds (s .history) b

hasVoted˘ : TraceInvariant HasVoted˘
hasVoted˘ (_ , refl , (_ )) ()
hasVoted˘ {s′} (_ , init , (_  st  s ⟩←— tr))
  {p}{b}{ch} st∈
  with IHhasVoted˘ (_ , init , tr)
  with st
... | Deliver _ = IH st∈
... | AdvanceEpoch = IH st∈
... | Drop _ = IH st∈
... | LocalStep {p = p′} ls→
  = QED
  where
  QED : p  voteIds (s′ .history) b
  QED with  ls→ |  st∈
  QED |  FinalizeBlock _ _ _ _ |  there st∈ = IH st∈
  QED |  RegisterVote _ _ |  there st∈ = IH st∈
  QED |  ProposeBlock {ch = ch↓} {txs = txs} _ refl _ (_  _  B↝)
      |  here (refl , refl , M.Any.just refl)
      = voteIds-here {m = M} refl refl
      where open ∣ProposeBlock∣ p′ s ch↓ txs
  QED |  ProposeBlock {ch = ch↓} {txs = txs} _ refl _ _
      |  there st∈
      = voteIds-there b $ IH st∈
  QED |  VoteBlock {H = H} {txs = txs} {ch = ch↓} _ _ _ _ _ _
      |  there st∈
      = ≪QED
    where
    open ∣VoteBlock∣ p′ s H txs

    ≪QED : p  voteIds (M  s .history) b
    ≪QED with b  B
    ... | no  _ = IH st∈
    ... | yes _ = there $ IH st∈
  QED |  VoteBlock {H = H} {txs = txs} _ _ _ _ _ _
      |  here (refl , refl , M.Any.just refl)
      = voteIds-here {m = M} refl refl
      where open ∣VoteBlock∣ p′ s H txs
... | DishonestLocalStep _ _
  = voteIds-there b $ IH st∈

HasVoted : TraceProperty
HasVoted tr@(s , _) =  {p b ch}  _ : Honest p  
   b -connects-to- ch
   p  voteIds (s .history) b
    ──────────────────────────
    tr ∋⋯ ≡[ p  b , ch ]

hasVoted : TraceInvariant HasVoted
hasVoted (_ , refl , (_ )) _ ()
hasVoted {s′} (_ , init , (_  st  s ⟩←— tr))
  {p}{b}{ch} b↝ p∈
  with IHhasVoted (_ , init , tr) {p}{b}{ch} b↝
  with st
... | Deliver _ = IH p∈
... | AdvanceEpoch = IH p∈
... | Drop _ = IH p∈
... | LocalStep (FinalizeBlock _ _ _ _)
  = there $ IH p∈
... | LocalStep (RegisterVote _ _)
  = there $ IH p∈
... | LocalStep s→@(ProposeBlock {ch = ch↓} {txs = txs} _ _ _ (_  _  B↝))
  = QED
  where
  open ∣ProposeBlock∣ p s ch↓ txs

  QED : Any ≡[ p  b , ch ] ((_  s→)  allLocalSteps tr)
  QED
    with b  B
  ... | no _ = there $ IH p∈
  ... | yes refl
    with  p∈
  ... |  there p∈
    = there $ IH p∈
  ... |  here refl
    = here $′ refl , refl , just bch≡
      where
      bch≡ : (b , ch)  (B , ch↓)
      bch≡ = cong (_ ,_) $ connects-to≡ b↝ B↝
... | LocalStep s→@(VoteBlock {H = H} {txs = txs} {ch = ch↓} _ _ _ _ _ (_  _  B↝))
  = QED
  where
  open ∣VoteBlock∣ p s H txs

  QED : Any ≡[ p  b , ch ] ((_  s→)  allLocalSteps tr)
  QED
    with b  B
  ... | no _ = there $ IH p∈
  ... | yes refl
    with  p∈
  ... |  there p∈
    = there $ IH p∈
  ... |  here refl
    = here $′ refl , refl , just bch≡
      where
      bch≡ : (b , ch)  (B , ch↓)
      bch≡ = cong (_ ,_) $ connects-to≡ b↝ B↝
... | DishonestLocalStep {p = p′}{m} ¬hp′ h⇒m∈
  = QED
  where
  open ∣DishonestLocalStep∣ p p′ ¬hp′ s m

  ≪p∈ : p  voteIds (s .history) b
  ≪p∈ with m ∙block  b
  ... | no ≢b = voteIds-∷˘′ ≢b p∈
  ... | yes refl
    with m ∙pid  p
  ... | no  ≢p = voteIds-∷˘ {ms = s .history} ≢p p∈
  ... | yes refl = voteIds-accept∈ (h⇒m∈ it) refl refl

  QED : Any ≡[ p  b , ch ] (allLocalSteps tr)
  QED = IH ≪p∈

HasVotedInbox : TraceProperty
HasVotedInbox tr@(s , _) =  {p m ch}  _ : Honest p   _ : Honest (m ∙pid)  
  let ls = s  p in
   m ∙block -connects-to- ch
   m  ls .inbox
    ─────────────────────────────────
    tr ∋⋯ ≡[ m ∙pid  m ∙block , ch ]

hasVotedInbox : TraceInvariant HasVotedInbox
hasVotedInbox {s} Rs {p}{m}{ch} b↝ m∈ = hasVoted Rs b↝ p∈
  where
  m∈′ : m  s .history
  m∈′ = inboxCompleteHonest Rs m∈

  p∈ : m ∙pid  voteIds (s .history) (m ∙block)
  p∈ = L.Mem.∈-map⁺ _∙pid
     $ L.Mem.∈-filter⁺ (((m ∙block ≟_)  _∙block)) m∈′ refl

Notarized∈ : TraceProperty
Notarized∈ tr@(s , _) =  {p b ch}  _ : Honest p  
  tr ∋⋯ ≡[ p  b , ch ]
  ────────────────────────────────
  ch notarized-chain-∈ (s  p) .db

notarized∈ : TraceInvariant Notarized∈
notarized∈ (_ , refl , (_ )) ()
notarized∈ {s′} (_ , init , (_  st  s ⟩←— tr))
  {p}{b}{ch} st∈
  with IHnotarized∈ (_ , init , tr) {p}{b}{ch}  it 
  with st
... | Deliver {env = [ p′  m′ } env∈
  = QED
  where
  open ∣Deliver∣ p s env∈

  QED : ch notarized-chain-∈ (s′  p) .db
  QED
    with honest? p′
  ... | no _ = IH st∈
  ... | yes hp′
    with p  p′
  ... | no p≢ rewrite lookup✖  hp′  p≢ = IH st∈
  ... | yes refl rewrite lookup✓  it  = IH st∈
... | AdvanceEpoch
  rewrite let open ∣AdvanceEpoch∣ p s in lookup✓
  = IH st∈
... | Drop _ = IH st∈
... | LocalStep {p = p′}{mm}{ls′} ls→
  = QED
  where
  open ∣LocalStep∣ p p′ s mm ls′

  QED : ch notarized-chain-∈ (s′  p) .db
  QED with  ls→ |  st∈
  QED |  FinalizeBlock ch↓ _ _ _ |  there st∈
    with p  p′
  ... | no p≢ rewrite lookup✖ p≢ = IH st∈
  ... | yes refl rewrite lookup✓ = IH st∈
  QED |  RegisterVote {sb = sb} M∈ M∉ |  there st∈
    with p  p′
  ... | yes refl rewrite lookup✓ = notarized-chain-∈-∷ $ IH st∈
  ... | no p≢ rewrite lookup✖ p≢ = IH st∈
  QED |  ProposeBlock {ch = ch↓} {txs = txs} _ refl _ _ |  there st∈
    with p  p′
  ... | no p≢ rewrite lookup✖ p≢ = IH st∈
  ... | yes refl rewrite lookup✓ = notarized-chain-∈-∷ $ IH st∈
  QED |  ProposeBlock {ch = ch↓} {txs = txs} _ refl (nch∈ , _) _
      |  here (refl , refl , just refl)
    with p  p′
  ... | no p≢ rewrite lookup✖ p≢ = nch∈
  ... | yes refl rewrite lookup✓ = notarized-chain-∈-∷ nch∈
  QED |  VoteBlock {H = H} {txs = txs} {ch = ch↓} M∈ _ _ _ _ _ |  there st∈
    with p  p′
  ... | no p≢ rewrite lookup✖ p≢ = IH st∈
  ... | yes refl rewrite lookup✓ = notarized-chain-∈-∷ $ notarized-chain-∈-∷ $ IH st∈
  QED |  VoteBlock {H = H} {txs = txs} {ch = ch↓} M∈ _ _ _ (nch∈ , _) _
      |  here (refl , refl , just refl)
    with p  p′
  ... | no p≢ rewrite lookup✖ p≢ = nch∈
  ... | yes refl rewrite lookup✓ = notarized-chain-∈-∷ $ notarized-chain-∈-∷ nch∈
... | DishonestLocalStep {p = p′}{mm} ¬hp′ h⇒m∈
  = subst (_ notarized-chain-∈_) db≡ $ IH st∈
  where
  open ∣DishonestLocalStep∣ p p′ ¬hp′ s mm

IncreasingEpochs⋯ : TraceProperty
IncreasingEpochs⋯ tr =  {p b ch b′ ch′} 
   length ch < length ch′
   tr ∋⋯ ≡[ p  b  , ch  ]
   tr ∋⋯ ≡[ p  b′ , ch′ ]
    ────────────────────────────
    b .epoch  b′ .epoch

private pattern HERE = here (refl , refl , just refl)

increasingEpochs⋯ : TraceInvariant IncreasingEpochs⋯
increasingEpochs⋯ (_ , refl , (_ )) _ ()
increasingEpochs⋯ {s′} (_ , init , (_  st  s ⟩←— tr))
  {p}{b}{ch}{b′}{ch′} len< st∈ st∈′
  with IHincreasingEpochs⋯ (_ , init , tr) {p}{b}{ch}{b′}{ch′} len<
  with IH-noFutVotnoFutureVotes≤ (_ , init , tr) {p}
  with IH-hasVothasVoted˘ (_ , init , tr) {p}
  with IH-not∈notarized∈ (_ , init , tr)
  with st
... | Deliver _ = IH st∈ st∈′
... | AdvanceEpoch = IH st∈ st∈′
... | Drop _ = IH st∈ st∈′
... | LocalStep ls→
  = QED
  where
  QED : b .epoch  b′ .epoch
  QED with  ls→ |  st∈ |  st∈′
  QED |  FinalizeBlock _ _ _ _ |  there st∈ |  there st∈′ = IH st∈ st∈′
  QED |  RegisterVote _ _ |  there st∈ |  there st∈′ = IH st∈ st∈′
  QED |  ProposeBlock _ _ _ _ |  there st∈ |  there st∈′ = IH st∈ st∈′
  QED |  ProposeBlock _ _ _ _ |  HERE |  HERE
    = ⊥-elim $ Nat.<-irrefl refl len<
  QED |  ProposeBlock {ch = ch↓} {txs = txs} _ _ (_ , mkLongest∈ lch) _
      |  HERE |  there st∈′
    = ⊥-elim $ Nat.<⇒≱ len< len≥
    where
    open ∣ProposeBlock∣ p s ch↓ txs

    ch∈′ : ch′ notarized-chain-∈ ((s  p) .db)
    ch∈′ = IH-not∈ st∈′

    len≥ : length ch↓  length ch′
    len≥ = lch ch∈′
  QED |  ProposeBlock {ch = ch↓} {txs = txs} _ refl _ _ |  there st∈ |  HERE
    = IH-noFutVot p∈
    where
    open ∣ProposeBlock∣ p s ch↓ txs

    p∈ : L  voteIds (s .history) b
    p∈ = IH-hasVot st∈
  QED |  VoteBlock {H = H} _ _ _ _ _ _ |  there st∈ |  there st∈′ = IH st∈ st∈′
  QED |  VoteBlock _ _ _ _ _ _ |  HERE |  HERE
    = ⊥-elim $ Nat.<-irrefl refl len<
  QED |  VoteBlock {H = H} {txs = txs} {ch = ch↓} _ _ _ _ (_ , mkLongest∈ lch) _ |  HERE |  there st∈′
    = ⊥-elim $ Nat.<⇒≱ len< len≥
    where
    open ∣VoteBlock∣ p s H txs

    ch∈′ : ch′ notarized-chain-∈ ((s  p) .db)
    ch∈′ = IH-not∈ st∈′

    len≥ : length ch↓  length ch′
    len≥ = lch ch∈′
  QED |  VoteBlock {H = H} {txs = txs} _ _ _ _ _ _ |  there st∈ |  HERE
    = IH-noFutVot p∈
    where
    open ∣VoteBlock∣ p s H txs

    p∈ : p  voteIds (s .history) b
    p∈ = IH-hasVot st∈
... | DishonestLocalStep _ _ = IH st∈ st∈′