Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Geb.Prototypes.Computability.BitTree.BinaryMachine.Simulation
public import Geb.Prototypes.Computability.BitTree.BinaryMachine.Accounting
public import Geb.Prototypes.Computability.BitTree.BinaryMachine.BitStep
import Mathlib.Tactic.IntervalCases

set_option doc.verso true

Executions of the binary-counter recognizer

The execution at a prefix boundary is indexed by the accumulated cost of the input and counter transitions. A fixed binary width bounds all prefixes of an input.

Main statements

configs_account realizes every prefix account within its accumulated cost.
headBound_start bounds the initialization transitions.

Tags

binary tree, Turing machine, execution, amortized complexity

              @[expose] public sectionnamespace Geb.BitTree.BinaryMachineopen Turing MultiTapeTM

Initialization emits no symbols.

theorem outputString_start (input : List (Fin 4)) :
    machine.outputString (machine.initCfg input) 2 = [] := rfl

The initialization steps visit only cells zero and one.

theorem headBound_start (input : List (Fin 4)) (width : ℕ) (hw : 1 ≤ width) :
    ∀ t ≤ 2, HeadBound width (machine.configs (machine.initCfg input) t) := byinput:List (Fin 4)width:ℕhw:1 ≤ width⊢ ∀ t ≤ 2, HeadBound width (configs (initCfg input) t)
  intro t ht iinput:List (Fin 4)width:ℕhw:1 ≤ widtht:ℕht:t ≤ 2i:Fin 3⊢ 0 ≤ (configs (initCfg input) t).workTapePos i ∧ (configs (initCfg input) t).workTapePos i ≤ ↑width
  interval_cases t«0»input:List (Fin 4)width:ℕhw:1 ≤ widtht:ℕi:Fin 3ht:0 ≤ 2⊢ 0 ≤ (configs (initCfg input) 0).workTapePos i ∧ (configs (initCfg input) 0).workTapePos i ≤ ↑width«1»input:List (Fin 4)width:ℕhw:1 ≤ widtht:ℕi:Fin 3ht:1 ≤ 2⊢ 0 ≤ (configs (initCfg input) 1).workTapePos i ∧ (configs (initCfg input) 1).workTapePos i ≤ ↑width«2»input:List (Fin 4)width:ℕhw:1 ≤ widtht:ℕi:Fin 3ht:2 ≤ 2⊢ 0 ≤ (configs (initCfg input) 2).workTapePos i ∧ (configs (initCfg input) 2).workTapePos i ≤ ↑width <;>«0»input:List (Fin 4)width:ℕhw:1 ≤ widtht:ℕi:Fin 3ht:0 ≤ 2⊢ 0 ≤ (configs (initCfg input) 0).workTapePos i ∧ (configs (initCfg input) 0).workTapePos i ≤ ↑width«1»input:List (Fin 4)width:ℕhw:1 ≤ widtht:ℕi:Fin 3ht:1 ≤ 2⊢ 0 ≤ (configs (initCfg input) 1).workTapePos i ∧ (configs (initCfg input) 1).workTapePos i ≤ ↑width«2»input:List (Fin 4)width:ℕhw:1 ≤ widtht:ℕi:Fin 3ht:2 ≤ 2⊢ 0 ≤ (configs (initCfg input) 2).workTapePos i ∧ (configs (initCfg input) 2).workTapePos i ≤ ↑width fin_cases i«2».«0»input:List (Fin 4)width:ℕhw:1 ≤ widtht:ℕht:2 ≤ 2⊢ 0 ≤ (configs (initCfg input) 2).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) ∧
  (configs (initCfg input) 2).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ↑width«2».«1»input:List (Fin 4)width:ℕhw:1 ≤ widtht:ℕht:2 ≤ 2⊢ 0 ≤ (configs (initCfg input) 2).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) ∧
  (configs (initCfg input) 2).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ↑width«2».«2»input:List (Fin 4)width:ℕhw:1 ≤ widtht:ℕht:2 ≤ 2⊢ 0 ≤ (configs (initCfg input) 2).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) ∧
  (configs (initCfg input) 2).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ↑width
  all_goals first
    | (change 0 ≤ (0 : ℤ) ∧ 0 ≤ (width : ℤ)«2».«2»input:List (Fin 4)width:ℕhw:1 ≤ widtht:ℕht:2 ≤ 2⊢ 0 ≤ (configs (initCfg input) 2).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) ∧
  (configs (initCfg input) 2).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ↑width; exact ⟨le_refl _, Int.natCast_nonneg _⟩All goals completed! 🐙)
    | (change 0 ≤ (1 : ℤ) ∧ 1 ≤ (width : ℤ)«2».«2»input:List (Fin 4)width:ℕhw:1 ≤ widtht:ℕht:2 ≤ 2⊢ 0 ≤ 1 ∧ 1 ≤ ↑width; exact ⟨byinput:List (Fin 4)width:ℕhw:1 ≤ widtht:ℕht:2 ≤ 2⊢ 0 ≤ 1 decideAll goals completed! 🐙, byinput:List (Fin 4)width:ℕhw:1 ≤ widtht:ℕht:2 ≤ 2⊢ 1 ≤ ↑width exact_mod_cast hwAll goals completed! 🐙⟩)

Every prefix boundary realizes the pure account and bounds the whole execution so far.

theorem configs_account (w : List Bool) :
    ∀ t, t ≤ w.length →
      let cost := 2 + runCost (w.take t)
      let now := machine.configs (machine.initCfg (w.map boolEmb)) cost
      let s := account (w.take t)
      Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
        now.inputPos.val = t + 1 ∧
        machine.outputString (machine.initCfg (w.map boolEmb)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size
          (machine.configs (machine.initCfg (w.map boolEmb)) u) := byw:List Bool⊢ ∀ t ≤ w.length,
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
  refine Nat.rec ?_ ?_refine_1w:List Bool⊢ Nat.zero ≤ w.length →
  let cost := 2 + runCost (List.take Nat.zero w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take Nat.zero w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = Nat.zero + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)refine_2w:List Bool⊢ ∀ (n : ℕ),
  (n ≤ w.length →
      let cost := 2 + runCost (List.take n w);
      let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
      let s := account (List.take n w);
      Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
        ↑now.inputPos = n + 1 ∧
          machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
            ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)) →
    n.succ ≤ w.length →
      let cost := 2 + runCost (List.take n.succ w);
      let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
      let s := account (List.take n.succ w);
      Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
        ↑now.inputPos = n.succ + 1 ∧
          machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
            ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
  ·refine_1w:List Bool⊢ Nat.zero ≤ w.length →
  let cost := 2 + runCost (List.take Nat.zero w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take Nat.zero w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = Nat.zero + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u) intro htrefine_1w:List Boolht:Nat.zero ≤ w.length⊢ let cost := 2 + runCost (List.take Nat.zero w);
let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
let s := account (List.take Nat.zero w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = Nat.zero + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    change Represents (w.length + 2).size
      (machine.configs (machine.initCfg (w.map boolEmb)) 2) stTree 1 0 ∧ _refine_1w:List Boolht:Nat.zero ≤ w.length⊢ Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) 2) stTree 1 0 ∧
  ↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take Nat.zero w))).inputPos = Nat.zero + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take Nat.zero w)) = [] ∧
      ∀ u ≤ 2 + runCost (List.take Nat.zero w),
        HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    rw [configs_startrefine_1w:List Boolht:Nat.zero ≤ w.length⊢ Represents (w.length + 2).size (startCfg (List.map (⇑boolEmb) w)) stTree 1 0 ∧
  ↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take Nat.zero w))).inputPos = Nat.zero + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take Nat.zero w)) = [] ∧
      ∀ u ≤ 2 + runCost (List.take Nat.zero w),
        HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)]refine_1w:List Boolht:Nat.zero ≤ w.length⊢ Represents (w.length + 2).size (startCfg (List.map (⇑boolEmb) w)) stTree 1 0 ∧
  ↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take Nat.zero w))).inputPos = Nat.zero + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take Nat.zero w)) = [] ∧
      ∀ u ≤ 2 + runCost (List.take Nat.zero w),
        HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    exact ⟨represents_startCfg _ _ (width_pos w.length), rfl,
      outputString_start _, headBound_start _ _ (width_pos w.length)⟩All goals completed! 🐙
  ·refine_2w:List Bool⊢ ∀ (n : ℕ),
  (n ≤ w.length →
      let cost := 2 + runCost (List.take n w);
      let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
      let s := account (List.take n w);
      Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
        ↑now.inputPos = n + 1 ∧
          machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
            ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)) →
    n.succ ≤ w.length →
      let cost := 2 + runCost (List.take n.succ w);
      let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
      let s := account (List.take n.succ w);
      Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
        ↑now.inputPos = n.succ + 1 ∧
          machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
            ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u) intro t ih htrefine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.length⊢ let cost := 2 + runCost (List.take t.succ w);
let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
let s := account (List.take t.succ w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = t.succ + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    obtain ⟨hr, hp, ho, hh⟩ := ih (byw:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.length⊢ t ≤ w.length omegaAll goals completed! 🐙)refine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ let cost := 2 + runCost (List.take t.succ w);
let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
let s := account (List.take t.succ w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = t.succ + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    have hlt : t < w.length := byw:List Bool⊢ ∀ t ≤ w.length,
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u) omegarefine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.length⊢ let cost := 2 + runCost (List.take t.succ w);
let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
let s := account (List.take t.succ w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = t.succ + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    have hs := prefix_size_le w (t + 1)refine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(account (List.take (t + 1) w)).forks.size ≤ (w.length + 2).size ∧
  (account (List.take (t + 1) w)).leaves.size ≤ (w.length + 2).size⊢ let cost := 2 + runCost (List.take t.succ w);
let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
let s := account (List.take t.succ w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = t.succ + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    rw [account_take_succ w t hltrefine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).size⊢ let cost := 2 + runCost (List.take t.succ w);
let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
let s := account (List.take t.succ w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = t.succ + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)] at hsrefine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).size⊢ let cost := 2 + runCost (List.take t.succ w);
let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
let s := account (List.take t.succ w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = t.succ + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    let cfg := machine.configs (machine.initCfg (w.map boolEmb)) (2 + runCost (w.take t))refine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))⊢ let cost := 2 + runCost (List.take t.succ w);
let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
let s := account (List.take t.succ w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = t.succ + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    have hstep := configs_bit w t hlt cfg hp (account (w.take t)) (w.length + 2).size
      (account_valid _) hr hs.1 hs.2refine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hstep:have cost := macroCost (account (List.take t w)) w[t];
have next := accountStep (account (List.take t w)) w[t];
Represents (w.length + 2).size (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
  ↑(configs cfg cost).inputPos = t + 2 ∧ machine.outputString cfg cost = []⊢ let cost := 2 + runCost (List.take t.succ w);
let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
let s := account (List.take t.succ w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = t.succ + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    have hbound := configs_bit_head_bounds w t hlt cfg hp (account (w.take t))
      (w.length + 2).size (account_valid _) hr hs.1 hs.2refine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hstep:have cost := macroCost (account (List.take t w)) w[t];
have next := accountStep (account (List.take t w)) w[t];
Represents (w.length + 2).size (configs cfg cost) (modeState next.mode) next.forks next.leaves ∧
  ↑(configs cfg cost).inputPos = t + 2 ∧ machine.outputString cfg cost = []hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)⊢ let cost := 2 + runCost (List.take t.succ w);
let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
let s := account (List.take t.succ w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = t.succ + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    obtain ⟨hr', hp', ho'⟩ := hsteprefine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []⊢ let cost := 2 + runCost (List.take t.succ w);
let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
let s := account (List.take t.succ w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = t.succ + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    have he : 2 + runCost (w.take (t + 1)) =
        (2 + runCost (w.take t)) + macroCost (account (w.take t)) w[t] := byw:List Bool⊢ ∀ t ≤ w.length,
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
      rw [runCost_take_succ w t hltw:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []⊢ 2 + (runCost (List.take t w) + macroCost (account (List.take t w)) w[t]) =
  2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]]w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []⊢ 2 + (runCost (List.take t w) + macroCost (account (List.take t w)) w[t]) =
  2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]
      omegarefine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]⊢ let cost := 2 + runCost (List.take t.succ w);
let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
let s := account (List.take t.succ w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = t.succ + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    have hc : machine.configs (machine.initCfg (w.map boolEmb))
        (2 + runCost (w.take (t + 1))) =
        machine.configs cfg (macroCost (account (w.take t)) w[t]) := byw:List Bool⊢ ∀ t ≤ w.length,
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
      rw [he,w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]⊢ configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]) =
  configs cfg (macroCost (account (List.take t w)) w[t]) configs_addw:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]⊢ configs (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
    (macroCost (account (List.take t w)) w[t]) =
  configs cfg (macroCost (account (List.take t w)) w[t])]refine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ let cost := 2 + runCost (List.take t.succ w);
let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
let s := account (List.take t.succ w);
Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
  ↑now.inputPos = t.succ + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    dsimp onlyrefine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t.succ w)))
    (modeState (account (List.take t.succ w)).mode) (account (List.take t.succ w)).forks
    (account (List.take t.succ w)).leaves ∧
  ↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t.succ w))).inputPos = t.succ + 1 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t.succ w)) = [] ∧
      ∀ u ≤ 2 + runCost (List.take t.succ w),
        HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    refine ⟨?_, ?_, ?_, ?_⟩refine_2.refine_1w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t.succ w)))
  (modeState (account (List.take t.succ w)).mode) (account (List.take t.succ w)).forks
  (account (List.take t.succ w)).leavesrefine_2.refine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ ↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t.succ w))).inputPos = t.succ + 1refine_2.refine_3w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t.succ w)) = []refine_2.refine_4w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ ∀ u ≤ 2 + runCost (List.take t.succ w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
    ·refine_2.refine_1w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t.succ w)))
  (modeState (account (List.take t.succ w)).mode) (account (List.take t.succ w)).forks
  (account (List.take t.succ w)).leaves rw [hc,refine_2.refine_1w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (account (List.take t.succ w)).mode) (account (List.take t.succ w)).forks
  (account (List.take t.succ w)).leaves account_take_succ w t hltrefine_2.refine_1w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaves]refine_2.refine_1w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaves
      exact hr'All goals completed! 🐙
    ·refine_2.refine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ ↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t.succ w))).inputPos = t.succ + 1 rw [hcrefine_2.refine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ ↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t.succ + 1]refine_2.refine_2w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ ↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t.succ + 1
      exact hp'All goals completed! 🐙
    ·refine_2.refine_3w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t.succ w)) = [] rw [he,refine_2.refine_3w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w))
    (2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]) =
  [] outputString_add_eq_append,refine_2.refine_3w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) ++
    machine.outputString (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
      (macroCost (account (List.take t w)) w[t]) =
  [] ho,refine_2.refine_3w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ [] ++
    machine.outputString (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
      (macroCost (account (List.take t w)) w[t]) =
  [] ho'refine_2.refine_3w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ [] ++ [] = []]refine_2.refine_3w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ [] ++ [] = []
      rflAll goals completed! 🐙
    ·refine_2.refine_4w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ ∀ u ≤ 2 + runCost (List.take t.succ w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u) rw [herefine_2.refine_4w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ ∀ u ≤ 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t],
  HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)]refine_2.refine_4w:List Boolt:ℕih:t ≤ w.length →
  let cost := 2 + runCost (List.take t w);
  let now := configs (initCfg (List.map (⇑boolEmb) w)) cost;
  let s := account (List.take t w);
  Represents (w.length + 2).size now (modeState s.mode) s.forks s.leaves ∧
    ↑now.inputPos = t + 1 ∧
      machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhr:Represents (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)))
  (modeState (account (List.take t w)).mode) (account (List.take t w)).forks (account (List.take t w)).leaveshp:↑(configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))).inputPos = t + 1ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w)) = []hh:∀ u ≤ 2 + runCost (List.take t w), HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)hlt:t < w.lengthhs:(accountStep (account (List.take t w)) w[t]).forks.size ≤ (w.length + 2).size ∧
  (accountStep (account (List.take t w)) w[t]).leaves.size ≤ (w.length + 2).sizecfg:Cfg 3 (Fin 4) (Fin 10) (List.map (⇑boolEmb) w) := configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take t w))hbound:∀ u ≤ macroCost (account (List.take t w)) w[t], HeadBound (w.length + 2).size (configs cfg u)hr':Represents (w.length + 2).size (configs cfg (macroCost (account (List.take t w)) w[t]))
  (modeState (accountStep (account (List.take t w)) w[t]).mode) (accountStep (account (List.take t w)) w[t]).forks
  (accountStep (account (List.take t w)) w[t]).leaveshp':↑(configs cfg (macroCost (account (List.take t w)) w[t])).inputPos = t + 2ho':machine.outputString cfg (macroCost (account (List.take t w)) w[t]) = []he:2 + runCost (List.take (t + 1) w) = 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]hc:configs (initCfg (List.map (⇑boolEmb) w)) (2 + runCost (List.take (t + 1) w)) =
  configs cfg (macroCost (account (List.take t w)) w[t])⊢ ∀ u ≤ 2 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t],
  HeadBound (w.length + 2).size (configs (initCfg (List.map (⇑boolEmb) w)) u)
      exact headBound_add _ _ _ _ hh hboundAll goals completed! 🐙

end Geb.BitTree.BinaryMachine