Registers kept by a block of counter code

Kept B base regs regs' says that a block of counter code, run on the registers regs, left the registers regs' of the same length, unchanged below base, with every register at most B. Compiled formulas and closure loops state their effect on the registers this way, and blocks run in sequence compose by Kept.trans.

Main definitions

• Turing.CounterProgram.Kept: the registers after a block.

Main results

• Turing.CounterProgram.Kept.trans, Turing.CounterProgram.Kept.mono: composing blocks and forgetting registers.
• Turing.CounterProgram.Kept.facts: the cardinality and the free-variable registers survive a block that keeps the registers below them.

structure Turing.CounterProgram.Kept (B base : ℕ) (regs regs' : List ℕ) : Prop

The registers after a block: the same length, unchanged below base, each at most B.

• length_eq : regs'.length = regs.length

  The block does not change the number of registers.

• getD_eq (i : ℕ) : i < base → regs'.getD i 0 = regs.getD i 0

  The block does not change the registers below base.

• bounded (r : ℕ) : r ∈ regs' → r ≤ B

  Every register is at most B after the block.

theorem Turing.CounterProgram.Kept.refl {B base : ℕ} {regs : List ℕ} (hB : ∀ r ∈ regs, r ≤ B) : Kept B base regs regs

theorem Turing.CounterProgram.Kept.trans {B base : ℕ} {r₁ r₂ r₃ : List ℕ} (h₁ : Kept B base r₁ r₂) (h₂ : Kept B base r₂ r₃) : Kept B base r₁ r₃

theorem Turing.CounterProgram.Kept.mono {B base base' : ℕ} {regs regs' : List ℕ} (h : Kept B base' regs regs') (hle : base ≤ base') : Kept B base regs regs'

Keeping the registers below base' keeps those below any base ≤ base'.

theorem Turing.CounterProgram.Kept.set_right {B base j m : ℕ} {regs regs' : List ℕ} (h : Kept B base regs regs') (hj : base ≤ j) (hm : m ≤ B) : Kept B base regs (regs'.set j m)

Setting a register at or above base to a value at most B keeps the registers.

theorem Turing.CounterProgram.Kept.of_set {B base m : ℕ} {regs regs' : List ℕ} (hk : Kept B (base + 1) (regs.set base m) regs') : Kept B base regs regs'

A block that keeps the registers below base + 1 after register base was set keeps the registers below base of the original registers.

theorem Turing.CounterProgram.Kept.facts {B base d n : ℕ} {regs regs' : List ℕ} {α : Type u_1} {fv : α → ℕ} {val : α → Fin n} (hk : Kept B base regs regs') (hbase : 0 < base) (hfv : ∀ (x : α), fv x < base) (hd : base + d ≤ regs.length) (h0 : regs.getD 0 0 = n) (hv : ∀ (x : α), regs.getD (fv x) 0 = ↑(val x)) : base + d ≤ regs'.length ∧ regs'.getD 0 0 = n ∧ ∀ (x : α), regs'.getD (fv x) 0 = ↑(val x)

The cardinality in register 0 and the values of free variables in registers fv x below base survive a block that keeps the registers below base.