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.Elias.MachineBit
public import Geb.Prototypes.Computability.BitTree.Elias.MachineAccounting
public import Geb.Prototypes.Computability.BitTree.Elias.MachineEnd

set_option doc.verso true

Whole-input execution of the Elias recognizer

Each complete input transition realizes one step of the pure scanner account. Composing those transitions bounds all intermediate head positions, including the counter sweeps between successive input bits.

Main statements

configs_account realizes every input prefix and bounds its visited space.

Tags

Elias delta code, Turing machine, execution, complexity

              @[expose] public sectionnamespace Geb.BitTree.Elias.Machineopen Turing MultiTapeTM

Every prefix realizes its account at the exact accumulated transition cost.

theorem configs_account (w : List Bool) :
    ∀ t, (ht : t ≤ w.length) →
      let cost := 1 + runCost (w.take t)
      let a := account (w.take t)
      machine.configs (machine.initCfg (w.map boolEmb)) cost =
          modelCfg (w.map boolEmb) ⟨t + 1, byw:List Boolt:ℕht:t ≤ w.lengthcost:ℕ := 1 + runCost (List.take t w)a:Account := account (List.take t w)⊢ t + 1 < (List.map (⇑boolEmb) w).length + 2 simp only [List.length_map]w:List Boolt:ℕht:t ≤ w.lengthcost:ℕ := 1 + runCost (List.take t w)a:Account := account (List.take t w)⊢ t + 1 < w.length + 2; omegaAll goals completed! 🐙⟩
            a.1 a.2.1 a.2.2 ∧
        machine.outputString (machine.initCfg (w.map boolEmb)) cost = [] ∧
        ∀ u ≤ cost, HeadBound (w.length + 1)
          (machine.configs (machine.initCfg (w.map boolEmb)) u) := byw:List Bool⊢ ∀ (t : ℕ) (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
  refine Nat.rec ?_ ?_refine_1w:List Bool⊢ ∀ (ht : Nat.zero ≤ w.length),
  let cost := 1 + runCost (List.take Nat.zero w);
  let a := account (List.take Nat.zero w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨Nat.zero + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)refine_2w:List Bool⊢ ∀ (n : ℕ),
  (∀ (ht : n ≤ w.length),
      let cost := 1 + runCost (List.take n w);
      let a := account (List.take n w);
      configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨n + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
        machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
          ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)) →
    ∀ (ht : n.succ ≤ w.length),
      let cost := 1 + runCost (List.take n.succ w);
      let a := account (List.take n.succ w);
      configs (initCfg (List.map (⇑boolEmb) w)) cost =
          modelCfg (List.map (⇑boolEmb) w) ⟨n.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
        machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
          ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
  ·refine_1w:List Bool⊢ ∀ (ht : Nat.zero ≤ w.length),
  let cost := 1 + runCost (List.take Nat.zero w);
  let a := account (List.take Nat.zero w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨Nat.zero + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u) intro htrefine_1w:List Boolht:Nat.zero ≤ w.length⊢ let cost := 1 + runCost (List.take Nat.zero w);
let a := account (List.take Nat.zero w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨Nat.zero + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    change machine.configs (machine.initCfg (w.map boolEmb)) 1 = _ ∧ _refine_1w:List Boolht:Nat.zero ≤ w.length⊢ configs (initCfg (List.map (⇑boolEmb) w)) 1 =
    modelCfg (List.map (⇑boolEmb) w) ⟨Nat.zero + 1, ⋯⟩ (account (List.take Nat.zero w)).1
      (account (List.take Nat.zero w)).2.1 (account (List.take Nat.zero w)).2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take Nat.zero w)) = [] ∧
    ∀ u ≤ 1 + runCost (List.take Nat.zero w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    refine ⟨?_, outputString_start _, headBound_start _ _ (byw:List Boolht:Nat.zero ≤ w.length⊢ 1 ≤ w.length + 1 omegaAll goals completed! 🐙)⟩
    rw [configs_startrefine_1w:List Boolht:Nat.zero ≤ w.length⊢ modelCfg (List.map (⇑boolEmb) w) 1 (Scanner.Mode.tree, 1) [] [] =
  modelCfg (List.map (⇑boolEmb) w) ⟨Nat.zero + 1, ⋯⟩ (account (List.take Nat.zero w)).1
    (account (List.take Nat.zero w)).2.1 (account (List.take Nat.zero w)).2.2]refine_1w:List Boolht:Nat.zero ≤ w.length⊢ modelCfg (List.map (⇑boolEmb) w) 1 (Scanner.Mode.tree, 1) [] [] =
  modelCfg (List.map (⇑boolEmb) w) ⟨Nat.zero + 1, ⋯⟩ (account (List.take Nat.zero w)).1
    (account (List.take Nat.zero w)).2.1 (account (List.take Nat.zero w)).2.2
    congr 1All goals completed! 🐙
  ·refine_2w:List Bool⊢ ∀ (n : ℕ),
  (∀ (ht : n ≤ w.length),
      let cost := 1 + runCost (List.take n w);
      let a := account (List.take n w);
      configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨n + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
        machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
          ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)) →
    ∀ (ht : n.succ ≤ w.length),
      let cost := 1 + runCost (List.take n.succ w);
      let a := account (List.take n.succ w);
      configs (initCfg (List.map (⇑boolEmb) w)) cost =
          modelCfg (List.map (⇑boolEmb) w) ⟨n.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
        machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
          ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u) intro t ih htrefine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.length⊢ let cost := 1 + runCost (List.take t.succ w);
let a := account (List.take t.succ w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    have hlt : t < w.length := byw:List Bool⊢ ∀ (t : ℕ) (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u) omegarefine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.length⊢ let cost := 1 + runCost (List.take t.succ w);
let a := account (List.take t.succ w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    obtain ⟨hc, ho, hh⟩ := ih (byw:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.length⊢ t ≤ w.length omegaAll goals completed! 🐙)refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)⊢ let cost := 1 + runCost (List.take t.succ w);
let a := account (List.take t.succ w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    let a := account (w.take t)refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)⊢ let cost := 1 + runCost (List.take t.succ w);
let a := account (List.take t.succ w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    let pos : Fin ((w.map boolEmb).length + 2) :=
      ⟨t + 1, byw:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)⊢ t + 1 < (List.map (⇑boolEmb) w).length + 2 simp only [List.length_map]w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)⊢ t + 1 < w.length + 2; omegaAll goals completed! 🐙⟩refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩⊢ let cost := 1 + runCost (List.take t.succ w);
let a := account (List.take t.succ w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    have hin := inputSymbol_at w t hlt
      (modelCfg (w.map boolEmb) pos a.1 a.2.1 a.2.2) rflrefine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])⊢ let cost := 1 + runCost (List.take t.succ w);
let a := account (List.take t.succ w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    obtain ⟨hs, hout⟩ := configs_bit (w.map boolEmb) pos a.1 a.2.1 a.2.2 w[t]
      (account_active _) (account_words _) hinrefine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []⊢ let cost := 1 + runCost (List.take t.succ w);
let a := account (List.take t.succ w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    have hp := account_pending_le (w.take t)refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1⊢ let cost := 1 + runCost (List.take t.succ w);
let a := account (List.take t.succ w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    have hz := account_zeros_le (w.take t)refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).length⊢ let cost := 1 + runCost (List.take t.succ w);
let a := account (List.take t.succ w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    obtain ⟨hb, hd⟩ := account_lengths_le (w.take t)refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).length⊢ let cost := 1 + runCost (List.take t.succ w);
let a := account (List.take t.succ w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    have hlen : (w.take t).length = t := List.length_take_of_le (byw:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).length⊢ t ≤ w.length omegaAll goals completed! 🐙)refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = t⊢ let cost := 1 + runCost (List.take t.succ w);
let a := account (List.take t.succ w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    have hbound := configs_bit_headBound (w.map boolEmb) pos a.1 a.2.1 a.2.2 w[t]
      (account_active _) (account_words _) hin (w.length + 1)
      (byw:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = t⊢ a.1.2 + 1 ≤ w.length + 1 dsimp only [a]w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = t⊢ (account (List.take t w)).1.2 + 1 ≤ w.length + 1; omegaAll goals completed! 🐙) (byw:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = t⊢ zeroCount a.1.1 + 1 ≤ w.length + 1 dsimp only [a]w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = t⊢ zeroCount (account (List.take t w)).1.1 + 1 ≤ w.length + 1; omegaAll goals completed! 🐙)
      (byw:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = t⊢ a.2.1.length + 2 ≤ w.length + 1 dsimp only [a]w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = t⊢ (account (List.take t w)).2.1.length + 2 ≤ w.length + 1; omegaAll goals completed! 🐙) (byw:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = t⊢ a.2.2.length + 2 ≤ w.length + 1 dsimp only [a]w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = t⊢ (account (List.take t w)).2.2.length + 2 ≤ w.length + 1; omegaAll goals completed! 🐙)refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)⊢ let cost := 1 + runCost (List.take t.succ w);
let a := account (List.take t.succ w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    have he : 1 + runCost (w.take (t + 1)) =
        (1 + runCost (w.take t)) + macroCost a w[t] := byw:List Bool⊢ ∀ (t : ℕ) (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
      dsimp only [a]w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)⊢ 1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]
      rw [runCost_take_succ w t hltw:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)⊢ 1 + (runCost (List.take t w) + macroCost (account (List.take t w)) w[t]) =
  1 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]]w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)⊢ 1 + (runCost (List.take t w) + macroCost (account (List.take t w)) w[t]) =
  1 + runCost (List.take t w) + macroCost (account (List.take t w)) w[t]
      omegarefine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]⊢ let cost := 1 + runCost (List.take t.succ w);
let a := account (List.take t.succ w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    have hpos : moveInputPos pos 1 =
        (⟨t + 1 + 1, byw:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]⊢ t + 1 + 1 < (List.map (⇑boolEmb) w).length + 2 simp only [List.length_map]w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]⊢ t + 1 + 1 < w.length + 2; omegaAll goals completed! 🐙⟩ :
          Fin ((w.map boolEmb).length + 2)) := byw:List Bool⊢ ∀ (t : ℕ) (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
      exact moveInputPos_pos_of_ne_right pos (byw:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]⊢ ↑pos ≠ (List.map (⇑boolEmb) w).length + 1
        dsimp only [pos]w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]⊢ t + 1 ≠ (List.map (⇑boolEmb) w).length + 1; simp only [List.length_map]w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]⊢ t + 1 ≠ w.length + 1; omegaAll goals completed! 🐙)refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ let cost := 1 + runCost (List.take t.succ w);
let a := account (List.take t.succ w);
configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
    ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    dsimp onlyrefine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t.succ w)) =
    modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ (account (List.take t.succ w)).1 (account (List.take t.succ w)).2.1
      (account (List.take t.succ w)).2.2 ∧
  machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t.succ w)) = [] ∧
    ∀ u ≤ 1 + runCost (List.take t.succ w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    refine ⟨?_, ?_, ?_⟩refine_2.refine_1w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t.succ w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ (account (List.take t.succ w)).1 (account (List.take t.succ w)).2.1
    (account (List.take t.succ w)).2.2refine_2.refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t.succ w)) = []refine_2.refine_3w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ ∀ u ≤ 1 + runCost (List.take t.succ w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
    ·refine_2.refine_1w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t.succ w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ (account (List.take t.succ w)).1 (account (List.take t.succ w)).2.1
    (account (List.take t.succ w)).2.2 rw [he,refine_2.refine_1w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w) + macroCost a w[t]) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ (account (List.take t.succ w)).1 (account (List.take t.succ w)).2.1
    (account (List.take t.succ w)).2.2 configs_add,refine_2.refine_1w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ configs (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w))) (macroCost a w[t]) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ (account (List.take t.succ w)).1 (account (List.take t.succ w)).2.1
    (account (List.take t.succ w)).2.2 hcrefine_2.refine_1w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ configs
    (modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
      (account (List.take t w)).2.2)
    (macroCost a w[t]) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ (account (List.take t.succ w)).1 (account (List.take t.succ w)).2.1
    (account (List.take t.succ w)).2.2]refine_2.refine_1w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ configs
    (modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
      (account (List.take t w)).2.2)
    (macroCost a w[t]) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ (account (List.take t.succ w)).1 (account (List.take t.succ w)).2.1
    (account (List.take t.succ w)).2.2
      change machine.configs (modelCfg (w.map boolEmb) pos a.1 a.2.1 a.2.2)
        (bitCost a.1.1 a.2.1 a.2.2 w[t]) = _refine_2.refine_1w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ (account (List.take t.succ w)).1 (account (List.take t.succ w)).2.1
    (account (List.take t.succ w)).2.2
      rw [hs,refine_2.refine_1w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2 =
  modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ (account (List.take t.succ w)).1 (account (List.take t.succ w)).2.1
    (account (List.take t.succ w)).2.2 hpos,refine_2.refine_1w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ modelCfg (List.map (⇑boolEmb) w) ⟨t + 1 + 1, ⋯⟩ (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2 =
  modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ (account (List.take t.succ w)).1 (account (List.take t.succ w)).2.1
    (account (List.take t.succ w)).2.2 account_take_succ w t hltrefine_2.refine_1w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ modelCfg (List.map (⇑boolEmb) w) ⟨t + 1 + 1, ⋯⟩ (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2 =
  modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ (accountStep (account (List.take t w)) w[t]).1
    (accountStep (account (List.take t w)) w[t]).2.1 (accountStep (account (List.take t w)) w[t]).2.2]refine_2.refine_1w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ modelCfg (List.map (⇑boolEmb) w) ⟨t + 1 + 1, ⋯⟩ (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2 =
  modelCfg (List.map (⇑boolEmb) w) ⟨t.succ + 1, ⋯⟩ (accountStep (account (List.take t w)) w[t]).1
    (accountStep (account (List.take t w)) w[t]).2.1 (accountStep (account (List.take t w)) w[t]).2.2
      rflAll goals completed! 🐙
    ·refine_2.refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t.succ w)) = [] rw [he,refine_2.refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w) + macroCost a w[t]) = [] outputString_add_eq_append,refine_2.refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) ++
    machine.outputString (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w))) (macroCost a w[t]) =
  [] ho,refine_2.refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ [] ++
    machine.outputString (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w))) (macroCost a w[t]) =
  [] hcrefine_2.refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ [] ++
    machine.outputString
      (modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
        (account (List.take t w)).2.2)
      (macroCost a w[t]) =
  []]refine_2.refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ [] ++
    machine.outputString
      (modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
        (account (List.take t w)).2.2)
      (macroCost a w[t]) =
  []
      change [] ++ machine.outputString (modelCfg (w.map boolEmb) pos a.1 a.2.1 a.2.2)
        (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []refine_2.refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ [] ++ machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []
      rw [houtrefine_2.refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ [] ++ [] = []]refine_2.refine_2w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ [] ++ [] = []
      rflAll goals completed! 🐙
    ·refine_2.refine_3w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ ∀ u ≤ 1 + runCost (List.take t.succ w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u) rw [herefine_2.refine_3w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ ∀ u ≤ 1 + runCost (List.take t w) + macroCost a w[t],
  HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)]refine_2.refine_3w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ ∀ u ≤ 1 + runCost (List.take t w) + macroCost a w[t],
  HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)
      apply headBound_add _ _ _ _ hhrefine_2.refine_3w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ ∀ t_1 ≤ macroCost a w[t],
  HeadBound (w.length + 1) (configs (configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w))) t_1)
      rw [hcrefine_2.refine_3w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ ∀ t_1 ≤ macroCost a w[t],
  HeadBound (w.length + 1)
    (configs
      (modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
        (account (List.take t w)).2.2)
      t_1)]refine_2.refine_3w:List Boolt:ℕih:∀ (ht : t ≤ w.length),
  let cost := 1 + runCost (List.take t w);
  let a := account (List.take t w);
  configs (initCfg (List.map (⇑boolEmb) w)) cost = modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ a.1 a.2.1 a.2.2 ∧
    machine.outputString (initCfg (List.map (⇑boolEmb) w)) cost = [] ∧
      ∀ u ≤ cost, HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)ht:t.succ ≤ w.lengthhlt:t < w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) =
  modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
    (account (List.take t w)).2.2ho:machine.outputString (initCfg (List.map (⇑boolEmb) w)) (1 + runCost (List.take t w)) = []hh:∀ u ≤ 1 + runCost (List.take t w), HeadBound (w.length + 1) (configs (initCfg (List.map (⇑boolEmb) w)) u)a:Account := account (List.take t w)pos:Fin ((List.map (⇑boolEmb) w).length + 2) := ⟨t + 1, ⋯⟩hin:(modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2).inputSymbol = some (boolEmb w[t])hs:configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) =
  modelCfg (List.map (⇑boolEmb) w) (moveInputPos pos 1) (Scanner.step a.1 w[t]) (nextWords a.1.1 a.2.1 a.2.2 w[t]).1
    (nextWords a.1.1 a.2.1 a.2.2 w[t]).2hout:machine.outputString (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) (bitCost a.1.1 a.2.1 a.2.2 w[t]) = []hp:(account (List.take t w)).1.2 ≤ (List.take t w).length + 1hz:zeroCount (account (List.take t w)).1.1 ≤ (List.take t w).lengthhb:(account (List.take t w)).2.1.length ≤ (List.take t w).lengthhd:(account (List.take t w)).2.2.length ≤ (List.take t w).lengthhlen:(List.take t w).length = thbound:∀ t_1 ≤ bitCost a.1.1 a.2.1 a.2.2 w[t],
  HeadBound (w.length + 1) (configs (modelCfg (List.map (⇑boolEmb) w) pos a.1 a.2.1 a.2.2) t_1)he:1 + runCost (List.take (t + 1) w) = 1 + runCost (List.take t w) + macroCost a w[t]hpos:moveInputPos pos 1 = ⟨t + 1 + 1, ⋯⟩⊢ ∀ t_1 ≤ macroCost a w[t],
  HeadBound (w.length + 1)
    (configs
      (modelCfg (List.map (⇑boolEmb) w) ⟨t + 1, ⋯⟩ (account (List.take t w)).1 (account (List.take t w)).2.1
        (account (List.take t w)).2.2)
      t_1)
      exact hboundAll goals completed! 🐙

end Geb.BitTree.Elias.Machine