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.TreeScanner.Steps
public import Mathlib.Tactic.FinCases
public import Geb.Prototypes.Computability.BitTree.BinaryMachine.Difference
public import Geb.Prototypes.Computability.BitTree.BinaryMachine.Machine

set_option doc.verso true

Binary-machine transition invariants

The two binary heads remain aligned throughout execution, and the input head never moves left. Initialization produces the counter values one and zero and places the mismatch head at one. These statements concern the actual CSLib configuration sequence.

Main statements

configs_binaryHeads_eq: the binary heads are aligned at every time.
configs_inputPos_mono: the input positions form a monotone sequence.
configs_start: the two initialization transitions.

Tags

Turing machine, simulation, binary counter

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

A transition preserves alignment of the two binary heads.

theorem step_binaryHeads_eq {input : List (Fin 4)}
    (cfg : Cfg 3 (Fin 4) (Fin 10) input)
    (h : cfg.workTapePos 0 = cfg.workTapePos 1) :
    (machine.step cfg).workTapePos 0 = (machine.step cfg).workTapePos 1 := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputh:cfg.workTapePos 0 = cfg.workTapePos 1⊢ (MultiTapeTM.step cfg).workTapePos 0 = (MultiTapeTM.step cfg).workTapePos 1
  unfold MultiTapeTM.stepinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputh:cfg.workTapePos 0 = cfg.workTapePos 1⊢ (match cfg.state with
      | none => cfg
      | some q =>
        match machine.tr q cfg.inputSymbol cfg.workTapeSymbols with
        | { inputMove := inputMove, workActions := workActions, outS := outS, q' := q' } =>
          { state := q', inputPos := moveInputPos cfg.inputPos inputMove,
            workTapes := fun i ↦
              match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4)) (workActions i).1 with
              | none => cfg.workTapes i
              | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
            workTapePos := fun i ↦ cfg.workTapePos i + ↑(workActions i).2 }).workTapePos
    0 =
  (match cfg.state with
      | none => cfg
      | some q =>
        match machine.tr q cfg.inputSymbol cfg.workTapeSymbols with
        | { inputMove := inputMove, workActions := workActions, outS := outS, q' := q' } =>
          { state := q', inputPos := moveInputPos cfg.inputPos inputMove,
            workTapes := fun i ↦
              match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4)) (workActions i).1 with
              | none => cfg.workTapes i
              | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
            workTapePos := fun i ↦ cfg.workTapePos i + ↑(workActions i).2 }).workTapePos
    1
  cases cfg.state with
  | none =>noneinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputh:cfg.workTapePos 0 = cfg.workTapePos 1⊢ (match none with
      | none => cfg
      | some q =>
        match machine.tr q cfg.inputSymbol cfg.workTapeSymbols with
        | { inputMove := inputMove, workActions := workActions, outS := outS, q' := q' } =>
          { state := q', inputPos := moveInputPos cfg.inputPos inputMove,
            workTapes := fun i ↦
              match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4)) (workActions i).1 with
              | none => cfg.workTapes i
              | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
            workTapePos := fun i ↦ cfg.workTapePos i + ↑(workActions i).2 }).workTapePos
    0 =
  (match none with
      | none => cfg
      | some q =>
        match machine.tr q cfg.inputSymbol cfg.workTapeSymbols with
        | { inputMove := inputMove, workActions := workActions, outS := outS, q' := q' } =>
          { state := q', inputPos := moveInputPos cfg.inputPos inputMove,
            workTapes := fun i ↦
              match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4)) (workActions i).1 with
              | none => cfg.workTapes i
              | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
            workTapePos := fun i ↦ cfg.workTapePos i + ↑(workActions i).2 }).workTapePos
    1 exact hAll goals completed! 🐙
  | some q =>someinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputh:cfg.workTapePos 0 = cfg.workTapePos 1q:Fin 10⊢ (match some q with
      | none => cfg
      | some q =>
        match machine.tr q cfg.inputSymbol cfg.workTapeSymbols with
        | { inputMove := inputMove, workActions := workActions, outS := outS, q' := q' } =>
          { state := q', inputPos := moveInputPos cfg.inputPos inputMove,
            workTapes := fun i ↦
              match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4)) (workActions i).1 with
              | none => cfg.workTapes i
              | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
            workTapePos := fun i ↦ cfg.workTapePos i + ↑(workActions i).2 }).workTapePos
    0 =
  (match some q with
      | none => cfg
      | some q =>
        match machine.tr q cfg.inputSymbol cfg.workTapeSymbols with
        | { inputMove := inputMove, workActions := workActions, outS := outS, q' := q' } =>
          { state := q', inputPos := moveInputPos cfg.inputPos inputMove,
            workTapes := fun i ↦
              match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4)) (workActions i).1 with
              | none => cfg.workTapes i
              | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
            workTapePos := fun i ↦ cfg.workTapePos i + ↑(workActions i).2 }).workTapePos
    1
    dsimp onlysomeinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputh:cfg.workTapePos 0 = cfg.workTapePos 1q:Fin 10⊢ cfg.workTapePos 0 + ↑((machine.2 q cfg.inputSymbol cfg.workTapeSymbols).workActions 0).2 =
  cfg.workTapePos 1 + ↑((machine.2 q cfg.inputSymbol cfg.workTapeSymbols).workActions 1).2
    rw [h,someinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputh:cfg.workTapePos 0 = cfg.workTapePos 1q:Fin 10⊢ cfg.workTapePos 1 + ↑((machine.2 q cfg.inputSymbol cfg.workTapeSymbols).workActions 0).2 =
  cfg.workTapePos 1 + ↑((machine.2 q cfg.inputSymbol cfg.workTapeSymbols).workActions 1).2 binaryHeads_move_eqsomeinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputh:cfg.workTapePos 0 = cfg.workTapePos 1q:Fin 10⊢ cfg.workTapePos 1 + ↑((machine.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions 1).2 =
  cfg.workTapePos 1 + ↑((machine.2 q cfg.inputSymbol cfg.workTapeSymbols).workActions 1).2]All goals completed! 🐙

Both binary heads are aligned at every time in the execution.

theorem configs_binaryHeads_eq (input : List (Fin 4)) (t : ℕ) :
    (machine.configs (machine.initCfg input) t).workTapePos 0 =
      (machine.configs (machine.initCfg input) t).workTapePos 1 := byinput:List (Fin 4)t:ℕ⊢ (configs (initCfg input) t).workTapePos 0 = (configs (initCfg input) t).workTapePos 1
  apply Nat.rec (motive := fun t ↦
    (machine.configs (machine.initCfg input) t).workTapePos 0 =
      (machine.configs (machine.initCfg input) t).workTapePos 1) ?_ ?_ tinput:List (Fin 4)t:ℕ⊢ (configs (initCfg input) Nat.zero).workTapePos 0 = (configs (initCfg input) Nat.zero).workTapePos 1input:List (Fin 4)t:ℕ⊢ ∀ (n : ℕ),
  (configs (initCfg input) n).workTapePos 0 = (configs (initCfg input) n).workTapePos 1 →
    (configs (initCfg input) n.succ).workTapePos 0 = (configs (initCfg input) n.succ).workTapePos 1
  ·input:List (Fin 4)t:ℕ⊢ (configs (initCfg input) Nat.zero).workTapePos 0 = (configs (initCfg input) Nat.zero).workTapePos 1 rflAll goals completed! 🐙
  ·input:List (Fin 4)t:ℕ⊢ ∀ (n : ℕ),
  (configs (initCfg input) n).workTapePos 0 = (configs (initCfg input) n).workTapePos 1 →
    (configs (initCfg input) n.succ).workTapePos 0 = (configs (initCfg input) n.succ).workTapePos 1 intro t ihinput:List (Fin 4)t✝:ℕt:ℕih:(configs (initCfg input) t).workTapePos 0 = (configs (initCfg input) t).workTapePos 1⊢ (configs (initCfg input) t.succ).workTapePos 0 = (configs (initCfg input) t.succ).workTapePos 1
    rw [configs_succ_eq_step'input:List (Fin 4)t✝:ℕt:ℕih:(configs (initCfg input) t).workTapePos 0 = (configs (initCfg input) t).workTapePos 1⊢ (MultiTapeTM.step (configs (initCfg input) t)).workTapePos 0 =
  (MultiTapeTM.step (configs (initCfg input) t)).workTapePos 1]input:List (Fin 4)t✝:ℕt:ℕih:(configs (initCfg input) t).workTapePos 0 = (configs (initCfg input) t).workTapePos 1⊢ (MultiTapeTM.step (configs (initCfg input) t)).workTapePos 0 =
  (MultiTapeTM.step (configs (initCfg input) t)).workTapePos 1
    exact step_binaryHeads_eq _ ihAll goals completed! 🐙

The input head never moves left in one machine step.

theorem step_inputPos_le {input : List (Fin 4)}
    (cfg : Cfg 3 (Fin 4) (Fin 10) input) :
    cfg.inputPos.val ≤ (machine.step cfg).inputPos.val := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) input⊢ ↑cfg.inputPos ≤ ↑(MultiTapeTM.step cfg).inputPos
  unfold MultiTapeTM.stepinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) input⊢ ↑cfg.inputPos ≤
  ↑(match cfg.state with
      | none => cfg
      | some q =>
        match machine.tr q cfg.inputSymbol cfg.workTapeSymbols with
        | { inputMove := inputMove, workActions := workActions, outS := outS, q' := q' } =>
          { state := q', inputPos := moveInputPos cfg.inputPos inputMove,
            workTapes := fun i ↦
              match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4)) (workActions i).1 with
              | none => cfg.workTapes i
              | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
            workTapePos := fun i ↦ cfg.workTapePos i + ↑(workActions i).2 }).inputPos
  cases cfg.state with
  | none =>noneinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) input⊢ ↑cfg.inputPos ≤
  ↑(match none with
      | none => cfg
      | some q =>
        match machine.tr q cfg.inputSymbol cfg.workTapeSymbols with
        | { inputMove := inputMove, workActions := workActions, outS := outS, q' := q' } =>
          { state := q', inputPos := moveInputPos cfg.inputPos inputMove,
            workTapes := fun i ↦
              match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4)) (workActions i).1 with
              | none => cfg.workTapes i
              | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
            workTapePos := fun i ↦ cfg.workTapePos i + ↑(workActions i).2 }).inputPos exact Nat.le_refl _All goals completed! 🐙
  | some q =>someinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputq:Fin 10⊢ ↑cfg.inputPos ≤
  ↑(match some q with
      | none => cfg
      | some q =>
        match machine.tr q cfg.inputSymbol cfg.workTapeSymbols with
        | { inputMove := inputMove, workActions := workActions, outS := outS, q' := q' } =>
          { state := q', inputPos := moveInputPos cfg.inputPos inputMove,
            workTapes := fun i ↦
              match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4)) (workActions i).1 with
              | none => cfg.workTapes i
              | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
            workTapePos := fun i ↦ cfg.workTapePos i + ↑(workActions i).2 }).inputPos exact le_moveInputPos _ _ (inputMove_ne_neg q _ _)All goals completed! 🐙

The input positions form a monotone sequence throughout execution.

theorem configs_inputPos_mono (input : List (Fin 4)) :
    Monotone (fun t ↦ (machine.configs (machine.initCfg input) t).inputPos.val) := byinput:List (Fin 4)⊢ Monotone fun t ↦ ↑(configs (initCfg input) t).inputPos
  apply monotone_nat_of_le_succinput:List (Fin 4)⊢ ∀ (n : ℕ), ↑(configs (initCfg input) n).inputPos ≤ ↑(configs (initCfg input) (n + 1)).inputPos
  intro tinput:List (Fin 4)t:ℕ⊢ ↑(configs (initCfg input) t).inputPos ≤ ↑(configs (initCfg input) (t + 1)).inputPos
  rw [configs_succ_eq_step'input:List (Fin 4)t:ℕ⊢ ↑(configs (initCfg input) t).inputPos ≤ ↑(MultiTapeTM.step (configs (initCfg input) t)).inputPos]input:List (Fin 4)t:ℕ⊢ ↑(configs (initCfg input) t).inputPos ≤ ↑(MultiTapeTM.step (configs (initCfg input) t)).inputPos
  exact step_inputPos_le _All goals completed! 🐙

After two transitions, scanning starts with one pending tree.

theorem configs_start (input : List (Fin 4)) :
    machine.configs (machine.initCfg input) 2 = startCfg input := byinput:List (Fin 4)⊢ configs (initCfg input) 2 = startCfg input
  rw [show 2 = 0 + 1 + 1 from rfl,input:List (Fin 4)⊢ configs (initCfg input) (0 + 1 + 1) = startCfg input configs_succ_eq_step',input:List (Fin 4)⊢ MultiTapeTM.step (configs (initCfg input) 1) = startCfg input configs_succ_eq_step',input:List (Fin 4)⊢ MultiTapeTM.step (MultiTapeTM.step (configs (initCfg input) 0)) = startCfg input
    configs_zeroinput:List (Fin 4)⊢ MultiTapeTM.step (MultiTapeTM.step (initCfg input)) = startCfg input]input:List (Fin 4)⊢ MultiTapeTM.step (MultiTapeTM.step (initCfg input)) = startCfg input
  dsimp [MultiTapeTM.step, initCfg, machine, stInit, stStart]input:List (Fin 4)⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
    workTapes := fun i ↦
      match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
        (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
      | none => fun x ↦ none
      | some s => Function.update (fun x ↦ none) 0 s,
    workTapePos := fun i ↦
      0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 + 0 } =
  startCfg input
  refine Cfg.ext ?_ ?_ ?_ ?_refine_1input:List (Fin 4)⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
        | none => fun x ↦ none
        | some s => Function.update (fun x ↦ none) 0 s,
      workTapePos := fun i ↦
        0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
          0 }.state =
  (startCfg input).staterefine_2input:List (Fin 4)⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
        | none => fun x ↦ none
        | some s => Function.update (fun x ↦ none) 0 s,
      workTapePos := fun i ↦
        0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
          0 }.inputPos =
  (startCfg input).inputPosrefine_3input:List (Fin 4)⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
        | none => fun x ↦ none
        | some s => Function.update (fun x ↦ none) 0 s,
      workTapePos := fun i ↦
        0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
          0 }.workTapes =
  (startCfg input).workTapesrefine_4input:List (Fin 4)⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
        | none => fun x ↦ none
        | some s => Function.update (fun x ↦ none) 0 s,
      workTapePos := fun i ↦
        0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
          0 }.workTapePos =
  (startCfg input).workTapePos
  ·refine_1input:List (Fin 4)⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
        | none => fun x ↦ none
        | some s => Function.update (fun x ↦ none) 0 s,
      workTapePos := fun i ↦
        0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
          0 }.state =
  (startCfg input).state rflAll goals completed! 🐙
  ·refine_2input:List (Fin 4)⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
        | none => fun x ↦ none
        | some s => Function.update (fun x ↦ none) 0 s,
      workTapePos := fun i ↦
        0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
          0 }.inputPos =
  (startCfg input).inputPos simp [startCfg]All goals completed! 🐙
  ·refine_3input:List (Fin 4)⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
        | none => fun x ↦ none
        | some s => Function.update (fun x ↦ none) 0 s,
      workTapePos := fun i ↦
        0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
          0 }.workTapes =
  (startCfg input).workTapes funext i zrefine_3input:List (Fin 4)i:Fin 3z:ℤ⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
          | none => fun x ↦ none
          | some s => Function.update (fun x ↦ none) 0 s,
        workTapePos := fun i ↦
          0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
            0 }.workTapes
    i z =
  (startCfg input).workTapes i z
    fin_cases irefine_3.«0»input:List (Fin 4)z:ℤ⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
          | none => fun x ↦ none
          | some s => Function.update (fun x ↦ none) 0 s,
        workTapePos := fun i ↦
          0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
            0 }.workTapes
    ((fun i ↦ i) ⟨0, ⋯⟩) z =
  (startCfg input).workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zrefine_3.«1»input:List (Fin 4)z:ℤ⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
          | none => fun x ↦ none
          | some s => Function.update (fun x ↦ none) 0 s,
        workTapePos := fun i ↦
          0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
            0 }.workTapes
    ((fun i ↦ i) ⟨1, ⋯⟩) z =
  (startCfg input).workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zrefine_3.«2»input:List (Fin 4)z:ℤ⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
          | none => fun x ↦ none
          | some s => Function.update (fun x ↦ none) 0 s,
        workTapePos := fun i ↦
          0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
            0 }.workTapes
    ((fun i ↦ i) ⟨2, ⋯⟩) z =
  (startCfg input).workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z <;>refine_3.«0»input:List (Fin 4)z:ℤ⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
          | none => fun x ↦ none
          | some s => Function.update (fun x ↦ none) 0 s,
        workTapePos := fun i ↦
          0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
            0 }.workTapes
    ((fun i ↦ i) ⟨0, ⋯⟩) z =
  (startCfg input).workTapes ((fun i ↦ i) ⟨0, ⋯⟩) zrefine_3.«1»input:List (Fin 4)z:ℤ⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
          | none => fun x ↦ none
          | some s => Function.update (fun x ↦ none) 0 s,
        workTapePos := fun i ↦
          0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
            0 }.workTapes
    ((fun i ↦ i) ⟨1, ⋯⟩) z =
  (startCfg input).workTapes ((fun i ↦ i) ⟨1, ⋯⟩) zrefine_3.«2»input:List (Fin 4)z:ℤ⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
          | none => fun x ↦ none
          | some s => Function.update (fun x ↦ none) 0 s,
        workTapePos := fun i ↦
          0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
            0 }.workTapes
    ((fun i ↦ i) ⟨2, ⋯⟩) z =
  (startCfg input).workTapes ((fun i ↦ i) ⟨2, ⋯⟩) z simp [Function.update_apply, startCfg]All goals completed! 🐙
  ·refine_4input:List (Fin 4)⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
        | none => fun x ↦ none
        | some s => Function.update (fun x ↦ none) 0 s,
      workTapePos := fun i ↦
        0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
          0 }.workTapePos =
  (startCfg input).workTapePos funext irefine_4input:List (Fin 4)i:Fin 3⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
          | none => fun x ↦ none
          | some s => Function.update (fun x ↦ none) 0 s,
        workTapePos := fun i ↦
          0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
            0 }.workTapePos
    i =
  (startCfg input).workTapePos i
    fin_cases irefine_4.«0»input:List (Fin 4)⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
          | none => fun x ↦ none
          | some s => Function.update (fun x ↦ none) 0 s,
        workTapePos := fun i ↦
          0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
            0 }.workTapePos
    ((fun i ↦ i) ⟨0, ⋯⟩) =
  (startCfg input).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩)refine_4.«1»input:List (Fin 4)⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
          | none => fun x ↦ none
          | some s => Function.update (fun x ↦ none) 0 s,
        workTapePos := fun i ↦
          0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
            0 }.workTapePos
    ((fun i ↦ i) ⟨1, ⋯⟩) =
  (startCfg input).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩)refine_4.«2»input:List (Fin 4)⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
          | none => fun x ↦ none
          | some s => Function.update (fun x ↦ none) 0 s,
        workTapePos := fun i ↦
          0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
            0 }.workTapePos
    ((fun i ↦ i) ⟨2, ⋯⟩) =
  (startCfg input).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) <;>refine_4.«0»input:List (Fin 4)⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
          | none => fun x ↦ none
          | some s => Function.update (fun x ↦ none) 0 s,
        workTapePos := fun i ↦
          0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
            0 }.workTapePos
    ((fun i ↦ i) ⟨0, ⋯⟩) =
  (startCfg input).workTapePos ((fun i ↦ i) ⟨0, ⋯⟩)refine_4.«1»input:List (Fin 4)⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
          | none => fun x ↦ none
          | some s => Function.update (fun x ↦ none) 0 s,
        workTapePos := fun i ↦
          0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
            0 }.workTapePos
    ((fun i ↦ i) ⟨1, ⋯⟩) =
  (startCfg input).workTapePos ((fun i ↦ i) ⟨1, ⋯⟩)refine_4.«2»input:List (Fin 4)⊢ { state := some stTree, inputPos := moveInputPos (moveInputPos 1 0) 0,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            (if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).1 with
          | none => fun x ↦ none
          | some s => Function.update (fun x ↦ none) 0 s,
        workTapePos := fun i ↦
          0 + ↑(if i = 0 then (some (some 3), 0) else if i = 1 then (some (some 2), 0) else (some (some 0), 1)).2 +
            0 }.workTapePos
    ((fun i ↦ i) ⟨2, ⋯⟩) =
  (startCfg input).workTapePos ((fun i ↦ i) ⟨2, ⋯⟩) rflAll goals completed! 🐙

A carry flips exactly the selected binary tape's current digit.

theorem step_carry_digits {input : List (Fin 4)}
    (cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool) (p : ℕ)
    (hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork))
    (hp : cfg.workTapePos (if leaf then 1 else 0) = p) :
    digits (machine.step cfg) (if leaf then 1 else 0) =
      Function.update (digits cfg (if leaf then 1 else 0)) p
        (!(digits cfg (if leaf then 1 else 0) p)) := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos (if leaf = true then 1 else 0) = ↑p⊢ digits (MultiTapeTM.step cfg) (if leaf = true then 1 else 0) =
  Function.update (digits cfg (if leaf = true then 1 else 0)) p !digits cfg (if leaf = true then 1 else 0) p
  funext jinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos (if leaf = true then 1 else 0) = ↑pj:ℕ⊢ digits (MultiTapeTM.step cfg) (if leaf = true then 1 else 0) j =
  Function.update (digits cfg (if leaf = true then 1 else 0)) p (!digits cfg (if leaf = true then 1 else 0) p) j
  rw [Geb.TreeScanner.step_of_state _ _ _ hq,input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos (if leaf = true then 1 else 0) = ↑pj:ℕ⊢ digits
    { state := (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol cfg.workTapeSymbols).q',
      inputPos :=
        moveInputPos cfg.inputPos
          (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                  cfg.workTapeSymbols).workActions
              i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦
        cfg.workTapePos i +
          ↑((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                    cfg.workTapeSymbols).workActions
                i).2 }
    (if leaf = true then 1 else 0) j =
  Function.update (digits cfg (if leaf = true then 1 else 0)) p (!digits cfg (if leaf = true then 1 else 0) p) j tr_carryinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos (if leaf = true then 1 else 0) = ↑pj:ℕ⊢ digits
    { state := (carry leaf cfg.workTapeSymbols).q',
      inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((carry leaf cfg.workTapeSymbols).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }
    (if leaf = true then 1 else 0) j =
  Function.update (digits cfg (if leaf = true then 1 else 0)) p (!digits cfg (if leaf = true then 1 else 0) p) j]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos (if leaf = true then 1 else 0) = ↑pj:ℕ⊢ digits
    { state := (carry leaf cfg.workTapeSymbols).q',
      inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((carry leaf cfg.workTapeSymbols).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }
    (if leaf = true then 1 else 0) j =
  Function.update (digits cfg (if leaf = true then 1 else 0)) p (!digits cfg (if leaf = true then 1 else 0) p) j
  cases leaffalseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕj:ℕhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos (if false = true then 1 else 0) = ↑p⊢ digits
    { state := (carry false cfg.workTapeSymbols).q',
      inputPos := moveInputPos cfg.inputPos (carry false cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((carry false cfg.workTapeSymbols).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry false cfg.workTapeSymbols).workActions i).2 }
    (if false = true then 1 else 0) j =
  Function.update (digits cfg (if false = true then 1 else 0)) p (!digits cfg (if false = true then 1 else 0) p) jtrueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕj:ℕhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos (if true = true then 1 else 0) = ↑p⊢ digits
    { state := (carry true cfg.workTapeSymbols).q',
      inputPos := moveInputPos cfg.inputPos (carry true cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((carry true cfg.workTapeSymbols).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry true cfg.workTapeSymbols).workActions i).2 }
    (if true = true then 1 else 0) j =
  Function.update (digits cfg (if true = true then 1 else 0)) p (!digits cfg (if true = true then 1 else 0) p) j
  all_goals
    simp only [Bool.false_eq_true, ↓reduceIte] at hptrueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕj:ℕhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos 1 = ↑p⊢ digits
    { state := (carry true cfg.workTapeSymbols).q',
      inputPos := moveInputPos cfg.inputPos (carry true cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((carry true cfg.workTapeSymbols).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry true cfg.workTapeSymbols).workActions i).2 }
    (if true = true then 1 else 0) j =
  Function.update (digits cfg (if true = true then 1 else 0)) p (!digits cfg (if true = true then 1 else 0) p) j
    dsimp [digits, carry]trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕj:ℕhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos 1 = ↑p⊢ digit (Function.update (cfg.workTapes 1) (cfg.workTapePos 1) (some (flipped (cfg.workTapeSymbols 1))) ↑j) =
  Function.update (digits cfg 1) p (!digit (cfg.workTapes 1 ↑p)) j
    rw [hpfalseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕj:ℕhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos 0 = ↑p⊢ digit (Function.update (cfg.workTapes 0) (↑p) (some (flipped (cfg.workTapeSymbols 0))) ↑j) =
  Function.update (digits cfg 0) p (!digit (cfg.workTapes 0 ↑p)) j]falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕj:ℕhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos 0 = ↑p⊢ digit (Function.update (cfg.workTapes 0) (↑p) (some (flipped (cfg.workTapeSymbols 0))) ↑j) =
  Function.update (digits cfg 0) p (!digit (cfg.workTapes 0 ↑p)) jtrueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕj:ℕhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos 1 = ↑p⊢ digit (Function.update (cfg.workTapes 1) (↑p) (some (flipped (cfg.workTapeSymbols 1))) ↑j) =
  Function.update (digits cfg 1) p (!digit (cfg.workTapes 1 ↑p)) j
    simp only [Function.update_apply]trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕj:ℕhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos 1 = ↑p⊢ digit (if ↑j = ↑p then some (flipped (cfg.workTapeSymbols 1)) else cfg.workTapes 1 ↑j) =
  if j = p then !digit (cfg.workTapes 1 ↑p) else digits cfg 1 j
    by_cases h : j = pposinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕj:ℕhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos 1 = ↑ph:j = p⊢ digit (if ↑j = ↑p then some (flipped (cfg.workTapeSymbols 1)) else cfg.workTapes 1 ↑j) =
  if j = p then !digit (cfg.workTapes 1 ↑p) else digits cfg 1 jneginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕj:ℕhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos 1 = ↑ph:¬j = p⊢ digit (if ↑j = ↑p then some (flipped (cfg.workTapeSymbols 1)) else cfg.workTapes 1 ↑j) =
  if j = p then !digit (cfg.workTapes 1 ↑p) else digits cfg 1 j
    ·posinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕj:ℕhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos 1 = ↑ph:j = p⊢ digit (if ↑j = ↑p then some (flipped (cfg.workTapeSymbols 1)) else cfg.workTapes 1 ↑j) =
  if j = p then !digit (cfg.workTapes 1 ↑p) else digits cfg 1 j subst jposinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos 1 = ↑p⊢ digit (if ↑p = ↑p then some (flipped (cfg.workTapeSymbols 1)) else cfg.workTapes 1 ↑p) =
  if p = p then !digit (cfg.workTapes 1 ↑p) else digits cfg 1 p
      simp only [ite_true, Cfg.workTapeSymbols, hp]posinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos 1 = ↑p⊢ digit (some (flipped (cfg.workTapes 1 ↑p))) = !digit (cfg.workTapes 1 ↑p)
      exact digit_flipped _All goals completed! 🐙
    ·neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕj:ℕhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos 1 = ↑ph:¬j = p⊢ digit (if ↑j = ↑p then some (flipped (cfg.workTapeSymbols 1)) else cfg.workTapes 1 ↑j) =
  if j = p then !digit (cfg.workTapes 1 ↑p) else digits cfg 1 j have hz : (j : ℤ) ≠ p := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos (if leaf = true then 1 else 0) = ↑p⊢ digits (MultiTapeTM.step cfg) (if leaf = true then 1 else 0) =
  Function.update (digits cfg (if leaf = true then 1 else 0)) p !digits cfg (if leaf = true then 1 else 0) p omeganeginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕj:ℕhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos 1 = ↑ph:¬j = phz:↑j ≠ ↑p⊢ digit (if ↑j = ↑p then some (flipped (cfg.workTapeSymbols 1)) else cfg.workTapes 1 ↑j) =
  if j = p then !digit (cfg.workTapes 1 ↑p) else digits cfg 1 j
      simp only [h, hz, ↓reduceIte]neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputp:ℕj:ℕhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hp:cfg.workTapePos 1 = ↑ph:¬j = phz:↑j ≠ ↑p⊢ digit (cfg.workTapes 1 ↑j) = digits cfg 1 j
      rflAll goals completed! 🐙

The other binary tape is unchanged by a carry.

theorem step_carry_other_digits {input : List (Fin 4)}
    (cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool)
    (hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork)) :
    digits (machine.step cfg) (if leaf then 0 else 1) =
      digits cfg (if leaf then 0 else 1) := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ digits (MultiTapeTM.step cfg) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
  funext jinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)j:ℕ⊢ digits (MultiTapeTM.step cfg) (if leaf = true then 0 else 1) j = digits cfg (if leaf = true then 0 else 1) j
  rw [Geb.TreeScanner.step_of_state _ _ _ hq,input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)j:ℕ⊢ digits
    { state := (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol cfg.workTapeSymbols).q',
      inputPos :=
        moveInputPos cfg.inputPos
          (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                  cfg.workTapeSymbols).workActions
              i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦
        cfg.workTapePos i +
          ↑((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                    cfg.workTapeSymbols).workActions
                i).2 }
    (if leaf = true then 0 else 1) j =
  digits cfg (if leaf = true then 0 else 1) j tr_carryinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)j:ℕ⊢ digits
    { state := (carry leaf cfg.workTapeSymbols).q',
      inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((carry leaf cfg.workTapeSymbols).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }
    (if leaf = true then 0 else 1) j =
  digits cfg (if leaf = true then 0 else 1) j]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)j:ℕ⊢ digits
    { state := (carry leaf cfg.workTapeSymbols).q',
      inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((carry leaf cfg.workTapeSymbols).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }
    (if leaf = true then 0 else 1) j =
  digits cfg (if leaf = true then 0 else 1) j
  cases leaffalseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputj:ℕhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)⊢ digits
    { state := (carry false cfg.workTapeSymbols).q',
      inputPos := moveInputPos cfg.inputPos (carry false cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((carry false cfg.workTapeSymbols).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry false cfg.workTapeSymbols).workActions i).2 }
    (if false = true then 0 else 1) j =
  digits cfg (if false = true then 0 else 1) jtrueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputj:ℕhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)⊢ digits
    { state := (carry true cfg.workTapeSymbols).q',
      inputPos := moveInputPos cfg.inputPos (carry true cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((carry true cfg.workTapeSymbols).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry true cfg.workTapeSymbols).workActions i).2 }
    (if true = true then 0 else 1) j =
  digits cfg (if true = true then 0 else 1) j <;>falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputj:ℕhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)⊢ digits
    { state := (carry false cfg.workTapeSymbols).q',
      inputPos := moveInputPos cfg.inputPos (carry false cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((carry false cfg.workTapeSymbols).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry false cfg.workTapeSymbols).workActions i).2 }
    (if false = true then 0 else 1) j =
  digits cfg (if false = true then 0 else 1) jtrueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputj:ℕhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)⊢ digits
    { state := (carry true cfg.workTapeSymbols).q',
      inputPos := moveInputPos cfg.inputPos (carry true cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((carry true cfg.workTapeSymbols).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry true cfg.workTapeSymbols).workActions i).2 }
    (if true = true then 0 else 1) j =
  digits cfg (if true = true then 0 else 1) j rflAll goals completed! 🐙

A carry updates the mismatch head by the displacement of its local digit comparison.

theorem step_carry_mismatchPos {input : List (Fin 4)}
    (cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool)
    (hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork)) :
    (machine.step cfg).workTapePos 2 = cfg.workTapePos 2 +
      (mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)).cast := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ (MultiTapeTM.step cfg).workTapePos 2 =
  cfg.workTapePos 2 + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1))
  rw [Geb.TreeScanner.step_of_state _ _ _ hq,input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ { state := (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol cfg.workTapeSymbols).q',
        inputPos :=
          moveInputPos cfg.inputPos
            (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                    cfg.workTapeSymbols).workActions
                i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦
          cfg.workTapePos i +
            ↑((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                      cfg.workTapeSymbols).workActions
                  i).2 }.workTapePos
    2 =
  cfg.workTapePos 2 + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) tr_carryinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ { state := (carry leaf cfg.workTapeSymbols).q',
        inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((carry leaf cfg.workTapeSymbols).workActions i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }.workTapePos
    2 =
  cfg.workTapePos 2 + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1))]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ { state := (carry leaf cfg.workTapeSymbols).q',
        inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((carry leaf cfg.workTapeSymbols).workActions i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }.workTapePos
    2 =
  cfg.workTapePos 2 + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1))
  cases leaffalseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)⊢ { state := (carry false cfg.workTapeSymbols).q',
        inputPos := moveInputPos cfg.inputPos (carry false cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((carry false cfg.workTapeSymbols).workActions i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry false cfg.workTapeSymbols).workActions i).2 }.workTapePos
    2 =
  cfg.workTapePos 2 + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1))trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)⊢ { state := (carry true cfg.workTapeSymbols).q',
        inputPos := moveInputPos cfg.inputPos (carry true cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((carry true cfg.workTapeSymbols).workActions i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry true cfg.workTapeSymbols).workActions i).2 }.workTapePos
    2 =
  cfg.workTapePos 2 + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) <;>falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)⊢ { state := (carry false cfg.workTapeSymbols).q',
        inputPos := moveInputPos cfg.inputPos (carry false cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((carry false cfg.workTapeSymbols).workActions i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry false cfg.workTapeSymbols).workActions i).2 }.workTapePos
    2 =
  cfg.workTapePos 2 + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1))trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)⊢ { state := (carry true cfg.workTapeSymbols).q',
        inputPos := moveInputPos cfg.inputPos (carry true cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((carry true cfg.workTapeSymbols).workActions i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry true cfg.workTapeSymbols).workActions i).2 }.workTapePos
    2 =
  cfg.workTapePos 2 + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) rflAll goals completed! 🐙

Every carry advances each binary head by one cell.

theorem step_carry_binaryPos {input : List (Fin 4)}
    (cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool) (i : Fin 3) (hi : i ≠ 2)
    (hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork)) :
    (machine.step cfg).workTapePos i = cfg.workTapePos i + 1 := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Booli:Fin 3hi:i ≠ 2hq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ (MultiTapeTM.step cfg).workTapePos i = cfg.workTapePos i + 1
  rw [Geb.TreeScanner.step_of_state _ _ _ hq,input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Booli:Fin 3hi:i ≠ 2hq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ { state := (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol cfg.workTapeSymbols).q',
        inputPos :=
          moveInputPos cfg.inputPos
            (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                    cfg.workTapeSymbols).workActions
                i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦
          cfg.workTapePos i +
            ↑((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                      cfg.workTapeSymbols).workActions
                  i).2 }.workTapePos
    i =
  cfg.workTapePos i + 1 tr_carryinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Booli:Fin 3hi:i ≠ 2hq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ { state := (carry leaf cfg.workTapeSymbols).q',
        inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((carry leaf cfg.workTapeSymbols).workActions i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }.workTapePos
    i =
  cfg.workTapePos i + 1]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Booli:Fin 3hi:i ≠ 2hq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ { state := (carry leaf cfg.workTapeSymbols).q',
        inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((carry leaf cfg.workTapeSymbols).workActions i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }.workTapePos
    i =
  cfg.workTapePos i + 1
  simp [carry, hi]All goals completed! 🐙

Carry propagation does not move the input head.

theorem step_carry_inputPos {input : List (Fin 4)}
    (cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool)
    (hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork)) :
    (machine.step cfg).inputPos = cfg.inputPos := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ (MultiTapeTM.step cfg).inputPos = cfg.inputPos
  rw [Geb.TreeScanner.step_of_state _ _ _ hq,input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ { state := (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol cfg.workTapeSymbols).q',
      inputPos :=
        moveInputPos cfg.inputPos
          (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                  cfg.workTapeSymbols).workActions
              i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦
        cfg.workTapePos i +
          ↑((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                    cfg.workTapeSymbols).workActions
                i).2 }.inputPos =
  cfg.inputPos tr_carryinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ { state := (carry leaf cfg.workTapeSymbols).q',
      inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((carry leaf cfg.workTapeSymbols).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }.inputPos =
  cfg.inputPos]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ { state := (carry leaf cfg.workTapeSymbols).q',
      inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((carry leaf cfg.workTapeSymbols).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }.inputPos =
  cfg.inputPos
  exact moveInputPos_zero _All goals completed! 🐙

A carry continues through ones and ends at the first zero.

theorem step_carry_state {input : List (Fin 4)}
    (cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool)
    (hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork)) :
    (machine.step cfg).state = some (if digit (cfg.workTapeSymbols (if leaf then 1 else 0))
      then (if leaf then stCarryLeaf else stCarryFork) else stReturn) := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ (MultiTapeTM.step cfg).state =
  some
    (if digit (cfg.workTapeSymbols (if leaf = true then 1 else 0)) = true then
      if leaf = true then stCarryLeaf else stCarryFork
    else stReturn)
  rw [Geb.TreeScanner.step_of_state _ _ _ hq,input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ { state := (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol cfg.workTapeSymbols).q',
      inputPos :=
        moveInputPos cfg.inputPos
          (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                  cfg.workTapeSymbols).workActions
              i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦
        cfg.workTapePos i +
          ↑((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                    cfg.workTapeSymbols).workActions
                i).2 }.state =
  some
    (if digit (cfg.workTapeSymbols (if leaf = true then 1 else 0)) = true then
      if leaf = true then stCarryLeaf else stCarryFork
    else stReturn) tr_carryinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ { state := (carry leaf cfg.workTapeSymbols).q',
      inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((carry leaf cfg.workTapeSymbols).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }.state =
  some
    (if digit (cfg.workTapeSymbols (if leaf = true then 1 else 0)) = true then
      if leaf = true then stCarryLeaf else stCarryFork
    else stReturn)]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ { state := (carry leaf cfg.workTapeSymbols).q',
      inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
      workTapes := fun i ↦
        match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
          ((carry leaf cfg.workTapeSymbols).workActions i).1 with
        | none => cfg.workTapes i
        | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
      workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }.state =
  some
    (if digit (cfg.workTapeSymbols (if leaf = true then 1 else 0)) = true then
      if leaf = true then stCarryLeaf else stCarryFork
    else stReturn)
  rflAll goals completed! 🐙

Carry propagation emits no output symbols.

theorem outputSymbol_carry {input : List (Fin 4)}
    (cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool)
    (hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork)) :
    machine.outputSymbol cfg = none := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ outputSymbol cfg = none
  simp only [outputSymbol, hq, tr_carry]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ (carry leaf cfg.workTapeSymbols).outS = none
  cases leaffalseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)⊢ (carry false cfg.workTapeSymbols).outS = nonetrueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)⊢ (carry true cfg.workTapeSymbols).outS = none <;>falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)⊢ (carry false cfg.workTapeSymbols).outS = nonetrueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)⊢ (carry true cfg.workTapeSymbols).outS = none rflAll goals completed! 🐙

A carry preserves every origin tag on the first binary tape.

theorem step_carry_origin {input : List (Fin 4)}
    (cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool) (z : ℤ)
    (hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork)) :
    origin ((machine.step cfg).workTapes 0 z) = origin (cfg.workTapes 0 z) := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolz:ℤhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ origin ((MultiTapeTM.step cfg).workTapes 0 z) = origin (cfg.workTapes 0 z)
  rw [Geb.TreeScanner.step_of_state _ _ _ hq,input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolz:ℤhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ origin
    ({ state := (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol cfg.workTapeSymbols).q',
          inputPos :=
            moveInputPos cfg.inputPos
              (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                  cfg.workTapeSymbols).inputMove,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
              ((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                      cfg.workTapeSymbols).workActions
                  i).1 with
            | none => cfg.workTapes i
            | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
          workTapePos := fun i ↦
            cfg.workTapePos i +
              ↑((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                        cfg.workTapeSymbols).workActions
                    i).2 }.workTapes
      0 z) =
  origin (cfg.workTapes 0 z) tr_carryinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolz:ℤhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ origin
    ({ state := (carry leaf cfg.workTapeSymbols).q',
          inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
              ((carry leaf cfg.workTapeSymbols).workActions i).1 with
            | none => cfg.workTapes i
            | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
          workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }.workTapes
      0 z) =
  origin (cfg.workTapes 0 z)]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolz:ℤhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ origin
    ({ state := (carry leaf cfg.workTapeSymbols).q',
          inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
              ((carry leaf cfg.workTapeSymbols).workActions i).1 with
            | none => cfg.workTapes i
            | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
          workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }.workTapes
      0 z) =
  origin (cfg.workTapes 0 z)
  cases leaf with
  | true =>trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputz:ℤhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)⊢ origin
    ({ state := (carry true cfg.workTapeSymbols).q',
          inputPos := moveInputPos cfg.inputPos (carry true cfg.workTapeSymbols).inputMove,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
              ((carry true cfg.workTapeSymbols).workActions i).1 with
            | none => cfg.workTapes i
            | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
          workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry true cfg.workTapeSymbols).workActions i).2 }.workTapes
      0 z) =
  origin (cfg.workTapes 0 z) rflAll goals completed! 🐙
  | false =>falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputz:ℤhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)⊢ origin
    ({ state := (carry false cfg.workTapeSymbols).q',
          inputPos := moveInputPos cfg.inputPos (carry false cfg.workTapeSymbols).inputMove,
          workTapes := fun i ↦
            match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
              ((carry false cfg.workTapeSymbols).workActions i).1 with
            | none => cfg.workTapes i
            | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
          workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry false cfg.workTapeSymbols).workActions i).2 }.workTapes
      0 z) =
  origin (cfg.workTapes 0 z)
    change origin (Function.update (cfg.workTapes 0) (cfg.workTapePos 0)
      (some (flipped (cfg.workTapeSymbols 0))) z) = _falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputz:ℤhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)⊢ origin (Function.update (cfg.workTapes 0) (cfg.workTapePos 0) (some (flipped (cfg.workTapeSymbols 0))) z) =
  origin (cfg.workTapes 0 z)
    by_cases hz : z = cfg.workTapePos 0posinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputz:ℤhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hz:z = cfg.workTapePos 0⊢ origin (Function.update (cfg.workTapes 0) (cfg.workTapePos 0) (some (flipped (cfg.workTapeSymbols 0))) z) =
  origin (cfg.workTapes 0 z)neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputz:ℤhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hz:¬z = cfg.workTapePos 0⊢ origin (Function.update (cfg.workTapes 0) (cfg.workTapePos 0) (some (flipped (cfg.workTapeSymbols 0))) z) =
  origin (cfg.workTapes 0 z)
    ·posinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputz:ℤhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hz:z = cfg.workTapePos 0⊢ origin (Function.update (cfg.workTapes 0) (cfg.workTapePos 0) (some (flipped (cfg.workTapeSymbols 0))) z) =
  origin (cfg.workTapes 0 z) subst zposinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)⊢ origin
    (Function.update (cfg.workTapes 0) (cfg.workTapePos 0) (some (flipped (cfg.workTapeSymbols 0)))
      (cfg.workTapePos 0)) =
  origin (cfg.workTapes 0 (cfg.workTapePos 0))
      rw [Function.update_selfposinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)⊢ origin (some (flipped (cfg.workTapeSymbols 0))) = origin (cfg.workTapes 0 (cfg.workTapePos 0))]posinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)⊢ origin (some (flipped (cfg.workTapeSymbols 0))) = origin (cfg.workTapes 0 (cfg.workTapePos 0))
      exact origin_flipped _All goals completed! 🐙
    ·neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputz:ℤhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hz:¬z = cfg.workTapePos 0⊢ origin (Function.update (cfg.workTapes 0) (cfg.workTapePos 0) (some (flipped (cfg.workTapeSymbols 0))) z) =
  origin (cfg.workTapes 0 z) rw [Function.update_of_ne hzneginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputz:ℤhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hz:¬z = cfg.workTapePos 0⊢ origin (cfg.workTapes 0 z) = origin (cfg.workTapes 0 z)]All goals completed! 🐙

Carry propagation never writes on the mismatch tape.

theorem step_carry_marker {input : List (Fin 4)}
    (cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool)
    (hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork)) :
    (machine.step cfg).workTapes 2 = cfg.workTapes 2 := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ (MultiTapeTM.step cfg).workTapes 2 = cfg.workTapes 2
  rw [Geb.TreeScanner.step_of_state _ _ _ hq,input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ { state := (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol cfg.workTapeSymbols).q',
        inputPos :=
          moveInputPos cfg.inputPos
            (machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                    cfg.workTapeSymbols).workActions
                i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦
          cfg.workTapePos i +
            ↑((machine.tr (if leaf = true then stCarryLeaf else stCarryFork) cfg.inputSymbol
                      cfg.workTapeSymbols).workActions
                  i).2 }.workTapes
    2 =
  cfg.workTapes 2 tr_carryinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ { state := (carry leaf cfg.workTapeSymbols).q',
        inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((carry leaf cfg.workTapeSymbols).workActions i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }.workTapes
    2 =
  cfg.workTapes 2]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ { state := (carry leaf cfg.workTapeSymbols).q',
        inputPos := moveInputPos cfg.inputPos (carry leaf cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((carry leaf cfg.workTapeSymbols).workActions i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry leaf cfg.workTapeSymbols).workActions i).2 }.workTapes
    2 =
  cfg.workTapes 2
  cases leaffalseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)⊢ { state := (carry false cfg.workTapeSymbols).q',
        inputPos := moveInputPos cfg.inputPos (carry false cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((carry false cfg.workTapeSymbols).workActions i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry false cfg.workTapeSymbols).workActions i).2 }.workTapes
    2 =
  cfg.workTapes 2trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)⊢ { state := (carry true cfg.workTapeSymbols).q',
        inputPos := moveInputPos cfg.inputPos (carry true cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((carry true cfg.workTapeSymbols).workActions i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry true cfg.workTapeSymbols).workActions i).2 }.workTapes
    2 =
  cfg.workTapes 2 <;>falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)⊢ { state := (carry false cfg.workTapeSymbols).q',
        inputPos := moveInputPos cfg.inputPos (carry false cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((carry false cfg.workTapeSymbols).workActions i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry false cfg.workTapeSymbols).workActions i).2 }.workTapes
    2 =
  cfg.workTapes 2trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputhq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)⊢ { state := (carry true cfg.workTapeSymbols).q',
        inputPos := moveInputPos cfg.inputPos (carry true cfg.workTapeSymbols).inputMove,
        workTapes := fun i ↦
          match (motive := Option (Option (Fin 4)) → ℤ → Option (Fin 4))
            ((carry true cfg.workTapeSymbols).workActions i).1 with
          | none => cfg.workTapes i
          | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s,
        workTapePos := fun i ↦ cfg.workTapePos i + ↑((carry true cfg.workTapeSymbols).workActions i).2 }.workTapes
    2 =
  cfg.workTapes 2 rflAll goals completed! 🐙

One carry transition preserves the mismatch-count invariant.

theorem step_carry_mismatch {input : List (Fin 4)}
    (cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool) (width p : ℕ)
    (hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork))
    (hp0 : cfg.workTapePos 0 = p) (hp1 : cfg.workTapePos 1 = p) (hp : p < width)
    (hm : cfg.workTapePos 2 = (mismatchCount width (digits cfg 0) (digits cfg 1) : ℤ)) :
    (machine.step cfg).workTapePos 2 =
      (mismatchCount width (digits (machine.step cfg) 0)
        (digits (machine.step cfg) 1) : ℤ) := byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕp:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))⊢ (MultiTapeTM.step cfg).workTapePos 2 =
  ↑(mismatchCount width (digits (MultiTapeTM.step cfg) 0) (digits (MultiTapeTM.step cfg) 1))
  have hd := step_carry_digits cfg leaf p hq (byinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕp:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))⊢ cfg.workTapePos (if leaf = true then 1 else 0) = ↑p cases leaffalseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)⊢ cfg.workTapePos (if false = true then 1 else 0) = ↑ptrueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)⊢ cfg.workTapePos (if true = true then 1 else 0) = ↑p <;>falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)⊢ cfg.workTapePos (if false = true then 1 else 0) = ↑ptrueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)⊢ cfg.workTapePos (if true = true then 1 else 0) = ↑p assumptionAll goals completed! 🐙)input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕp:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hd:digits (MultiTapeTM.step cfg) (if leaf = true then 1 else 0) =
  Function.update (digits cfg (if leaf = true then 1 else 0)) p !digits cfg (if leaf = true then 1 else 0) p⊢ (MultiTapeTM.step cfg).workTapePos 2 =
  ↑(mismatchCount width (digits (MultiTapeTM.step cfg) 0) (digits (MultiTapeTM.step cfg) 1))
  have he := step_carry_other_digits cfg leaf hqinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕp:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hd:digits (MultiTapeTM.step cfg) (if leaf = true then 1 else 0) =
  Function.update (digits cfg (if leaf = true then 1 else 0)) p !digits cfg (if leaf = true then 1 else 0) phe:digits (MultiTapeTM.step cfg) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ (MultiTapeTM.step cfg).workTapePos 2 =
  ↑(mismatchCount width (digits (MultiTapeTM.step cfg) 0) (digits (MultiTapeTM.step cfg) 1))
  rw [step_carry_mismatchPos cfg leaf hq,input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕp:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hd:digits (MultiTapeTM.step cfg) (if leaf = true then 1 else 0) =
  Function.update (digits cfg (if leaf = true then 1 else 0)) p !digits cfg (if leaf = true then 1 else 0) phe:digits (MultiTapeTM.step cfg) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ cfg.workTapePos 2 + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits (MultiTapeTM.step cfg) 0) (digits (MultiTapeTM.step cfg) 1)) hminput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕp:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hd:digits (MultiTapeTM.step cfg) (if leaf = true then 1 else 0) =
  Function.update (digits cfg (if leaf = true then 1 else 0)) p !digits cfg (if leaf = true then 1 else 0) phe:digits (MultiTapeTM.step cfg) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits (MultiTapeTM.step cfg) 0) (digits (MultiTapeTM.step cfg) 1))]input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolwidth:ℕp:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hd:digits (MultiTapeTM.step cfg) (if leaf = true then 1 else 0) =
  Function.update (digits cfg (if leaf = true then 1 else 0)) p !digits cfg (if leaf = true then 1 else 0) phe:digits (MultiTapeTM.step cfg) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits (MultiTapeTM.step cfg) 0) (digits (MultiTapeTM.step cfg) 1))
  cases leaffalseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) (if false = true then 1 else 0) =
  Function.update (digits cfg (if false = true then 1 else 0)) p !digits cfg (if false = true then 1 else 0) phe:digits (MultiTapeTM.step cfg) (if false = true then 0 else 1) = digits cfg (if false = true then 0 else 1)⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits (MultiTapeTM.step cfg) 0) (digits (MultiTapeTM.step cfg) 1))trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) (if true = true then 1 else 0) =
  Function.update (digits cfg (if true = true then 1 else 0)) p !digits cfg (if true = true then 1 else 0) phe:digits (MultiTapeTM.step cfg) (if true = true then 0 else 1) = digits cfg (if true = true then 0 else 1)⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits (MultiTapeTM.step cfg) 0) (digits (MultiTapeTM.step cfg) 1)) <;>falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) (if false = true then 1 else 0) =
  Function.update (digits cfg (if false = true then 1 else 0)) p !digits cfg (if false = true then 1 else 0) phe:digits (MultiTapeTM.step cfg) (if false = true then 0 else 1) = digits cfg (if false = true then 0 else 1)⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits (MultiTapeTM.step cfg) 0) (digits (MultiTapeTM.step cfg) 1))trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) (if true = true then 1 else 0) =
  Function.update (digits cfg (if true = true then 1 else 0)) p !digits cfg (if true = true then 1 else 0) phe:digits (MultiTapeTM.step cfg) (if true = true then 0 else 1) = digits cfg (if true = true then 0 else 1)⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits (MultiTapeTM.step cfg) 0) (digits (MultiTapeTM.step cfg) 1)) simp only [Bool.false_eq_true, ↓reduceIte] at hd hetrueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 1 = Function.update (digits cfg 1) p !digits cfg 1 phe:digits (MultiTapeTM.step cfg) 0 = digits cfg 0⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits (MultiTapeTM.step cfg) 0) (digits (MultiTapeTM.step cfg) 1))
  ·falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 0 = Function.update (digits cfg 0) p !digits cfg 0 phe:digits (MultiTapeTM.step cfg) 1 = digits cfg 1⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits (MultiTapeTM.step cfg) 0) (digits (MultiTapeTM.step cfg) 1)) rw [hd,falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 0 = Function.update (digits cfg 0) p !digits cfg 0 phe:digits (MultiTapeTM.step cfg) 1 = digits cfg 1⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (Function.update (digits cfg 0) p !digits cfg 0 p) (digits (MultiTapeTM.step cfg) 1)) hefalseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 0 = Function.update (digits cfg 0) p !digits cfg 0 phe:digits (MultiTapeTM.step cfg) 1 = digits cfg 1⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (Function.update (digits cfg 0) p !digits cfg 0 p) (digits cfg 1))]falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 0 = Function.update (digits cfg 0) p !digits cfg 0 phe:digits (MultiTapeTM.step cfg) 1 = digits cfg 1⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (Function.update (digits cfg 0) p !digits cfg 0 p) (digits cfg 1))
    rw [← flipAt,falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 0 = Function.update (digits cfg 0) p !digits cfg 0 phe:digits (MultiTapeTM.step cfg) 1 = digits cfg 1⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (flipAt (digits cfg 0) p) (digits cfg 1)) mismatchCount_flip_left width p _ _ hpfalseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 0 = Function.update (digits cfg 0) p !digits cfg 0 phe:digits (MultiTapeTM.step cfg) 1 = digits cfg 1⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + if digits cfg 0 p = digits cfg 1 p then 1 else -1]falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 0 = Function.update (digits cfg 0) p !digits cfg 0 phe:digits (MultiTapeTM.step cfg) 1 = digits cfg 1⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + if digits cfg 0 p = digits cfg 1 p then 1 else -1
    congr 1false.e_ainput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 0 = Function.update (digits cfg 0) p !digits cfg 0 phe:digits (MultiTapeTM.step cfg) 1 = digits cfg 1⊢ ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) = if digits cfg 0 p = digits cfg 1 p then 1 else -1
    simp only [mismatchMove, Cfg.workTapeSymbols, hp0, hp1, digits, beq_iff_eq]false.e_ainput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 0 = Function.update (digits cfg 0) p !digits cfg 0 phe:digits (MultiTapeTM.step cfg) 1 = digits cfg 1⊢ ↑(if digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p) then 1 else -1) =
  if digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p) then 1 else -1
    split_ifsposinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 0 = Function.update (digits cfg 0) p !digits cfg 0 phe:digits (MultiTapeTM.step cfg) 1 = digits cfg 1h✝:digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p)⊢ ↑1 = if digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p) then 1 else -1neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 0 = Function.update (digits cfg 0) p !digits cfg 0 phe:digits (MultiTapeTM.step cfg) 1 = digits cfg 1h✝:¬digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p)⊢ ↑(-1) = if digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p) then 1 else -1 <;>posinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 0 = Function.update (digits cfg 0) p !digits cfg 0 phe:digits (MultiTapeTM.step cfg) 1 = digits cfg 1h✝:digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p)⊢ ↑1 = if digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p) then 1 else -1neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if false = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 0 = Function.update (digits cfg 0) p !digits cfg 0 phe:digits (MultiTapeTM.step cfg) 1 = digits cfg 1h✝:¬digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p)⊢ ↑(-1) = if digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p) then 1 else -1 simp_allAll goals completed! 🐙
  ·trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 1 = Function.update (digits cfg 1) p !digits cfg 1 phe:digits (MultiTapeTM.step cfg) 0 = digits cfg 0⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits (MultiTapeTM.step cfg) 0) (digits (MultiTapeTM.step cfg) 1)) rw [he,trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 1 = Function.update (digits cfg 1) p !digits cfg 1 phe:digits (MultiTapeTM.step cfg) 0 = digits cfg 0⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits cfg 0) (digits (MultiTapeTM.step cfg) 1)) hdtrueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 1 = Function.update (digits cfg 1) p !digits cfg 1 phe:digits (MultiTapeTM.step cfg) 0 = digits cfg 0⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits cfg 0) (Function.update (digits cfg 1) p !digits cfg 1 p))]trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 1 = Function.update (digits cfg 1) p !digits cfg 1 phe:digits (MultiTapeTM.step cfg) 0 = digits cfg 0⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits cfg 0) (Function.update (digits cfg 1) p !digits cfg 1 p))
    rw [← flipAt,trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 1 = Function.update (digits cfg 1) p !digits cfg 1 phe:digits (MultiTapeTM.step cfg) 0 = digits cfg 0⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits cfg 0) (flipAt (digits cfg 1) p)) mismatchCount_flip_right width p _ _ hptrueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 1 = Function.update (digits cfg 1) p !digits cfg 1 phe:digits (MultiTapeTM.step cfg) 0 = digits cfg 0⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + if digits cfg 0 p = digits cfg 1 p then 1 else -1]trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 1 = Function.update (digits cfg 1) p !digits cfg 1 phe:digits (MultiTapeTM.step cfg) 0 = digits cfg 0⊢ ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) =
  ↑(mismatchCount width (digits cfg 0) (digits cfg 1)) + if digits cfg 0 p = digits cfg 1 p then 1 else -1
    congr 1true.e_ainput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 1 = Function.update (digits cfg 1) p !digits cfg 1 phe:digits (MultiTapeTM.step cfg) 0 = digits cfg 0⊢ ↑(mismatchMove (cfg.workTapeSymbols 0) (cfg.workTapeSymbols 1)) = if digits cfg 0 p = digits cfg 1 p then 1 else -1
    simp only [mismatchMove, Cfg.workTapeSymbols, hp0, hp1, digits, beq_iff_eq]true.e_ainput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 1 = Function.update (digits cfg 1) p !digits cfg 1 phe:digits (MultiTapeTM.step cfg) 0 = digits cfg 0⊢ ↑(if digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p) then 1 else -1) =
  if digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p) then 1 else -1
    split_ifsposinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 1 = Function.update (digits cfg 1) p !digits cfg 1 phe:digits (MultiTapeTM.step cfg) 0 = digits cfg 0h✝:digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p)⊢ ↑1 = if digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p) then 1 else -1neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 1 = Function.update (digits cfg 1) p !digits cfg 1 phe:digits (MultiTapeTM.step cfg) 0 = digits cfg 0h✝:¬digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p)⊢ ↑(-1) = if digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p) then 1 else -1 <;>posinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 1 = Function.update (digits cfg 1) p !digits cfg 1 phe:digits (MultiTapeTM.step cfg) 0 = digits cfg 0h✝:digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p)⊢ ↑1 = if digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p) then 1 else -1neginput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputwidth:ℕp:ℕhp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑php:p < widthhm:cfg.workTapePos 2 = ↑(mismatchCount width (digits cfg 0) (digits cfg 1))hq:cfg.state = some (if true = true then stCarryLeaf else stCarryFork)hd:digits (MultiTapeTM.step cfg) 1 = Function.update (digits cfg 1) p !digits cfg 1 phe:digits (MultiTapeTM.step cfg) 0 = digits cfg 0h✝:¬digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p)⊢ ↑(-1) = if digit (cfg.workTapes 0 ↑p) = digit (cfg.workTapes 1 ↑p) then 1 else -1 simp_allAll goals completed! 🐙

end Geb.BitTree.BinaryMachine