General properties of well-quasiorders.

module WQO 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
  using (≤-refl; ≤-trans; <-trans; <-irrefl; m≤n+m; +-monoˡ-<; <-transʳ; <-transˡ; m≤m⊔n; m≤n⊔m; +-assoc; m≤n⇒m≤o+n; m≤n⇒m≤n+o)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂ ; ∃; Σ-syntax; ∃-syntax; ∃₂)
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_]′ to case-⊎)
open import Relation.Nullary using (¬_)
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.Maybe using (Maybe; just; nothing)

open import Miscellaneous

open import Classical

private
  variable
    A B : Set

Reflexive : (A → A → Set) → Set
Reflexive _≼_ = ∀ {x} → x ≼ x

Transitive : (A → A → Set) → Set
Transitive _≼_ = ∀ {x y z} → x ≼ y → y ≼ z → x ≼ z

record IsQO (_≼_ : A → A → Set) : Set where
  field
    reflexive : Reflexive _≼_ -- (x : A) → x ≼ x
    transitive : Transitive _≼_ -- {x y z : A} → x ≼ y → y ≼ z → x ≼ z

open IsQO

Good : (_≼_ : A → A → Set) → (ℕ → A) → Set
Good _≼_ f = ∃₂ (λ i j → i < j × f i ≼ f j)

good-extensional : {_≼_ : A → A → Set} (f g : ℕ → A) → ((n : ℕ) → f n ≡ g n) → 
                   Good _≼_ f → Good _≼_ g
good-extensional {A} {_≼_} f g f≗g (i , j , i<j , f[i]≼f[j]) = i , j , i<j , g[i]≼g[j]
  where
  g[i]≼g[j] : g i ≼ g j
  g[i]≼g[j] rewrite sym (f≗g i) | sym (f≗g j) = f[i]≼f[j]

VeryGood : (_≼_ : A → A → Set) → (ℕ → A) → Set
VeryGood _≼_ f = (r : ℕ → ℕ) → Increasing _<_ r → Good _≼_ (f ∘ r)

veryGood-extensional : {_≼_ : A → A → Set} (f g : ℕ → A)
  → ((n : ℕ) → f n ≡ g n)
  → VeryGood _≼_ f
  ----------------
  → VeryGood _≼_ g
veryGood-extensional {A} {_≼_} f g f≗g f-veryGood r r-increasing = i , j , i<j , g∘r[i]≼g∘r[j]
  where
  h : ∃₂ (λ i j → i < j × f (r i) ≼ f (r j))
  h = f-veryGood r r-increasing
  i = proj₁ h
  j = proj₁ (proj₂ h)
  i<j = proj₁ (proj₂ (proj₂ h))
  f∘r[i]≼f∘r[j] : f (r i) ≼ f (r j)
  f∘r[i]≼f∘r[j] = proj₂ (proj₂ (proj₂ h))
  g∘r[i]≼g∘r[j] : g (r i) ≼ g (r j)
  g∘r[i]≼g∘r[j] = subst (λ z → z ≼ g (r j)) (f≗g (r i)) (subst (λ z → f (r i) ≼ z) (f≗g (r j)) f∘r[i]≼f∘r[j])

veryGood-mono : (_≼₁_ _≼₂_ : A → A → Set) (f : ℕ → A) →
  ((x y : A) → x ≼₁ y → x ≼₂ y) →
  VeryGood _≼₁_ f → VeryGood _≼₂_ f
veryGood-mono _≼₁_ _≼₂_ f h₁ h₂ r r-increasing = i , j , i<j , f∘r[i]≼₂f∘r[j] 
  where
  [1] : Good _≼₁_ (f ∘ r)
  [1] = h₂ r r-increasing
  i j : ℕ
  i = proj₁ [1]
  j = proj₁ (proj₂ [1])
  i<j : i < j
  i<j = proj₁ (proj₂ (proj₂ [1]))
  f∘r[i]≼₁f∘r[j] : f (r i) ≼₁ f (r j)
  f∘r[i]≼₁f∘r[j] = proj₂ (proj₂ (proj₂ [1]))
  f∘r[i]≼₂f∘r[j] : f (r i) ≼₂ f (r j)
  f∘r[i]≼₂f∘r[j] = h₁ (f (r i)) (f (r j)) f∘r[i]≼₁f∘r[j]


veryGood⇒good : (_≼_ : A → A → Set) (f : ℕ → A) → VeryGood _≼_ f → Good _≼_ f
veryGood⇒good _≼_ f f-veryGood = f-veryGood id id-increasing

subseq-veryGood : (_≼_ : A → A → Set) (f : ℕ → A) (r : ℕ → ℕ)
  → VeryGood _≼_ f
  → Increasing _<_ r
  ----------------------
  → VeryGood _≼_ (f ∘ r)
subseq-veryGood _≼_ f r f-veryGood r-increasing r₁ r₁-increasing
  = f-veryGood (r ∘ r₁) r∘r₁-increasing
  where
  r∘r₁-increasing : Increasing _<_ (r ∘ r₁)
  r∘r₁-increasing = subseq-increasing _<_ r r₁ r-increasing r₁-increasing

ClosedUnderSubseq : (P : (ℕ → A) → Set) → Set
ClosedUnderSubseq {A} P = (f : ℕ → A) (r : ℕ → ℕ) → Increasing _<_ r → P f → P (f ∘ r)

lemma-good-veryGood : {_≼_ : A → A → Set} (P : (ℕ → A) → Set)
  → ClosedUnderSubseq P
  → ((f : ℕ → A) → P f → Good _≼_ f)
  → (f : ℕ → A)
  → P f 
  → VeryGood _≼_ f
lemma-good-veryGood P P-closed h f Pf r r-increasing = h (f ∘ r) (P-closed f r r-increasing Pf)

AlmostFull : (_≼_ : A → A → Set) → Set
AlmostFull _≼_ = ∀ f → Good _≼_ f

almostFull-mon : (_≼₁_ _≼₂_ : A → A → Set)
  → ((x y : A) → (x ≼₁ y) → (x ≼₂ y))
  → AlmostFull _≼₁_
  → AlmostFull _≼₂_
almostFull-mon _≼₁_ _≼₂_ h ≼₁-almostFull f with ≼₁-almostFull f
... | i , j , i<j , fi≼₁fj = i , j , i<j , h (f i) (f j) fi≼₁fj

record IsWQO (_≼_ : A → A → Set) : Set where
  field
    isQO : IsQO _≼_
    almostFull : AlmostFull _≼_

open IsWQO

module _ (_≼_ : A → A → Set) where

  module _ (f : ℕ → A) where

    almostFull-veryGood : AlmostFull _≼_ → VeryGood _≼_ f
    almostFull-veryGood h r r-increasing = h (f ∘ r)

    NearTerminal : ℕ → Set
    NearTerminal m = Finite (λ n → f m ≼ f n)
      -- ∃[ k ] ((n : ℕ) → k < n → ¬ f m ≼ f n)

    NonNearTerminal : ℕ → Set
    NonNearTerminal m = Infinite (λ n → f m ≼ f n)
      -- (k : ℕ) → ∃[ n ] (k < n × f m ≼ f n)

    ¬NearTerminal⇒NonNearTerminal : (m : ℕ) → ¬ NearTerminal m → NonNearTerminal m
    ¬NearTerminal⇒NonNearTerminal m h = ¬finite⇒infinite (λ n → f m ≼ f n) h

    ¬NonNearTerminal⇒NearTerminal : (m : ℕ) → ¬ NonNearTerminal m →
      NearTerminal m
    ¬NonNearTerminal⇒NearTerminal m h = ¬infinite⇒finite (λ n → f m ≼ f n) h

    veryGood⇒nonNearTerminal : VeryGood _≼_ f → Satisfiable NonNearTerminal
    veryGood⇒nonNearTerminal f-veryGood = ¬¬-elim [1]
      where
      [1] : ¬ (¬ Satisfiable NonNearTerminal)
      [1] h₁ = f∘r-bad f∘r-good
        where
        [2] : (n : ℕ) → NearTerminal n
        [2] n = ¬NonNearTerminal⇒NearTerminal n (¬∃⟶∀¬ h₁ n)

        r : ℕ → ℕ
        
        r zero    = zero
        r (suc n) = suc (k ⊔ r n)
          where
          [3] : ∃[ k ] ((m : ℕ) → k < m → ¬ f (r n) ≼ f m)
          [3] = [2] (r n)

          k = proj₁ [3]

        r-step : (n : ℕ) → r n < r (suc n)
        r-step n = s≤s (m≤n⊔m _ (r n))

        r-increasing : Increasing _<_ r
        r-increasing = step-increasing r r-step

        r-spec : (n m : ℕ) → r (suc n) ≤ m → ¬ f (r n) ≼ f m
        r-spec n m r[1+n]≤m f∘r[n]≼f[m] = proj₂ [4] m k<m f∘r[n]≼f[m]
          where
          [4] : ∃[ k ] ((m : ℕ) → k < m → ¬ f (r n) ≼ f m)
          [4] = [2] (r n)

          k = proj₁ [4]

          k<m : k < m
          k<m = <-transˡ (s≤s (m≤m⊔n k (r n))) r[1+n]≤m

        f∘r-bad : ¬ Good _≼_ (f ∘ r)
        f∘r-bad (i , j , i<j , f∘r[i]≼f∘r[j]) = r-spec i (r j) r[1+i]≤r[j] f∘r[i]≼f∘r[j]
          where
          r[1+i]≤r[j] : r (suc i) ≤ r j
          r[1+i]≤r[j] = increasing-≤ r r-increasing (suc i) j i<j

        f∘r-good : Good _≼_ (f ∘ r)
        f∘r-good = f-veryGood r r-increasing

    nonNearTerminal⇒LowerBoundSubseq :
      NonNearTerminal zero → 
      Σ[ r ∈ (ℕ → ℕ) ] (Increasing _<_ r × zero < r zero × All (f zero ≼_) (f ∘ r))
    nonNearTerminal⇒LowerBoundSubseq h = r , r-increasing , [1] , [2]
      where
      r : ℕ → ℕ
      r zero    = proj₁ (h zero)
      r (suc n) = proj₁ (h (r n))

      r-step : (n : ℕ) → r n < r (suc n)
      r-step n = proj₁ (proj₂ (h (r n)))

      r-increasing : Increasing _<_ r
      r-increasing = step-increasing r r-step

      [1] : zero < r zero
      [1] = proj₁ (proj₂ (h zero))

      [2] : (n : ℕ) → f zero ≼ f (r n)
      [2] zero = proj₂ (proj₂ (h zero))
      [2] (suc n) = proj₂ (proj₂ (h (r n)))

  nonNearTerminal-tail : (f : ℕ → A) (x : ℕ) (y : ℕ) →
    NonNearTerminal f (x + y) → NonNearTerminal (f ∘ (_+ y)) x
  nonNearTerminal-tail f x y h k = 
    o + suc k , m≤n⇒m≤o+n o ≤-refl , subst (λ z → f (x + y) ≼ f z) [2] (proj₂ (proj₂ (h (k + y))))
    where
    -- h (k + y) : ∃[ l ] (k + y < l × f (x + y) ≼ f l)

    l = proj₁ (h (k + y))

    k+y<l : k + y < l
    k+y<l = proj₁ (proj₂ (h (k + y)))

    [1] : ∃[ o ] o + (suc k + y) ≡ l
    [1] = m≤n⇒∃[o]o+m≡n k+y<l

    o = proj₁ [1]

    [2] : l ≡ (o + suc k) + y
    [2] = sym (trans (+-assoc o (suc k) y) (proj₂ [1]))

  veryGood⇒ascendingSubseq : 
    (f : ℕ → A) → VeryGood _≼_ f →
    Σ[ r ∈ (ℕ → ℕ) ] (Increasing _<_ r × Increasing _≼_ (f ∘ r))
  veryGood⇒ascendingSubseq f f-veryGood = r , r-increasing , [14]
    where
    [1] : Satisfiable (NonNearTerminal f)
    [1] = veryGood⇒nonNearTerminal f f-veryGood

    n₀ = proj₁ [1]

    n₀-spec : NonNearTerminal f n₀
    n₀-spec = proj₂ [1]

    f′ : ℕ → A
    f′ n = f (n + n₀)

    +n₀-increasing : Increasing _<_ (_+ n₀)
    +n₀-increasing m n m<n = +-monoˡ-< n₀ m<n

    nonNearTerminal-f′ : NonNearTerminal f′ zero
    nonNearTerminal-f′ = nonNearTerminal-tail f zero n₀ n₀-spec

    f′-veryGood : VeryGood _≼_ f′
    f′-veryGood = subseq-veryGood _≼_ f (_+ n₀) f-veryGood +n₀-increasing

We’re going to construct an infinite sequence of subsequences of f:

f ∘ (r′ 0) , f ∘ (r′ 1) , f ∘ (r′ 2) , ...

For each j, f ∘ (r′ (suc j)) is a subsequence of f ∘ (r′ j), i.e., there is an increasing sequence s′ j such that r′ (suc j) equals r′ j ∘ s′ j. This makes each r′ j an increasing function, so that f ∘ (r′ j) is a subsequence of f and is hence very good. Moreover, r′ j zero has the following properties:

• r′ j zero ∈ NonNearTerminal (f ∘ r′ j)
• r′ j zero < r′ (suc j) zero
• f (r′ j zero) ≼ f (r′ (suc j) n) for all n

    r′ : ℕ → ℕ → ℕ
    r′-spec₁ : (j : ℕ) → Increasing _<_ (r′ j)
    r′-spec₂ : (j : ℕ) → NonNearTerminal (f ∘ r′ j) zero
    r′-spec₃ : (j : ℕ) → r′ j zero < r′ (suc j) zero
    r′-spec₄ : (j n : ℕ) → f (r′ j zero) ≼ f (r′ (suc j) n)
    s : ℕ → ℕ → ℕ
    s-spec₁ : (j : ℕ) → Increasing _<_ (s j)
    s-spec₂ : (j : ℕ) → zero < s j zero
    s-spec₃ : (j : ℕ) → All (f (r′ j zero) ≼_) (f ∘ r′ j ∘ s j)
    s-spec₄ : (j : ℕ) → Satisfiable (NonNearTerminal (f ∘ (r′ j ∘ s j)))

    r′-helper : 
      (j : ℕ) → Σ[ s ∈ (ℕ → ℕ) ] (Increasing _<_ s × zero < s zero × 
                                  All (f (r′ j zero) ≼_) (f ∘ r′ j ∘ s))

    s′ : ℕ → ℕ → ℕ
    s′-increasing : (j : ℕ) → Increasing _<_ (s′ j)

    r′ zero = _+ n₀
    r′ (suc j) = r′ j ∘ s j ∘ (_+ n)
      where
      n = proj₁ (s-spec₄ j)

    r′-spec₁ zero m n m<n = +-monoˡ-< n₀ m<n
    r′-spec₁ (suc j) = 
      compose-increasing (compose-increasing (λ o p o<p → +-monoˡ-< n o<p) (s-spec₁ j)) (r′-spec₁ j)
      where
      n = proj₁ (s-spec₄ j)

    r′-spec₂ zero    = nonNearTerminal-f′
    r′-spec₂ (suc j) = nonNearTerminal-tail (f ∘ (r′ j ∘ s j)) zero n n-spec
      where
      n = proj₁ (s-spec₄ j)
      n-spec : NonNearTerminal (f ∘ (r′ j ∘ s j)) n
      n-spec = proj₂ (s-spec₄ j)

    r′-spec₃ j = <-transˡ (r′-spec₁ j zero (s j zero) (s-spec₂ j)) (r′[j]∘s[j]-nondecreasing zero n z≤n)
      where
      n = proj₁ (s-spec₄ j)
      r′[j]∘s[j]-increasing : Increasing _<_ (r′ j ∘ s j)
      r′[j]∘s[j]-increasing = compose-increasing (s-spec₁ j) (r′-spec₁ j)
      r′[j]∘s[j]-nondecreasing : (o p : ℕ) → o ≤ p → (r′ j (s j o) ≤ r′ j (s j p))
      r′[j]∘s[j]-nondecreasing = increasing-≤ (r′ j ∘ s j) r′[j]∘s[j]-increasing

    r′-spec₄ j = all-compose {P = f (r′ j zero) ≼_} (_+ n) (s-spec₃ j)
      where
      n = proj₁ (s-spec₄ j)

    r′-helper j = nonNearTerminal⇒LowerBoundSubseq (f ∘ r′ j) (r′-spec₂ j)

    s j = proj₁ (r′-helper j)

    s-spec₁ j = proj₁ (proj₂ (r′-helper j))

    s-spec₂ j = proj₁ (proj₂ (proj₂ (r′-helper j)))

    s-spec₃ j = proj₂ (proj₂ (proj₂ (r′-helper j)))

    s-spec₄ j = veryGood⇒nonNearTerminal (f ∘ r′ j ∘ s j) f∘r′[j]∘s[j]-veryGood
      where
      r′[j]∘s[j]-increasing : Increasing _<_ (r′ j ∘ s j)
      r′[j]∘s[j]-increasing = compose-increasing (s-spec₁ j) (r′-spec₁ j)
      f∘r′[j]∘s[j]-veryGood : VeryGood _≼_ (f ∘ r′ j ∘ s j)
      f∘r′[j]∘s[j]-veryGood = subseq-veryGood _≼_ f (r′ j ∘ s j) f-veryGood r′[j]∘s[j]-increasing

    s′ j = s j ∘ (_+ proj₁ (s-spec₄ j))

    s′-increasing j = compose-increasing (λ o p o<p → +-monoˡ-< n o<p) (s-spec₁ j)
      where
      n = proj₁ (s-spec₄ j)

    [2] : (j : ℕ) → r′ j ∘ s′ j ≡ r′ (suc j)
    [2] j = refl

    [3] : (j p : ℕ) → Σ[ t ∈ (ℕ → ℕ) ] (Increasing _<_ t × r′ j ∘ t ≗ r′ (p + j))
    [3] j zero    = id , id-increasing , λ x → refl
    [3] j (suc p) = 
      t ∘ s′ (p + j) , 
      compose-increasing (s′-increasing (p + j)) t-increasing , 
      λ x → trans ([4] (s′ (p + j) x)) ([5] x)
      where
      t = proj₁ ([3] j p)
      t-increasing = proj₁ (proj₂ ([3] j p))
      [4] : r′ j ∘ t ≗ r′ (p + j)
      [4] = proj₂ (proj₂ ([3] j p))
      [5] : r′ (p + j) ∘ s′ (p + j) ≗ r′ (suc p + j)
      [5] x = subst (λ z → z x ≡ r′ (suc p + j) x) (sym ([2] (p + j))) refl

    [6] : (j p o : ℕ) → f (r′ j zero) ≼ f (r′ (p + suc j) o)
    [6] j p o = [13] o
      where
      t = proj₁ ([3] (suc j) p)
      [7] : r′ (suc j) ∘ t ≗ r′ (p + suc j)
      [7] = proj₂ (proj₂ ([3] (suc j) p))
      [8] : All (f (r′ j zero) ≼_) (f ∘ r′ (suc j))
      [8] = r′-spec₄ j
      [9] : All (f (r′ j zero) ≼_) ((f ∘ r′ (suc j)) ∘ t)
      [9] = all-compose {P = f (r′ j zero) ≼_} t [8]
      [10] : (f ∘ r′ (suc j)) ∘ t ≗ f ∘ (r′ (suc j) ∘ t)
      [10] = ∘-assoc t (r′ (suc j)) f
      [11] : All (f (r′ j zero) ≼_) (f ∘ (r′ (suc j) ∘ t))
      [11] = all-extensional {P = f (r′ j zero) ≼_} [10] [9]
      [12] : f ∘ (r′ (suc j) ∘ t) ≗ f ∘ r′ (p + suc j)
      [12] x = cong f ([7] x)
      [13] : All (f (r′ j zero) ≼_) (f ∘ r′ (p + suc j))
      [13] = all-extensional {P = f (r′ j zero) ≼_} [12] [11]

    r : ℕ → ℕ
    r i = r′ i zero

    [14] : (i j : ℕ) → i < j → f (r i) ≼ f (r j)
    [14] i j i<j = subst (λ z → f (r′ i zero) ≼ f (r′ z zero)) p+suc[i]≡j ([6] i p zero)
      where
      [15] : ∃[ p ] p + suc i ≡ j
      [15] = m<n⇒∃[o]o+suc[m]≡n i<j
      p = proj₁ [15]
      p+suc[i]≡j : p + suc i ≡ j
      p+suc[i]≡j = proj₂ [15]

    r-step : (i : ℕ) → r i < r (suc i)
    r-step i = r′-spec₃ i

    r-increasing : Increasing _<_ r
    r-increasing = step-increasing r r-step

  -- ascendingSubseq : IsWQO _≼_
  --   → Σ[ r ∈ (ℕ → ℕ) ] (Increasing _<_ r × Increasing _≼_ (f ∘ r))
  -- ascendingSubseq h =
  --   veryGood⇒ascendingSubseq (almostFull-veryGood (almostFull h))

prodSeq : (ℕ → A) → (ℕ → B) → (ℕ → A × B)
prodSeq f g n = f n , g n

prodOrder : (A → A → Set) → (B → B → Set) → A × B → A × B → Set
prodOrder _≼₁_ _≼₂_ x y = (proj₁ x ≼₁ proj₁ y) × (proj₂ x ≼₂ proj₂ y)

prod-reflexive : (_≼₁_ : A → A → Set) (_≼₂_ : B → B → Set)
  → Reflexive _≼₁_
  → Reflexive _≼₂_
  → Reflexive (prodOrder _≼₁_ _≼₂_)
prod-reflexive _≼₁_ _≼₂_ h₁ h₂ = h₁ , h₂

prod-transitive : (_≼₁_ : A → A → Set) (_≼₂_ : B → B → Set)
  → Transitive _≼₁_
  → Transitive _≼₂_
  → Transitive (prodOrder _≼₁_ _≼₂_)
prod-transitive _≼₁_ _≼₂_ h₁ h₂ xy yz = (h₁ (proj₁ xy) (proj₁ yz)) , h₂ (proj₂ xy) (proj₂ yz)

prod-isQO : (_≼₁_ : A → A → Set) (_≼₂_ : B → B → Set)
  → IsQO _≼₁_
  → IsQO _≼₂_
  ----------------------------
  → IsQO (prodOrder _≼₁_ _≼₂_)

prod-isQO _≼₁_ _≼₂_ h₁ h₂ = 
  record
    { reflexive = prod-reflexive _≼₁_ _≼₂_ (reflexive h₁) (reflexive h₂)
    ; transitive = prod-transitive _≼₁_ _≼₂_ (transitive h₁) (transitive h₂)
    }

prod-veryGood : {_≼₁_ : A → A → Set} {_≼₂_ : B → B → Set}
  {f : ℕ → A} {g : ℕ → B}
  → VeryGood _≼₁_ f
  → VeryGood _≼₂_ g
  ----------------------------------------------
  → VeryGood (prodOrder _≼₁_ _≼₂_) (prodSeq f g)
prod-veryGood {_≼₁_ = _≼₁_} {_≼₂_ = _≼₂_} {f = f} {g = g} 
  f-veryGood g-veryGood r r-increasing
  = r₁ i , r₁ j , r₁-increasing i j i<j , ( frr₁i≼₁frr₁j , grr₁i≼₂grr₁j )
  where
  _≼_ = prodOrder _≼₁_ _≼₂_
  f∘r-veryGood : VeryGood _≼₁_ (f ∘ r)
  f∘r-veryGood = subseq-veryGood _≼₁_ f r f-veryGood r-increasing
  f∘r-ascendingSubseq : 
    Σ[ r₁ ∈ (ℕ → ℕ) ] Increasing _<_ r₁ × Increasing _≼₁_ (f ∘ r ∘ r₁)
  f∘r-ascendingSubseq = 
    veryGood⇒ascendingSubseq _≼₁_ (f ∘ r)
    f∘r-veryGood
  r₁ : ℕ → ℕ
  r₁ = proj₁ f∘r-ascendingSubseq
  r₁-increasing : Increasing _<_ r₁
  r₁-increasing = proj₁ (proj₂ f∘r-ascendingSubseq)
  f∘r∘r₁-increasing : Increasing _≼₁_ (f ∘ r ∘ r₁)
  f∘r∘r₁-increasing = proj₂ (proj₂ f∘r-ascendingSubseq)
  r∘r₁-increasing : Increasing _<_ (r ∘ r₁)
  r∘r₁-increasing = subseq-increasing _<_ r r₁ r-increasing r₁-increasing
  g∘r∘r₁-good : Good _≼₂_ (g ∘ r ∘ r₁)
  g∘r∘r₁-good = g-veryGood (r ∘ r₁) r∘r₁-increasing
  i j : ℕ
  i = proj₁ g∘r∘r₁-good
  j = proj₁ (proj₂ g∘r∘r₁-good)
  i<j : i < j
  i<j = proj₁ (proj₂ (proj₂ g∘r∘r₁-good))
  grr₁i≼₂grr₁j : g (r (r₁ i)) ≼₂ g (r (r₁ j))
  grr₁i≼₂grr₁j = proj₂ (proj₂ (proj₂ g∘r∘r₁-good))
  frr₁i≼₁frr₁j : f (r (r₁ i)) ≼₁ f (r (r₁ j))
  frr₁i≼₁frr₁j = f∘r∘r₁-increasing i j i<j

prod-isWQO : (_≼₁_ : A → A → Set) (_≼₂_ : B → B → Set)
  → IsWQO _≼₁_
  → IsWQO _≼₂_
  -------------------------------------
  → IsWQO {A × B} (prodOrder _≼₁_ _≼₂_)
prod-isWQO {A = A} {B = B} _≼₁_ _≼₂_ h₁ h₂ = 
  record
    { isQO = prod-isQO _≼₁_ _≼₂_ (isQO h₁) (isQO h₂)
    ; almostFull = ≼-almostFull
    }
  where
  _≼_ = prodOrder _≼₁_ _≼₂_
  ≼-almostFull : (f : ℕ → A × B) → Good _≼_ f
  ≼-almostFull f = f₁f₂-good
    where
    f₁ : ℕ → A
    f₁ n = proj₁ (f n)
    f₂ : ℕ → B
    f₂ n = proj₂ (f n)
    f₁-veryGood : VeryGood _≼₁_ f₁
    f₁-veryGood = almostFull-veryGood _≼₁_ f₁ (almostFull h₁)
    f₂-veryGood : VeryGood _≼₂_ f₂
    f₂-veryGood = almostFull-veryGood _≼₂_ f₂ (almostFull h₂)
    f₁f₂-veryGood : VeryGood (prodOrder _≼₁_ _≼₂_) (prodSeq f₁ f₂)
    f₁f₂-veryGood = 
      prod-veryGood {_≼₁_ = _≼₁_} {_≼₂_ = _≼₂_} {f = f₁} {g = f₂}
        -- (transitive (isQO h₁))
      f₁-veryGood f₂-veryGood
    f₁f₂-good : Good (prodOrder _≼₁_ _≼₂_) (prodSeq f₁ f₂)
    f₁f₂-good = veryGood⇒good (prodOrder _≼₁_ _≼₂_) (prodSeq f₁ f₂) f₁f₂-veryGood

module M (_≼_ : A → A → Set) where
  _≼′_ : Maybe A → Maybe A → Set
  just x  ≼′ just y  = x ≼ y
  just x  ≼′ nothing = ⊥
  nothing ≼′ just y  = ⊥
  nothing ≼′ nothing = ⊤ -- ??

  maybe-almostFull : AlmostFull _≼_ → AlmostFull _≼′_
  maybe-almostFull ≼-almostFull f = f-good
    where
    Inf = (k : ℕ) → Σ[ l ∈ ℕ ] k < l × f l ≡ nothing
    Cof = Σ[ k ∈ ℕ ] ((l : ℕ) → k < l → f l ≢ nothing)
    h₁ : Inf ⊎ Cof
    h₁ = infinite∨finite (λ z → f z ≡ nothing)
    f-good : Good _≼′_ f
    f-good with h₁
    ... | inj₁ inf = i , j , i<j , fi≼′fj
      where
      i j : ℕ
      i = proj₁ (inf zero)
      j = proj₁ (inf i) 
      i<j : i < j
      i<j = proj₁ (proj₂ (inf i))
      fi≡nothing : f i ≡ nothing
      fi≡nothing = proj₂ (proj₂ (inf zero))
      fj≡nothing : f j ≡ nothing
      fj≡nothing = proj₂ (proj₂ (inf i))
      fi≼′fj : f i ≼′ f j
      fi≼′fj rewrite fi≡nothing | fj≡nothing = tt
    ... | inj₂ cof = i + suc k , j + suc k , i+1+k<j+1+k , fi+1+k≼′fj+1+k
      where
      k = proj₁ cof
      cof′ : (l : ℕ) → k < l → ∃[ x ] f l ≡ just x
      cof′ l k<l with f l in eq
      ... | just x = x , refl
      ... | nothing = ⊥-elim (proj₂ cof l k<l eq)
      g : (n : ℕ) → ∃[ x ] f (n + suc k) ≡ just x
      g n = cof′ (n + suc k) (m≤n+m (suc k) n)
      f′ : ℕ → A
      f′ n = proj₁ (g n)
      f-f′ : (n : ℕ) → f (n + suc k) ≡ just (f′ n)
      f-f′ n = proj₂ (g n)
      f′-good : Good _≼_ f′
      f′-good = ≼-almostFull f′
      i j : ℕ
      i = proj₁ f′-good
      j = proj₁ (proj₂ f′-good)
      i<j : i < j
      i<j = proj₁ (proj₂ (proj₂ f′-good))
      f′i≼f′j : f′ i ≼ f′ j
      f′i≼f′j = proj₂ (proj₂ (proj₂ f′-good))
      i+1+k<j+1+k : i + suc k < j + suc k
      i+1+k<j+1+k = +-monoˡ-< (suc k) i<j
      fi+1+k≼′fj+1+k : f (i + suc k) ≼′ f (j + suc k)
      fi+1+k≼′fj+1+k rewrite f-f′ i | f-f′ j = f′i≼f′j