Imports
/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module
public import Geb.Prototypes.Computability.BitTree.BinaryMachine.Steps
public import Geb.Prototypes.Computability.BitTree.Counterset_option doc.verso trueBinary carry execution
An initial sequence of one-bits is reset while both binary heads advance. The first zero-bit ends the carry after being set to one. The statements here follow the actual machine steps.
Main statements
-
configs_carry_prefixdescribes every intermediate carry configuration. -
configs_carry_bitsidentifies the terminal counter with binary-list increment. -
configs_carry_bits_posgives both binary head positions throughout the carry.
Implementation notes
The module relates list-level increment to CSLib's configuration sequence. Its machine statements inherit the axioms of CSLib's input-symbol access through the step function.
Tags
Turing machine, binary counter, carry propagation
@[expose] public sectionnamespace Geb.BitTree.BinaryMachineopen Turing MultiTapeTMResetting an initial sequence of ones preserves the carry state and advances both heads.
theorem configs_carry_prefix {input : List (Fin 4)}
(cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool) (p k : ℕ)
(hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork))
(hp0 : cfg.workTapePos 0 = p) (hp1 : cfg.workTapePos 1 = p)
(hones : ∀ j < k, digits cfg (if leaf then 1 else 0) (p + j) = true)
(t : ℕ) (ht : t ≤ k) :
let now := machine.configs cfg t
now.state = some (if leaf then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = (p + t : ℕ) ∧ now.workTapePos 1 = (p + t : ℕ) ∧
now.inputPos = cfg.inputPos ∧
digits now (if leaf then 1 else 0) =
(fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf then 1 else 0) j) ∧
digits now (if leaf then 0 else 1) = digits cfg (if leaf then 0 else 1) := input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet:ℕht:t ≤ k⊢ let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet:ℕ⊢ t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet:ℕ⊢ Nat.zero ≤ k →
let now := configs cfg Nat.zero;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + Nat.zero) ∧
now.workTapePos 1 = ↑(p + Nat.zero) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + Nat.zero then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet:ℕ⊢ ∀ (n : ℕ),
(n ≤ k →
let now := configs cfg n;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + n) ∧
now.workTapePos 1 = ↑(p + n) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + n then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)) →
n.succ ≤ k →
let now := configs cfg n.succ;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + n.succ) ∧
now.workTapePos 1 = ↑(p + n.succ) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + n.succ then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet:ℕ⊢ Nat.zero ≤ k →
let now := configs cfg Nat.zero;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + Nat.zero) ∧
now.workTapePos 1 = ↑(p + Nat.zero) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + Nat.zero then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet:ℕa✝:Nat.zero ≤ k⊢ let now := configs cfg Nat.zero;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + Nat.zero) ∧
now.workTapePos 1 = ↑(p + Nat.zero) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + Nat.zero then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet:ℕa✝:Nat.zero ≤ k⊢ digits (configs cfg Nat.zero) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + Nat.zero then false else digits cfg (if leaf = true then 1 else 0) j
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet:ℕa✝:Nat.zero ≤ kj:ℕ⊢ digits (configs cfg Nat.zero) (if leaf = true then 1 else 0) j =
if p ≤ j ∧ j < p + Nat.zero then false else digits cfg (if leaf = true then 1 else 0) j
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet:ℕa✝:Nat.zero ≤ kj:ℕhj:¬(p ≤ j ∧ j < p + 0)⊢ digits (configs cfg Nat.zero) (if leaf = true then 1 else 0) j =
if p ≤ j ∧ j < p + Nat.zero then false else digits cfg (if leaf = true then 1 else 0) j
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet:ℕ⊢ ∀ (n : ℕ),
(n ≤ k →
let now := configs cfg n;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + n) ∧
now.workTapePos 1 = ↑(p + n) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + n then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)) →
n.succ ≤ k →
let now := configs cfg n.succ;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + n.succ) ∧
now.workTapePos 1 = ↑(p + n.succ) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + n.succ then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ k⊢ let now := configs cfg t.succ;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t.succ) ∧
now.workTapePos 1 = ↑(p + t.succ) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ let now := configs cfg t.succ;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t.succ) ∧
now.workTapePos 1 = ↑(p + t.succ) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg t⊢ let now := configs cfg t.succ;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t.succ) ∧
now.workTapePos 1 = ↑(p + t.succ) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)⊢ let now := configs cfg t.succ;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t.succ) ∧
now.workTapePos 1 = ↑(p + t.succ) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = true⊢ let now := configs cfg t.succ;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t.succ) ∧
now.workTapePos 1 = ↑(p + t.succ) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ let now := configs cfg t.succ;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t.succ) ∧
now.workTapePos 1 = ↑(p + t.succ) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ let now := MultiTapeTM.step (configs cfg t);
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t.succ) ∧
now.workTapePos 1 = ↑(p + t.succ) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ (MultiTapeTM.step (configs cfg t)).state = some (if leaf = true then stCarryLeaf else stCarryFork)input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ (MultiTapeTM.step (configs cfg t)).workTapePos 0 = ↑(p + t.succ)input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ (MultiTapeTM.step (configs cfg t)).workTapePos 1 = ↑(p + t.succ)input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ (MultiTapeTM.step (configs cfg t)).inputPos = cfg.inputPosinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ digits (MultiTapeTM.step (configs cfg t)) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) jinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ digits (MultiTapeTM.step (configs cfg t)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ (MultiTapeTM.step (configs cfg t)).state = some (if leaf = true then stCarryLeaf else stCarryFork) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ some (if true = true then if leaf = true then stCarryLeaf else stCarryFork else stReturn) =
some (if leaf = true then stCarryLeaf else stCarryFork)
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ (MultiTapeTM.step (configs cfg t)).workTapePos 0 = ↑(p + t.succ) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ ↑(p + t) + 1 = ↑(p + t.succ)
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ (MultiTapeTM.step (configs cfg t)).workTapePos 1 = ↑(p + t.succ) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ ↑(p + t) + 1 = ↑(p + t.succ)
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ (MultiTapeTM.step (configs cfg t)).inputPos = cfg.inputPos All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ digits (MultiTapeTM.step (configs cfg t)) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) j input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ (Function.update (fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) (p + t)
!(fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) (p + t)) =
fun j ↦ if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) j
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = truej:ℕ⊢ Function.update (fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) (p + t)
(!(fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) (p + t)) j =
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) j
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = truej:ℕhj:j = p + t⊢ Function.update (fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) (p + t)
(!(fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) (p + t)) j =
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) jinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = truej:ℕhj:¬j = p + t⊢ Function.update (fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) (p + t)
(!(fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) (p + t)) j =
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) j
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = truej:ℕhj:j = p + t⊢ Function.update (fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) (p + t)
(!(fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) (p + t)) j =
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) j input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ Function.update (fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) (p + t)
(!(fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) (p + t)) (p + t) =
if p ≤ p + t ∧ p + t < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) (p + t)
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = truej:ℕhj:¬j = p + t⊢ Function.update (fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) (p + t)
(!(fun j ↦ if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) (p + t)) j =
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) j input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = truej:ℕhj:¬j = p + t⊢ (if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) =
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) j
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = truej:ℕhj:¬j = p + the:p ≤ j ∧ j < p + t ↔ p ≤ j ∧ j < p + (t + 1)⊢ (if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) =
if p ≤ j ∧ j < p + t.succ then false else digits cfg (if leaf = true then 1 else 0) j
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet✝:ℕt:ℕih:t ≤ k →
let now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(p + t) ∧
now.workTapePos 1 = ↑(p + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)ht:t.succ ≤ khstate:(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg t).workTapePos 0 = ↑(p + t)hpos1:(configs cfg t).workTapePos 1 = ↑(p + t)hin:(configs cfg t).inputPos = cfg.inputPoshselected:digits (configs cfg t) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + t then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg t) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg thp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + t)hone:digits cfg (if leaf = true then 1 else 0) (p + t) = truehd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = true⊢ digits (MultiTapeTM.step (configs cfg t)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) All goals completed! 🐙The first zero ends carry propagation after being changed to one.
theorem configs_carry_terminal {input : List (Fin 4)}
(cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool) (p k : ℕ)
(hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork))
(hp0 : cfg.workTapePos 0 = p) (hp1 : cfg.workTapePos 1 = p)
(hones : ∀ j < k, digits cfg (if leaf then 1 else 0) (p + j) = true)
(hzero : digits cfg (if leaf then 1 else 0) (p + k) = false) :
let now := machine.configs cfg (k + 1)
now.state = some stReturn ∧
now.workTapePos 0 = (p + (k + 1) : ℕ) ∧
now.workTapePos 1 = (p + (k + 1) : ℕ) ∧ now.inputPos = cfg.inputPos ∧
digits now (if leaf then 1 else 0) =
(fun j ↦ if j = p + k then true else
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf then 1 else 0) j) ∧
digits now (if leaf then 0 else 1) = digits cfg (if leaf then 0 else 1) := input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = false⊢ let now := configs cfg (k + 1);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(p + (k + 1)) ∧
now.workTapePos 1 = ↑(p + (k + 1)) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if j = p + k then true
else if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ let now := configs cfg (k + 1);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(p + (k + 1)) ∧
now.workTapePos 1 = ↑(p + (k + 1)) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if j = p + k then true
else if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg k⊢ let now := configs cfg (k + 1);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(p + (k + 1)) ∧
now.workTapePos 1 = ↑(p + (k + 1)) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if j = p + k then true
else if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)⊢ let now := configs cfg (k + 1);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(p + (k + 1)) ∧
now.workTapePos 1 = ↑(p + (k + 1)) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if j = p + k then true
else if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ let now := configs cfg (k + 1);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(p + (k + 1)) ∧
now.workTapePos 1 = ↑(p + (k + 1)) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if j = p + k then true
else if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ let now := MultiTapeTM.step (configs cfg k);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(p + (k + 1)) ∧
now.workTapePos 1 = ↑(p + (k + 1)) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if j = p + k then true
else if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ (MultiTapeTM.step (configs cfg k)).state = some stReturninput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ (MultiTapeTM.step (configs cfg k)).workTapePos 0 = ↑(p + (k + 1))input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ (MultiTapeTM.step (configs cfg k)).workTapePos 1 = ↑(p + (k + 1))input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ (MultiTapeTM.step (configs cfg k)).inputPos = cfg.inputPosinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ digits (MultiTapeTM.step (configs cfg k)) (if leaf = true then 1 else 0) = fun j ↦
if j = p + k then true else if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ digits (MultiTapeTM.step (configs cfg k)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ (MultiTapeTM.step (configs cfg k)).state = some stReturn input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ some (if false = true then if leaf = true then stCarryLeaf else stCarryFork else stReturn) = some stReturn
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ (MultiTapeTM.step (configs cfg k)).workTapePos 0 = ↑(p + (k + 1)) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ ↑(p + k) + 1 = ↑(p + (k + 1))
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ (MultiTapeTM.step (configs cfg k)).workTapePos 1 = ↑(p + (k + 1)) input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ ↑(p + k) + 1 = ↑(p + (k + 1))
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ (MultiTapeTM.step (configs cfg k)).inputPos = cfg.inputPos All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ digits (MultiTapeTM.step (configs cfg k)) (if leaf = true then 1 else 0) = fun j ↦
if j = p + k then true else if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ (Function.update (fun j ↦ if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) (p + k)
!(fun j ↦ if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) (p + k)) =
fun j ↦ if j = p + k then true else if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = falsej:ℕ⊢ Function.update (fun j ↦ if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) (p + k)
(!(fun j ↦ if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) (p + k)) j =
if j = p + k then true else if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = falsej:ℕhj:j = p + k⊢ Function.update (fun j ↦ if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) (p + k)
(!(fun j ↦ if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) (p + k)) j =
if j = p + k then true else if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = falsej:ℕhj:¬j = p + k⊢ Function.update (fun j ↦ if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) (p + k)
(!(fun j ↦ if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) (p + k)) j =
if j = p + k then true else if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = falsej:ℕhj:j = p + k⊢ Function.update (fun j ↦ if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) (p + k)
(!(fun j ↦ if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) (p + k)) j =
if j = p + k then true else if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ Function.update (fun j ↦ if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) (p + k)
(!(fun j ↦ if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) (p + k)) (p + k) =
if p + k = p + k then true
else if p ≤ p + k ∧ p + k < p + k then false else digits cfg (if leaf = true then 1 else 0) (p + k)
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = falsej:ℕhj:¬j = p + k⊢ Function.update (fun j ↦ if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) (p + k)
(!(fun j ↦ if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j) (p + k)) j =
if j = p + k then true else if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) j All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (p + k) = falsehstate:(configs cfg k).state = some (if leaf = true then stCarryLeaf else stCarryFork)hpos0:(configs cfg k).workTapePos 0 = ↑(p + k)hpos1:(configs cfg k).workTapePos 1 = ↑(p + k)hin:(configs cfg k).inputPos = cfg.inputPoshselected:digits (configs cfg k) (if leaf = true then 1 else 0) = fun j ↦
if p ≤ j ∧ j < p + k then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg k) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)now:Cfg 3 (Fin 4) (Fin 10) input := configs cfg khp:now.workTapePos (if leaf = true then 1 else 0) = ↑(p + k)hd:digit (now.workTapeSymbols (if leaf = true then 1 else 0)) = false⊢ digits (MultiTapeTM.step (configs cfg k)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) All goals completed! 🐙Carry propagation emits nothing, including the step that ends the carry.
theorem outputString_carry {input : List (Fin 4)}
(cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool) (p k : ℕ)
(hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork))
(hp0 : cfg.workTapePos 0 = p) (hp1 : cfg.workTapePos 1 = p)
(hones : ∀ j < k, digits cfg (if leaf then 1 else 0) (p + j) = true) :
machine.outputString cfg (k + 1) = [] := input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = true⊢ machine.outputString cfg (k + 1) = []
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = true⊢ ∀ x ∈ List.range (k + 1), (outputSymbol (configs cfg x)).toList = []
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet:ℕht:t ∈ List.range (k + 1)⊢ (outputSymbol (configs cfg t)).toList = []
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet:ℕht:t ∈ List.range (k + 1)hq':(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ (outputSymbol (configs cfg t)).toList = []
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolp:ℕk:ℕhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = ↑php1:cfg.workTapePos 1 = ↑phones:∀ j < k, digits cfg (if leaf = true then 1 else 0) (p + j) = truet:ℕht:t ∈ List.range (k + 1)hq':(configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork)⊢ none.toList = []
All goals completed! 🐙Carry from the origin implements binary-list increment in exactly its bit-change count.
theorem configs_carry_bits {input : List (Fin 4)}
(cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool) (bs : List Bool)
(hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork))
(hp0 : cfg.workTapePos 0 = 0) (hp1 : cfg.workTapePos 1 = 0)
(hbits : ∀ j, digits cfg (if leaf then 1 else 0) j = bs[j]?.getD false) :
let now := machine.configs cfg (Counter.flips bs)
now.state = some stReturn ∧
now.workTapePos 0 = Counter.flips bs ∧ now.workTapePos 1 = Counter.flips bs ∧
now.inputPos = cfg.inputPos ∧
digits now (if leaf then 1 else 0) = (fun j ↦ (Counter.increment bs)[j]?.getD false) ∧
digits now (if leaf then 0 else 1) = digits cfg (if leaf then 0 else 1) ∧
machine.outputString cfg (Counter.flips bs) = [] := input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD false⊢ let now := configs cfg (Counter.flips bs);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(Counter.flips bs) ∧
now.workTapePos 1 = ↑(Counter.flips bs) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment bs)[j]?.getD false) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧
machine.outputString cfg (Counter.flips bs) = []
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bs⊢ let now := configs cfg (Counter.flips bs);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(Counter.flips bs) ∧
now.workTapePos 1 = ↑(Counter.flips bs) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment bs)[j]?.getD false) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧
machine.outputString cfg (Counter.flips bs) = []
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bs⊢ let now := configs cfg (Counter.flips bs);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(Counter.flips bs) ∧
now.workTapePos 1 = ↑(Counter.flips bs) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment bs)[j]?.getD false) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧
machine.outputString cfg (Counter.flips bs) = []
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = true⊢ let now := configs cfg (Counter.flips bs);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(Counter.flips bs) ∧
now.workTapePos 1 = ↑(Counter.flips bs) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment bs)[j]?.getD false) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧
machine.outputString cfg (Counter.flips bs) = []
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = false⊢ let now := configs cfg (Counter.flips bs);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(Counter.flips bs) ∧
now.workTapePos 1 = ↑(Counter.flips bs) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment bs)[j]?.getD false) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧
machine.outputString cfg (Counter.flips bs) = []
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehterm:have now := configs cfg (Counter.flips bs - 1 + 1);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(0 + (Counter.flips bs - 1 + 1)) ∧
now.workTapePos 1 = ↑(0 + (Counter.flips bs - 1 + 1)) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if j = 0 + (Counter.flips bs - 1) then true
else
if 0 ≤ j ∧ j < 0 + (Counter.flips bs - 1) then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ let now := configs cfg (Counter.flips bs);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(Counter.flips bs) ∧
now.workTapePos 1 = ↑(Counter.flips bs) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment bs)[j]?.getD false) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧
machine.outputString cfg (Counter.flips bs) = []
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehterm:(configs cfg (Counter.flips bs)).state = some stReturn ∧
(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs) ∧
(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs) ∧
(configs cfg (Counter.flips bs)).inputPos = cfg.inputPos ∧
(digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) =
digits cfg (if leaf = true then 0 else 1)⊢ let now := configs cfg (Counter.flips bs);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(Counter.flips bs) ∧
now.workTapePos 1 = ↑(Counter.flips bs) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment bs)[j]?.getD false) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧
machine.outputString cfg (Counter.flips bs) = []
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ let now := configs cfg (Counter.flips bs);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(Counter.flips bs) ∧
now.workTapePos 1 = ↑(Counter.flips bs) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment bs)[j]?.getD false) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧
machine.outputString cfg (Counter.flips bs) = []
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment bs)[j]?.getD falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ machine.outputString cfg (Counter.flips bs) = []
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment bs)[j]?.getD false input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕ⊢ digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) j = (Counter.increment bs)[j]?.getD false
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕ⊢ (fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) j)
j =
if j + 1 < Counter.flips bs then false else if j + 1 = Counter.flips bs then true else bs[j]?.getD false
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕ⊢ (if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) j) =
if j + 1 < Counter.flips bs then false else if j + 1 = Counter.flips bs then true else bs[j]?.getD false
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕ⊢ (if j = Counter.flips bs - 1 then true else if j < Counter.flips bs - 1 then false else bs[j]?.getD false) =
if j + 1 < Counter.flips bs then false else if j + 1 = Counter.flips bs then true else bs[j]?.getD false
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝¹:j = Counter.flips bs - 1h✝:j + 1 < Counter.flips bs⊢ Falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝²:j = Counter.flips bs - 1h✝¹:¬j + 1 < Counter.flips bsh✝:j + 1 = Counter.flips bs⊢ true = trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝²:j = Counter.flips bs - 1h✝¹:¬j + 1 < Counter.flips bsh✝:¬j + 1 = Counter.flips bs⊢ true = bs[j]?.getD falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝²:¬j = Counter.flips bs - 1h✝¹:j < Counter.flips bs - 1h✝:j + 1 < Counter.flips bs⊢ false = falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝³:¬j = Counter.flips bs - 1h✝²:j < Counter.flips bs - 1h✝¹:¬j + 1 < Counter.flips bsh✝:j + 1 = Counter.flips bs⊢ Falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝³:¬j = Counter.flips bs - 1h✝²:j < Counter.flips bs - 1h✝¹:¬j + 1 < Counter.flips bsh✝:¬j + 1 = Counter.flips bs⊢ false = bs[j]?.getD falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝²:¬j = Counter.flips bs - 1h✝¹:¬j < Counter.flips bs - 1h✝:j + 1 < Counter.flips bs⊢ bs[j]?.getD false = falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝³:¬j = Counter.flips bs - 1h✝²:¬j < Counter.flips bs - 1h✝¹:¬j + 1 < Counter.flips bsh✝:j + 1 = Counter.flips bs⊢ bs[j]?.getD false = trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝³:¬j = Counter.flips bs - 1h✝²:¬j < Counter.flips bs - 1h✝¹:¬j + 1 < Counter.flips bsh✝:¬j + 1 = Counter.flips bs⊢ bs[j]?.getD false = bs[j]?.getD false input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝¹:j = Counter.flips bs - 1h✝:j + 1 < Counter.flips bs⊢ Falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝²:j = Counter.flips bs - 1h✝¹:¬j + 1 < Counter.flips bsh✝:j + 1 = Counter.flips bs⊢ true = trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝²:j = Counter.flips bs - 1h✝¹:¬j + 1 < Counter.flips bsh✝:¬j + 1 = Counter.flips bs⊢ true = bs[j]?.getD falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝²:¬j = Counter.flips bs - 1h✝¹:j < Counter.flips bs - 1h✝:j + 1 < Counter.flips bs⊢ false = falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝³:¬j = Counter.flips bs - 1h✝²:j < Counter.flips bs - 1h✝¹:¬j + 1 < Counter.flips bsh✝:j + 1 = Counter.flips bs⊢ Falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝³:¬j = Counter.flips bs - 1h✝²:j < Counter.flips bs - 1h✝¹:¬j + 1 < Counter.flips bsh✝:¬j + 1 = Counter.flips bs⊢ false = bs[j]?.getD falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝²:¬j = Counter.flips bs - 1h✝¹:¬j < Counter.flips bs - 1h✝:j + 1 < Counter.flips bs⊢ bs[j]?.getD false = falseinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝³:¬j = Counter.flips bs - 1h✝²:¬j < Counter.flips bs - 1h✝¹:¬j + 1 < Counter.flips bsh✝:j + 1 = Counter.flips bs⊢ bs[j]?.getD false = trueinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)j:ℕh✝³:¬j = Counter.flips bs - 1h✝²:¬j < Counter.flips bs - 1h✝¹:¬j + 1 < Counter.flips bsh✝:¬j + 1 = Counter.flips bs⊢ bs[j]?.getD false = bs[j]?.getD false first | All goals completed! 🐙 | All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ machine.outputString cfg (Counter.flips bs) = [] input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falsehf:0 < Counter.flips bshe:Counter.flips bs - 1 + 1 = Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = truehzero:digits cfg (if leaf = true then 1 else 0) (0 + (Counter.flips bs - 1)) = falsehstate:(configs cfg (Counter.flips bs)).state = some stReturnhpos0:(configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs)hpos1:(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)hin:(configs cfg (Counter.flips bs)).inputPos = cfg.inputPoshselected:digits (configs cfg (Counter.flips bs)) (if leaf = true then 1 else 0) = fun j ↦
if j = Counter.flips bs - 1 then true
else if j < Counter.flips bs - 1 then false else digits cfg (if leaf = true then 1 else 0) jhother:digits (configs cfg (Counter.flips bs)) (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)hout:machine.outputString cfg (Counter.flips bs - 1 + 1) = []⊢ machine.outputString cfg (Counter.flips bs) = []
All goals completed! 🐙Every configuration before the final carry step remains in the carry state.
theorem configs_carry_bits_state {input : List (Fin 4)}
(cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool) (bs : List Bool)
(hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork))
(hp0 : cfg.workTapePos 0 = 0) (hp1 : cfg.workTapePos 1 = 0)
(hbits : ∀ j, digits cfg (if leaf then 1 else 0) j = bs[j]?.getD false)
(t : ℕ) (ht : t < Counter.flips bs) :
(machine.configs cfg t).state = some (if leaf then stCarryLeaf else stCarryFork) ∧
(machine.configs cfg t).workTapePos 0 = t ∧
(machine.configs cfg t).workTapePos 1 = t := input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falset:ℕht:t < Counter.flips bs⊢ (configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
(configs cfg t).workTapePos 0 = ↑t ∧ (configs cfg t).workTapePos 1 = ↑t
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falset:ℕht:t < Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = true⊢ (configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
(configs cfg t).workTapePos 0 = ↑t ∧ (configs cfg t).workTapePos 1 = ↑t
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falset:ℕht:t < Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = trueh:have now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(0 + t) ∧
now.workTapePos 1 = ↑(0 + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if 0 ≤ j ∧ j < 0 + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ (configs cfg t).state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
(configs cfg t).workTapePos 0 = ↑t ∧ (configs cfg t).workTapePos 1 = ↑t
exact ⟨h.1, input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falset:ℕht:t < Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = trueh:have now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(0 + t) ∧
now.workTapePos 1 = ↑(0 + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if 0 ≤ j ∧ j < 0 + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ (configs cfg t).workTapePos 0 = ↑t All goals completed! 🐙,
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falset:ℕht:t < Counter.flips bshones:∀ j < Counter.flips bs - 1, digits cfg (if leaf = true then 1 else 0) (0 + j) = trueh:have now := configs cfg t;
now.state = some (if leaf = true then stCarryLeaf else stCarryFork) ∧
now.workTapePos 0 = ↑(0 + t) ∧
now.workTapePos 1 = ↑(0 + t) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦
if 0 ≤ j ∧ j < 0 + t then false else digits cfg (if leaf = true then 1 else 0) j) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1)⊢ (configs cfg t).workTapePos 1 = ↑t All goals completed! 🐙⟩The binary heads equal elapsed time throughout a carry, including its terminal state.
theorem configs_carry_bits_pos {input : List (Fin 4)}
(cfg : Cfg 3 (Fin 4) (Fin 10) input) (leaf : Bool) (bs : List Bool)
(hq : cfg.state = some (if leaf then stCarryLeaf else stCarryFork))
(hp0 : cfg.workTapePos 0 = 0) (hp1 : cfg.workTapePos 1 = 0)
(hbits : ∀ j, digits cfg (if leaf then 1 else 0) j = bs[j]?.getD false)
(t : ℕ) (ht : t ≤ Counter.flips bs) :
(machine.configs cfg t).workTapePos 0 = t ∧
(machine.configs cfg t).workTapePos 1 = t := input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falset:ℕht:t ≤ Counter.flips bs⊢ (configs cfg t).workTapePos 0 = ↑t ∧ (configs cfg t).workTapePos 1 = ↑t
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falset:ℕht:t ≤ Counter.flips bshe:t = Counter.flips bs⊢ (configs cfg t).workTapePos 0 = ↑t ∧ (configs cfg t).workTapePos 1 = ↑tinput:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falset:ℕht:t ≤ Counter.flips bshe:¬t = Counter.flips bs⊢ (configs cfg t).workTapePos 0 = ↑t ∧ (configs cfg t).workTapePos 1 = ↑t
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falset:ℕht:t ≤ Counter.flips bshe:t = Counter.flips bs⊢ (configs cfg t).workTapePos 0 = ↑t ∧ (configs cfg t).workTapePos 1 = ↑t input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falseht:Counter.flips bs ≤ Counter.flips bs⊢ (configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs) ∧
(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falseht:Counter.flips bs ≤ Counter.flips bsh:have now := configs cfg (Counter.flips bs);
now.state = some stReturn ∧
now.workTapePos 0 = ↑(Counter.flips bs) ∧
now.workTapePos 1 = ↑(Counter.flips bs) ∧
now.inputPos = cfg.inputPos ∧
(digits now (if leaf = true then 1 else 0) = fun j ↦ (Counter.increment bs)[j]?.getD false) ∧
digits now (if leaf = true then 0 else 1) = digits cfg (if leaf = true then 0 else 1) ∧
machine.outputString cfg (Counter.flips bs) = []⊢ (configs cfg (Counter.flips bs)).workTapePos 0 = ↑(Counter.flips bs) ∧
(configs cfg (Counter.flips bs)).workTapePos 1 = ↑(Counter.flips bs)
All goals completed! 🐙
input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falset:ℕht:t ≤ Counter.flips bshe:¬t = Counter.flips bs⊢ (configs cfg t).workTapePos 0 = ↑t ∧ (configs cfg t).workTapePos 1 = ↑t exact (configs_carry_bits_state cfg leaf bs hq hp0 hp1 hbits t (input:List (Fin 4)cfg:Cfg 3 (Fin 4) (Fin 10) inputleaf:Boolbs:List Boolhq:cfg.state = some (if leaf = true then stCarryLeaf else stCarryFork)hp0:cfg.workTapePos 0 = 0hp1:cfg.workTapePos 1 = 0hbits:∀ (j : ℕ), digits cfg (if leaf = true then 1 else 0) j = bs[j]?.getD falset:ℕht:t ≤ Counter.flips bshe:¬t = Counter.flips bs⊢ t < Counter.flips bs All goals completed! 🐙)).2end Geb.BitTree.BinaryMachine