Inductive counting for negated closures

A negated closure ¬ TC E s₀ z₀ over k-tuples of a universe of size n is certified nondeterministically by the inductive counting of [Imm88] and [Sze87]. Tuples are coded by numbers below n ^ k: the code of xs is (finFunctionFinEquiv xs : ℕ), which is Cslib.Logic.tupleIndex xs by definition, spelled as in the closure loop and codeE. Round i is the set of codes reachable from the code of s₀ within i steps (Cslib.InductiveCounting.roundSet for codeEdge E). Knowing the size of round i, one test decides membership of a code y in round i + 1: it guesses the members of round i in increasing order, certifies each by a walk of at most i steps, certifies for each whether it reaches y in at most one step, and checks the number guessed. Counting the members of round i + 1 this way gives its size; the final test of the code of z₀ at round n ^ k decides reachability.

Main definitions

• Cslib.Logic.FO.Ordered.TCModelChecker.codeEdge: the edge relation on codes.
• Cslib.Logic.FO.Ordered.TCModelChecker.countRound: round i, the codes reachable within i steps.
• Cslib.Logic.FO.Ordered.TCModelChecker.TestPre: the state before one test.

Main results

• Cslib.Logic.FO.Ordered.TCModelChecker.mem_roundSet_codeEdge_iff: rounds are bounded reachability.
• Cslib.Logic.FO.Ordered.TCModelChecker.test_sound, Cslib.Logic.FO.Ordered.TCModelChecker.test_complete: one test.
• Cslib.Logic.FO.Ordered.TCModelChecker.count_sound, Cslib.Logic.FO.Ordered.TCModelChecker.count_complete: the counting block.

References

• N. Immerman, Nondeterministic Space is Closed Under Complementation
• R. Szelepcsényi, The Method of Forcing for Nondeterministic Automata

noncomputable def Cslib.Logic.FO.Ordered.TCModelChecker.codeEdge {n k : ℕ} (E : (Fin k → Fin n) → (Fin k → Fin n) → Prop) (c d : ℕ) : Bool

The edge relation E on tuples, on their codes below n ^ k.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.codeEdge_code {n k : ℕ} {E : (Fin k → Fin n) → (Fin k → Fin n) → Prop} (xs ys : Fin k → Fin n) : codeEdge E ↑(finFunctionFinEquiv xs) ↑(finFunctionFinEquiv ys) = true ↔ E xs ys

theorem Cslib.Logic.FO.Ordered.TCModelChecker.relatesWithinSteps_codeEdge_iff {n k : ℕ} {E : (Fin k → Fin n) → (Fin k → Fin n) → Prop} {xs ys : Fin k → Fin n} {m : ℕ} : Relation.RelatesWithinSteps (InductiveCounting.Graph (n ^ k) (codeEdge E)) (↑(finFunctionFinEquiv xs)) (↑(finFunctionFinEquiv ys)) m ↔ Relation.RelatesWithinSteps E xs ys m

Walks between codes are walks between tuples.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.mem_roundSet_codeEdge_iff {n k : ℕ} {E : (Fin k → Fin n) → (Fin k → Fin n) → Prop} {xs ys : Fin k → Fin n} {i : ℕ} : ↑(finFunctionFinEquiv ys) ∈ InductiveCounting.roundSet (n ^ k) (codeEdge E) (↑(finFunctionFinEquiv xs)) i ↔ Relation.RelatesWithinSteps E xs ys i

Rounds are bounded reachability: the code of ys is in round i exactly when ys is reached from xs within i steps.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.mem_roundSet_pow_iff {n k : ℕ} {E : (Fin k → Fin n) → (Fin k → Fin n) → Prop} {xs ys : Fin k → Fin n} : ↑(finFunctionFinEquiv ys) ∈ InductiveCounting.roundSet (n ^ k) (codeEdge E) (↑(finFunctionFinEquiv xs)) (n ^ k) ↔ Relation.ReflTransGen E xs ys

Round n ^ k is reachability.

noncomputable def Cslib.Logic.FO.Ordered.TCModelChecker.countRound {n k : ℕ} (E : (Fin k → Fin n) → (Fin k → Fin n) → Prop) (s₀ : Fin k → Fin n) (i : ℕ) : Finset ℕ

Round i of inductive counting from s₀: the codes of the tuples reached from s₀ within i steps.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.countTestCode_parts {P : Turing.CounterProgram} {b base k : ℕ} {src : Fin k → Turing.CounterProgram.Expr} {wb et ef : List Turing.CounterProgram.Instr} {T R w₁ : ℕ} (hw : w₁ = b + 14 + 5 * k + wb.length) (hP : P.CodeAt b (countTestCode b base k src wb et ef T R)) : P.instr b = (Turing.CounterProgram.Instr.assign (base + 6) (Turing.CounterProgram.Expr.const 0) (b + 1)).shift ∧ P.instr (b + 1) = (Turing.CounterProgram.Instr.assign (base + 5) (Turing.CounterProgram.Expr.const 0) (b + 2)).shift ∧ P.instr (b + 2) = (Turing.CounterProgram.Instr.assign (base + 4) (Turing.CounterProgram.Expr.const 0) (b + 3)).shift ∧ P.instr (b + 3) = (Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.reg (base + 4)) ((Turing.CounterProgram.Expr.reg 0).pow k) (b + 4) (w₁ + 10 + et.length + ef.length)).shift ∧ P.instr (b + 4) = (Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.const 0) (Turing.CounterProgram.Expr.const 0) (b + 5) (b + 5)).shift ∧ P.instr (b + 5) = Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.reg 0) (Turing.CounterProgram.Expr.const 1) (b + 6) (w₁ + 9 + et.length + ef.length) ∧ P.CodeAt (b + 6) (assignChain (b + 6) (base + 7) k (ClosureKernel.digitE (base + 4))) ∧ P.CodeAt (b + 6 + k) (assignChain (b + 6 + k) (base + 7 + k) k (ClosureKernel.digitE (base + 3))) ∧ P.CodeAt (b + 6 + 2 * k) (tcCode (b + 6 + 2 * k) (base + 7 + 2 * k) k src (fun (i : Fin k) => ClosureKernel.digitE (base + 4) ↑i) (Turing.CounterProgram.Expr.reg base) wb w₁ R) ∧ P.instr w₁ = (Turing.CounterProgram.Instr.assign (base + 5) ((Turing.CounterProgram.Expr.reg (base + 5)).add (Turing.CounterProgram.Expr.const 1)) (w₁ + 1)).shift ∧ P.instr (w₁ + 1) = (Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.const 0) (Turing.CounterProgram.Expr.const 0) (w₁ + 2) (w₁ + 2)).shift ∧ P.instr (w₁ + 2) = Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.reg 0) (Turing.CounterProgram.Expr.const 1) (w₁ + 3) (w₁ + 8 + et.length) ∧ P.instr (w₁ + 3) = (Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.const 0) (Turing.CounterProgram.Expr.const 0) (w₁ + 4) (w₁ + 4)).shift ∧ P.instr (w₁ + 4) = Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.reg 0) (Turing.CounterProgram.Expr.const 1) (w₁ + 5) (w₁ + 8) ∧ P.instr (w₁ + 5) = (Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.const 0) (distE (base + 4) (base + 3)) R (w₁ + 6)).shift ∧ P.instr (w₁ + 6) = (Turing.CounterProgram.Instr.assign (base + 6) (Turing.CounterProgram.Expr.const 1) (w₁ + 9 + et.length + ef.length)).shift ∧ P.instr (w₁ + 7) = (Turing.CounterProgram.Instr.assign (base + 6) (Turing.CounterProgram.Expr.const 1) (w₁ + 9 + et.length + ef.length)).shift ∧ P.CodeAt (w₁ + 8) et ∧ P.instr (w₁ + 8 + et.length) = (Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.const 0) (distE (base + 4) (base + 3)) (w₁ + 9 + et.length) R).shift ∧ P.CodeAt (w₁ + 9 + et.length) ef ∧ P.instr (w₁ + 9 + et.length + ef.length) = (Turing.CounterProgram.Instr.assign (base + 4) ((Turing.CounterProgram.Expr.reg (base + 4)).add (Turing.CounterProgram.Expr.const 1)) (b + 3)).shift ∧ P.instr (w₁ + 10 + et.length + ef.length) = (Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.const 0) (distE (base + 5) (base + 1)) R T).shift

theorem Cslib.Logic.FO.Ordered.TCModelChecker.countCode_parts {P : Turing.CounterProgram} {b base k : ℕ} {dst : Fin k → Turing.CounterProgram.Expr} {t₁ t₂ : List Turing.CounterProgram.Instr} {T R : ℕ} (hP : P.CodeAt b (countCode b base k dst t₁ t₂ T R)) : P.instr b = (Turing.CounterProgram.Instr.assign base (Turing.CounterProgram.Expr.const 0) (b + 1)).shift ∧ P.instr (b + 1) = (Turing.CounterProgram.Instr.assign (base + 1) (Turing.CounterProgram.Expr.const 1) (b + 2)).shift ∧ P.instr (b + 2) = (Turing.CounterProgram.Instr.lt ((Turing.CounterProgram.Expr.reg base).add (Turing.CounterProgram.Expr.const 1)) ((Turing.CounterProgram.Expr.reg 0).pow k) (b + 3) (b + t₁.length + 10)).shift ∧ P.instr (b + 3) = (Turing.CounterProgram.Instr.assign (base + 2) (Turing.CounterProgram.Expr.const 0) (b + 4)).shift ∧ P.instr (b + 4) = (Turing.CounterProgram.Instr.assign (base + 3) (Turing.CounterProgram.Expr.const 0) (b + 5)).shift ∧ P.instr (b + 5) = (Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.reg (base + 3)) ((Turing.CounterProgram.Expr.reg 0).pow k) (b + 6) (b + t₁.length + 8)).shift ∧ P.CodeAt (b + 6) t₁ ∧ P.instr (b + t₁.length + 6) = (Turing.CounterProgram.Instr.assign (base + 2) ((Turing.CounterProgram.Expr.reg (base + 2)).add (Turing.CounterProgram.Expr.reg (base + 6))) (b + t₁.length + 7)).shift ∧ P.instr (b + t₁.length + 7) = (Turing.CounterProgram.Instr.assign (base + 3) ((Turing.CounterProgram.Expr.reg (base + 3)).add (Turing.CounterProgram.Expr.const 1)) (b + 5)).shift ∧ P.instr (b + t₁.length + 8) = (Turing.CounterProgram.Instr.assign (base + 1) (Turing.CounterProgram.Expr.reg (base + 2)) (b + t₁.length + 9)).shift ∧ P.instr (b + t₁.length + 9) = (Turing.CounterProgram.Instr.assign base ((Turing.CounterProgram.Expr.reg base).add (Turing.CounterProgram.Expr.const 1)) (b + 2)).shift ∧ P.instr (b + t₁.length + 10) = (Turing.CounterProgram.Instr.assign (base + 3) (codeE k dst) (b + t₁.length + 11)).shift ∧ P.CodeAt (b + t₁.length + 11) t₂ ∧ P.instr (b + t₁.length + 11 + t₂.length) = (Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.reg (base + 6)) (Turing.CounterProgram.Expr.const 1) T R).shift

theorem Cslib.Logic.FO.Ordered.TCModelChecker.eval_codeE {n k : ℕ} {z : Fin k → Turing.CounterProgram.Expr} {zs : Fin k → Fin n} {regs : List ℕ} (h0 : regs.getD 0 0 = n) (hz : ∀ (i : Fin k), Turing.CounterProgram.Expr.eval regs (z i) = ↑(zs i)) : Turing.CounterProgram.Expr.eval regs (codeE k z) = ↑(finFunctionFinEquiv zs)

structure Cslib.Logic.FO.Ordered.TCModelChecker.TestPre (B : ℕ) {n k : ℕ} (base : ℕ) (E : (Fin k → Fin n) → (Fin k → Fin n) → Prop) (s₀ : Fin k → Fin n) (regs₀ : List ℕ) (i y : ℕ) (regs : List ℕ) : Prop

The state before one test of inductive counting: registers below base as in regs₀, the round i < n ^ k in register base, its size in base + 1, and the candidate y < n ^ k in base + 3.

• kept : Turing.CounterProgram.Kept B base regs₀ regs

  The registers below base and the length are kept, and every register is bounded.

• le_length : base + 9 + 4 * k ≤ regs.length

  The test's registers exist.

• size : regs.getD 0 0 = n

  The universe size is in register 0.

• round : regs.getD base 0 = i

  The round is in register base.

• round_lt : i < n ^ k

  The round is below n ^ k.

• card : regs.getD (base + 1) 0 = (countRound E s₀ i).card

  The size of the round is in register base + 1.

• cand : regs.getD (base + 3) 0 = y

  The candidate is in register base + 3.

• cand_lt : y < n ^ k

  The candidate is below n ^ k.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.test_sound {P : Turing.CounterProgram} {w : List Bool} {B : ℕ} {Post : Turing.CounterProgram.Config → Prop} {n k b base T R w₁ : ℕ} {src : Fin k → Turing.CounterProgram.Expr} {wb et ef : List Turing.CounterProgram.Instr} {E : (Fin k → Fin n) → (Fin k → Fin n) → Prop} {s₀ : Fin k → Fin n} {regs₀ : List ℕ} (hw : w₁ = b + 14 + 5 * k + wb.length) (hP : P.CodeAt b (countTestCode b base k src wb et ef T R)) (hB1 : 1 ≤ B) (hnB : n ≤ B) (hNB : n ^ k ≤ B) (hR : (P.instr R).halts = true) (hPost : ∀ (s : Turing.CounterProgram.Config), s.1 = R → Post s) (hsrc : ∀ (regs : List ℕ), (∀ j < base, regs.getD j 0 = regs₀.getD j 0) → ∀ (j : Fin k), Turing.CounterProgram.Expr.eval regs (src j) = ↑(s₀ j)) (hwb : ∀ (regsW : List ℕ) (us ws : Fin k → Fin n) (t : ℕ) (regs₃ : List ℕ), Turing.CounterProgram.Kept B base regs₀ regsW → LoopMid n B (base + 7 + 2 * k) k regsW us ws t regs₃ → Turing.CounterProgram.Block.Sound P w B Post (b + 6 + 2 * k + 2 * k + 7) regs₃ (b + 6 + 2 * k + 2 * k + 7 + wb.length) fun (regs' : List ℕ) => Turing.CounterProgram.Kept B (base + 7 + 2 * k + 2 * k + 2) regs₃ regs' ∧ E us ws) (het : ∀ (regs₂ : List ℕ) (xs ys : Fin k → Fin n), Turing.CounterProgram.Kept B base regs₀ regs₂ → (∀ (j : Fin k), regs₂.getD (base + 7 + ↑j) 0 = ↑(xs j)) → (∀ (j : Fin k), regs₂.getD (base + 7 + k + ↑j) 0 = ↑(ys j)) → Turing.CounterProgram.Block.Sound P w B Post (w₁ + 8) regs₂ (w₁ + 7) fun (regs' : List ℕ) => Turing.CounterProgram.Kept B (base + 7 + 2 * k) regs₂ regs' ∧ E xs ys) (hef : ∀ (regs₂ : List ℕ) (xs ys : Fin k → Fin n), Turing.CounterProgram.Kept B base regs₀ regs₂ → (∀ (j : Fin k), regs₂.getD (base + 7 + ↑j) 0 = ↑(xs j)) → (∀ (j : Fin k), regs₂.getD (base + 7 + k + ↑j) 0 = ↑(ys j)) → Turing.CounterProgram.Block.Sound P w B Post (w₁ + 9 + et.length) regs₂ (w₁ + 9 + et.length + ef.length) fun (regs' : List ℕ) => Turing.CounterProgram.Kept B (base + 7 + 2 * k) regs₂ regs' ∧ ¬E xs ys) {i y : ℕ} {regs : List ℕ} (hpre : TestPre B base E s₀ regs₀ i y regs) : Turing.CounterProgram.Block.Sound P w B Post b regs T fun (regs' : List ℕ) => Turing.CounterProgram.Kept B (base + 4) regs regs' ∧ regs'.getD (base + 6) 0 = if y ∈ countRound E s₀ (i + 1) then 1 else 0

Soundness of one test: from the state before a test of y against round i, every branch rejects or reaches T with register base + 6 recording whether y is in round i + 1, given sound walk and edge codes.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.test_complete {P : Turing.CounterProgram} {w : List Bool} {B n k b base T R w₁ : ℕ} {src : Fin k → Turing.CounterProgram.Expr} {wb et ef : List Turing.CounterProgram.Instr} {E : (Fin k → Fin n) → (Fin k → Fin n) → Prop} {s₀ : Fin k → Fin n} {regs₀ : List ℕ} (hw : w₁ = b + 14 + 5 * k + wb.length) (hP : P.CodeAt b (countTestCode b base k src wb et ef T R)) (hB1 : 1 ≤ B) (hnB : n ≤ B) (hNB : n ^ k ≤ B) (hsrc : ∀ (regs : List ℕ), (∀ j < base, regs.getD j 0 = regs₀.getD j 0) → ∀ (j : Fin k), Turing.CounterProgram.Expr.eval regs (src j) = ↑(s₀ j)) (hwb : ∀ (regsW : List ℕ) (us ws : Fin k → Fin n) (t : ℕ) (regs₃ : List ℕ), Turing.CounterProgram.Kept B base regs₀ regsW → LoopMid n B (base + 7 + 2 * k) k regsW us ws t regs₃ → E us ws → Turing.CounterProgram.Block.Complete P w (b + 6 + 2 * k + 2 * k + 7) regs₃ (b + 6 + 2 * k + 2 * k + 7 + wb.length) (Turing.CounterProgram.Kept B (base + 7 + 2 * k + 2 * k + 2) regs₃)) (het : ∀ (regs₂ : List ℕ) (xs ys : Fin k → Fin n), Turing.CounterProgram.Kept B base regs₀ regs₂ → (∀ (j : Fin k), regs₂.getD (base + 7 + ↑j) 0 = ↑(xs j)) → (∀ (j : Fin k), regs₂.getD (base + 7 + k + ↑j) 0 = ↑(ys j)) → E xs ys → Turing.CounterProgram.Block.Complete P w (w₁ + 8) regs₂ (w₁ + 7) (Turing.CounterProgram.Kept B (base + 7 + 2 * k) regs₂)) (hef : ∀ (regs₂ : List ℕ) (xs ys : Fin k → Fin n), Turing.CounterProgram.Kept B base regs₀ regs₂ → (∀ (j : Fin k), regs₂.getD (base + 7 + ↑j) 0 = ↑(xs j)) → (∀ (j : Fin k), regs₂.getD (base + 7 + k + ↑j) 0 = ↑(ys j)) → ¬E xs ys → Turing.CounterProgram.Block.Complete P w (w₁ + 9 + et.length) regs₂ (w₁ + 9 + et.length + ef.length) (Turing.CounterProgram.Kept B (base + 7 + 2 * k) regs₂)) {i y : ℕ} {regs : List ℕ} (hpre : TestPre B base E s₀ regs₀ i y regs) : Turing.CounterProgram.Block.Complete P w b regs T fun (regs' : List ℕ) => Turing.CounterProgram.Kept B (base + 4) regs regs' ∧ regs'.getD (base + 6) 0 = if y ∈ countRound E s₀ (i + 1) then 1 else 0

Completeness of one test: from the state before a test of y against round i, some branch reaches T with register base + 6 recording whether y is in round i + 1, given complete walk and edge codes.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.count_sound {P : Turing.CounterProgram} {w : List Bool} {B : ℕ} {Post : Turing.CounterProgram.Config → Prop} {n k b base T R : ℕ} {dst : Fin k → Turing.CounterProgram.Expr} {t₁ t₂ : List Turing.CounterProgram.Instr} {E : (Fin k → Fin n) → (Fin k → Fin n) → Prop} {s₀ z₀ : Fin k → Fin n} {regs₀ : List ℕ} (hP : P.CodeAt b (countCode b base k dst t₁ t₂ T R)) (hbase : 0 < base) (hB1 : 1 ≤ B) (hNB : n ^ k ≤ B) (hR : (P.instr R).halts = true) (hPost : ∀ (s : Turing.CounterProgram.Config), s.1 = R → Post s) (hdst : ∀ (regs : List ℕ), (∀ j < base, regs.getD j 0 = regs₀.getD j 0) → ∀ (j : Fin k), Turing.CounterProgram.Expr.eval regs (dst j) = ↑(z₀ j)) (ht₁ : ∀ (i y : ℕ) (regs : List ℕ), TestPre B base E s₀ regs₀ i y regs → Turing.CounterProgram.Block.Sound P w B Post (b + 6) regs (b + t₁.length + 6) fun (regs' : List ℕ) => Turing.CounterProgram.Kept B (base + 4) regs regs' ∧ regs'.getD (base + 6) 0 = if y ∈ countRound E s₀ (i + 1) then 1 else 0) (ht₂ : ∀ (i y : ℕ) (regs : List ℕ), TestPre B base E s₀ regs₀ i y regs → Turing.CounterProgram.Block.Sound P w B Post (b + t₁.length + 11) regs (b + t₁.length + 11 + t₂.length) fun (regs' : List ℕ) => Turing.CounterProgram.Kept B (base + 4) regs regs' ∧ regs'.getD (base + 6) 0 = if y ∈ countRound E s₀ (i + 1) then 1 else 0) (hlen : base + 9 + 4 * k ≤ regs₀.length) (h0 : regs₀.getD 0 0 = n) (hB : ∀ r ∈ regs₀, r ≤ B) : Turing.CounterProgram.Block.Sound P w B Post b regs₀ T fun (regs' : List ℕ) => Turing.CounterProgram.Kept B base regs₀ regs' ∧ ¬Relation.ReflTransGen E s₀ z₀

Soundness of the counting block: every branch rejects or reaches T with the target z₀ not reachable from s₀, given sound tests.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.count_complete {P : Turing.CounterProgram} {w : List Bool} {B n k b base T R : ℕ} {dst : Fin k → Turing.CounterProgram.Expr} {t₁ t₂ : List Turing.CounterProgram.Instr} {E : (Fin k → Fin n) → (Fin k → Fin n) → Prop} {s₀ z₀ : Fin k → Fin n} {regs₀ : List ℕ} (hP : P.CodeAt b (countCode b base k dst t₁ t₂ T R)) (hbase : 0 < base) (hB1 : 1 ≤ B) (hNB : n ^ k ≤ B) (hdst : ∀ (regs : List ℕ), (∀ j < base, regs.getD j 0 = regs₀.getD j 0) → ∀ (j : Fin k), Turing.CounterProgram.Expr.eval regs (dst j) = ↑(z₀ j)) (ht₁ : ∀ (i y : ℕ) (regs : List ℕ), TestPre B base E s₀ regs₀ i y regs → Turing.CounterProgram.Block.Complete P w (b + 6) regs (b + t₁.length + 6) fun (regs' : List ℕ) => Turing.CounterProgram.Kept B (base + 4) regs regs' ∧ regs'.getD (base + 6) 0 = if y ∈ countRound E s₀ (i + 1) then 1 else 0) (ht₂ : ∀ (i y : ℕ) (regs : List ℕ), TestPre B base E s₀ regs₀ i y regs → Turing.CounterProgram.Block.Complete P w (b + t₁.length + 11) regs (b + t₁.length + 11 + t₂.length) fun (regs' : List ℕ) => Turing.CounterProgram.Kept B (base + 4) regs regs' ∧ regs'.getD (base + 6) 0 = if y ∈ countRound E s₀ (i + 1) then 1 else 0) (hlen : base + 9 + 4 * k ≤ regs₀.length) (h0 : regs₀.getD 0 0 = n) (hB : ∀ r ∈ regs₀, r ≤ B) (hreach : ¬Relation.ReflTransGen E s₀ z₀) : Turing.CounterProgram.Block.Complete P w b regs₀ T (Turing.CounterProgram.Kept B base regs₀)

Completeness of the counting block: when the target z₀ is not reachable from s₀, some branch reaches T, given complete tests.