An Agda Formalization of Friedman’s Extended Kruskal Theorem

March 2023 (last updated 2023-03-09)

This is an Agda formalization of Friedman’s theorem about tree embedding with a gap condition.

Simpson, Stephen G. (1985), “Nonprovability of certain combinatorial properties of finite trees”, in Harrington, L. A.; Morley, M.; Scedrov, A.; et al. (eds.), Harvey Friedman’s Research on the Foundations of Mathematics, Studies in Logic and the Foundations of Mathematics, North-Holland, pp. 87–117

A restriction of this theorem to monadic trees was posed as the “TPPmark” challenge for the 18th TPP meeting.

I deviate from Friedman’s proof in reasoning about sequences that are “very good” with respect to a given binary relation, rather than the property of a relation being a WQO. This allows us to state stronger lemmas, as well as (hopefully) to simplify Friedman’s inductive proof, albeit at the cost of (slightly) complicating (and generalizing) the minimal bad sequence argument.

Poster presented at PPL 2023:

Poster PDF

I use the development version of agda-stdlib 2.0 as of February 8, 2023:

agda-stdlib development version

Tested with Agda 2.6.3.

module Friedman where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; _≢_; sym; trans; subst; cong)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; s≤s; z≤n; _<_; _⊓_)
open import Data.Nat.Properties
  -- don't use the library version of ≤-<-connex
  -- use m≤n⇒m≤1+n instead of ≤-step
  using (suc-injective; ≤-reflexive; ≤-refl; ≤-trans; <-irrefl; <⇒≤; 
        m≤n⇒m≤1+n; <-transˡ; <-transʳ; 
        ≤∧≢⇒<; +-monoˡ-<; m≤m+n; m≤n+m; m≤n⇒m≤o+n; +-mono-≤; +-monoˡ-≤;
        m<n⇒m⊓o<n; m≤n⇒m⊓n≡m; ⊓-comm; -- ≤-total; 
        m⊓n≤m; ≤-pred; <⇒≱)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂ ; ∃; Σ-syntax; ∃-syntax; ∃₂)
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_]′ to case-⊎)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Unary using (_∈_; Satisfiable)
open import Function using (_∘_; id)
open import Data.List using (List; []; _∷_; _++_; length; sum; _ʳ++_)
import Data.Fin as F
open F using (Fin; toℕ; fromℕ<)
open import Data.Fin.Properties using 
  (pigeonhole; toℕ-mono-<; toℕ<n; fromℕ<-toℕ; fromℕ<-cong; toℕ-fromℕ<; 
  toℕ-injective; fromℕ<-injective)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Maybe.Properties using (just-injective)
open import Relation.Binary.Core using (_⇒_)

Miscellaneous stuff:

open import Miscellaneous

Some consequences of the excluded middle:

open import Classical

Definitions concerning WQO and Dickson’s lemma:

open import WQO

Minimal bad sequence argument, slightly generalized:

open import MinimalBadSeq

Higman’s lemma:

import Higman as H

Some stuff about Fin n:

open import Fin

Definitions about trees and tree embedding, as well as some facts about them:

open import Tree

private
  variable
    A : Set
    n : ℕ

Friedman’s “star” function on trees locates highest nodes with the minimal interior node label, replaces each of those nodes with a leaf labeled by the subtree rooted at that node, and decrements the lables of all remaining nodes. As was the case with the definition of μ in Tree, the definition of this function is hard to reason with, and we have to state many easy lemmas about it for later use.

module _ {A : Set} {n : ℕ} where

  star-helper : Fin (suc n) → Tree A (suc n) → Tree (Tree A (suc n)) n
  star-helper-list : Fin (suc n) → List (Tree A (suc n)) → 
                     List (Tree (Tree A (suc n)) n)

  star-helper m (leaf a)            = leaf (leaf a)
  star-helper m (node i ts {ts≢[]}) with ≤-<-connex (toℕ i) (toℕ m)
  star-helper m (node i ts {ts≢[]})       | inj₁ i≤m   = leaf (node i ts {ts≢[]})
  star-helper m (node (F.suc i) (t ∷ ts)) | inj₂ 1+i>m = 
    node i (star-helper m t ∷ star-helper-list m ts)

  star-helper-list m ([])     = []
  star-helper-list m (t ∷ ts) = star-helper m t ∷ star-helper-list m ts

  star-helper-≤ : (m i : Fin (suc n)) (ts : List (Tree A (suc n))) → 
                  {ts≢[] : Nonempty ts} → i F.≤ m → 
                  star-helper m (node i ts {ts≢[]}) ≡ leaf (node i ts {ts≢[]})
  star-helper-≤ m i ts i≤m rewrite ≤-<-connex-≤ (toℕ i) (toℕ m) i≤m = refl

  star-helper-i-node-i : (ts : List (Tree A (suc n))) {ts≢[] : Nonempty ts}
                         (i : Fin (suc n)) → 
                         star-helper i (node i ts {ts≢[]}) ≡ leaf (node i ts {ts≢[]})
  star-helper-i-node-i ts i = star-helper-≤ i i ts ≤′-refl

  star-helper-> : (m i : Fin (suc n)) (t : Tree A (suc n)) 
                  (ts : List (Tree A (suc n))) → m F.< i →
                  ∃[ i′ ] (i ≡ F.suc i′ × 
                           star-helper m (node i (t ∷ ts)) ≡ 
                              node i′ (star-helper m t ∷ star-helper-list m ts))
  star-helper-> m (F.suc i) t ts 1+i>m 
    rewrite ≤-<-connex-> (toℕ (F.suc i)) (toℕ m) 1+i>m = i , refl , refl

  star-helper->-suc : (m : Fin (suc n)) (i : Fin n) (t : Tree A (suc n)) 
                      (ts : List (Tree A (suc n))) {ts≢[] : Nonempty ts} → 
                      m F.< F.suc i → 
                      star-helper m (node (F.suc i) (t ∷ ts)) ≡ 
                        node i (star-helper m t ∷ star-helper-list m ts)
  star-helper->-suc m i t ts i>m 
    rewrite ≤-<-connex-> (toℕ (F.suc i)) (toℕ m) i>m = refl

  star-helper-list-elem⁺ :
    (m : Fin (suc n)) (t : Tree A (suc n)) 
    (ts : List (Tree A (suc n))) → t elem ts → 
    star-helper m t elem (star-helper-list m ts)
  star-helper-list-elem⁺ m t (.t ∷ ts) here = here
  star-helper-list-elem⁺ m t (u ∷ ts) (there x) = 
    there (star-helper-list-elem⁺ m t ts x)

  star-helper-list-elem⁻ : 
    (m : Fin (suc n)) (ts : List (Tree A (suc n))) 
    (v : Tree (Tree A (suc n)) n) → v elem (star-helper-list m ts) →
    ∃[ t ] t elem ts × v ≡ star-helper m t
  star-helper-list-elem⁻ m (t ∷ ts) .(star-helper m t) here = t , here , refl
  star-helper-list-elem⁻ m (t ∷ ts) v (there h) with star-helper-list-elem⁻ m ts v h
  ... | t′ , h′ , refl = t′ , there h′ , refl

  star : Tree A (suc n) → Tree (Tree A (suc n)) n
  star t with μ t
  ... | just m = star-helper m t
  ... | nothing = leaf t

  star-just : (m : Fin (suc n)) (t : Tree A (suc n)) → μ t ≡ just m → 
              star t ≡ star-helper m t
  star-just m t h with μ t
  star-just .m₁ t refl | just m₁ = refl

  star-nothing : (t : Tree A (suc n)) → μ t ≡ nothing → star t ≡ leaf t
  star-nothing t h with μ t
  ... | nothing = refl

Every leaf of star t is a subtree of t. I had to add a size parameter to the auxiliary function to make Agda termination checking pass.

  isLeaf-star⇒⊑ : (t u : Tree A (suc n)) → IsLeaf u (star t) → u ⊑ t
  isLeaf-star⇒⊑ t u h with μ t
  ... | nothing rewrite isLeaf-leaf h = ⊑-refl
  ... | just m  = helper t (size t) ≤-refl h 
    where
    helper : (t : Tree A (suc n)) (k : ℕ) →
      size t ≤ k → IsLeaf u (star-helper m t) → u ⊑ t
    helper (leaf a) k 1≤k h rewrite isLeaf-leaf h = ⊑-refl
    helper (node i (t ∷ ts)) (suc k) (s≤s size[t∷ts]≤k) h with ≤-<-connex (toℕ i) (toℕ m)
    ... | inj₁ i≤m rewrite isLeaf-leaf h = ⊑-refl
    ... | inj₂ i>m with star-helper-> m i t ts i>m
    ... | i′ , refl , eq with isLeaf-node h
    -- ... | v , h₁ , h₂ with star-helper-list-elem⁻ m (t ∷ ts) v h₁
    -- ... | t′ , h′ , refl = ⊑-step (F.suc i′) (t ∷ ts) (helper t′ h₂) h′
    ... | v , h₁ , h₂ with isLeaf-node h
    ... | t′ , h₃ , h₄ with star-helper-list-elem⁻ m (t ∷ ts) t′ h₃
    ... | t′′ , h₅ , refl = ⊑-step (F.suc i′) (t ∷ ts) u⊑t′′ h₅
      where
      size[t′′]≤k : size t′′ ≤ k
      size[t′′]≤k = ≤-trans (elem-size-≤ h₅) size[t∷ts]≤k

      u⊑t′′ : u ⊑ t′′
      u⊑t′′ = helper t′′ k size[t′′]≤k h₄

  isLeaf⇔IsLeaf-IsLeaf-star : (t : Tree A (suc n)) (u : A) → 
    IsLeaf {n = suc n} u t ⇔ 
      (Σ[ v ∈ Tree A (suc n)] (IsLeaf {n = suc n} u v × IsLeaf {n = n} v (star t)))
  isLeaf⇔IsLeaf-IsLeaf-star t u with μ t
  ... | nothing = ⟨⇒⟩ , ⟨⇐⟩
    where
    ⟨⇒⟩ : IsLeaf u t → Σ[ v ∈ Tree A (suc n) ] (IsLeaf u v × IsLeaf v (leaf t))
    ⟨⇒⟩ h = t , h , here

    ⟨⇐⟩ : Σ[ v ∈ Tree A (suc n) ] (IsLeaf u v × IsLeaf v (leaf t)) → IsLeaf u t
    ⟨⇐⟩ (v , h₁ , here) = h₁ 
  ... | just m  = helper t (size t) ≤-refl
    where
    helper : (t : Tree A (suc n)) (k : ℕ) → size t ≤ k → 
             IsLeaf u t ⇔ 
             (Σ[ v ∈ Tree A (suc n)] (IsLeaf u v × IsLeaf v (star-helper m t)))
    helper (leaf a) k 1≤k = ⟨⇒⟩ , ⟨⇐⟩
      where
      ⟨⇒⟩ : IsLeaf u (leaf a) → 
             Σ[ v ∈ Tree A (suc n)] (IsLeaf u v × IsLeaf v (star-helper m (leaf a)))
      ⟨⇒⟩ h = leaf a , h , here

      ⟨⇐⟩ : Σ[ v ∈ Tree A (suc n)] (IsLeaf u v × IsLeaf v (star-helper m (leaf a))) →
            IsLeaf u (leaf a)
      ⟨⇐⟩ (.(leaf a) , h₁ , here) = h₁
    helper (node i (t ∷ ts)) (suc k) (s≤s size[t∷ts]≤k) with ≤-<-connex (toℕ i) (toℕ m)
    ... | inj₁ i≤m = ⟨⇒⟩ , ⟨⇐⟩
      where
      ⟨⇒⟩ : IsLeaf u (node i (t ∷ ts)) → 
            Σ[ v ∈ Tree A (suc n) ] (IsLeaf u v × IsLeaf v (leaf (node i (t ∷ ts))))
      ⟨⇒⟩ h = node i (t ∷ ts) , h , here

      ⟨⇐⟩ : Σ[ v ∈ Tree A (suc n) ] (IsLeaf u v × IsLeaf v (leaf (node i (t ∷ ts)))) →  
            IsLeaf u (node i (t ∷ ts))
      ⟨⇐⟩ (.(node i (t ∷ ts)) , h₁ , here) = h₁
    ... | inj₂ i>m with star-helper-> m i t ts i>m 
    ... | i′ , refl , eq rewrite eq = ⟨⇒⟩ , ⟨⇐⟩
      where
      ⟨⇒⟩ : IsLeaf u (node (F.suc i′) (t ∷ ts)) → 
            Σ[ v ∈ Tree A (suc n) ] 
            (IsLeaf u v × IsLeaf v (node i′ (star-helper m t ∷ star-helper-list m ts)))
      ⟨⇒⟩ (there {t = t₂} h h₁) = v , [1] , there (star-helper-list-elem⁺ m t₂ (t ∷ ts) h) [2]
        where
        size[t₂]≤k : size t₂ ≤ k
        size[t₂]≤k = ≤-trans (elem-size-≤ h) size[t∷ts]≤k

        w : Σ[ v ∈ Tree A (suc n) ] (IsLeaf u v × IsLeaf v (star-helper m t₂))
        w = proj₁ (helper t₂ k size[t₂]≤k) h₁

        v = proj₁ w

        [1] : IsLeaf u v
        [1] = proj₁ (proj₂ w)

        [2] : IsLeaf v (star-helper m t₂)
        [2] = proj₂ (proj₂ w)

      ⟨⇐⟩ : Σ[ v ∈ Tree A (suc n) ] 
            (IsLeaf u v × IsLeaf v (node i′ (star-helper m t ∷ star-helper-list m ts))) → 
            IsLeaf u (node (F.suc i′) (t ∷ ts))
      ⟨⇐⟩ (v , h₁ , there {t = t₁} h h₂) with star-helper-list-elem⁻ m (t ∷ ts) t₁ h
      ... | t′ , h₃ , refl = there h₃ [3]
        where
        size[t′]≤k : size t′ ≤ k
        size[t′]≤k = ≤-trans (elem-size-≤ h₃) size[t∷ts]≤k

        [3] : IsLeaf u t′
        [3] = proj₂ (helper t′ k size[t′]≤k) (v , h₁ , h₂)

Lemma 4.5

Let t u : Tree A (suc n). If μ t ≡ μ u and star t and star u are related by Embedding-gap⁺ (Embedding-gap _≼_), then t and u are related by Embedding-gap⁺ _≼_. This supposedly ‘straightforward’ proof is extremely long and tedious. It has turned out to be the toughest part of the proof to formalize. There is a lot of repetitive code, so there is some room for cleaning up.

module _ {A : Set} {n : ℕ} {_≼_ : A → A → Set} where

  embed-star-helper-Embed-nothing : 
    (m : Fin (suc n)) (a : A) (u : Tree A (suc n)) (k : ℕ) → size u ≤ k →
    Embedding-gap⁺ (Embedding-gap _≼_) (star-helper m (leaf a)) (star-helper m u) → 
    Embedding-gap⁺ _≼_ (leaf a) u

  embed-star-helper-Embed-nothing m a u zero size[u]≤0 h = 
    ⊥-elim (<⇒≱ (s≤s size[u]≤0) (size≥1 u))
  embed-star-helper-Embed-nothing m a u (suc k) size[u]≤1+k
    h with μ u in eq[μu]
  ... | just m₁ = subst (Embedding-gap⁺ _≼_ (leaf a)) (sym eq[u]) (goal₁ [2])
    where
    [1] : Σ[ j ∈ Fin (suc n) ] Σ[ u₁ ∈ Tree A (suc n) ] 
          Σ[ us ∈ List (Tree A (suc n)) ] u ≡ node j (u₁ ∷ us)
    [1] = μ-just′ u m₁ eq[μu]

    j = proj₁ [1]

    u₁ = proj₁ (proj₂ [1])

    us = proj₁ (proj₂ (proj₂ [1]))

    eq[u] : u ≡ node j (u₁ ∷ us)
    eq[u] = proj₂ (proj₂ (proj₂ [1]))

    size[u₁∷us]≤k : size-list (u₁ ∷ us) ≤ k
    size[u₁∷us]≤k = ≤-pred [2]
      where
      [2] : size (node j (u₁ ∷ us)) ≤ suc k
      [2] = subst (λ z → size z ≤ suc k) eq[u] size[u]≤1+k

    [2] : Embedding-gap⁺ (Embedding-gap _≼_) (leaf (leaf a)) 
            (star-helper m (node j (u₁ ∷ us)))
    [2] = subst (λ z → Embedding-gap⁺ (Embedding-gap _≼_) (leaf (leaf a)) (star-helper m z)) 
            eq[u] h

    goal₁ : 
      Embedding-gap⁺ (Embedding-gap _≼_) (leaf (leaf a)) 
                      (star-helper m (node j (u₁ ∷ us))) → 
      Embedding-gap⁺ _≼_ (leaf a) (node j (u₁ ∷ us))
    goal₁ h₁ with ≤-<-connex (toℕ j) (toℕ m)
    goal₁ (leaf h₂) | inj₁ j≤m = emb-gap-μ-emb-gap⁺ _≼_ {t = leaf a} tt h₂
    goal₁ h₁        | inj₂ j>m = goal₂
      where
      [3] : ∃[ j′ ] (j ≡ F.suc j′ × 
                     star-helper m (node j (u₁ ∷ us)) ≡ node j′ (star-helper-list m (u₁ ∷ us)))

      [3] = star-helper-> m j u₁ us j>m

      j′ = proj₁ [3]

      j≡1+j′ : j ≡ F.suc j′
      j≡1+j′ = proj₁ (proj₂ [3])

      [4] : star-helper m (node j (u₁ ∷ us)) ≡ 
              node j′ (star-helper m u₁ ∷ star-helper-list m us)
      [4] = proj₂ (proj₂ [3])

      [5] : Embedding-gap⁺ (Embedding-gap _≼_) (leaf (leaf a)) 
              (node j′ (star-helper m u₁ ∷ star-helper-list m us))
      [5] rewrite sym [4] = [2]

      goal₂ : Embedding-gap⁺ _≼_ (leaf a) (node j (u₁ ∷ us))
      goal₂ with [5]
      ... | pass {u = u₂} _ h₃ h₄ = pass tt [10] [7]
        where
        [6] : ∃[ v ] v elem (u₁ ∷ us) × u₂ ≡ star-helper m v
        [6] = star-helper-list-elem⁻ m (u₁ ∷ us) u₂ h₄

        v = proj₁ [6]

        [7] : v elem (u₁ ∷ us)
        [7] = proj₁ (proj₂ [6])

        [8] : u₂ ≡ star-helper m v
        [8] = proj₂ (proj₂ [6])

        size[v]≤k : size v ≤ k
        size[v]≤k = ≤-trans (elem-size-≤ [7]) size[u₁∷us]≤k

        [9] : Embedding-gap⁺ (Embedding-gap _≼_) (leaf (leaf a)) (star-helper m v)
        [9] rewrite sym [8] = h₃

        [10] : Embedding-gap⁺ _≼_ (leaf a) v
        [10] = embed-star-helper-Embed-nothing m a v k size[v]≤k [9]
  ... | nothing = subst (Embedding-gap⁺ _≼_ (leaf a)) (sym eq[u]) [4]
    where
    [1] : ∃[ b ] u ≡ leaf b
    [1] = μ-nothing u eq[μu]

    b = proj₁ [1]

    eq[u] : u ≡ leaf b
    eq[u] = proj₂ [1]

    [2] : star-helper m u ≡ leaf (leaf b)
    [2] = cong (star-helper m) eq[u]

    [3] : Embedding-gap⁺ {n = n} (Embedding-gap {n = suc n} _≼_) 
              (leaf (leaf a)) (leaf (leaf b))
    [3] rewrite sym [2] = h

    [4] : Embedding-gap⁺ {n = suc n} _≼_ (leaf a) (leaf b)
    [4] with [3]
    ... | leaf (mk h₁) = h₁

  embed-star-helper-list-Embed-nothing :
    (m : Fin (suc n)) (ts us : List (Tree A (suc n))) →
    μ-list ts ≡ nothing →
    Embedding-gap⁺-list (Embedding-gap _≼_) (star-helper-list m ts) (star-helper-list m us) →
    Embedding-gap⁺-list _≼_ ts us
  embed-star-helper-list-Embed-nothing m [] us eq[μts] h = 
    embedding-gap⁺-list-[] _≼_ us
  embed-star-helper-list-Embed-nothing m (t ∷ ts) (u ∷ us) eq[μts] (.(star-helper m u) ∷ʳ h) = 
    u ∷ʳ embed-star-helper-list-Embed-nothing m (t ∷ ts) us eq[μts] h
  embed-star-helper-list-Embed-nothing m (t ∷ ts) (u ∷ us) eq[μts] (h₁ ∷ h₂) = 
    [5] ∷ embed-star-helper-list-Embed-nothing m ts us [6] h₂
    where
    [1] : μ t ≡ nothing
    [1] = ⊓′-nothing₁ (μ t) (μ-list ts) eq[μts]

    [2] : ∃[ a ] t ≡ leaf a
    [2] = μ-nothing t [1]

    a = proj₁ [2]

    eq[t] : t ≡ leaf a
    eq[t] = proj₂ [2]

    [3] : star-helper m t ≡ leaf (leaf a)
    [3] = cong (star-helper m) eq[t]

    [4] : Embedding-gap⁺ (Embedding-gap _≼_) (star-helper m (leaf a)) 
            (star-helper m u)
    [4] rewrite sym [3] = h₁

    [5] : Embedding-gap⁺ _≼_ t u
    [5] rewrite eq[t] = embed-star-helper-Embed-nothing m a u (size u) ≤-refl [4]

    [6] : μ-list ts ≡ nothing
    [6] = ⊓′-nothing₂ (μ t) (μ-list ts) eq[μts]
  
  embed-star-helper-just-nothing :
    (m m₁ : Fin (suc n)) (t u : Tree A (suc n)) → 
    μ t ≡ just m₁ → μ u ≡ nothing →
    ¬ Embedding-gap⁺ (Embedding-gap _≼_) (star-helper m t) (star-helper m u)
  embed-star-helper-just-nothing m m₁ t u eq[μt] eq[μu] h = contra
    where
    [1] : Σ[ i ∈ Fin (suc n) ] Σ[ t₁ ∈ Tree A (suc n) ] 
          Σ[ ts₁ ∈ List (Tree A (suc n)) ] t ≡ node i (t₁ ∷ ts₁)
    [1] = μ-just′ t m₁ eq[μt]

    i = proj₁ [1]

    t₁ = proj₁ (proj₂ [1])

    ts₁ = proj₁ (proj₂ (proj₂ [1]))

    eq[t] : t ≡ node i (t₁ ∷ ts₁)
    eq[t] = proj₂ (proj₂ (proj₂ [1]))

    [2] : ∃[ b ] u ≡ leaf b
    [2] = μ-nothing u eq[μu]

    b = proj₁ [2]

    eq[u] : u ≡ leaf b
    eq[u] = proj₂ [2]

    [3] : star-helper m u ≡ leaf (leaf b)
    [3] = cong (star-helper m) eq[u]

    [4] : Embedding-gap⁺ {n = n} (Embedding-gap _≼_) 
            (star-helper m (node i (t₁ ∷ ts₁))) (leaf (leaf b))
    [4] = subst (λ z → Embedding-gap⁺ {n = n} (Embedding-gap _≼_) (star-helper m z) (leaf (leaf b))) 
                eq[t] 
            (subst (λ z → Embedding-gap⁺ {n = n} (Embedding-gap _≼_) (star-helper m t) (star-helper m z))
                eq[u] h)

    contra : ⊥
    contra with ≤-<-connex (toℕ i) (toℕ m)
    ... | inj₁ i≤m = contra₁
      where
      [5] : star-helper m (node i (t₁ ∷ ts₁)) ≡ leaf (node i (t₁ ∷ ts₁))
      [5] = star-helper-≤ m i (t₁ ∷ ts₁) i≤m

      [6] : Embedding-gap⁺ {n = n} (Embedding-gap _≼_) 
              (leaf (node i (t₁ ∷ ts₁))) (leaf (leaf b))
      [6] = subst (λ z → Embedding-gap⁺ {n = n} (Embedding-gap _≼_) z (leaf (leaf b))) 
              [5] [4]

      contra₁ : ⊥
      contra₁ with [6]
      ... | leaf (mk ())
    ... | inj₂ i>m = contra₁
      where
      [5] : ∃[ i′ ] (i ≡ F.suc i′ × 
                     star-helper m (node i (t₁ ∷ ts₁)) ≡ 
                      node i′ (star-helper m t₁ ∷ star-helper-list m ts₁))
      [5] = star-helper-> m i t₁ ts₁ i>m

      i′ = proj₁ [5]

      i≡1+i′ : i ≡ F.suc i′
      i≡1+i′ = proj₁ (proj₂ [5])

      [6] : star-helper m (node i (t₁ ∷ ts₁)) ≡ 
              node i′ (star-helper m t₁ ∷ star-helper-list m ts₁)
      [6] = proj₂ (proj₂ [5])

      [7] : Embedding-gap⁺ {n = n} (Embedding-gap _≼_) 
              (node i′ (star-helper m t₁ ∷ star-helper-list m ts₁)) (leaf (leaf b))
      [7] = subst (λ z → Embedding-gap⁺ {n = n} (Embedding-gap _≼_) z (leaf (leaf b)))
              [6] [4]

      contra₁ : ⊥
      contra₁ with [7]
      ... | ()

  embed-star-helper-list-just-nothing :
    (m m₁ : Fin (suc n)) (ts us : List (Tree A (suc n))) → {Nonempty ts} →
    μ-list ts ≡ just m₁ → μ-list us ≡ nothing →
    ¬ Embedding-gap⁺-list (Embedding-gap _≼_) (star-helper-list m ts) (star-helper-list m us)
  -- embed-star-helper-list-just-nothing m (t ∷ ts) [] eq[μts] eq[μus] ()
  embed-star-helper-list-just-nothing m m₁ (t ∷ ts) (u ∷ us) eq[μts] eq[μus] (.(star-helper m u) ∷ʳ h) = 
    embed-star-helper-list-just-nothing m m₁ (t ∷ ts) us eq[μts] [1] h
    where
    [1] : μ-list us ≡ nothing
    [1] = ⊓′-nothing₂ (μ u) (μ-list us) eq[μus]
  embed-star-helper-list-just-nothing m m₁ (t ∷ ts) (u ∷ us) eq[μts] eq[μus] (h₁ ∷ h₂) 
    with μ t in eq[μt]
  ... | nothing = embed-star-helper-list-just-nothing m m₁ ts us {ts≢[]} [1] [2] h₂
    where
    [1] : μ-list ts ≡ just m₁
    [1] = ⊓′-nothing-just (μ-list ts) m₁ eq[μts]

    ts≢[] : Nonempty ts
    ts≢[] = μ-list-just-nonempty [1]

    [2] : μ-list us ≡ nothing
    [2] = ⊓′-nothing₂ (μ u) (μ-list us) eq[μus]
  ... | just m₂ = ⊥-elim (embed-star-helper-just-nothing m m₂ t u eq[μt] [1] h₁)
    where
    [1] : μ u ≡ nothing
    [1] = ⊓′-nothing₁ (μ u) (μ-list us) eq[μus]

  embed-star-Embed-nothing : 
    (t u : Tree A (suc n)) → μ t ≡ nothing → μ u ≡ nothing →
    Embedding-gap⁺ (Embedding-gap _≼_) (star t) (star u) → 
    Embedding-gap⁺ _≼_ t u

  embed-star-Embed-nothing t u eq[μt] eq[μu] h = goal
    where
    [1] : star t ≡ leaf t
    [1] = star-nothing t eq[μt]

    [2] : star u ≡ leaf u
    [2] = star-nothing u eq[μu]

    [3] : Embedding-gap⁺ (Embedding-gap _≼_) (leaf t) (leaf u)
    [3] rewrite sym [1] | sym [2] = h

    [4] : ∃[ b ] u ≡ leaf b
    [4] = μ-nothing u eq[μu]

    b = proj₁ [4]

    eq[u] : u ≡ leaf b
    eq[u] = proj₂ [4]

    [5] : Embedding-gap⁺ (Embedding-gap _≼_) (leaf t) (leaf (leaf b))
    [5] rewrite sym eq[u] = [3]

    [6] : Embedding-gap⁺ _≼_ t (leaf b)
    [6] with [5]
    ... | leaf (mk h′) = h′

    goal : Embedding-gap⁺ _≼_ t u
    goal rewrite eq[u] = [6]

For the following mutually recursive lemmas, I had to use a hacked version of size to avoid the failure of Agda’s termination checking. The problem was the presence of a with-abstraction intervening a call of one function by another, both with suc k as an argument. See https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#termination-checking.

  embed-star-helper-Embed-just : 
    (m : Fin (suc n)) (t u : Tree A (suc n)) (k : ℕ) → size′ u ≤ k →
    just m ≤′ μ t → just m ≤′ μ u →
    Embedding-gap⁺ (Embedding-gap _≼_) (star-helper m t) (star-helper m u) →
    Embedding-gap⁺ _≼_ t u

  embed-star-helper-list-Embed-just : 
    (m : Fin (suc n)) (ts us : List (Tree A (suc n))) (k : ℕ) → size-list′ us ≤ k →
    just m ≤′ μ-list ts → just m ≤′ μ-list us →
    Embedding-gap⁺-list (Embedding-gap _≼_) (star-helper-list m ts) (star-helper-list m us) →
    Embedding-gap⁺-list _≼_ ts us
  
  embed-star-helper-Embed-just 
    m (node i (t ∷ ts)) (node j (u ∷ us)) (suc k) (s≤s size[u∷us]≤k) ineq[μt∷ts] ineq[μu∷us] h = 
    goal h
    where
    goal : 
      Embedding-gap⁺ (Embedding-gap _≼_) (star-helper m (node i (t ∷ ts))) 
        (star-helper m (node j (u ∷ us))) →
      Embedding-gap⁺ _≼_ (node i (t ∷ ts)) (node j (u ∷ us))
    goal h
      with ≤-<-connex (toℕ i) (toℕ m) in eq[i] | ≤-<-connex (toℕ j) (toℕ m) in eq[j]
    goal (leaf h) | inj₁ i≤m | inj₁ j≤m = emb-gap-μ-emb-gap⁺ _≼_ [1] h -- goal (leaf h)
      where
      [1] : head (node i (t ∷ ts)) ≤′ μ (node j (u ∷ us))
      [1]  = ≤′-trans i≤m ineq[μu∷us]
    goal h | inj₁ i≤m | inj₂ j>m = goal₁
      where
      eq[t] : star-helper m (node i (t ∷ ts)) ≡ leaf (node i (t ∷ ts))
      eq[t] = star-helper-≤ m i (t ∷ ts) i≤m

      [1] : ∃[ j′ ] (j ≡ F.suc j′ × 
              star-helper m (node j (u ∷ us)) ≡ 
                node j′ (star-helper m u ∷ star-helper-list m us))
      [1] = star-helper-> m j u us j>m

      j′ = proj₁ [1]

      j≡1+j′ : j ≡ F.suc j′
      j≡1+j′ = proj₁ (proj₂ [1])

      [2] : star-helper m (node j (u ∷ us)) ≡ 
              node j′ (star-helper m u ∷ star-helper-list m us)
      [2] = proj₂ (proj₂ [1])

      h′ : Embedding-gap⁺ (Embedding-gap _≼_) (leaf (node i (t ∷ ts))) 
            (node j′ (star-helper m u ∷ star-helper-list m us))
      h′ rewrite sym j≡1+j′ | sym [2] | eq[j] = h

      goal₁ : Embedding-gap⁺ _≼_ (node i (t ∷ ts)) (node j (u ∷ us))
      goal₁ with h′ 
      ... | pass {u = u₁} _ h₂ h₃ = goal₂
        where
        [3] : ∃[ v ] v elem (u ∷ us) × u₁ ≡ star-helper m v
        [3] = star-helper-list-elem⁻ m (u ∷ us) u₁ h₃

        v = proj₁ [3]

        [4] : v elem (u ∷ us)
        [4] = proj₁ (proj₂ [3])

        [5] : u₁ ≡ star-helper m v
        [5] = proj₂ (proj₂ [3])

        size[v]≤k : size′ v ≤ k
        size[v]≤k = ≤-trans (elem-size′-≤ [4]) size[u∷us]≤k

        [6] : Embedding-gap⁺ (Embedding-gap _≼_) (leaf (node i (t ∷ ts))) 
                (star-helper m v)
        [6] rewrite sym [5] = h₂

        [7] : Embedding-gap⁺ (Embedding-gap _≼_) (star-helper m (node i (t ∷ ts))) 
                (star-helper m v)
        [7] rewrite eq[t] = [6]

        goal₂ : Embedding-gap⁺ _≼_ (node i (t ∷ ts)) (node j (u ∷ us))
        goal₂ with μ v in eq[μv]
        ... | just m₁ = pass [15] [14] [4]
          where
          [8] : ∃[ l ] μ-list (u ∷ us) ≡ just l
          [8] = elem-μ-list-just eq[μv] [4]

          l = proj₁ [8]

          eq[μu∷us] : μ-list (u ∷ us) ≡ just l
          eq[μu∷us] = proj₂ [8]

          [9] : μ-list (u ∷ us) ≤′ just m₁
          [9] = elem-μ-list-≤-μ eq[μv] [4]

          [10] : just l ≤′ just m₁
          [10] = ≤′-trans (≤′-reflexive (sym eq[μu∷us])) [9]

          [11] : (just j ⊓′ just l) ≤′ just l
          [11] = ⊓′-≤′₂ j l

          [12] : μ (node j (u ∷ us)) ≤′ just l
          [12] = subst (λ z → (just j ⊓′ z) ≤′ just l) (sym eq[μu∷us]) [11]

          [13] : just m ≤′ just l
          [13] = ≤′-trans ineq[μu∷us] [12]

          ineq[μv] : just m ≤′ μ v
          ineq[μv] rewrite eq[μv] = ≤′-trans [13] [10]

          [14] : Embedding-gap⁺ _≼_ (node i (t ∷ ts)) v
          [14] = embed-star-helper-Embed-just m (node i (t ∷ ts)) v k size[v]≤k 
                  ineq[μt∷ts] ineq[μv] [7]

          [15] : head (node i (t ∷ ts)) ≤′ just j
          [15] = ≤-trans i≤m (<⇒≤ j>m)
        ... | nothing = ⊥-elim contra
          where
          [16] : ∃[ a ] v ≡ leaf a
          [16] = μ-nothing v eq[μv]

          a = proj₁ [16]

          eq[v] : v ≡ leaf a
          eq[v] = proj₂ [16]

          [17] : star-helper m (leaf a) ≡ leaf (leaf a)
          [17] = refl

          [18] : star-helper m v ≡ leaf (leaf a)
          [18] = trans (cong (star-helper m) eq[v]) [17]

          [19] : Embedding-gap⁺ (Embedding-gap _≼_) (leaf (node i (t ∷ ts))) (leaf (leaf a))
          [19] rewrite sym [18] = [6]

          contra : ⊥
          contra with [19]
          ... | leaf (mk ())
    goal h | inj₂ i>m | inj₁ j≤m = ⊥-elim contra
      where
      [1] : ∃[ i′ ] (i ≡ F.suc i′ × 
              star-helper m (node i (t ∷ ts)) ≡ 
                node i′ (star-helper m t ∷ star-helper-list m ts))
      [1] = star-helper-> m i t ts i>m

      i′ = proj₁ [1]

      i≡1+i′ : i ≡ F.suc i′
      i≡1+i′ = proj₁ (proj₂ [1])

      [2] : star-helper m (node i (t ∷ ts)) ≡ 
              node i′ (star-helper m t ∷ star-helper-list m ts)
      [2] = proj₂ (proj₂ [1])

      h′ : Embedding-gap⁺ (Embedding-gap _≼_) 
            (node i′ (star-helper m t ∷ star-helper-list m ts)) (leaf (node j (u ∷ us))) 
      h′ rewrite sym [2] | eq[i] = h

      contra : ⊥
      contra with h′
      ... | ()
    goal h | inj₂ i>m | inj₂ j>m = goal₁
      where
      [1] : ∃[ i′ ] (i ≡ F.suc i′ × 
              star-helper m (node i (t ∷ ts)) ≡ 
                node i′ (star-helper m t ∷ star-helper-list m ts))
      [1] = star-helper-> m i t ts i>m

      i′ = proj₁ [1]

      i≡1+i′ : i ≡ F.suc i′
      i≡1+i′ = proj₁ (proj₂ [1])

      [2] : star-helper m (node i (t ∷ ts)) ≡ 
              node i′ (star-helper m t ∷ star-helper-list m ts)
      [2] = proj₂ (proj₂ [1])

      [3] : ∃[ j′ ] (j ≡ F.suc j′ × 
              star-helper m (node j (u ∷ us)) ≡ 
              node j′ (star-helper m u ∷ star-helper-list m us))
      [3] = star-helper-> m j u us j>m

      j′ = proj₁ [3]

      j≡1+j′ : j ≡ F.suc j′
      j≡1+j′ = proj₁ (proj₂ [3])

      [4] : star-helper m (node j (u ∷ us)) ≡ node j′ (star-helper m u ∷ star-helper-list m us)
      [4] = proj₂ (proj₂ [3])

      h′ : Embedding-gap⁺ (Embedding-gap _≼_) 
            (node i′ (star-helper m t ∷ star-helper-list m ts)) 
            (node j′ (star-helper m u ∷ star-helper-list m us))
      h′ rewrite sym [2] | sym [4] | eq[i] | eq[j] = h

      goal₁ : Embedding-gap⁺ _≼_ (node i (t ∷ ts)) (node j (u ∷ us))
      goal₁ with j′ in eq[j′] | h′
      ... | j′′ | pass {u = u₁} h₁ h₂ h₃ = goal₂
        where
        [5] : ∃[ v ] v elem (u ∷ us) × u₁ ≡ star-helper m v
        [5] = star-helper-list-elem⁻ m (u ∷ us) u₁ h₃

        v = proj₁ [5]

        [6] : v elem (u ∷ us)
        [6] = proj₁ (proj₂ [5])

        [7] : u₁ ≡ star-helper m v
        [7] = proj₂ (proj₂ [5])

        size[v]≤k : size′ v ≤ k
        size[v]≤k = ≤-trans (elem-size′-≤ [6]) size[u∷us]≤k

        [8] : Embedding-gap⁺ (Embedding-gap _≼_) 
                (node i′ (star-helper m t ∷ star-helper-list m ts)) (star-helper m v)
        [8] rewrite sym [7] = h₂

        [9] : Embedding-gap⁺ (Embedding-gap _≼_) 
                (star-helper m (node i (t ∷ ts))) (star-helper m v)
        [9] rewrite [2] = [8]

        goal₂ : Embedding-gap⁺ _≼_ (node i (t ∷ ts)) (node j (u ∷ us))
        goal₂ with μ v in eq[μv]
        ... | just m₁ = pass [17] [16] [6]
          where
          [10] : ∃[ l ] μ-list (u ∷ us) ≡ just l
          [10] = elem-μ-list-just eq[μv] [6]

          l = proj₁ [10]

          eq[μu∷us] : μ-list (u ∷ us) ≡ just l
          eq[μu∷us] = proj₂ [10]

          [11] : μ-list (u ∷ us) ≤′ just m₁
          [11] = elem-μ-list-≤-μ eq[μv] [6]

          [12] : just l ≤′ just m₁
          [12] = ≤′-trans (≤′-reflexive (sym eq[μu∷us])) [11]

          [13] : (just j ⊓′ just l) ≤′ just l
          [13] = ⊓′-≤′₂ j l

          [14] : μ (node j (u ∷ us)) ≤′ just l
          [14] = subst (λ z → (just j ⊓′ z) ≤′ just l) (sym eq[μu∷us]) [13]

          [15] : just m ≤′ just l
          [15] = ≤′-trans ineq[μu∷us] [14]

          ineq[μv] : just m ≤′ μ v
          ineq[μv] rewrite eq[μv] = ≤′-trans [15] [12]

          [16] : Embedding-gap⁺ _≼_ (node i (t ∷ ts)) v
          [16] = embed-star-helper-Embed-just m (node i (t ∷ ts)) v k size[v]≤k ineq[μt∷ts] ineq[μv] [9]

          [17] : head (node i (t ∷ ts)) ≤′ just j
          [17] rewrite sym eq[j′] = 
                ≤-trans (≤-reflexive (cong toℕ i≡1+i′)) (≤-trans (s≤s h₁) 
                        (≤-reflexive (sym (cong toℕ j≡1+j′))))
        ... | nothing = ⊥-elim contra
          where
          [18] : ∃[ a ] v ≡ leaf a
          [18] = μ-nothing v eq[μv]

          a = proj₁ [18]

          eq[v] : v ≡ leaf a
          eq[v] = proj₂ [18]

          [19] : star-helper m (leaf a) ≡ leaf (leaf a)
          [19] = refl

          [20] : star-helper m v ≡ leaf (leaf a)
          [20] = trans (cong (star-helper m) eq[v]) [19]

          [21] : Embedding-gap⁺ (Embedding-gap _≼_) 
                  (node i′ (star-helper m t ∷ star-helper-list m ts)) (leaf (leaf a))
          [21] rewrite sym [20] = [8]

          contra : ⊥
          contra with [21]
          ... | ()
      ... | .i′ | match .i′ h₁ = [6] i≡j
        where
        [5] : F.suc i′ ≡ F.suc j′
        [5] = cong F.suc (sym eq[j′])

        i≡j : i ≡ j
        i≡j = trans i≡1+i′ (trans [5] (sym j≡1+j′))

        [6] : i ≡ j → -- Embedding-gap⁺-list _≼_ (t ∷ ts) (u ∷ us) →
              Embedding-gap⁺ _≼_ (node i (t ∷ ts)) (node j (u ∷ us))
        [6] refl with μ-list (t ∷ ts) in eq[μt∷ts] | μ-list (u ∷ us) in eq[μu∷us]
        ... | just l₁ | just l₂ = 
          match i (embed-star-helper-list-Embed-just m (t ∷ ts) (u ∷ us) k size[u∷us]≤k [8] [10] h₁)
          where
          [7] : just m ≤′ just l₁ 
          [7] = ≤′-trans ineq[μt∷ts] (⊓′-≤′₂ i l₁)

          [8] : just m ≤′ μ-list (t ∷ ts)
          [8] = ≤′-trans [7] (≤′-reflexive (sym eq[μt∷ts]))

          [9] : just m ≤′ just l₂ 
          [9] = ≤′-trans ineq[μu∷us] (⊓′-≤′₂ i l₂)

          [10] : just m ≤′ μ-list (u ∷ us)
          [10] = ≤′-trans [9] (≤′-reflexive (sym eq[μu∷us]))
        ... | just l₁ | nothing = 
          ⊥-elim (embed-star-helper-list-just-nothing m l₁ (t ∷ ts) (u ∷ us) eq[μt∷ts] eq[μu∷us] h₁)
        ... | nothing | _       = 
          match i (embed-star-helper-list-Embed-nothing m (t ∷ ts) (u ∷ us) eq[μt∷ts] h₁)

  embed-star-helper-list-Embed-just m [] us _ _ _ _ h = embedding-gap⁺-list-[] _≼_  us
  embed-star-helper-list-Embed-just m (t ∷ ts) us zero size[us]≤0 ineq[μt∷ts] ineq[μus] h = 
    ⊥-elim (1≰0 1≤0)
    where
    [1] : 1 ≤ size-list′ us
    [1] = size-list′≥1 us

    1≤0 : 1 ≤ zero
    1≤0 = ≤-trans [1] size[us]≤0

    1≰0 : ¬ 1 ≤ zero
    1≰0 ()
  embed-star-helper-list-Embed-just m (t ∷ ts) (u ∷ us) 
    (suc k) size[u∷us]≤1+k ineq[μt∷ts] ineq[μu∷us] (.(star-helper m u) ∷ʳ h) = 
    goal
    where
    [1] : ∃[ m₁ ] μ-list (t ∷ ts) ≡ just m₁
    [1] = ≤′-just-just m (μ-list (t ∷ ts)) ineq[μt∷ts]

    m₁ = proj₁ [1]

    eq[μt∷ts] : μ-list (t ∷ ts) ≡ just m₁
    eq[μt∷ts] = proj₂ [1]

    [2] : ∃[ m₂ ] μ-list (u ∷ us) ≡ just m₂
    [2] = ≤′-just-just m (μ-list (u ∷ us)) ineq[μu∷us]

    m₂ = proj₁ [2]

    eq[μu∷us] : μ-list (u ∷ us) ≡ just m₂
    eq[μu∷us] = proj₂ [2]

    goal : Embedding-gap⁺-list _≼_ (t ∷ ts) (u ∷ us)
    goal with μ-list us in eq[μus]
    ... | just m₂ = 
      u ∷ʳ embed-star-helper-list-Embed-just m (t ∷ ts) us k size[us]≤k 
      ineq[μt∷ts] (≤′-trans [3] (≤′-reflexive (sym eq[μus]))) h
      where
      size[us]≤k : size-list′ us ≤ k
      size[us]≤k = ≤-pred (≤-trans (tail-size-list′-< u us) size[u∷us]≤1+k)

      [3] : just m ≤′ just m₂
      [3] = ≤′-trans ineq[μu∷us] (⊓′-≤′₄ (μ u) m₂)
    ... | nothing = ⊥-elim (embed-star-helper-list-just-nothing m m₁ (t ∷ ts) us eq[μt∷ts] eq[μus] h)
  embed-star-helper-list-Embed-just m (t ∷ ts) (u ∷ us) (suc k) size[u∷us]≤1+k ineq[μt∷ts] ineq[μu∷us] (h₁ ∷ h₂) = 
    subgoal₁ ∷ subgoal₂
    where
    -- size[u]≤1+k : size u ≤ suc k
    -- size[u]≤1+k = ≤-trans (m≤m+n (size u) (size-list us)) size[u∷us]≤1+k

    size[u]≤k : size′ u ≤ k
    size[u]≤k = ≤-pred (≤-trans (head-size′-< u us) size[u∷us]≤1+k)

    subgoal₁ : Embedding-gap⁺ _≼_ t u
    subgoal₁ with μ t in eq[μt] | μ u in eq[μu]
    ... | just n₁ | just n₂ = embed-star-helper-Embed-just m t u k size[u]≤k ineq[μt] ineq[μu] h₁ -- (suc k) size[u]≤1+k
      where
      ineq[μt] : just m ≤′ μ t
      ineq[μt] rewrite eq[μt] = ≤′-trans ineq[μt∷ts] (⊓′-≤′₃ n₁ (μ-list ts))

      ineq[μu] : just m ≤′ μ u
      ineq[μu] rewrite eq[μu] = ≤′-trans ineq[μu∷us] (⊓′-≤′₃ n₂ (μ-list us))
    ... | just n₁ | nothing = 
      ⊥-elim (embed-star-helper-just-nothing m n₁ t u eq[μt] eq[μu] h₁)
    ... | nothing | _       = subst (λ z → Embedding-gap⁺ _≼_ z u) (sym eq[t]) [6]
      where
      [4] : ∃[ a ] t ≡ leaf a
      [4] = μ-nothing t eq[μt]

      a = proj₁ [4]

      eq[t] : t ≡ leaf a
      eq[t] = proj₂ [4]

      [5] : Embedding-gap⁺ (Embedding-gap _≼_) (star-helper m (leaf a)) (star-helper m u)
      [5] = subst (λ z → Embedding-gap⁺ (Embedding-gap _≼_) (star-helper m z) 
              (star-helper m u)) eq[t] h₁

      [6] : Embedding-gap⁺ _≼_ (leaf a) u
      [6] = embed-star-helper-Embed-nothing m a u (size u) ≤-refl [5]

    subgoal₂ : Embedding-gap⁺-list _≼_ ts us
    subgoal₂ with μ-list ts in eq[μts] | μ-list us in eq[μus]
    ... | just o₁ | just o₂ = 
      embed-star-helper-list-Embed-just m ts us k size[us]≤k ineq[μts] ineq[μus] h₂
      where
      size[us]≤k : size-list′ us ≤ k
      size[us]≤k = ≤-pred (≤-trans (tail-size-list′-< u us) size[u∷us]≤1+k)

      ineq[μts] : just m ≤′ μ-list ts
      ineq[μts] rewrite eq[μts] = ≤′-trans ineq[μt∷ts] (⊓′-≤′₄ (μ t) o₁)

      ineq[μus] : just m ≤′ μ-list us
      ineq[μus] rewrite eq[μus] = ≤′-trans ineq[μu∷us] (⊓′-≤′₄ (μ u) o₂)
    ... | just o₁ | nothing = 
      ⊥-elim (embed-star-helper-list-just-nothing m o₁ ts us {ts≢[]} eq[μts] eq[μus] h₂)
      where
      ts≢[] : Nonempty ts
      ts≢[] = μ-list-just-nonempty eq[μts]
    ... | nothing | _ = embed-star-helper-list-Embed-nothing m ts us eq[μts] h₂

The statement of Lemma 4.5:

  embed-star-Embed : (t u : Tree A (suc n)) → μ t ≡ μ u →
    Embedding-gap⁺ (Embedding-gap _≼_) (star t) (star u) →
    Embedding-gap⁺ _≼_ t u

  embed-star-Embed t u eq h with μ t in eq[μt]
  ... | just m  = 
    embed-star-helper-Embed-just m t u (size′ u) ≤-refl 
      (≤′-reflexive (sym eq[μt])) (≤′-reflexive eq) [2]
    where
    [1] : star u ≡ star-helper m u
    [1] = star-just m u (sym eq)

    [2] : Embedding-gap⁺ (Embedding-gap _≼_) (star-helper m t) (star-helper m u)
    [2] rewrite [1] = h
  ... | nothing = embed-star-Embed-nothing t u eq[μt] (sym eq) [2]
    where
    [1] : star t ≡ leaf t
    [1] = star-nothing t eq[μt]

    [2] : Embedding-gap⁺ (Embedding-gap _≼_) (star t) (star u)
    [2] rewrite [1] = h

Definition of the conditions on n that are used in (my variants of) Lemmas 4.6 and 4.7.

Gap⁺ n means that for every A equipped with a binary relarion ≼ and for every sequence f of trees in Tree A n, if every sequence related to f by IsLeaf term by term is very good with respect to ≼, then f is very good with respect to Embedding-gap⁺ ≼. We first need a lemma about subsequences and the IsLeaf relation.

equiv-Sub-IsLeaf :
  (g : ℕ → A) (f : ℕ → Tree A n) → 
  Sub IsLeaf f g → 
  Σ[ g′ ∈ (ℕ → A) ] (TermByTerm IsLeaf g′ f × 
                     Σ[ r ∈ (ℕ → ℕ) ] (Increasing _<_ r × ((x : ℕ) → g′ (r x) ≡ g x)))
equiv-Sub-IsLeaf g f h = equiv-Sub IsLeaf f g h (λ i → isLeaf-nonempty (f i))

subseq-leaf-veryGood : {A : Set} (_≼_ : A → A → Set)
  (f : ℕ → Tree A n) →
  ((g : ℕ → A) → TermByTerm IsLeaf g f → VeryGood _≼_ g) →
  (g : ℕ → A) →
  Sub IsLeaf f g →
  VeryGood _≼_ g
subseq-leaf-veryGood {A = A} _≼_ f h g (r , r-increasing , h₁) = [5]
  where
  w : Σ[ g′ ∈ (ℕ → A) ] (TermByTerm IsLeaf g′ f × 
                         Σ[ r₁ ∈ (ℕ → ℕ) ] (Increasing _<_ r₁ × ((x : ℕ) → g′ (r₁ x) ≡ g x)))
  w = equiv-Sub-IsLeaf g f (r , r-increasing , h₁)

  g′ : ℕ → A
  g′ = proj₁ w

  [2] : TermByTerm IsLeaf g′ f
  [2] = proj₁ (proj₂ w)

  r₁ : ℕ → ℕ
  r₁ = proj₁ (proj₂ (proj₂ w))

  r₁-increasing : Increasing _<_ r₁
  r₁-increasing = proj₁ (proj₂ (proj₂ (proj₂ w)))

  g′∘r≗g : (x : ℕ) → g′ (r x) ≡ g x
  g′∘r≗g = proj₂ (proj₂ (proj₂ (proj₂ w)))

  [3] : VeryGood _≼_ g′
  [3] = h g′ [2]

  [4] : VeryGood _≼_ (g′ ∘ r₁)
  [4] = subseq-veryGood _≼_ g′ r₁ [3] r₁-increasing

  [5] : VeryGood _≼_ g
  [5] = veryGood-extensional {_≼_ = _≼_} (g′ ∘ r₁) g g′∘r≗g [4]


Gap⁺-good : ℕ → Set₁
Gap⁺-good n = {A : Set} (_≼_ : A → A → Set) (f : ℕ → Tree A n) →
  ((g : ℕ → A) → TermByTerm IsLeaf g f → VeryGood _≼_ g) →
  Good (Embedding-gap⁺ _≼_) f

Gap⁺ : ℕ → Set₁
Gap⁺ n = {A : Set} (_≼_ : A → A → Set) (f : ℕ → Tree A n) →
  ((g : ℕ → A) → TermByTerm IsLeaf g f → VeryGood _≼_ g) →
  VeryGood (Embedding-gap⁺ _≼_) f

gap⁺-good⇒gap⁺ : (n : ℕ) → Gap⁺-good n → Gap⁺ n 
gap⁺-good⇒gap⁺ n gap⁺-good {A = A} _≼_ f h r r-increasing = gap⁺-good _≼_ (f ∘ r) [1]
  where
  [1] : (g : ℕ → A) → TermByTerm IsLeaf g (f ∘ r) → VeryGood _≼_ g
  [1] g h₁ = subseq-leaf-veryGood _≼_ f h g (r , r-increasing , h₁)

Gap-suc n means that for every A equipped with a binary relation ≼ on A and every infinite sequence f of trees in Tree A (suc n), if every sequence related to f by IsLeaf term by term is very good with respect to ≼, then f is very good with respect to Embedding-gap ≼.

Gap-suc-good : ℕ → Set₁
Gap-suc-good n = {A : Set} (_≼_ : A → A → Set) (f : ℕ → Tree A (suc n)) →
  ((g : ℕ → A) → TermByTerm IsLeaf g f → VeryGood _≼_ g) →
  Good (Embedding-gap _≼_) f

Gap-suc : ℕ → Set₁
Gap-suc n = {A : Set} (_≼_ : A → A → Set) (f : ℕ → Tree A (suc n)) →
  ((g : ℕ → A) → TermByTerm IsLeaf g f → VeryGood _≼_ g) →
  VeryGood (Embedding-gap _≼_) f

gap-suc-good⇒gap-suc : (n : ℕ) → Gap-suc-good n → Gap-suc n 
gap-suc-good⇒gap-suc n gap-suc-good {A = A} _≼_ f h r r-increasing = 
  gap-suc-good _≼_ (f ∘ r) [1]
  where
  [1] : (g : ℕ → A) → TermByTerm IsLeaf g (f ∘ r) → VeryGood _≼_ g
  [1] g h₁ = subseq-leaf-veryGood _≼_ f h g (r , r-increasing , h₁)

Lemma 4.6

gap-suc-gap⁺⇒gap⁺-suc : (n : ℕ) → Gap-suc n → Gap⁺ n → Gap⁺ (suc n) 
gap-suc-gap⁺⇒gap⁺-suc n gap-suc-n gap⁺-n = 
  gap⁺-good⇒gap⁺ (suc n) gap⁺-good-suc-n
  where
  gap⁺-good-suc-n : Gap⁺-good (suc n)
  gap⁺-good-suc-n {A} _≼_ f h = i , j , i<j , [10]
    where
    [1] : (l : ℕ → Tree A (suc n)) → TermByTerm IsLeaf l (star ∘ f) → 
          VeryGood (Embedding-gap _≼_) l
    [1] l h₁ = gap-suc-n _≼_ l [2]
      where
      [2] : (l′ : ℕ → A) → TermByTerm IsLeaf l′ l → VeryGood _≼_ l′
      [2] l′ h₂ = h l′ [3]
        where
        [3] : TermByTerm IsLeaf l′ f
        [3] i = proj₂ (isLeaf⇔IsLeaf-IsLeaf-star (f i) (l′ i)) (l i , h₂ i , h₁ i)

    [4] : VeryGood (Embedding-gap⁺ (Embedding-gap _≼_)) (star ∘ f)
    [4] = gap⁺-n (Embedding-gap _≼_) (star ∘ f) [1]

    p = prodOrder (_≡_ {A = Maybe (Fin (suc n))}) 
          (Embedding-gap⁺ {n = n} (Embedding-gap {n = suc n} _≼_))

    [5] : VeryGood (_≡_ {A = Maybe (Fin (suc n))}) (μ ∘ f)
    [5] = almostFull-veryGood _≡_ (μ ∘ f) MaybeFin-≡.almostFull

    [6] : VeryGood p (prodSeq (μ ∘ f) (star ∘ f))
    [6] = prod-veryGood {_≼₁_ = _≡_ {A = Maybe (Fin (suc n))}} 
            {_≼₂_ = Embedding-gap⁺ (Embedding-gap _≼_)} {f = μ ∘ f} {g = star ∘ f} [5] [4]

    [7] : Good p (prodSeq (μ ∘ f) (star ∘ f))
    [7] = veryGood⇒good p (prodSeq (μ ∘ f) (star ∘ f)) [6]

    i = proj₁ [7]
    j = proj₁ (proj₂ [7])
    i<j = proj₁ (proj₂ (proj₂ [7]))
    
    [8] : Embedding-gap⁺ (Embedding-gap _≼_) (star (f i)) (star (f j))
    [8] = proj₂ (proj₂ (proj₂ (proj₂ [7])))

    [9] : (μ ∘ f) i ≡ (μ ∘ f) j
    [9] = proj₁ (proj₂ (proj₂ (proj₂ [7])))

    [10] : Embedding-gap⁺ _≼_ (f i) (f j)
    [10] = embed-star-Embed (f i) (f j) [9] [8]

Lemma 4.7

gap⁺⇒gap-suc : (n : ℕ) → Gap⁺ n → Gap-suc n
gap⁺⇒gap-suc n gap⁺-n = gap-suc-good⇒gap-suc n gap-suc-good
  where
  gap-suc-good : Gap-suc-good n
  gap-suc-good {A} _≼_ f h = ¬¬-elim f-notBad
    where
    f-notBad : ¬ (¬ Good (Embedding-gap _≼_) f)
    f-notBad f-bad = mbs-bad mbs-good
      where
      open MBS {A = Tree A (suc n)} size (Embedding-gap _≼_) _⊑_ ⊑-refl {f = f} f-bad hiding (_⊏_)

We let f be a sequence such that every sequence that is related to it term by term by IsLeaf is very good. Supposing f is bad, mbs is the minimal bad sequence constructed from f. This sequence is related term by term to some subsequence of f by the subtree relation. We will show that mbs is in fact good. This contradiction refutes the hypothesis that f is bad.

Every sequence g that is related to mbs term by term by the IsLeaf relation is very good.

      [1] : (g : ℕ → A) → TermByTerm IsLeaf g mbs → VeryGood _≼_ g
      [1] g h₁ = [3] g ([2] g h₁)
        where
        s : ℕ → ℕ
        s = proj₁ (mbs-sub-⊑)

        s-increasing : Increasing _<_ s
        s-increasing = proj₁ (proj₂ mbs-sub-⊑)

        [2] : (g : ℕ → A) → TermByTerm IsLeaf g mbs → TermByTerm IsLeaf g (f ∘ s)
        [2] g h₂ i = ⊑-IsLeaf-⊆ (proj₂ (proj₂ mbs-sub-⊑) i) (h₂ i)

        [3] : (g : ℕ → A) → TermByTerm IsLeaf g (f ∘ s) → VeryGood _≼_ g
        [3] g h₃ = subseq-leaf-veryGood _≼_ f h g (s , s-increasing , h₃)

Either there are infinitely many terms of mbs that are size 1 trees, or there are only finitely many of them. Supposing the former leads to a contradiction, so the latter must be the case.

      -- reasoning by cases
      Inf = (k : ℕ) → Σ[ l ∈ ℕ ] k < l × size (mbs l) ≡ 1

      [4] : Inf ⊎ Σ[ k ∈ ℕ ] ((l : ℕ) → k < l → size (mbs l) ≢ 1)
      [4] = infinite∨finite (λ i → size (mbs i) ≡ 1)

      [5] : Inf → ⊥
      [5] inf = contra
        where
        k = proj₁ (inf zero)
        r : ℕ → ℕ
        r zero = k
        r (suc x) = proj₁ (inf (r x))
        r-step : (i : ℕ) → r i < r (suc i)
        r-step i = proj₁ (proj₂ (inf (r i)))
        r-increasing : Increasing _<_ r
        r-increasing = step-increasing r r-step
        [6] : (i : ℕ) → ∃[ a ] mbs (r i) ≡ leaf a
        [6] zero = size≡1 (mbs k) (proj₂ (proj₂ (inf zero)))
        [6] (suc i) = size≡1 (mbs (r (suc i))) (proj₂ (proj₂ (inf (r i))))
        g : ℕ → A
        g i = proj₁ ([6] i)
        [7] : TermByTerm IsLeaf g (mbs ∘ r)
        [7] i rewrite proj₂ ([6] i) = here
          
        [8] : Σ[ g′ ∈ (ℕ → A) ] (TermByTerm IsLeaf g′ mbs × 
                Σ[ r₁ ∈ (ℕ → ℕ) ] (Increasing _<_ r₁ × ((x : ℕ) → g′ (r₁ x) ≡ g x)))
        [8] = equiv-Sub-IsLeaf g mbs (r , r-increasing , [7])
        g′ = proj₁ [8]
        [9] : TermByTerm IsLeaf g′ mbs
        [9] = proj₁ (proj₂ [8])
        r₁ : ℕ → ℕ
        r₁ = proj₁ (proj₂ (proj₂ [8]))
        r₁-increasing : Increasing _<_ r₁
        r₁-increasing = proj₁ (proj₂ (proj₂ (proj₂ [8])))
        g′∘r≗g : (x : ℕ) → g′ (r₁ x) ≡ g x
        g′∘r≗g = proj₂ (proj₂ (proj₂ (proj₂ [8])))
        g′-veryGood : VeryGood _≼_ g′
        g′-veryGood = [1] g′ [9]
        g′∘r₁-good : Good _≼_ (g′ ∘ r₁)
        g′∘r₁-good = g′-veryGood r₁ r₁-increasing
        g-good : Good _≼_ g
        g-good = good-extensional {_≼_ = _≼_} (g′ ∘ r₁) g g′∘r≗g g′∘r₁-good
        i = proj₁ g-good
        j = proj₁ (proj₂ g-good)
        i<j : i < j
        i<j = proj₁ (proj₂ (proj₂ g-good))
        g[i]≼g[j] : g i ≼ g j 
        g[i]≼g[j] = proj₂ (proj₂ (proj₂ g-good))
        [10] : Embedding-gap {A = A} {n = suc n} _≼_ (leaf (g i)) (leaf (g j))
        [10] = mk (leaf g[i]≼g[j])
        [11] : Embedding-gap {A = A} {n = suc n} _≼_ (mbs (r i)) (mbs (r j))
        [11] = subst (λ z → Embedding-gap {A = A} {n = suc n} _≼_ z (mbs (r j))) (sym (proj₂ ([6] i))) 
                (subst (λ z → Embedding-gap {A = A} {n = suc n} _≼_ (leaf (g i)) z) (sym (proj₂ ([6] j))) [10])
        contra : ⊥
        contra = mbs-bad (r i , r j , r-increasing i j i<j , [11])

      [12] : Σ[ k ∈ ℕ ] ((l : ℕ) → k < l → size (mbs l) ≢ 1)
      [12] = ⊎-¬ˡ [4] [5]

So all but finitely many terms of mbs are of size ≢ 1. Let k be such that for all l > k, the lth term of mbs is of size ≢ 1.

      k = proj₁ [12]

      cof : (l : ℕ) → k < l → 1 < size (mbs l)
      cof l k<l = ≤∧≢⇒< (size≥1 (mbs l)) (λ z → proj₂ [12] l k<l (sym z))

So for all l > k, the lth term of mbs is of size > 1, meaning that those terms are of the form node i ts. Let g be the sequence of lists of trees consisting of the immediate subtrees of the root of those trees. Let mbs′ be the sequence obtained from mbs by dropping the first k terms, and g be the sequence consisting of the list of immediate subtrees of the root of each term of mbs′.

      mbs′ : ℕ → Tree A (suc n)
      mbs′ l = mbs (l + (1 + k))

      g-helper : (l : ℕ) → ∃₂ (λ i ts → ∃[ ts≢[] ] mbs′ l ≡ node i ts {ts≢[]})
      g-helper l = size>1 (mbs′ l) ineq
        where
        ineq : 1 < size (mbs′ l)
        ineq = cof (l + (1 + k)) ((m≤n+m (1 + k)) l) 

      g : ℕ → List (Tree A (suc n))
      g l = proj₁ (proj₂ (g-helper l))

      g-nonempty : (l : ℕ) → Nonempty (g l)
      g-nonempty l = proj₁ (proj₂ (proj₂ (g-helper l)))

      mbs′-root : ℕ → Fin (suc n)
      mbs′-root l = proj₁ (g-helper l)

      mbs′-g : (l : ℕ) → mbs′ l ≡ node (mbs′-root l) (g l) {g-nonempty l}
      mbs′-g l = proj₂ (proj₂ (proj₂ (g-helper l)))

We want to show that g is very good w.r.t.

Embedding-gap-list {A = A} {n = suc n} _≼_

By Higman’s lemma, it suffices to show that every sequence that is related to g term by term by _elem_ is very good w.r.t.

Embedding-gap⁺ {A = A} {n = suc n} _≼_

Let g₁ be such a sequence.

      [13] : (g₁ : ℕ → Tree A (suc n)) → TermByTerm _elem_ g₁ g →
             VeryGood (Embedding-gap⁺ {A = A} {n = suc n} _≼_) g₁
      [13] g₁ g₁-elem-g = g₁-veryGood-emb-gap⁺-suc
        where
        g₁-⊏-mbs′ : (l : ℕ) → g₁ l ⊏ mbs′ l
        g₁-⊏-mbs′ l = 
          subst (g₁ l ⊏_) (sym (mbs′-g l)) 
                (immediate-subtree-⊏ (mbs′-root l) (g l) (g₁ l) (g₁-elem-g l))

        open Sub-⊑-⊏ ⊏-size-< (emb-gap-⊑-emb-gap _≼_) ⊑-transitive

        g₁∈Sub-⊏-mbs : g₁ ∈ Sub _⊏_ mbs
        g₁∈Sub-⊏-mbs = r , r-increasing , g₁-⊏-mbs′
          where
          r : ℕ → ℕ
          r i = i + (1 + k)
          r-increasing : Increasing _<_ r
          r-increasing m n m<n = +-monoˡ-< (1 + k) m<n

        g₁* : ℕ → Tree (Tree A (suc n)) n
        g₁* i = star (g₁ i)

We can use the hypothesis that Gap⁺ n holds to show that g₁* is very good w.r.t.

Embedding-gap⁺ {A = Tree A (suc n)} {n = n} (Embedding-gap {A = A} {n = suc n} _≼_)

        [16] : (g₂ : ℕ → Tree A (suc n)) → TermByTerm IsLeaf g₂ g₁* →
               VeryGood (Embedding-gap {A = A} {n = suc n} _≼_) g₂
        [16] g₂ h₁ = Sub-⊏-mbs⇒VeryGood g₂ [17]
          where
          [17] : g₂ ∈ Sub _⊏_ mbs
          [17] = (_+ (1 + k)) , (λ _ _ → +-monoˡ-< (1 + k)) , λ i → ⊑-⊏-⊏ (isLeaf-star⇒⊑ (g₁ i) (g₂ i) (h₁ i)) (g₁-⊏-mbs′ i)

        g₁*-veryGood-emb-gap⁺ : 
          VeryGood (Embedding-gap⁺ {A = Tree A (suc n)} {n = n} (Embedding-gap {A = A} {n = suc n} _≼_)) g₁*
        g₁*-veryGood-emb-gap⁺ = 
          gap⁺-n {A = Tree A (suc n)} (Embedding-gap {A = A} {n = suc n} _≼_) g₁* [16]

We are now going to use Lemma 4.5 to show that g₁ is very good w.r.t.

Embedding-gap⁺ {A = A} {n = suc n} _≼_

        p = prodOrder (_≡_ {A = Maybe (Fin (suc n))})
              (Embedding-gap⁺ {A = Tree A (suc n)} {n = n} (Embedding-gap {A = A} {n = suc n} _≼_))

        seq = prodSeq (μ ∘ g₁) g₁*

        μ∘g₁,g₁*-veryGood-emb-gap+ : VeryGood p seq -- (λ i → μ (g₁ i) , g₁* i)
        μ∘g₁,g₁*-veryGood-emb-gap+ = 
          prod-veryGood 
            {_≼₁_ = _≡_}
            {_≼₂_ = Embedding-gap⁺ {A = Tree A (suc n)} {n = n} (Embedding-gap {A = A} {n = suc n} _≼_)} 
            {f = μ ∘ g₁} {g = g₁*}
            (almostFull-veryGood {A = Maybe (Fin (suc n))} _≡_ (μ ∘ g₁) MaybeFin-≡.almostFull) 
            g₁*-veryGood-emb-gap⁺

        g₁-veryGood-emb-gap⁺-suc : VeryGood (Embedding-gap⁺ {A = A} {n = suc n} _≼_) g₁
        g₁-veryGood-emb-gap⁺-suc r r-increasing = 
          i , j , i<j , (embed-star-Embed (g₁ (r i)) (g₁ (r j)) [18] [19])
          where
          seq∘r-good : Good p (seq ∘ r)
          seq∘r-good = μ∘g₁,g₁*-veryGood-emb-gap+ r r-increasing
          i j : ℕ
          i = proj₁ seq∘r-good
          j = proj₁ (proj₂ seq∘r-good)
          i<j : i < j
          i<j = proj₁ (proj₂ (proj₂ seq∘r-good))
          [18] : μ (g₁ (r i)) ≡ μ (g₁ (r j))
          [18] = proj₁ (proj₂ (proj₂ (proj₂ seq∘r-good)))
          [19] : Embedding-gap⁺ {A = Tree A (suc n)} {n = n} 
                              (Embedding-gap {A = A} {n = suc n} _≼_) (g₁* (r i)) (g₁* (r j))
          [19] = proj₂ (proj₂ (proj₂ (proj₂ seq∘r-good)))

It’s now time to invoke Higman’s lemma to show that g is very good w.r.t.

Embedding-gap⁺-list {A = A} {n = suc n} _≼_

What we just established

[13] : (g₁ : ℕ → Tree A (suc n)) → TermByTerm _elem_ g₁ g →
       VeryGood (Embedding-gap⁺ {A = A} {n = suc n} _≼_) g₁

does not quite fit the hypothesis of Higman’s lemma as we stated it, though it’s certainly sufficient.

      g-veryGood-Higman-emb-gap⁺ : 
        VeryGood (H.Embedding (Embedding-gap⁺ {A = A} {n = suc n} _≼_)) g
      g-veryGood-Higman-emb-gap⁺ = 
        H.sub-elem-veryGood-veryGood (Embedding-gap⁺ {A = A} {n = suc n} _≼_) g [20]
        where
        [20] : (g₁ : ℕ → Tree A (suc n)) → 
               g₁ ∈ Sub _elem_ g → VeryGood (Embedding-gap⁺ _≼_) g₁
        [20] g₁ g₁-Sub = g₁-veryGood
          where
          [21] : Σ[ g′ ∈ (ℕ → Tree A (suc n)) ] TermByTerm _elem_ g′ g × 
                  Σ[ r ∈ (ℕ → ℕ) ] (Increasing _<_ r × ((x : ℕ) → g′ (r x) ≡ g₁ x))
          [21] = equiv-Sub _elem_ g g₁ g₁-Sub (λ i → nonempty-elem (g-nonempty i))
          
          g′ = proj₁ [21]

          [22] : TermByTerm _elem_ g′ g
          [22] = proj₁ (proj₂ [21])

          g′-veryGood : VeryGood (Embedding-gap⁺ {A = A} {n = suc n } _≼_) g′
          g′-veryGood = [13] g′ [22]

          r = proj₁ (proj₂ (proj₂ [21]))

          r-increasing = proj₁ (proj₂ (proj₂ (proj₂ [21])))

          g′∘r≗g₁ : (x : ℕ) → g′ (r x) ≡ g₁ x
          g′∘r≗g₁ = proj₂ (proj₂ (proj₂ (proj₂ [21])))

          g′∘r-veryGood : VeryGood (Embedding-gap⁺ {A = A} {n = suc n } _≼_) (g′ ∘ r)
          g′∘r-veryGood = 
            subseq-veryGood (Embedding-gap⁺ {A = A} {n = suc n } _≼_) g′ r g′-veryGood r-increasing

          g₁-veryGood : VeryGood (Embedding-gap⁺ {A = A} {n = suc n } _≼_) g₁
          g₁-veryGood = 
            veryGood-extensional {A = Tree A (suc n)}
            {_≼_ = Embedding-gap⁺ {A = A} {n = suc n } _≼_}
            (g′ ∘ r) g₁ g′∘r≗g₁ g′∘r-veryGood

      g-veryGood-emb-gap⁺-suc : VeryGood (Embedding-gap⁺-list {A = A} {n = suc n} _≼_) g
      g-veryGood-emb-gap⁺-suc = 
        veryGood-mono {A = List (Tree A (suc n))} 
        (H.Embedding (Embedding-gap⁺ {A = A} {n = suc n} _≼_)) 
        (Embedding-gap⁺-list {A = A} {n = suc n} _≼_) 
        g [23] g-veryGood-Higman-emb-gap⁺
        where
        [23] : (ts us : List (Tree A (suc n))) → 
               H.Embedding (Embedding-gap⁺ {A = A} {n = suc n} _≼_) ts us →
               Embedding-gap⁺-list {A = A} {n = suc n} _≼_ ts us
        [23] ts us = proj₂ (embedding-gap⁺-Higman _≼_ ts us)

Finally, we use Dickson’s lemma to show that mbs is good.

      p₁ = prodOrder (_≡_ {A = Fin (suc n)})
                    (Embedding-gap⁺-list {A = A} {n = suc n} _≼_)

      seq₁ = prodSeq mbs′-root g

      [24] : VeryGood p₁ seq₁
      [24] = prod-veryGood {_≼₁_ = _≡_} {_≼₂_ = Embedding-gap⁺-list {A = A} {n = suc n} _≼_} 
          {f = mbs′-root}
          {g = g}
          (almostFull-veryGood _≡_ mbs′-root Fin-≡.almostFull)
          g-veryGood-emb-gap⁺-suc
      [25] : Good p₁ seq₁
      [25] = veryGood⇒good p₁ seq₁ [24]
      i j : ℕ
      i = proj₁ [25]
      j = proj₁ (proj₂ [25])
      i<j : i < j
      i<j = proj₁ (proj₂ (proj₂ [25]))
      [26] : p₁ (seq₁ i) (seq₁ j)
      [26] = proj₂ (proj₂ (proj₂ [25]))
      [27] : mbs′-root i ≡ mbs′-root j
      [27] = proj₁ [26]
      [28] : Embedding-gap⁺-list {A = A} {n = suc n} _≼_ (g i) (g j)
      [28] = proj₂ [26]
      [29] : Embedding-gap⁺ {A = A} {n = suc n} _≼_ (mbs (i + (1 + k))) (mbs (j + (1 + k)))
      [29] = subst (λ z → Embedding-gap⁺ {A = A} {n = suc n} _≼_ z (mbs (j + (1 + k)))) (sym (mbs′-g i)) 
              (subst (Embedding-gap⁺ {A = A} {n = suc n} _≼_ (node (mbs′-root i) (g i) {g-nonempty i})) (sym (mbs′-g j)) 
              (subst (λ z → Embedding-gap⁺ {A = A} {n = suc n} _≼_ (node (mbs′-root i) (g i) {g-nonempty i}) (node z (g j) {g-nonempty j})) [27] 
              (match (mbs′-root i) [28])))
      i+1+k<j+1+k : i + (1 + k) < j + (1 + k)
      i+1+k<j+1+k = +-monoˡ-< (1 + k) i<j
      mbs-good : Good (Embedding-gap {A = A} {n = suc n} _≼_) mbs
      mbs-good = (i + (1 + k) , j + (1 + k) , i+1+k<j+1+k , mk [29])

This looks a little weird, since by omitting mk in the last line, you can see that mbs is Good with respect to Embedding-gap⁺ {A = A} {n = suc n} _≼_. Of course, this doesn’t mean that this proof suffices for (n : ℕ) → Gap⁺ n → Gap⁺ (suc n), since we’ve only derived a contradition under the assumption that there is a bad sequence with respect to Embedding-gap {A = A} {n = suc n} _≼_.

Theorem 4.8

gap⁺ : (n : ℕ) → Gap⁺ n
gap-suc : (n : ℕ) → Gap-suc n

gap⁺ zero {A = A} _≼_ f h r r-increasing = goal
  where
  f′ : ℕ → A
  f′ i with f i
  ... | leaf a = a

  [1] : (i : ℕ) → f i ≡ leaf (f′ i)
  [1] i with f i
  ... | leaf a = refl

  [2] : TermByTerm IsLeaf f′ f
  [2] i with f i 
  ... | leaf a = here

  [3] : VeryGood _≼_ f′
  [3] = h f′ [2]

  [4] : Good _≼_ (f′ ∘ r)
  [4] = [3] r r-increasing

  goal : Good (Embedding-gap⁺ _≼_) (f ∘ r)
  goal with [4]
  ... | i , j , i<j , f′∘r[i]≼f′∘r[j] = i , j , i<j , [6]
    where
    [5] : Embedding-gap⁺ {A = A} {n = zero} _≼_ (leaf (f′ (r i))) (leaf (f′ (r j)))
    [5] = leaf f′∘r[i]≼f′∘r[j]

    [6] : Embedding-gap⁺ {A = A} {n = zero} _≼_ (f (r i)) (f (r j))
    [6] = subst (λ z → Embedding-gap⁺ {A = A} {n = zero} _≼_ z (f (r j))) 
            (sym ([1] (r i)))
            (subst (Embedding-gap⁺ {A = A} {n = zero} _≼_ (leaf (f′ (r i)))) (sym ([1] (r j))) [5])
gap⁺ (suc n) = gap-suc-gap⁺⇒gap⁺-suc n (gap-suc n) (gap⁺ n)

gap-suc n = gap⁺⇒gap-suc n (gap⁺ n)

emb-gap⁺-almostFull : {A : Set} (_≼_ : A → A → Set)
  → AlmostFull _≼_
  → (n : ℕ) → AlmostFull {A = Tree A n} (Embedding-gap⁺ {A = A} {n = n} _≼_)
emb-gap⁺-almostFull {A} _≼_ ≼-almostFull n f = 
  veryGood⇒good (Embedding-gap⁺ {A = A} {n = n} _≼_) f [2]
  where
  [1] : (g : ℕ → A) → TermByTerm IsLeaf g f → VeryGood _≼_ g
  [1] g _ = almostFull-veryGood _≼_ g ≼-almostFull

  [2] : VeryGood (Embedding-gap⁺ {A = A} {n = n} _≼_) f
  [2] = gap⁺ n _≼_ f [1]

emb-gap⁺-isWQO : {A : Set} {_≼_ : A → A → Set} → IsWQO _≼_ → (n : ℕ) → 
  IsWQO (Embedding-gap⁺ {A = A} {n = n} _≼_)
emb-gap⁺-isWQO {A} {_≼_} ≼-isWQO n = 
  record
-- a bit inconsistent about when to make an argument implicit
  { isQO        = emb-gap⁺-isQO {n = n} _≼_ (IsWQO.isQO ≼-isWQO)
  ; almostFull  = emb-gap⁺-almostFull _≼_ (IsWQO.almostFull ≼-isWQO) n
  }