def operator \chain\upchain^\mu:
  A <- C[0]
  Z <- C[-1]
  C` <- []
  while Z \neq A:
    if level(Z) \geq \mu:
      C`.prepend(Z)
    Z <- Z.interlink[\mu]
  C`.prepend(A)

def operator \chain`\downchain_\chain:
  A <- C`[0]
  Z <- \chain'[-1]
  a <- index_of(A, \chain)
  z <- index_of(Z, \chain)
  return \chain[a:z]

def operator \chain`\updownchain^\mu_\chain:
  return \chain`\downchain_\chain\upchain^\mu

def operator \chain\{B:\}:
  \chain' <- []
  Z <- C[-1]
  while Z \neq B:
    \chain`.prepend(Z)
    Z <- Z.interlink[0]
  \chain'.prepend(B)

def prove_{m,k,\delta}(\chain):
  B <- \chain[0]
  \tilde\pi <- \emptyset
  for \mu <- |C[-1].interlink| - 1 to 0:
    \pi = \chain\{B:\}\upchain^\mu
    \tilde\pi \cup<- \pi
    if good(\pi):
      B <- \pi[-m]
  return \tilde\pi

def superchain(b, \mu, B):
  \pi <- [b]
  do:
    b <- b.interlink[\mu]
    if level(b) \geq \mu:
      \pi.prepend(b)
  while b \neq B
  return \pi

def v1 good_{m,\delta}(\chain`, \chain, \mu):
  if |\chain`| < m:
    return False
  if (1 - \delta)2^{-\mu}|\chain`\downchain^\chain| > |\chain`|:
    return False
  return True

def verify_m(\Pi):
  return max(\Pi)

def v1 operator \tilde\pi_\mathcal{A} \geq \tilde\pi_B:
  b <- LCA(\tilde\pi_\mathcal{A}, \tilde\pi_B)
  \tilde\pi_A <- parse(\tilde\pi_\mathcal{A})
  \tilde\pi_B <- parse(\tilde\pi_B)

  (\mu_A, \alpha_A) <- best_arg(\overline\pi_\mathcal{A})
  (\mu_B, \alpha_B) <- best_arg(\overline\pi_B)

  return 2^{\mu_\mathcal{A}}|\alpha_A| \geq 2^{\mu_B}|\alpha_B|

def best_arg(\overline\pi):
  \mu <-
    argmax_{0 \leq \mu < |\overline\pi| \land (|\overline\pi[\mu]| \geq m \lor \mu = 0)}
           {2^\mu|\overline\pi[\mu]|}
  return (\mu, \overline\pi[\mu])

def v2 good_{m,\delta}(\chain`, \chain, \mu):
  if |\chain'| < m:
    return False
  for \chain^* \in {\chain`[i:i + m - 1]: 0 \leq i < |\chain`| - m}:
    if m < (1 - \delta)2^{-\mu}|\chain^*\downchain_\chain|:
      return False
  return True

def v2 operator \tilde\pi_\mathcal{A} \geq \tilde\pi_B:
  b <- LCA(\tilde\pi_\mathcal{A}, \tilde\pi_B)
  \tilde\pi_A <- parse(\tilde\pi_\mathcal{A})
  \tilde\pi_B <- parse(\tilde\pi_B)

  \overline\pi_\mathcal{A}` <- map(_{b:}, \overline\pi_\mathcal{A})
  \overline\pi_B`           <- map(_{b:}, \overline\pi_B)

  (\mu_A, \alpha_A) <- best_arg(\overline\pi_\mathcal{A}`)
  (\mu_B, \alpha_B) <- best_arg(\overline\pi_B`)

  return 2^{\mu_\mathcal{A}}|\alpha_A| \geq 2^{\mu_B}|\alpha_B|

Lemma: Suppose \tilde\pi_\mathcal{A} \geq \tilde\pi_B is called, where B is honest.
       Let \mu_B` be the highest "good" superchain level for B,
       and let b = LCA(\tilde\pi_\mathcal{A}, \tilde\pi_B).
       Then \mu_B` \geq \mu_B.

Pf: By \mu_B winning argument condition we have:
    2^{\mu_B}|\chain\{b:\}\upchain^{\mu_B}| > 2^{\mu_B}|\chain\{b:\}|. (1)

    By \mu_B badness condition:
    2^{\mu_B}|\chain\{b:\}\upchain^{\mu_B}| < (1 - \delta)|\chain\{b:\}|. (2)

    By \mu_B` goodness condition:
    2^{\mu_B`}|\chain\{b:}\upchain^{\mu_B`} > (1 - \delta)|\chain\{b:\}|. (3)

    (1)(2) => (1 - \delta)|\chain\{b:\}| > 2^{\mu_B`}|\chain\{b:\}\upchain^{\mu_B`}| (4)
    (3)(4) => \bot. \qed

Thm: Suffix NIPoPoW is secure with overwhelming probability in \kappa.

Pf: Suppose \tilde_\mathcal{A} \geq \tilde_B. Then let b = LCA(\tilde\pi_\mathcal{A}, \tilde\pi_B).
    Let 2^{\mu_\mathcal{A}}|\alpha_A| \geq 2^{\mu_B}|\alpha_B|.
    Let \mu_B` be the highest "good" superchain level for B.
    (and note that it is possible that \mu_B \neq \mu_B` if \mu_B contains more PoW).

Claim: If \mu_\mathcal{A} \geq \mu_B, then all \mu_B`-level blocks honestly adopted by B after b are included in \alpha_B.
       Therefore the chains \alpha_\mathcal{A}, \alpha_B are disjoint.