Parity condition on infinite sequences

DefinitionLargest infinitely occurring value#✓fully proved

Let \((p_k)_{k \in \mathbb{N}}\) be a sequence of natural numbers and \(n \in \mathbb{N}\). Then \(n\) is the largest value occurring infinitely often in \((p_k)\) if \(p_k = n\) for infinitely many \(k\), and every \(m \in \mathbb{N}\) with \(p_k = m\) for infinitely many \(k\) satisfies \(m \le n\).

Larger values may still occur, each only finitely often; for bounded sequences they eventually stop occurring.

def IsMaxInfOcc (ps : ωSequence ℕ) (n : ℕ) : Prop :=
  (∃ᶠ k in atTop, ps k = n) ∧ ∀ m, (∃ᶠ k in atTop, ps k = m) → m ≤ n

Used by 15

Used bySequences that stay at the win state are won by the even player · Sequences that stay at the lose state are won by the odd player · Every state sequence of a finite parity automaton has a parity winner · The tail of a bounded sequence is bounded by its largest infinitely occurring value · Bounded sequences have a largest infinitely occurring value · Prefix independence of the largest infinitely occurring value · Even max-parity condition · Max-parity with priorities 1 and 2 is the Büchi condition · Odd max-parity condition · For bounded sequences the odd parity condition is the negation of the even one · No play is won by both players · Winning is prefix independent · Bounded priorities give every play a winner · Parity-to-Rabin conversion preserves the language · Parity-to-Streett conversion preserves the language

DefinitionEven max-parity condition#✓fully proved

A sequence \((p_k)_{k \in \mathbb{N}}\) of natural numbers (priorities) satisfies the even max-parity condition if there is an even \(n\) that is the largest value occurring infinitely often in \((p_k)\).

This is the winning condition of the even player under the max-parity convention.

def ParityEven (ps : ωSequence ℕ) : Prop :=
  ∃ n, Even n ∧ IsMaxInfOcc ps n

Uses 1 · Used by 11

Statement usesLargest infinitely occurring value

Used byBüchi-to-parity conversion preserves the language · Every state sequence of a finite parity automaton has a parity winner · Max-parity with priorities 1 and 2 is the Büchi condition · For bounded sequences the odd parity condition is the negation of the even one · No play is won by both players · Parity winning condition of a player · Winning is prefix independent · Bounded priorities give every play a winner · Parity-to-Muller conversion preserves the language · Parity-to-Rabin conversion preserves the language · Parity-to-Streett conversion preserves the language

DefinitionOdd max-parity condition#✓fully proved

A sequence \((p_k)_{k \in \mathbb{N}}\) of natural numbers (priorities) satisfies the odd max-parity condition if there is an odd \(n\) that is the largest value occurring infinitely often in \((p_k)\).

This is the winning condition of the odd player under the max-parity convention.

def ParityOdd (ps : ωSequence ℕ) : Prop :=
  ∃ n, Odd n ∧ IsMaxInfOcc ps n

Uses 1 · Used by 6

Statement usesLargest infinitely occurring value

Used byEvery state sequence of a finite parity automaton has a parity winner · For bounded sequences the odd parity condition is the negation of the even one · No play is won by both players · Parity winning condition of a player · Winning is prefix independent · Bounded priorities give every play a winner

TheoremBounded sequences have a largest infinitely occurring value#✓fully proved

Let \(d \in \mathbb{N}\). If a sequence \((p_k)_{k \in \mathbb{N}}\) of natural numbers satisfies \(p_k \le d\) for all \(k\), then some natural number \(n \le d\) is the largest value occurring infinitely often in \((p_k)\).

theorem exists_isMaxInfOcc {d : ℕ} (hb : ∀ k, ps k ≤ d) : ∃ n ≤ d, IsMaxInfOcc ps n

Uses 1 · Used by 4

Statement usesLargest infinitely occurring value

Used byEvery state sequence of a finite parity automaton has a parity winner · For bounded sequences the odd parity condition is the negation of the even one · Bounded priorities give every play a winner · Parity-to-Streett conversion preserves the language

TheoremThe tail of a bounded sequence is bounded by its largest infinitely occurring value#✓fully proved

Let \(d \in \mathbb{N}\), let \((p_k)_{k \in \mathbb{N}}\) be a sequence of natural numbers with \(p_k \le d\) for all \(k\), and let \(n\) be the largest value occurring infinitely often in \((p_k)\). Then \(p_k \le n\) for all sufficiently large \(k\).

theorem IsMaxInfOcc.eventually_le {n d : ℕ} (hn : IsMaxInfOcc ps n) (hb : ∀ k, ps k ≤ d) :
    ∀ᶠ k in atTop, ps k ≤ n

Uses 1 · Used by 1

Statement usesLargest infinitely occurring value

Used byParity-to-Rabin conversion preserves the language

TheoremFor bounded sequences the odd parity condition is the negation of the even one#✓fully proved

Let \(d \in \mathbb{N}\). If a sequence \((p_k)_{k \in \mathbb{N}}\) of natural numbers satisfies \(p_k \le d\) for all \(k\), then it satisfies the odd max-parity condition if and only if it does not satisfy the even max-parity condition.

theorem parityOdd_iff_not_parityEven {d : ℕ} (hb : ∀ k, ps k ≤ d) :
    ParityOdd ps ↔ ¬ ParityEven ps

Uses 4

Statement usesEven max-parity condition · Odd max-parity condition

Proof usesLargest infinitely occurring value · Bounded sequences have a largest infinitely occurring value

TheoremMax-parity with priorities 1 and 2 is the Büchi condition#✓fully proved

Let \((p_k)_{k \in \mathbb{N}}\) be a sequence of natural numbers with \(p_k \in \{1, 2\}\) for every \(k\). Then \((p_k)\) satisfies the even max-parity condition if and only if \(p_k = 2\) for infinitely many \(k\).

theorem parityEven_iff_frequently_two {ps : ωSequence ℕ} (h : ∀ k, ps k = 1 ∨ ps k = 2) :
    ParityEven ps ↔ ∃ᶠ k in atTop, ps k = 2

Uses 2 · Used by 1

Statement usesEven max-parity condition

Proof usesLargest infinitely occurring value

Used byBüchi-to-parity conversion preserves the language

TheoremPrefix independence of the largest infinitely occurring value#✓fully proved

Let \((p_k)_{k \in \mathbb{N}}\) be a sequence of natural numbers and let \(j, n \in \mathbb{N}\). Then \(n\) is the largest value occurring infinitely often in the shifted sequence \((p_{j+k})_{k \in \mathbb{N}}\) if and only if \(n\) is the largest value occurring infinitely often in \((p_k)\).

theorem isMaxInfOcc_drop_iff (j n : ℕ) : IsMaxInfOcc (ps.drop j) n ↔ IsMaxInfOcc ps n

Uses 1 · Used by 1

Statement usesLargest infinitely occurring value

Used byWinning is prefix independent

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.