Registers as counters and as loop positions

The registers of DescriptiveComplexity.InductiveCounting.Cfg hold values in WithBot V, read in two ways: as a count, through DescriptiveComplexity.orank (so ⊥ is 0 and each cover adds one), and as a loop position, through DescriptiveComplexity.InductiveCounting.predSet (the set of nodes already scanned). This file collects the arithmetic of the two readings: how a cover moves a loop past one more node, how the count of a set restricted to the scanned part grows, and when a counter still has room to be incremented.

instance DescriptiveComplexity.InductiveCounting.instFiniteWithBot {V : Type} [Finite V] : Finite (WithBot V)

Covers in a finite linear order

Counts

@[simp]

theorem DescriptiveComplexity.InductiveCounting.orank_bot {V : Type} [LinearOrder V] : orank ⊥ = 0

Loop positions

def DescriptiveComplexity.InductiveCounting.predSet {V : Type} [LinearOrder V] (r : WithBot V) : Set V

The set of nodes strictly below the value of a register: the nodes a loop holding that value has already scanned.

Equations

• DescriptiveComplexity.InductiveCounting.predSet r = {y : V | ↑y < r}

@[simp]

theorem DescriptiveComplexity.InductiveCounting.predSet_bot {V : Type} [LinearOrder V] : predSet ⊥ = ∅

Counting the scanned part of a set

theorem DescriptiveComplexity.InductiveCounting.ncard_le_card {V : Type} [Finite V] (P : Set V) : P.ncard ≤ Nat.card V