An Agda proof of Friedman's theorem about tree embedding with a gap condition, restricted to monadic trees (words).
(It should be fairly easy to remove the restriction.)
This was the problem posed as the "TPPmark" for the 18th TPP meeting.
https://www.jaist.ac.jp/~hirokawa/trs-meeting/original/57/TPPmark2022.pdf
https://www.jaist.ac.jp/~hirokawa/trs-meeting/original/57.html#tpp
The general philosophy in the formalization is to reason 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,
at the cost of complicating the minimal bad sequence argument.
```agda
module TPP2022 where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; _≢_; sym; trans; subst)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; s≤s; z≤n; _<_)
open import Data.Nat.Properties
using (≤-refl; ≤-trans; <-irrefl; <⇒≤; ≤-step; <-transˡ; <-transʳ; ≤∧≢⇒<; +-monoˡ-<; m≤n+m)
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 (_∈_)
open import Function using (_∘_; id)
import Data.Fin as F
open F using (Fin; toℕ)
open import Data.Fin.Properties using (pigeonhole; toℕ-mono-<)
open import Data.Maybe using (Maybe; just; nothing)
open import Relation.Binary.Core using (_⇒_)
open import Miscellaneous
open import Classical
open import WQO
open import MinimalBadSeq
```
Equality is a WQO on Fin n.
```agda
module Fin-≡ where
almostFull : {n : ℕ} → AlmostFull {Fin n} _≡_
almostFull {n} f = toℕ i , toℕ j , toℕ-mono-< i<j , gi≡gj
where
g : Fin (suc n) → Fin n
g = f ∘ toℕ
h : ∃₂ (λ i j → i F.< j × g i ≡ g j)
h = pigeonhole ≤-refl g
i = proj₁ h
j = proj₁ (proj₂ h)
i<j = proj₁ (proj₂ (proj₂ h))
gi≡gj = proj₂ (proj₂ (proj₂ h))
isWQO : (n : ℕ) → IsWQO {A = Fin n} _≡_
isWQO n =
record
{ isQO = record { reflexive = refl ; transitive = trans }
; almostFull = almostFull
}
```
Define inequality on Maybe (Fin n) so that nothing is the bottom element.
Equality on Maybe (Fin n) is almost full.
```agda
module _ {n : ℕ} where
_≤′_ : Maybe (Fin n) → Maybe (Fin n) → Set
just i ≤′ just j = i F.≤ j
just _ ≤′ nothing = ⊥
nothing ≤′ just _ = ⊤
nothing ≤′ nothing = ⊤
≤′-refl : Reflexive _≤′_
≤′-refl {just x} = ≤-refl
≤′-refl {nothing} = tt
≤′-reflexive : _≡_ ⇒ _≤′_
≤′-reflexive refl = ≤′-refl
≤′-trans : Transitive _≤′_
≤′-trans {just x} {just y} {just z} xy yz = ≤-trans xy yz
≤′-trans {nothing} {just y} {just z} xy yz = tt
≤′-trans {nothing} {nothing} {just z} xy yz = tt
≤′-trans {nothing} {nothing} {nothing} xy yz = tt
module MaybeFin-≡ {n : ℕ} where
open M {Fin n} _≡_
≡-≼′ : (x y : Maybe (Fin n)) → (x ≡ y) ⇔ (x ≼′ y)
≡-≼′ (just x) (just y) = (λ {refl → refl}) , (λ {refl → refl})
≡-≼′ (just x) nothing = (λ {()}) , λ {()}
≡-≼′ nothing (just y) = (λ {()}) , λ {()}
≡-≼′ nothing nothing = (λ {refl → tt}) , λ _ → refl
almostFull : AlmostFull {Maybe (Fin n)} _≡_
almostFull f with maybe-almostFull Fin-≡.almostFull f
... | i , j , i<j , h = i , j , i<j , proj₂ (≡-≼′ (f i) (f j)) h
```
Monadic trees (words) with leaf labels in A and internal node labels in Fin n.
A word with no internal node has size 1.
```agda
data Word (A : Set) (n : ℕ) : Set where
end : (a : A) → Word A n
cons : (i : Fin n) → (x : Word A n) → Word A n
module _ {A : Set} {n : ℕ} where
size : Word A n → ℕ
size (end a) = 1
size (cons i x) = suc (size x)
size≥1 : (x : Word A n) → 1 ≤ size x
size≥1 (end x) = ≤-refl
size≥1 (cons x x₁) = s≤s z≤n
leaf : Word A n → A
leaf (end a) = a
leaf (cons i x) = leaf x
size≡1 : (x : Word A n) → size x ≡ 1 → x ≡ end (leaf x)
size≡1 (end a) h = refl
size≡1 (cons i x) h = ⊥-elim (<-irrefl (sym h) (s≤s (size≥1 x)))
size>1 : (x : Word A n) → 1 < size x → ∃₂ λ i x₁ → x ≡ cons i x₁
size>1 (end a) h = ⊥-elim (<-irrefl refl h)
size>1 (cons i x) h = i , x , refl
```
The "is a suffix" relation on words.
```agda
data _⊑_ : Word A n → Word A n → Set where
⊑-refl : (x : Word A n) → x ⊑ x
⊑-step : {x y : Word A n} (i : Fin n) → x ⊑ y → x ⊑ cons i y
⊑-transitive : Transitive _⊑_
⊑-transitive {x} {y} {.y} x⊑y (⊑-refl .y) = x⊑y
⊑-transitive {x} {y} {.(cons i _)} x⊑y (⊑-step i y⊑z) = ⊑-step i (⊑-transitive x⊑y y⊑z)
⊑-size-≤ : {x y : Word A n} → x ⊑ y → size x ≤ size y
⊑-size-≤ (⊑-refl _) = ≤-refl
⊑-size-≤ (⊑-step i x) = ≤-step (⊑-size-≤ x)
⊑-size-≡ : {x y : Word A n} → x ⊑ y → size x ≡ size y → x ≡ y
⊑-size-≡ (⊑-refl _) _ = refl
⊑-size-≡ {x} {y} (⊑-step i xy) h with ⊑-size-≤ xy
... | w rewrite h = ⊥-elim (<-irrefl refl w)
⊑-leaf : {x y : Word A n} → x ⊑ y → leaf x ≡ leaf y
⊑-leaf (⊑-refl _) = refl
⊑-leaf (⊑-step i x⊑y) = ⊑-leaf x⊑y
_⊏_ : Word A n → Word A n → Set
x ⊏ y = x ⊑ y × x ≢ y
tail-⊏ : (i : Fin n) (x : Word A n) → x ⊏ cons i x
tail-⊏ i x = (⊑-step i (⊑-refl x)) , (λ {()})
⊏-size-< : {x y : Word A n} → x ⊏ y → size x < size y
⊏-size-< x⊏y = ≤∧≢⇒< (⊑-size-≤ (proj₁ x⊏y))
(λ h → ⊥-elim (proj₂ x⊏y (⊑-size-≡ (proj₁ x⊏y) h)))
⊏-⊑-⊏ : {x y z : Word A n} → x ⊏ y → y ⊑ z → x ⊏ z
⊏-⊑-⊏ {x} {y} {z} x⊏y@(x⊑y , x≢y) y⊑z = ⊑-transitive x⊑y y⊑z , (λ {refl → <-irrefl refl h})
where
h : size x < size z
h = <-transˡ (⊏-size-< x⊏y) (⊑-size-≤ y⊑z)
⊑-⊏-⊏ : {x y z : Word A n} → x ⊑ y → y ⊏ z → x ⊏ z
⊑-⊏-⊏ {x} {y} {z} x⊑y y⊏z@(y⊑z , y≢z) = ⊑-transitive x⊑y y⊑z , (λ {refl → <-irrefl refl h})
where
h : size x < size z
h = <-transʳ (⊑-size-≤ x⊑y) (⊏-size-< y⊏z)
```
If x is a word, min x is the minimal internal leaf label in x (if there is one).
```agda
head : Word A n → Maybe (Fin n)
head (end a) = nothing
head (cons i x) = just i
min : Word A n → Maybe (Fin n)
min (end a) = nothing
min (cons i x) with min x
... | just m = case-⊎ (λ _ → just i) (λ _ → just m) (≤-<-connex (toℕ i) (toℕ m))
... | nothing = just i
```
This definition of min is rather hard to reason with. We state many obvious properties of the function.
```agda
min-cons-≤ : (x : Word A n) (m i : Fin n) → min x ≡ just m → toℕ i ≤ toℕ m → min (cons i x) ≡ just i
min-cons-≤ x m i h i≤m rewrite h | ≤-<-connex-≤ (toℕ i) (toℕ m) i≤m = refl
min-cons-> : (x : Word A n) (m i : Fin n) → min x ≡ just m → toℕ m < toℕ i → min (cons i x) ≡ just m
min-cons-> x m i h i>m rewrite h | ≤-<-connex-> (toℕ i) (toℕ m) i>m = refl
min-cons-nothing : (x : Word A n) (i : Fin n) → min x ≡ nothing → min (cons i x) ≡ just i
min-cons-nothing x i h with min x
... | nothing = refl
min-cons : (i : Fin n) (x : Word A n) → Σ[ m ∈ Fin n ] min (cons i x) ≡ just m
min-cons i x with min x
min-cons i x | just m₁ with ≤-<-connex (toℕ i) (toℕ m₁)
... | inj₁ i≤m₁ = i , refl
... | inj₂ i>m₁ = m₁ , refl
min-cons i x | nothing = i , refl
min-nothing : (x : Word A n) → min x ≡ nothing → ∃[ a ] x ≡ end a
min-nothing (end a) refl = a , refl
min-nothing (cons i x) h with min-cons i x
... | m , eq = ⊥-elim (just≢nothing (trans (sym eq) h))
min-just : (x : Word A n) (m : Fin n) → min x ≡ just m → Σ[ i ∈ Fin n ] Σ[ x₁ ∈ Word A n ] x ≡ cons i x₁
min-just (cons i x) m h = i , x , refl
min-≤-min-tail : (i m : Fin n) (x : Word A n) → min x ≡ just m → min (cons i x) ≤′ just m
min-≤-min-tail i m x h with min x
min-≤-min-tail i m x h | just m₁ with ≤-<-connex (toℕ i) (toℕ m₁)
min-≤-min-tail i m x refl | just m₁ | inj₁ i≤m₁ = i≤m₁
min-≤-min-tail i .m₁ x refl | just m₁ | inj₂ i>m₁ = ≤-refl
min-≤-head : {i : Fin n} {x : Word A n} → min (cons i x) ≤′ just i
min-≤-head {i} {x} with min x
min-≤-head {i} {x} | just m with ≤-<-connex (toℕ i) (toℕ m)
... | inj₁ i≤m = ≤-refl
... | inj₂ i>m = <⇒≤ i>m
min-≤-head {i} {x} | nothing = ≤-refl
```
We could define min as an inductive predicate. This definition might fascilitate reasoning,
but I don't find it very intuititve.
```
```
Friedman's tree embedding relation with a "gap" condition (restricted to words).
There are two variants of the condition.
The variant without the "+" requires that all nodes between two matched nodes
in the right tree (word) have labels that are not smaller than the label of the
lower of the matched nodes.
In addition, the variant with the "+" requires that all nodes above the highest
matched node have labels that are not smaller than the label of that node.
The two embedding relations are defined inductively.
```agda
module _ {A : Set} {n : ℕ} (_≼_ : A → A → Set) where
data Embedding-gap⁺ : Word A n → Word A n → Set
data Embedding-gap⁺ where
end : ∀ {a b} (h : a ≼ b) → Embedding-gap⁺ (end a) (end b)
_∷ʳ_ : {x y : Word A n} {j : Fin n}
→ (h : head x ≤′ (just j))
→ Embedding-gap⁺ x y
→ Embedding-gap⁺ x (cons j y)
_∷_ : {x y : Word A n} (i : Fin n)
→ (h : Embedding-gap⁺ x y)
→ Embedding-gap⁺ (cons i x) (cons i y)
```
It takes some effort to prove the "+" version is transitive.
```
emb-gap⁺-head : {x y : Word A n}
→ (h : Embedding-gap⁺ x y)
→ head x ≤′ head y
emb-gap⁺-head {.(end _)} {.(end _)} (end h) = tt
emb-gap⁺-head {x} {.(cons _ _)} (h ∷ʳ h₁) = h
emb-gap⁺-head {.(cons i _)} {.(cons i _)} (i ∷ h) = ≤-refl
emb-gap⁺-transitive : (h : Transitive _≼_) {x y z : Word A n}
→ (h₁ : Embedding-gap⁺ x y)
→ (h₂ : Embedding-gap⁺ y z)
→ Embedding-gap⁺ x z
emb-gap⁺-transitive h {.(end _)} {.(end _)} {.(end _)} (end h₁) (end h₂) =
end (h h₁ h₂)
emb-gap⁺-transitive h {x} {y} {.(cons _ _)} h₁ (h₂ ∷ʳ h₃) =
≤′-trans (emb-gap⁺-head h₁) h₂ ∷ʳ emb-gap⁺-transitive h h₁ h₃
emb-gap⁺-transitive h {x} {.(cons i _)} {.(cons i _)} (h₁ ∷ʳ h₂) (i ∷ h₃) =
h₁ ∷ʳ emb-gap⁺-transitive h h₂ h₃
emb-gap⁺-transitive h {.(cons i _)} {.(cons i _)} {.(cons i _)} (.i ∷ h₁) (i ∷ h₂) =
i ∷ emb-gap⁺-transitive h h₁ h₂
emb-gap⁺-isQO : IsQO {A = A} _≼_ → IsQO {A = Word A n} Embedding-gap⁺
emb-gap⁺-isQO h =
record
{ reflexive = emb-gap⁺-reflexive
; transitive = emb-gap⁺-transitive (IsQO.transitive h)
}
where
emb-gap⁺-reflexive : Reflexive Embedding-gap⁺
emb-gap⁺-reflexive {end a} = end (IsQO.reflexive h)
emb-gap⁺-reflexive {cons i x} = i ∷ emb-gap⁺-reflexive {x}
emb-gap⁺-size : {x y : Word A n} → (h : Embedding-gap⁺ x y) → size x ≤ size y
emb-gap⁺-size {.(end _)} {.(end _)} (end h) = ≤-refl
emb-gap⁺-size {x} {.(cons _ _)} (h ∷ʳ h₁) = ≤-step (emb-gap⁺-size h₁)
emb-gap⁺-size {.(cons i _)} {.(cons i _)} (i ∷ h) = s≤s (emb-gap⁺-size h)
```
The version without the "+".
```
data Embedding-gap : Word A n → Word A n → Set where
mk : {x y : Word A n}
→ (h : Embedding-gap⁺ x y)
→ Embedding-gap x y
_∷ʳ_ : (j : Fin n) {x y : Word A n}
→ (h : Embedding-gap x y)
→ Embedding-gap x (cons j y)
emb-gap-isQO : IsQO {A = A} _≼_ → IsQO {A = Word A n} Embedding-gap
emb-gap-isQO h =
record
{ reflexive = emb-gap-reflexive
; transitive = emb-gap-transitive
}
where
emb-gap-reflexive : Reflexive Embedding-gap
emb-gap-reflexive {x} = mk (IsQO.reflexive (emb-gap⁺-isQO h))
emb-gap-transitive : Transitive Embedding-gap
emb-gap-transitive {x} {y} {z} (mk xy) (mk yz) =
mk (IsQO.transitive (emb-gap⁺-isQO h) xy yz)
emb-gap-transitive {x} {cons j y} {cons k z} (j ∷ʳ xy) (mk (m≤1+k ∷ʳ jyz)) =
k ∷ʳ emb-gap-transitive (j ∷ʳ xy) (mk jyz)
emb-gap-transitive {x} {cons j y} {cons j z} (j ∷ʳ xy) (mk (.j ∷ yz)) =
j ∷ʳ emb-gap-transitive xy (mk yz)
emb-gap-transitive {x} {y} {cons j z} xy (j ∷ʳ yz) = j ∷ʳ emb-gap-transitive xy yz
emb-gap-size : {x y : Word A n} → (h : Embedding-gap x y) → size x ≤ size y
emb-gap-size {x} {y} (mk h) = emb-gap⁺-size h
emb-gap-size {x} {.(cons j _)} (j ∷ʳ h) = ≤-step (emb-gap-size h)
emb-gap-⊑-emb-gap : {x y z : Word A n} → (h : Embedding-gap x y) → y ⊑ z → Embedding-gap x z
emb-gap-⊑-emb-gap h (⊑-refl _) = h
emb-gap-⊑-emb-gap h (⊑-step i h₁) = i ∷ʳ emb-gap-⊑-emb-gap h h₁
emb-gap-min-emb-gap⁺ : {x y : Word A n}
→ (h₁ : head x ≤′ min y)
→ (h₂ : Embedding-gap x y)
→ Embedding-gap⁺ x y
emb-gap-min-emb-gap⁺ {x} {y} h₁ (mk h₂) = h₂
emb-gap-min-emb-gap⁺ {end a} {cons .j (end b)} h₁ (j ∷ʳ mk h) = tt ∷ʳ h
emb-gap-min-emb-gap⁺ {cons i x} {cons .j (end b)} h₁ (j ∷ʳ mk ())
emb-gap-min-emb-gap⁺ {x} {cons .j (cons i y)} h₁ (j ∷ʳ h₂) = h₉ ∷ʳ h₇
where
h₃ : Σ[ m ∈ Fin n ] min (cons i y) ≡ just m
h₃ = min-cons i y
m = proj₁ h₃
eq : min (cons i y) ≡ just m
eq = proj₂ h₃
h₄ : min (cons j (cons i y)) ≤′ just m
h₄ = min-≤-min-tail j m (cons i y) eq
h₅ : min (cons j (cons i y)) ≤′ min (cons i y)
h₅ = subst (min (cons j (cons i y)) ≤′_) (sym eq) h₄
h₆ : head x ≤′ min (cons i y)
h₆ = ≤′-trans h₁ h₅
h₇ : Embedding-gap⁺ x (cons i y)
h₇ = emb-gap-min-emb-gap⁺ h₆ h₂
h₈ : min (cons j (cons i y)) ≤′ just j
h₈ = min-≤-head {i = j} {x = cons i y}
h₉ : head x ≤′ just j
h₉ = ≤′-trans h₁ h₈
```
Friedman's "star" function on trees locates the highest node with the minimal internal node label,
replaces that node with the subtree rooted at that node, and decrements the lables of all higher nodes.
Again, the definition of this function is hard to reason with, and we have to state many easy lemmas
about it for later use.
```agda
module _ {A : Set} {n : ℕ} where
star-helper : Fin (suc n) → Word A (suc n) → Word (Word A (suc n)) n
star-helper m (end a) = end (end a)
star-helper m (cons i x) with ≤-<-connex (toℕ i) (toℕ m)
star-helper m (cons i x) | inj₁ i≤m = end (cons i x)
star-helper m (cons (F.suc i) x) | inj₂ 1+i>m = cons i (star-helper m x)
star-helper-≤ : (m i : Fin (suc n)) (x : Word A (suc n))
→ i F.≤ m
→ star-helper m (cons i x) ≡ end (cons i x)
star-helper-≤ m i x i≤m rewrite ≤-<-connex-≤ (toℕ i) (toℕ m) i≤m = refl
star-helper-i-cons-i : (x : Word A (suc n)) (i : Fin (suc n))
→ star-helper i (cons i x) ≡ end (cons i x)
star-helper-i-cons-i x i = star-helper-≤ i i x ≤′-refl
star-helper-> : (m i : Fin (suc n)) (x : Word A (suc n))
→ m F.< i
→ ∃[ i′ ] (i ≡ F.suc i′ × star-helper m (cons i x) ≡ cons i′ (star-helper m x))
star-helper-> m (F.suc i) x 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) (x : Word A (suc n))
→ m F.< F.suc i
→ star-helper m (cons (F.suc i) x) ≡ cons i (star-helper m x)
star-helper->-suc m i x i>m rewrite ≤-<-connex-> (toℕ (F.suc i)) (toℕ m) i>m = refl
star : Word A (suc n) → Word (Word A (suc n)) n
star x with min x
... | just m = star-helper m x
... | nothing = end x
star-just : (m : Fin (suc n)) (x : Word A (suc n)) → min x ≡ just m → star x ≡ star-helper m x
star-just m x h with min x
star-just .m₁ x refl | just m₁ = refl
star-nothing : (x : Word A (suc n)) → min x ≡ nothing → star x ≡ end x
star-nothing x h with min x
... | nothing = refl
leaf∘star-⊑ : (x : Word A (suc n)) → leaf (star x) ⊑ x
leaf∘star-⊑ x with min x
... | just m = leaf∘star-helper-⊑ x
where
leaf∘star-helper-⊑ : (x : Word A (suc n)) → leaf (star-helper m x) ⊑ x
leaf∘star-helper-⊑ (end a) = ⊑-refl (end a)
leaf∘star-helper-⊑ (cons i x) with ≤-<-connex (toℕ i) (toℕ m)
leaf∘star-helper-⊑ (cons i x) | inj₁ i≤m = ⊑-refl (cons i x)
leaf∘star-helper-⊑ (cons (F.suc i) x) | inj₂ 1+i>m = ⊑-step (F.suc i) (leaf∘star-helper-⊑ x)
... | nothing = ⊑-refl x
leaf≡leaf∘leaf∘star : (x : Word A (suc n)) → leaf x ≡ leaf (leaf (star x))
leaf≡leaf∘leaf∘star x with min x
... | nothing = refl
... | just m = helper x
where
helper : (x : Word A (suc n)) → leaf x ≡ leaf (leaf (star-helper m x))
helper (end a) = refl
helper (cons i x) with ≤-<-connex (toℕ i) (toℕ m)
helper (cons i x) | inj₁ i≤m = refl
helper (cons (F.suc i) x) | inj₂ 1+i>m = helper x
```
Lemma 4.5
This supposedly `straightforward' proof is very long and tedious.
It turned out to be the toughest part of the proof to formalize.
```
module _ {A : Set} {n : ℕ} {_≼_ : A → A → Set} where
embed-star-Embed : (x y : Word A (suc n))
→ min x ≡ min y
→ Embedding-gap⁺ (Embedding-gap _≼_) (star x) (star y)
→ Embedding-gap⁺ _≼_ x y
embed-star-Embed (end a) (end b) h₁ (end (mk h)) = h
embed-star-Embed (end a) (cons j y) h₁ h₂ = ⊥-elim (just≢nothing (sym (trans h₁ h₄)))
where
h₃ : Σ[ m ∈ Fin (suc n) ] min (cons j y) ≡ just m
h₃ = min-cons j y
m : Fin (suc n)
m = proj₁ h₃
h₄ : min (cons j y) ≡ just m
h₄ = proj₂ h₃
embed-star-Embed (cons i x) (end b) h₁ h₂ = ⊥-elim (just≢nothing (trans (sym h₄) h₁))
where
h₃ : Σ[ m ∈ Fin (suc n) ] min (cons i x) ≡ just m
h₃ = min-cons i x
m : Fin (suc n)
m = proj₁ h₃
h₄ : min (cons i x) ≡ just m
h₄ = proj₂ h₃
embed-star-Embed (cons i x) (cons j y) h₁ h₂ with min x in eq₁ | min y in eq₂
embed-star-Embed (cons i x) (cons j y) h₁ h₂ | just m₁ | just m₂
with ≤-<-connex (toℕ i) (toℕ m₁) | ≤-<-connex (toℕ j) (toℕ m₂)
embed-star-Embed (cons i x) (cons .i y) refl h₂ | just m₁ | just m₂ | inj₁ i≤m₁ | inj₁ i≤m₂
rewrite star-helper-i-cons-i x i | star-helper-i-cons-i y i with h₂
... | end h = h₅
where
h₃ : min (cons i y) ≡ just i
h₃ = min-cons-≤ y m₂ i eq₂ i≤m₂
h₄ : just i ≤′ min (cons i y)
h₄ = ≤′-reflexive (sym h₃)
h₅ : Embedding-gap⁺ _≼_ (cons i x) (cons i y)
h₅ = emb-gap-min-emb-gap⁺ _≼_ {x = cons i x} {y = cons i y} h₄ h
embed-star-Embed (cons m₂ x) (cons (F.suc j) y) refl h₂ | just m₁ | just m₂ | inj₁ m₂≤m₁ | inj₂ 1+j>m₂
rewrite star-helper-i-cons-i x m₂ | star-helper->-suc m₂ j y 1+j>m₂ with h₂
... | tt ∷ʳ h = <⇒≤ 1+j>m₂ ∷ʳ h₇
where
h₃ : min (cons m₂ x) ≡ just m₂
h₃ = min-cons-≤ x m₁ m₂ eq₁ m₂≤m₁
h₄ : star (cons m₂ x) ≡ end (cons m₂ x)
h₄ =
begin
star (cons m₂ x)
≡⟨ star-just m₂ (cons m₂ x) h₃ ⟩
star-helper m₂ (cons m₂ x)
≡⟨ star-helper-i-cons-i x m₂ ⟩
end (cons m₂ x)
∎
h₅ : star y ≡ star-helper m₂ y
h₅ = star-just m₂ y eq₂
h₆ : Embedding-gap⁺ (Embedding-gap _≼_) (star (cons m₂ x)) (star y)
h₆ rewrite h₄ | h₅ = h
h₇ : Embedding-gap⁺ _≼_ (cons m₂ x) y
h₇ = embed-star-Embed (cons m₂ x) y (trans h₃ (sym eq₂)) h₆
embed-star-Embed (cons (F.suc i) x) (cons .m₁ y) refl h₂ | just m₁ | just m₂ | inj₂ 1+i>m₁ | inj₁ j≤m₂
rewrite star-helper->-suc m₁ i x 1+i>m₁ | star-helper-i-cons-i y m₁ with h₂
... | ()
embed-star-Embed (cons (F.suc i) x) (cons (F.suc j) y) refl h₂ | just m₁ | just .m₁ | inj₂ 1+i>m₁ | inj₂ 1+j>m₁
rewrite star-helper->-suc m₁ i x 1+i>m₁ | star-helper->-suc m₁ j y 1+j>m₁ with h₂
... | i≤j ∷ʳ h = s≤s i≤j ∷ʳ h₇
where
h₃ : min (cons (F.suc i) x) ≡ just m₁
h₃ = min-cons-> x m₁ (F.suc i) eq₁ 1+i>m₁
h₄ : star (cons (F.suc i) x) ≡ cons i (star-helper m₁ x)
h₄ =
begin
star (cons (F.suc i) x)
≡⟨ star-just m₁ (cons (F.suc i) x) h₃ ⟩
star-helper m₁ (cons (F.suc i) x)
≡⟨ star-helper->-suc m₁ i x 1+i>m₁ ⟩
cons i (star-helper m₁ x)
∎
h₅ : star y ≡ star-helper m₁ y
h₅ = star-just m₁ y eq₂
h₆ : Embedding-gap⁺ (Embedding-gap _≼_)
(star (cons (F.suc i) x)) (star y)
h₆ rewrite h₄ | h₅ = h
h₇ : Embedding-gap⁺ _≼_ (cons (F.suc i) x) y
h₇ = embed-star-Embed (cons (F.suc i) x) y (trans h₃ (sym eq₂)) h₆
... | .j ∷ h = (F.suc j) ∷ h₆
where
h₃ : star x ≡ star-helper m₁ x
h₃ = star-just m₁ x eq₁
h₄ : star y ≡ star-helper m₁ y
h₄ = star-just m₁ y eq₂
h₅ : Embedding-gap⁺ (Embedding-gap _≼_) (star x) (star y)
h₅ rewrite h₃ | h₄ = h
h₆ : Embedding-gap⁺ _≼_ x y
h₆ = embed-star-Embed x y (trans eq₁ (sym eq₂)) h₅
embed-star-Embed (cons i x) (cons j y) h₁ h₂ | just m₁ | nothing with ≤-<-connex (toℕ i) (toℕ m₁)
```
Here a contradition is already apparent since if min x ≡ just m₁ and min y ≡ nothing, then
size x ≥ 2 and size y ≡ 1, which means that star (cons i x) cannot embed into star (cons j y).
Rather than state and prove this general fact, we let Agda look for a proof of such an embedding
and fail.
```agda
embed-star-Embed (cons i x) (cons .i y) refl h₂ | just m₁ | nothing | inj₁ i≤m₁
rewrite star-helper-i-cons-i x i | star-helper-i-cons-i y i with min-nothing y eq₂
... | a , refl with h₂
... | end (mk (.i ∷ end h)) = ⊥-elim (just≢nothing (sym eq₁))
... | end (.i ∷ʳ mk ())
embed-star-Embed (cons (F.suc i) x) (cons .m₁ y) refl h₂ | just m₁ | nothing | inj₂ 1+i>m₁
rewrite star-helper->-suc m₁ i x 1+i>m₁ | star-helper-i-cons-i y m₁ with h₂
... | ()
embed-star-Embed (cons i x) (cons j y) h₁ h₂ | nothing | just m₁ with ≤-<-connex (toℕ j) (toℕ m₁)
embed-star-Embed (cons .j x) (cons j y) refl h₂ | nothing | just m₁ | inj₁ j≤m₁
rewrite star-helper-i-cons-i x j | star-helper-i-cons-i y j with h₂
... | end h = emb-gap-min-emb-gap⁺ _≼_ h₄ h
where
h₃ : min (cons j y) ≡ just j
h₃ = min-cons-≤ y m₁ j eq₂ j≤m₁
h₄ : just j ≤′ min (cons j y)
h₄ = ≤′-reflexive (sym h₃)
embed-star-Embed (cons m₁ x) (cons (F.suc j) y) refl h₂ | nothing | just m₁ | inj₂ 1+j>m₁
rewrite star-helper-i-cons-i x m₁ | star-helper->-suc m₁ j y 1+j>m₁ with h₂
... | tt ∷ʳ h = ≤-trans (≤-step ≤-refl) 1+j>m₁ ∷ʳ h₇
where
h₃ : min (cons m₁ x) ≡ just m₁
h₃ = min-cons-nothing x m₁ eq₁
h₄ : star (cons m₁ x) ≡ end (cons m₁ x)
h₄ =
begin
star (cons m₁ x)
≡⟨ star-just m₁ (cons m₁ x) h₃ ⟩
star-helper m₁ (cons m₁ x)
≡⟨ star-helper-i-cons-i x m₁ ⟩
end (cons m₁ x)
∎
h₅ : star y ≡ star-helper m₁ y
h₅ = star-just m₁ y eq₂
h₆ : Embedding-gap⁺ (Embedding-gap _≼_) (star (cons m₁ x)) (star y)
h₆ rewrite h₄ | h₅ = h
h₇ : Embedding-gap⁺ _≼_ (cons m₁ x) y
h₇ = embed-star-Embed (cons m₁ x) y (trans h₃ (sym eq₂)) h₆
embed-star-Embed (cons i x) (cons .i y) refl h₂ | nothing | nothing
rewrite star-helper-i-cons-i x i | star-helper-i-cons-i y i with h₂
... | end h = emb-gap-min-emb-gap⁺ _≼_ h₄ h
where
h₃ : min (cons i y) ≡ just i
h₃ = min-cons-nothing y i eq₂
h₄ : just i ≤′ min (cons i y)
h₄ = ≤′-reflexive (sym 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 together with a binary relarion _≼_ and for every sequence f of words in Word A n,
if its leaf sequence is very good with respect to _≼_, then f is very good with respect to Embedding-gap⁺ _≼_.
```agda
Gap⁺-good : (n : ℕ) → Set₁
Gap⁺-good n = {A : Set} (_≼_ : A → A → Set) (f : ℕ → Word A n)
→ VeryGood _≼_ (leaf ∘ f)
→ Good (Embedding-gap⁺ _≼_) f
Gap⁺ : (n : ℕ) → Set₁
Gap⁺ n = {A : Set} (_≼_ : A → A → Set) (f : ℕ → Word A n)
→ VeryGood _≼_ (leaf ∘ f)
→ VeryGood (Embedding-gap⁺ _≼_) f
gap⁺-good-gap⁺ : (n : ℕ) → Gap⁺-good n → Gap⁺ n
gap⁺-good-gap⁺ n hgood _≼_ f h r r-increasing =
hgood _≼_ (f ∘ r) (subseq-veryGood _≼_ (leaf ∘ f) r h r-increasing)
```
Gap-suc n means that for every A with a binary relation _≼_ on A and every sequence f of words in Word A (suc n),
if its leaf sequence is very good with respect to _≼_, then f is very good with respect to Embedding-gap _≼_.
```agda
Gap-suc-good : (n : ℕ) → Set₁
Gap-suc-good n = {A : Set} (_≼_ : A → A → Set) (f : ℕ → Word A (suc n))
→ VeryGood _≼_ (leaf ∘ f)
→ Good (Embedding-gap _≼_) f
Gap-suc : (n : ℕ) → Set₁
Gap-suc n = {A : Set} (_≼_ : A → A → Set) (f : ℕ → Word A (suc n))
→ VeryGood _≼_ (leaf ∘ f)
→ 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-n _≼_ f h r r-increasing =
gap-suc-good-n _≼_ (f ∘ r) (subseq-veryGood _≼_ (leaf ∘ f) r h r-increasing)
```
Lemma 4.6
```agda
gap-suc-gap⁺-implies-gap⁺-suc : (n : ℕ) → Gap-suc n → Gap⁺ n → Gap⁺ (suc n)
gap-suc-gap⁺-implies-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 leaf∘f-veryGood = i , j , i<j , fifj
where
l : ℕ → Word A (suc n)
l i = leaf (star (f i))
h₁ : (i : ℕ) → (leaf ∘ f) i ≡ (leaf ∘ l) i
h₁ i = leaf≡leaf∘leaf∘star (f i)
h₂ : VeryGood _≼_ (leaf ∘ l)
h₂ = veryGood-extensional {A = A} {_≼_ = _≼_} (leaf ∘ f) (leaf ∘ l) h₁ leaf∘f-veryGood
h₃ : VeryGood (Embedding-gap _≼_) l
h₃ = gap-suc-n _≼_ l h₂
h₄ : VeryGood (Embedding-gap⁺ (Embedding-gap _≼_)) (star ∘ f)
h₄ = gap⁺-n (Embedding-gap _≼_) (star ∘ f) h₃
p = prodOrder (_≡_ {A = Maybe (Fin (suc n))}) (Embedding-gap⁺ (Embedding-gap _≼_))
h₅ : VeryGood (_≡_ {A = Maybe (Fin (suc n))}) (min ∘ f)
h₅ = almostFull-veryGood _≡_ (min ∘ f) MaybeFin-≡.almostFull
h₆ : VeryGood p (prodSeq (min ∘ f) (star ∘ f))
h₆ = prod-veryGood {_≼₁_ = _≡_ {A = Maybe (Fin (suc n))}} {_≼₂_ = Embedding-gap⁺ (Embedding-gap _≼_)}
{f = min ∘ f} {g = star ∘ f} trans h₅ h₄
h₇ = veryGood⇒good p (prodSeq (min ∘ f) (star ∘ f)) h₆
i = proj₁ h₇
j = proj₁ (proj₂ h₇)
i<j = proj₁ (proj₂ (proj₂ h₇))
sfisfj : Embedding-gap⁺ (Embedding-gap _≼_) (star (f i)) (star (f j))
sfisfj = proj₂ (proj₂ (proj₂ (proj₂ h₇)))
mfi≡mfj = proj₁ (proj₂ (proj₂ (proj₂ h₇)))
fifj : Embedding-gap⁺ _≼_ (f i) (f j)
fifj = embed-star-Embed (f i) (f j) mfi≡mfj sfisfj
```
Lemma 4.7
```agda
gap⁺-implies-gap-suc : (n : ℕ) → Gap⁺ n → Gap-suc n
gap⁺-implies-gap-suc n gap⁺-n = gap-suc-good-gap-suc n gap-suc-good-n
where
gap-suc-good-n : Gap-suc-good n
gap-suc-good-n {A} _≼_ f leaf∘f-veryGood = ¬¬-elim f-notBad
where
f-notBad : ¬ (¬ Good (Embedding-gap _≼_) f)
f-notBad f-bad = mbs-bad mbs-good
where
open MBS {A = Word A (suc n)} size (Embedding-gap _≼_) _⊑_ (λ {x} → ⊑-refl x) {f = f} f-bad hiding (_⊏_)
leaf∘mbs-veryGood : VeryGood _≼_ (leaf ∘ mbs)
leaf∘mbs-veryGood =
veryGood-extensional {A = A} {_≼_ = _≼_}
(leaf ∘ f ∘ s) (leaf ∘ mbs) (sym ∘ leaf∘mbs≡leaf∘f∘s) leaf∘f∘s-veryGood
where
s : ℕ → ℕ
s = proj₁ (mbs-sub-⊑)
s-increasing : Increasing _<_ s
s-increasing = proj₁ (proj₂ mbs-sub-⊑)
leaf∘mbs≡leaf∘f∘s : (i : ℕ) → leaf (mbs i) ≡ leaf (f (s i))
leaf∘mbs≡leaf∘f∘s i = ⊑-leaf (proj₂ (proj₂ mbs-sub-⊑) i)
leaf∘f∘s-veryGood : VeryGood _≼_ (leaf ∘ f ∘ s)
leaf∘f∘s-veryGood = subseq-veryGood _≼_ (leaf ∘ f) s leaf∘f-veryGood s-increasing
Inf = (k : ℕ) → Σ[ l ∈ ℕ ] k < l × size (mbs l) ≡ 1
h₁ : Inf ⊎ Σ[ k ∈ ℕ ] ((l : ℕ) → k < l → size (mbs l) ≢ 1)
h₁ = infinite-or-cofinite-¬ (λ i → size (mbs i) ≡ 1)
h₂ : Inf → ⊥
h₂ 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 = increasing-step-increasing r r-step
h₃ : (i : ℕ) → mbs (r i) ≡ end (leaf (mbs (r i)))
h₃ zero = size≡1 (mbs k) (proj₂ (proj₂ (inf zero)))
h₃ (suc i) = size≡1 (mbs (r (suc i))) (proj₂ (proj₂ (inf (r i))))
leaf∘mbs∘r-good : Good _≼_ (leaf ∘ mbs ∘ r)
leaf∘mbs∘r-good = leaf∘mbs-veryGood r r-increasing
i = proj₁ leaf∘mbs∘r-good
j = proj₁ (proj₂ leaf∘mbs∘r-good)
i<j = proj₁ (proj₂ (proj₂ leaf∘mbs∘r-good))
h₄ : leaf (mbs (r i)) ≼ leaf (mbs (r j))
h₄ = proj₂ (proj₂ (proj₂ leaf∘mbs∘r-good))
h₅ : Embedding-gap {A = A} {n = suc n} _≼_ (end (leaf (mbs (r i)))) (end (leaf (mbs (r j))))
h₅ = mk (end h₄)
h₆ : Embedding-gap {A = A} {n = suc n} _≼_ (mbs (r i)) (mbs (r j))
h₆ = subst (λ z → Embedding-gap {A = A} {n = suc n} _≼_ z (mbs (r j))) (sym (h₃ i))
(subst (Embedding-gap {A = A} {n = suc n} _≼_ (end (leaf (mbs (r i))))) (sym (h₃ j)) h₅)
contra : ⊥
contra = mbs-bad (r i , r j , r-increasing i j i<j , h₆)
h₇ : Σ[ k ∈ ℕ ] ((l : ℕ) → k < l → size (mbs l) ≢ 1)
h₇ = ⊎-¬ˡ h₁ h₂
k = proj₁ h₇
cof : (l : ℕ) → k < l → 1 < size (mbs l)
cof l k<l = ≤∧≢⇒< (size≥1 (mbs l)) (λ z → proj₂ h₇ l k<l (sym z))
g-helper : (l : ℕ) → ∃₂ (λ i x → mbs (l + (1 + k)) ≡ cons i x)
g-helper l = size>1 (mbs (l + (1 + k))) ineq
where
ineq : 1 < size (mbs (l + (1 + k)))
ineq = cof (l + (1 + k)) ((m≤n+m (1 + k)) l)
g : ℕ → Word A (suc n)
g l = proj₁ (proj₂ (g-helper l))
g-head : ℕ → Fin (suc n)
g-head l = proj₁ (g-helper l)
g-cons : (l : ℕ) → mbs (l + (1 + k)) ≡ cons (g-head l) (g l)
g-cons l = proj₂ (proj₂ (g-helper l))
g-⊏ : (l : ℕ) → g l ⊏ mbs (l + (1 + k))
g-⊏ l = subst (g l ⊏_) (sym (g-cons l)) (tail-⊏ (g-head l) (g l))
open Sub-⊑-⊏ ⊏-size-< (emb-gap-⊑-emb-gap _≼_) ⊑-transitive
g∈Sub-⊏-mbs : g ∈ Sub-⊏ mbs
g∈Sub-⊏-mbs = r , r-increasing , g-⊏
where
r : ℕ → ℕ
r i = i + (1 + k)
r-increasing : Increasing _<_ r
r-increasing m n m<n = +-monoˡ-< (1 + k) m<n
g* : ℕ → Word (Word A (suc n)) n
g* i = star (g i)
leaf∘g*-veryGood-emb-gap-suc : VeryGood (Embedding-gap {A = A} {n = suc n} _≼_) (leaf ∘ g*)
leaf∘g*-veryGood-emb-gap-suc = Sub-⊏-mbs⇒VeryGood (leaf ∘ g*) leaf∘g*∈Sub-⊏-mbs
where
leaf∘g*∈Sub-⊏-mbs : leaf ∘ g* ∈ Sub-⊏ mbs
leaf∘g*∈Sub-⊏-mbs =
(_+ (1 + k)) , (λ _ _ → +-monoˡ-< (1 + k)) , λ i → ⊑-⊏-⊏ (leaf∘star-⊑ (g i)) (g-⊏ i)
g*-veryGood-emb-gap⁺ :
VeryGood (Embedding-gap⁺ {A = Word A (suc n)} {n = n} (Embedding-gap {A = A} {n = suc n} _≼_)) g*
g*-veryGood-emb-gap⁺ =
gap⁺-n {A = Word A (suc n)} (Embedding-gap {A = A} {n = suc n} _≼_) g* leaf∘g*-veryGood-emb-gap-suc
p = prodOrder (_≡_ {A = Maybe (Fin (suc n))})
(Embedding-gap⁺ {A = Word A (suc n)} {n = n} (Embedding-gap {A = A} {n = suc n} _≼_))
seq = prodSeq (min ∘ g) g*
min∘g,g*-veryGood-emb-gap+ : VeryGood p seq
min∘g,g*-veryGood-emb-gap+ =
prod-veryGood
{_≼₁_ = _≡_}
{_≼₂_ = Embedding-gap⁺ {A = Word A (suc n)} {n = n} (Embedding-gap {A = A} {n = suc n} _≼_)}
{f = min ∘ g} {g = g*}
trans
(almostFull-veryGood {A = Maybe (Fin (suc n))} _≡_ (min ∘ 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)) h₁₀ h₁₁)
where
h₉ : Good p (seq ∘ r)
h₉ = min∘g,g*-veryGood-emb-gap+ r r-increasing
i j : ℕ
i = proj₁ h₉
j = proj₁ (proj₂ h₉)
i<j : i < j
i<j = proj₁ (proj₂ (proj₂ h₉))
h₁₀ : min (g (r i)) ≡ min (g (r j))
h₁₀ = proj₁ (proj₂ (proj₂ (proj₂ h₉)))
h₁₁ : Embedding-gap⁺ {A = Word A (suc n)} {n = n}
(Embedding-gap {A = A} {n = suc n} _≼_) (g* (r i)) (g* (r j))
h₁₁ = proj₂ (proj₂ (proj₂ (proj₂ h₉)))
p₁ = prodOrder (_≡_ {A = Fin (suc n)})
(Embedding-gap⁺ {A = A} {n = suc n} _≼_)
seq₁ = prodSeq g-head g
g-head,g-veryGood-emb-gap⁺-suc : VeryGood p₁ seq₁
g-head,g-veryGood-emb-gap⁺-suc =
prod-veryGood
{_≼₁_ = _≡_}
{_≼₂_ = Embedding-gap⁺ {A = A} {n = suc n} _≼_}
{f = g-head}
{g = g}
trans
(almostFull-veryGood _≡_ g-head Fin-≡.almostFull)
g-veryGood-emb-gap⁺-suc
g-head,g-Good-emb-gap⁺-suc : Good p₁ seq₁
g-head,g-Good-emb-gap⁺-suc = veryGood⇒good p₁ seq₁ g-head,g-veryGood-emb-gap⁺-suc
i j : ℕ
i = proj₁ g-head,g-Good-emb-gap⁺-suc
j = proj₁ (proj₂ g-head,g-Good-emb-gap⁺-suc)
i<j : i < j
i<j = proj₁ (proj₂ (proj₂ g-head,g-Good-emb-gap⁺-suc))
h₁₂ : p₁ (seq₁ i) (seq₁ j)
h₁₂ = proj₂ (proj₂ (proj₂ g-head,g-Good-emb-gap⁺-suc))
h₁₃ : g-head i ≡ g-head j
h₁₃ = proj₁ h₁₂
h₁₄ : Embedding-gap⁺ {A = A} {n = suc n} _≼_ (g i) (g j)
h₁₄ = proj₂ h₁₂
h₁₅ : Embedding-gap⁺ {A = A} {n = suc n} _≼_ (mbs (i + (1 + k))) (mbs (j + (1 + k)))
h₁₅ =
subst
(λ z → Embedding-gap⁺ _≼_ z (mbs (j + (1 + k))))
(sym (g-cons i))
(subst
(Embedding-gap⁺ _≼_ (cons (g-head i) (g i)))
(sym (g-cons j))
(subst
(λ z → Embedding-gap⁺ _≼_ (cons (g-head i) (g i)) (cons z (g j)))
h₁₃
(g-head i ∷ h₁₄)))
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 h₁₅)
```
This is weird. With h₁₅ in place of mk h₁₅ in the above line, you can prove 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
```agda
gap⁺ : (n : ℕ) → Gap⁺ n
gap-suc : (n : ℕ) → Gap-suc n
gap⁺ zero {A = A} _≼_ f leaf∘f-veryGood r r-increasing = i , j , i<j , h₂
where
leaf∘f∘r-good : Good _≼_ (leaf ∘ (f ∘ r))
leaf∘f∘r-good = leaf∘f-veryGood r r-increasing
f≡end∘leaf∘f : (k : ℕ) → f k ≡ end (leaf (f k))
f≡end∘leaf∘f k with f k
... | end a = refl
i j : ℕ
i = proj₁ leaf∘f∘r-good
j = proj₁ (proj₂ leaf∘f∘r-good)
i<j = proj₁ (proj₂ (proj₂ leaf∘f∘r-good))
h₁ : leaf (f (r i)) ≼ leaf (f (r j))
h₁ = proj₂ (proj₂ (proj₂ leaf∘f∘r-good))
h₂ : Embedding-gap⁺ {A = A} {n = zero} _≼_ (f (r i)) (f (r j))
h₂ rewrite f≡end∘leaf∘f (r i) | f≡end∘leaf∘f (r j) = end h₁
gap⁺ (suc n) = gap-suc-gap⁺-implies-gap⁺-suc n (gap-suc n) (gap⁺ n)
gap-suc n = gap⁺-implies-gap-suc n (gap⁺ n)
emb-gap⁺-almostFull : {A : Set} (_≼_ : A → A → Set)
→ AlmostFull _≼_
→ (n : ℕ) → AlmostFull {A = Word A n} (Embedding-gap⁺ {A = A} {n = n} _≼_)
emb-gap⁺-almostFull {A} _≼_ ≼-almostFull n f = veryGood⇒good (Embedding-gap⁺ {A = A} {n = n} _≼_) f f-veryGood
where
leaf∘f-veryGood : VeryGood _≼_ (leaf ∘ f)
leaf∘f-veryGood = almostFull-veryGood _≼_ (leaf ∘ f) ≼-almostFull
f-veryGood : VeryGood (Embedding-gap⁺ {A = A} {n = n} _≼_) f
f-veryGood = gap⁺ n _≼_ f leaf∘f-veryGood
emb-gap⁺-isWQO : {A : Set} {_≼_ : A → A → Set} → IsWQO _≼_ → (n : ℕ) → IsWQO (Embedding-gap⁺ {A = A} {n = n} _≼_)
emb-gap⁺-isWQO {A} {_≼_} ≼-isWQO n =
record
{ isQO = emb-gap⁺-isQO {n = n} _≼_ (IsWQO.isQO ≼-isWQO)
; almostFull = emb-gap⁺-almostFull _≼_ (IsWQO.almostFull ≼-isWQO) n
}
```