Reading a finite prefix and its completion

These elementary bookkeeping facts make precise the paper's statements that “the terms ... which lie in P form an initial segment” and that extending a prefix does not move any of its old entries. They are independent of the special binary order.

theorem FourAP.completion_cons (R : ℕ → ℕ → Prop) (P : List ℕ) (t a b : ℕ) : Completion R (t :: P) a b ↔ a = t ∧ b ≠ t ∨ a ≠ t ∧ b ≠ t ∧ Completion R P a b

The completion of a word beginning with t: t comes first, and deleting it leaves the completion of the remaining word. This is bookkeeping for the paper's operation of putting a finite word before the binary-ordered tail.

theorem FourAP.completion_mem_notMem {R : ℕ → ℕ → Prop} {P : List ℕ} {a b : ℕ} (ha : a ∈ P) (hb : ¬b ∈ P) : Completion R P a b

In 𝒞(P), each entry of P precedes every unused integer.

theorem FourAP.completion_of_notMem {R : ℕ → ℕ → Prop} {P : List ℕ} {a b : ℕ} (ha : ¬a ∈ P) (hb : ¬b ∈ P) : Completion R P a b ↔ R a b

On the unused integers, 𝒞(P) agrees with the background order.

theorem FourAP.completion_mem_left {R : ℕ → ℕ → Prop} {P : List ℕ} {a b : ℕ} (h : Completion R P a b) (hb : b ∈ P) : a ∈ P

No entry outside the prefix can precede an entry inside it.

theorem FourAP.completion_asymm {R : ℕ → ℕ → Prop} {P : List ℕ} {a b : ℕ} (hR : ∀ ⦃x y : ℕ⦄, R x y → ¬R y x) (h : Completion R P a b) : ¬Completion R P b a

A completion is asymmetric whenever its background order is asymmetric.

theorem FourAP.completion_irrefl {R : ℕ → ℕ → Prop} {P : List ℕ} (hR : ∀ (x : ℕ), ¬R x x) (a : ℕ) : ¬Completion R P a a

The completed order is irreflexive whenever the background order is. Together with the next two lemmas, this verifies that the paper's 𝒞(P) is a strict linear order rather than merely a relation.

theorem FourAP.completion_trans {R : ℕ → ℕ → Prop} {P : List ℕ} {a b c : ℕ} (hR : ∀ ⦃x y z : ℕ⦄, R x y → R y z → R x z) (hab : Completion R P a b) (hbc : Completion R P b c) : Completion R P a c

Concatenating the finite prefix and its background-ordered complement preserves transitivity, as required by the paper's definition of 𝒞(P).

theorem FourAP.completion_total {R : ℕ → ℕ → Prop} {P : List ℕ} {a b : ℕ} (hR : ∀ ⦃x y : ℕ⦄, x ≠ y → R x y ∨ R y x) (hne : a ≠ b) : Completion R P a b ∨ Completion R P b a

Every two distinct entries are comparable in 𝒞(P) when they are comparable in the background order. Thus the finite-prefix construction in the paper indeed defines a strict linear order.

theorem FourAP.completion_prefix_left {R : ℕ → ℕ → Prop} {P Q : List ℕ} {a b : ℕ} (hp : P <+: Q) (ha : a ∈ P) (h : Completion R Q a b) : Completion R P a b

Prefix extension preserves all comparisons whose first entry was already placed. This is used twice in the contradiction argument in Lemma 2.

theorem FourAP.completion_prefix_mem_left {R : ℕ → ℕ → Prop} {P Q : List ℕ} {a b : ℕ} (hp : P <+: Q) (hb : b ∈ P) (h : Completion R Q a b) : a ∈ P

In an extended completion, the old word is still an initial segment.