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 Cslib.Computability.Machines.Turing.MultiTape.Deterministic public import Geb.Prototypes.Computability.TreeScanner.Machine

The tree scanner's transition, resolved

treeScanner.tr resolved at each configuration the machine reaches, one statement per case of its transition table, together with the input-symbol projections those resolutions consume and the emission facts they yield.

Turing.MultiTapeTM.step and Turing.MultiTapeTM.outputSymbol apply tm.tr q cfg.inputSymbol cfg.workTapeSymbols to identical arguments, so one resolution per case serves both a step lemma and the matching no-emission lemma, and the input symbol is resolved once rather than twice.

Main statements

    step_of_state — a step from a known state, in the form that names tr.

    seekCfg_inputSymbol, seekCfg_inputSymbol_end, sweepCfg_inputSymbol_succ, sweepCfg_inputSymbol_zero — the input symbol at each configuration.

    tr_seek_mid, tr_seek_exit, tr_plant, tr_live_leaf, tr_live_node_deep, tr_live_node_shallow, tr_live_end_accept, tr_live_end_reject, tr_dead_mid, tr_dead_end — the transition resolved at each case.

    outputSymbol_seekCfg, outputSymbol_plantCfg, outputSymbol_sweepCfg_succ — the configurations that emit nothing.

    seekCfg_step, configs_seek — the seek phase: one step against the closed form, and the configuration and the output at every step up to the input's length.

    seekCfg_exit, plantCfg_step — the two phase boundaries: the seek's exit step, which writes the first marker, and the planting step, which writes the second and enters the sweep.

    sweepCfg_step, configs_sweep — the sweep phase: one step against the closed form, matching the machine's state and work head to the scan's liveness and pending count one bit at a time, and the configuration and the output at every step down to the input's left end.

    sweepCfg_zero_halts, outputSymbol_sweepCfg_zero — the emitting step at the input's left end: the machine halts, and the symbol it emits is RankedAlphabet.Binary.binRanked.validBool at the input.

    halts_at, outputString_eq — the three phases composed: the machine halts after 2 * w.length + 3 steps having emitted that one symbol.

Implementation notes

The module is admitted to GebMeta.classicalAllowedModules. Its subject is the machine's behaviour under Turing.MultiTapeTM.step, Turing.MultiTapeTM.configs and Turing.MultiTapeTM.outputString, and its statements read the input through Turing.MultiTapeTM.Cfg.inputSymbol; each of those depends on Classical.choice through Cslib's Cfg.inputSymbol and inputSymbolInner, so nothing here can be stated choice-free.

treeScanner's transition is an ite chain on state equality against named definitions wrapping a match on Option (Fin 2). Unfolded the chain presents as if ⟨3, _⟩ = ⟨0, _⟩ then …, which no simp set resolves and rfl does, so each resolution rewrites its arguments to literals and closes by rfl. Where a case reads the work symbol, an equation collapsing the work tape to a constant function comes first: rewriting by sweepCfg_workTapeSymbols_eq alone leaves an ite on an opaque depth inside the argument of tr, and the transition does not reduce.

A resolution lemma takes no liveness hypothesis. tr receives the state as an explicit argument, so the resolution cannot consult liveness; the state is supplied by the caller from sweepCfg_state_live or sweepCfg_state_dead.

The sections group by kind up to the emission facts — InputSymbol, Transition, OutputSymbol — and by phase thereafter — Seek, Plant, Sweep, Emission.

Tags

Turing machine, transition, tree, preorder encoding

@[expose] public sectionnamespace Geb.TreeScanneropen Turing MultiTapeTM RankedAlphabet.Binary

A machine's step from a known state, in the form that names tr.

theorem step_of_state {k : } {Symbol State : Type} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (q : State) (hq : cfg.state = some q) : tm.step cfg = { state := (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).q' inputPos := moveInputPos cfg.inputPos (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).inputMove workTapes := fun i match ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s workTapePos := fun i cfg.workTapePos i + ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions i).2 } := k:Symbol:TypeState:Typeinput:List Symboltm:MultiTapeTM k Symbol Statecfg:Cfg k Symbol State inputq:Statehq:cfg.state = some qstep cfg = { state := (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).q', inputPos := moveInputPos cfg.inputPos (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).inputMove, workTapes := fun i match (motive := Option (Option Symbol) Option Symbol) ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i cfg.workTapePos i + ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions i).2 } k:Symbol:TypeState:Typeinput:List Symboltm:MultiTapeTM k Symbol Statecfg:Cfg k Symbol State inputq:Statehq:cfg.state = some q(match cfg.state with | none => cfg | some q => match tm.tr q cfg.inputSymbol cfg.workTapeSymbols with | { inputMove := inputMove, workActions := workActions, outS := outS, q' := q' } => { state := q', inputPos := moveInputPos cfg.inputPos inputMove, workTapes := fun i match (motive := Option (Option Symbol) Option Symbol) (workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i cfg.workTapePos i + (workActions i).2 }) = { state := (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).q', inputPos := moveInputPos cfg.inputPos (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).inputMove, workTapes := fun i match (motive := Option (Option Symbol) Option Symbol) ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i cfg.workTapePos i + ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions i).2 } k:Symbol:TypeState:Typeinput:List Symboltm:MultiTapeTM k Symbol Statecfg:Cfg k Symbol State inputq:Statehq:cfg.state = some q(match some q with | none => cfg | some q => match tm.tr q cfg.inputSymbol cfg.workTapeSymbols with | { inputMove := inputMove, workActions := workActions, outS := outS, q' := q' } => { state := q', inputPos := moveInputPos cfg.inputPos inputMove, workTapes := fun i match (motive := Option (Option Symbol) Option Symbol) (workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i cfg.workTapePos i + (workActions i).2 }) = { state := (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).q', inputPos := moveInputPos cfg.inputPos (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).inputMove, workTapes := fun i match (motive := Option (Option Symbol) Option Symbol) ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s, workTapePos := fun i cfg.workTapePos i + ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions i).2 } All goals completed! 🐙
section InputSymbol

Short of the input's right end the seek configuration reads the bit at its own index.

theorem seekCfg_inputSymbol (w : List Bool) (t : ) (h : t < w.length) : (seekCfg w t (Nat.le_of_lt h)).inputSymbol = some (boolEmb w[t]) := w:List Boolt:h:t < w.length(seekCfg w t ).inputSymbol = some (boolEmb w[t]) w:List Boolt:h:t < w.lengthhi:(seekCfg w t ).inputSymbol = some (List.map (⇑boolEmb) w)[t](seekCfg w t ).inputSymbol = some (boolEmb w[t]) All goals completed! 🐙

At the input's right end the seek configuration reads blank. This takes Turing.MultiTapeTM.Cfg.inputSymbol's second guard, an equality at .

theorem seekCfg_inputSymbol_end (w : List Bool) : (seekCfg w w.length (Nat.le_refl _)).inputSymbol = none := w:List Bool(seekCfg w w.length ).inputSymbol = none w:List Boolhend:(seekCfg w w.length ).inputPos = (List.map (⇑boolEmb) w).length + 1(seekCfg w w.length ).inputSymbol = none w:List Boolhend:(seekCfg w w.length ).inputPos = (List.map (⇑boolEmb) w).length + 1(if h₁ : (seekCfg w w.length ).inputPos = 0 then none else if h₂ : (seekCfg w w.length ).inputPos = (List.map (⇑boolEmb) w).length + 1 then none else some (List.map (⇑boolEmb) w)[(seekCfg w w.length ).inputPos - 1]) = none w:List Boolhend:(seekCfg w w.length ).inputPos = (List.map (⇑boolEmb) w).length + 1h✝:(seekCfg w w.length ).inputPos = 0none = nonew:List Boolhend:(seekCfg w w.length ).inputPos = (List.map (⇑boolEmb) w).length + 1h✝:¬(seekCfg w w.length ).inputPos = 0none = none w:List Boolhend:(seekCfg w w.length ).inputPos = (List.map (⇑boolEmb) w).length + 1h✝:(seekCfg w w.length ).inputPos = 0none = nonew:List Boolhend:(seekCfg w w.length ).inputPos = (List.map (⇑boolEmb) w).length + 1h✝:¬(seekCfg w w.length ).inputPos = 0none = none All goals completed! 🐙

At a positive index the sweep configuration reads the bit one cell to the left of its index.

theorem sweepCfg_inputSymbol_succ (w : List Bool) (k : ) (h : k + 1 w.length) : (sweepCfg w (k + 1) h).inputSymbol = some (boolEmb w[k]) := w:List Boolk:h:k + 1 w.length(sweepCfg w (k + 1) h).inputSymbol = some (boolEmb w[k]) w:List Boolk:h:k + 1 w.lengthhi:(sweepCfg w (k + 1) h).inputSymbol = some (List.map (⇑boolEmb) w)[k](sweepCfg w (k + 1) h).inputSymbol = some (boolEmb w[k]) All goals completed! 🐙

At the input's left end the sweep configuration reads blank. This takes Turing.MultiTapeTM.Cfg.inputSymbol's first guard, an equality at Fin (n + 2).

theorem sweepCfg_inputSymbol_zero (w : List Bool) : (sweepCfg w 0 (Nat.zero_le _)).inputSymbol = none := w:List Bool(sweepCfg w 0 ).inputSymbol = none w:List Bool(if h₁ : (sweepCfg w 0 ).inputPos = 0 then none else if h₂ : (sweepCfg w 0 ).inputPos = (List.map (⇑boolEmb) w).length + 1 then none else some (List.map (⇑boolEmb) w)[(sweepCfg w 0 ).inputPos - 1]) = none w:List Boolh₁:(sweepCfg w 0 ).inputPos = 0none = nonew:List Boolh₁:¬(sweepCfg w 0 ).inputPos = 0h₂:(sweepCfg w 0 ).inputPos = (List.map (⇑boolEmb) w).length + 1none = nonew:List Boolh₁:¬(sweepCfg w 0 ).inputPos = 0h₂:¬(sweepCfg w 0 ).inputPos = (List.map (⇑boolEmb) w).length + 1False w:List Boolh₁:(sweepCfg w 0 ).inputPos = 0none = none All goals completed! 🐙 w:List Boolh₁:¬(sweepCfg w 0 ).inputPos = 0h₂:(sweepCfg w 0 ).inputPos = (List.map (⇑boolEmb) w).length + 1none = none All goals completed! 🐙 w:List Boolh₁:¬(sweepCfg w 0 ).inputPos = 0h₂:¬(sweepCfg w 0 ).inputPos = (List.map (⇑boolEmb) w).length + 1False All goals completed! 🐙
end InputSymbolsection Transition

Short of the input's right end the seek step advances the input head.

theorem tr_seek_mid (w : List Bool) (t : ) (h : t < w.length) : treeScanner.tr stSeek (seekCfg w t (Nat.le_of_lt h)).inputSymbol (seekCfg w t (Nat.le_of_lt h)).workTapeSymbols = { inputMove := 1, workActions := fun _ (none, 0), outS := none, q' := some stSeek } := w:List Boolt:h:t < w.lengthtreeScanner.tr stSeek (seekCfg w t ).inputSymbol (seekCfg w t ).workTapeSymbols = { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek } w:List Boolt:h:t < w.lengthtreeScanner.tr stSeek (some (boolEmb w[t])) (seekCfg w t ).workTapeSymbols = { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek } All goals completed! 🐙

At the input's right end the seek step writes the first marker and enters the planting state.

theorem tr_seek_exit (w : List Bool) : treeScanner.tr stSeek (seekCfg w w.length (Nat.le_refl _)).inputSymbol (seekCfg w w.length (Nat.le_refl _)).workTapeSymbols = { inputMove := -1, workActions := fun _ (some (some 0), 1), outS := none, q' := some stPlant } := w:List BooltreeScanner.tr stSeek (seekCfg w w.length ).inputSymbol (seekCfg w w.length ).workTapeSymbols = { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant } w:List BooltreeScanner.tr stSeek none (seekCfg w w.length ).workTapeSymbols = { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant } All goals completed! 🐙

The planting step writes the second marker at cell 1, returns the work head to cell 0 and enters the live state. It is uniform in the input symbol: its row of the transition table is a catch-all in the input column.

theorem tr_plant (w : List Bool) : treeScanner.tr stPlant (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols = { inputMove := 0, workActions := fun _ (some (some 1), -1), outS := none, q' := some stLive } := rfl

A live sweep over a leaf bit raises the pending count by one, moving the work head right.

theorem tr_live_leaf (w : List Bool) (k : ) (h : k + 1 w.length) (hbit : w[k] = false) : treeScanner.tr stLive (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun _ (none, 1), outS := none, q' := some stLive } := w:List Boolk:h:k + 1 w.lengthhbit:w[k] = falsetreeScanner.tr stLive (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive } w:List Boolk:h:k + 1 w.lengthhbit:w[k] = falsetreeScanner.tr stLive (some (boolEmb false)) (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive } All goals completed! 🐙

A live sweep over a node bit with at least two pending consumes two and pushes one, so it stays live and lowers the pending count by one, moving the work head left.

theorem tr_live_node_deep (w : List Bool) (k : ) (h : k + 1 w.length) (hbit : w[k] = true) (hd : 2 depth (w.drop (k + 1))) : treeScanner.tr stLive (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun _ (none, -1), outS := none, q' := some stLive } := w:List Boolk:h:k + 1 w.lengthhbit:w[k] = truehd:2 depth (List.drop (k + 1) w)treeScanner.tr stLive (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive } w:List Boolk:h:k + 1 w.lengthhbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hw:(sweepCfg w (k + 1) h).workTapeSymbols = fun x nonetreeScanner.tr stLive (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive } w:List Boolk:h:k + 1 w.lengthhbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hw:(sweepCfg w (k + 1) h).workTapeSymbols = fun x none(treeScanner.tr stLive (some (boolEmb true)) fun x none) = { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive } All goals completed! 🐙

A live sweep over a node bit with fewer than two pending has met a node with too few subterms to its right, and dies.

theorem tr_live_node_shallow (w : List Bool) (k : ) (h : k + 1 w.length) (hbit : w[k] = true) (hd : depth (w.drop (k + 1)) < 2) : treeScanner.tr stLive (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun _ (none, 0), outS := none, q' := some stDead } := w:List Boolk:h:k + 1 w.lengthhbit:w[k] = truehd:depth (List.drop (k + 1) w) < 2treeScanner.tr stLive (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead } w:List Boolk:h:k + 1 w.lengthhbit:w[k] = truehd:depth (List.drop (k + 1) w) < 2treeScanner.tr stLive (some (boolEmb true)) (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead } w:List Boolk:h:k + 1 w.lengthhbit:w[k] = truehd:depth (List.drop (k + 1) w) < 2hd0:depth (List.drop (k + 1) w) = 0treeScanner.tr stLive (some (boolEmb true)) (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }w:List Boolk:h:k + 1 w.lengthhbit:w[k] = truehd:depth (List.drop (k + 1) w) < 2hd0:¬depth (List.drop (k + 1) w) = 0treeScanner.tr stLive (some (boolEmb true)) (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead } w:List Boolk:h:k + 1 w.lengthhbit:w[k] = truehd:depth (List.drop (k + 1) w) < 2hd0:depth (List.drop (k + 1) w) = 0treeScanner.tr stLive (some (boolEmb true)) (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead } w:List Boolk:h:k + 1 w.lengthhbit:w[k] = truehd:depth (List.drop (k + 1) w) < 2hd0:depth (List.drop (k + 1) w) = 0hw:(sweepCfg w (k + 1) h).workTapeSymbols = fun x some 0treeScanner.tr stLive (some (boolEmb true)) (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead } w:List Boolk:h:k + 1 w.lengthhbit:w[k] = truehd:depth (List.drop (k + 1) w) < 2hd0:depth (List.drop (k + 1) w) = 0hw:(sweepCfg w (k + 1) h).workTapeSymbols = fun x some 0(treeScanner.tr stLive (some (boolEmb true)) fun x some 0) = { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead } All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhbit:w[k] = truehd:depth (List.drop (k + 1) w) < 2hd0:¬depth (List.drop (k + 1) w) = 0treeScanner.tr stLive (some (boolEmb true)) (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead } w:List Boolk:h:k + 1 w.lengthhbit:w[k] = truehd:depth (List.drop (k + 1) w) < 2hd0:¬depth (List.drop (k + 1) w) = 0hw:(sweepCfg w (k + 1) h).workTapeSymbols = fun x some 1treeScanner.tr stLive (some (boolEmb true)) (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead } w:List Boolk:h:k + 1 w.lengthhbit:w[k] = truehd:depth (List.drop (k + 1) w) < 2hd0:¬depth (List.drop (k + 1) w) = 0hw:(sweepCfg w (k + 1) h).workTapeSymbols = fun x some 1(treeScanner.tr stLive (some (boolEmb true)) fun x some 1) = { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead } All goals completed! 🐙

A live sweep at the input's left end with exactly one pending emits acceptance and halts.

theorem tr_live_end_accept (w : List Bool) (hd : depth w = 1) : treeScanner.tr stLive (sweepCfg w 0 (Nat.zero_le _)).inputSymbol (sweepCfg w 0 (Nat.zero_le _)).workTapeSymbols = { inputMove := 0, workActions := fun _ (none, 0), outS := some 1, q' := none } := w:List Boolhd:depth w = 1treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols = { inputMove := 0, workActions := fun x (none, 0), outS := some 1, q' := none } w:List Boolhd:depth w = 1hw:(sweepCfg w 0 ).workTapeSymbols = fun x some 1treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols = { inputMove := 0, workActions := fun x (none, 0), outS := some 1, q' := none } w:List Boolhd:depth w = 1hw:(sweepCfg w 0 ).workTapeSymbols = fun x some 1(treeScanner.tr stLive none fun x some 1) = { inputMove := 0, workActions := fun x (none, 0), outS := some 1, q' := none } All goals completed! 🐙

A live sweep at the input's left end with a pending count other than one emits rejection and halts.

theorem tr_live_end_reject (w : List Bool) (hd : depth w 1) : treeScanner.tr stLive (sweepCfg w 0 (Nat.zero_le _)).inputSymbol (sweepCfg w 0 (Nat.zero_le _)).workTapeSymbols = { inputMove := 0, workActions := fun _ (none, 0), outS := some 0, q' := none } := w:List Boolhd:depth w 1treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols = { inputMove := 0, workActions := fun x (none, 0), outS := some 0, q' := none } w:List Boolhd:depth w 1treeScanner.tr stLive none (sweepCfg w 0 ).workTapeSymbols = { inputMove := 0, workActions := fun x (none, 0), outS := some 0, q' := none } w:List Boolhd:depth w 1hd0:depth w = 0treeScanner.tr stLive none (sweepCfg w 0 ).workTapeSymbols = { inputMove := 0, workActions := fun x (none, 0), outS := some 0, q' := none }w:List Boolhd:depth w 1hd0:¬depth w = 0treeScanner.tr stLive none (sweepCfg w 0 ).workTapeSymbols = { inputMove := 0, workActions := fun x (none, 0), outS := some 0, q' := none } w:List Boolhd:depth w 1hd0:depth w = 0treeScanner.tr stLive none (sweepCfg w 0 ).workTapeSymbols = { inputMove := 0, workActions := fun x (none, 0), outS := some 0, q' := none } w:List Boolhd:depth w 1hd0:depth w = 0hw:(sweepCfg w 0 ).workTapeSymbols = fun x some 0treeScanner.tr stLive none (sweepCfg w 0 ).workTapeSymbols = { inputMove := 0, workActions := fun x (none, 0), outS := some 0, q' := none } w:List Boolhd:depth w 1hd0:depth w = 0hw:(sweepCfg w 0 ).workTapeSymbols = fun x some 0(treeScanner.tr stLive none fun x some 0) = { inputMove := 0, workActions := fun x (none, 0), outS := some 0, q' := none } All goals completed! 🐙 w:List Boolhd:depth w 1hd0:¬depth w = 0treeScanner.tr stLive none (sweepCfg w 0 ).workTapeSymbols = { inputMove := 0, workActions := fun x (none, 0), outS := some 0, q' := none } w:List Boolhd:depth w 1hd0:¬depth w = 0hw:(sweepCfg w 0 ).workTapeSymbols = fun x nonetreeScanner.tr stLive none (sweepCfg w 0 ).workTapeSymbols = { inputMove := 0, workActions := fun x (none, 0), outS := some 0, q' := none } w:List Boolhd:depth w 1hd0:¬depth w = 0hw:(sweepCfg w 0 ).workTapeSymbols = fun x none(treeScanner.tr stLive none fun x none) = { inputMove := 0, workActions := fun x (none, 0), outS := some 0, q' := none } All goals completed! 🐙

A dead sweep short of the input's left end walks on unchanged.

theorem tr_dead_mid (w : List Bool) (k : ) (h : k + 1 w.length) : treeScanner.tr stDead (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun _ (none, 0), outS := none, q' := some stDead } := w:List Boolk:h:k + 1 w.lengthtreeScanner.tr stDead (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead } w:List Boolk:h:k + 1 w.lengthtreeScanner.tr stDead (some (boolEmb w[k])) (sweepCfg w (k + 1) h).workTapeSymbols = { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead } All goals completed! 🐙

A dead sweep at the input's left end emits rejection and halts.

theorem tr_dead_end (w : List Bool) : treeScanner.tr stDead (sweepCfg w 0 (Nat.zero_le _)).inputSymbol (sweepCfg w 0 (Nat.zero_le _)).workTapeSymbols = { inputMove := 0, workActions := fun _ (none, 0), outS := some 0, q' := none } := w:List BooltreeScanner.tr stDead (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols = { inputMove := 0, workActions := fun x (none, 0), outS := some 0, q' := none } w:List BooltreeScanner.tr stDead none (sweepCfg w 0 ).workTapeSymbols = { inputMove := 0, workActions := fun x (none, 0), outS := some 0, q' := none } All goals completed! 🐙
end Transitionsection OutputSymbol

The seek phase emits nothing, at its exit step as at every other.

theorem outputSymbol_seekCfg (w : List Bool) (t : ) (h : t w.length) : treeScanner.outputSymbol (seekCfg w t h) = none := w:List Boolt:h:t w.lengthoutputSymbol (seekCfg w t h) = none w:List Boolt:h:t w.length(match (seekCfg w t h).state with | none => none | some q => (treeScanner.tr q (seekCfg w t h).inputSymbol (seekCfg w t h).workTapeSymbols).outS) = none w:List Boolt:h:t w.length(treeScanner.tr stSeek (seekCfg w t h).inputSymbol (seekCfg w t h).workTapeSymbols).outS = none w:List Boolt:h:t w.lengthht:t = w.length(treeScanner.tr stSeek (seekCfg w t h).inputSymbol (seekCfg w t h).workTapeSymbols).outS = nonew:List Boolt:h:t w.lengthht:¬t = w.length(treeScanner.tr stSeek (seekCfg w t h).inputSymbol (seekCfg w t h).workTapeSymbols).outS = none w:List Boolt:h:t w.lengthht:t = w.length(treeScanner.tr stSeek (seekCfg w t h).inputSymbol (seekCfg w t h).workTapeSymbols).outS = none w:List Boolh:w.length w.length(treeScanner.tr stSeek (seekCfg w w.length h).inputSymbol (seekCfg w w.length h).workTapeSymbols).outS = none All goals completed! 🐙 w:List Boolt:h:t w.lengthht:¬t = w.length(treeScanner.tr stSeek (seekCfg w t h).inputSymbol (seekCfg w t h).workTapeSymbols).outS = none All goals completed! 🐙

The planting step emits nothing.

theorem outputSymbol_plantCfg (w : List Bool) : treeScanner.outputSymbol (plantCfg w) = none := w:List BooloutputSymbol (plantCfg w) = none w:List Bool(match (plantCfg w).state with | none => none | some q => (treeScanner.tr q (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).outS) = none w:List Bool(treeScanner.tr stPlant (plantCfg w).inputSymbol (plantCfg w).workTapeSymbols).outS = none All goals completed! 🐙

The sweep emits nothing short of the input's left end, live or dead.

theorem outputSymbol_sweepCfg_succ (w : List Bool) (k : ) (h : k + 1 w.length) : treeScanner.outputSymbol (sweepCfg w (k + 1) h) = none := w:List Boolk:h:k + 1 w.lengthoutputSymbol (sweepCfg w (k + 1) h) = none w:List Boolk:h:k + 1 w.length(match (sweepCfg w (k + 1) h).state with | none => none | some q => (treeScanner.tr q (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols).outS) = none w:List Boolk:h:k + 1 w.lengthhok:ok (List.drop (k + 1) w) = true(match (sweepCfg w (k + 1) h).state with | none => none | some q => (treeScanner.tr q (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols).outS) = nonew:List Boolk:h:k + 1 w.lengthhok:¬ok (List.drop (k + 1) w) = true(match (sweepCfg w (k + 1) h).state with | none => none | some q => (treeScanner.tr q (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols).outS) = none w:List Boolk:h:k + 1 w.lengthhok:ok (List.drop (k + 1) w) = true(match (sweepCfg w (k + 1) h).state with | none => none | some q => (treeScanner.tr q (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols).outS) = none w:List Boolk:h:k + 1 w.lengthhok:ok (List.drop (k + 1) w) = true(treeScanner.tr stLive (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols).outS = none cases hbit : w[k] with w:List Boolk:h:k + 1 w.lengthhok:ok (List.drop (k + 1) w) = truehbit:w[k] = false(treeScanner.tr stLive (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols).outS = none All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhok:ok (List.drop (k + 1) w) = truehbit:w[k] = true(treeScanner.tr stLive (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols).outS = none w:List Boolk:h:k + 1 w.lengthhok:ok (List.drop (k + 1) w) = truehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)(treeScanner.tr stLive (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols).outS = nonew:List Boolk:h:k + 1 w.lengthhok:ok (List.drop (k + 1) w) = truehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)(treeScanner.tr stLive (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols).outS = none w:List Boolk:h:k + 1 w.lengthhok:ok (List.drop (k + 1) w) = truehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)(treeScanner.tr stLive (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols).outS = none All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhok:ok (List.drop (k + 1) w) = truehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)(treeScanner.tr stLive (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols).outS = none All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhok:¬ok (List.drop (k + 1) w) = true(match (sweepCfg w (k + 1) h).state with | none => none | some q => (treeScanner.tr q (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols).outS) = none w:List Boolk:h:k + 1 w.lengthhok:ok (List.drop (k + 1) w) = false(match (sweepCfg w (k + 1) h).state with | none => none | some q => (treeScanner.tr q (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols).outS) = none w:List Boolk:h:k + 1 w.lengthhok:ok (List.drop (k + 1) w) = false(treeScanner.tr stDead (sweepCfg w (k + 1) h).inputSymbol (sweepCfg w (k + 1) h).workTapeSymbols).outS = none All goals completed! 🐙
end OutputSymbolsection Seek

Short of the input's right end one seek step advances the input head by one cell and leaves the blank work tape and its head untouched.

theorem seekCfg_step (w : List Bool) (t : ) (h : t + 1 w.length) : treeScanner.step (seekCfg w t (w:List Boolt:h:t + 1 w.lengtht w.length All goals completed! 🐙)) = seekCfg w (t + 1) h := w:List Boolt:h:t + 1 w.lengthstep (seekCfg w t ) = seekCfg w (t + 1) h w:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPosstep (seekCfg w t ) = seekCfg w (t + 1) h w:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPos{ state := { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.q', inputPos := moveInputPos (seekCfg w t ).inputPos { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).1 with | none => (seekCfg w t ).workTapes i | some s => Function.update ((seekCfg w t ).workTapes i) ((seekCfg w t ).workTapePos i) s, workTapePos := fun i (seekCfg w t ).workTapePos i + ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).2 } = seekCfg w (t + 1) h w:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPos{ state := { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.q', inputPos := moveInputPos (seekCfg w t ).inputPos { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).1 with | none => (seekCfg w t ).workTapes i | some s => Function.update ((seekCfg w t ).workTapes i) ((seekCfg w t ).workTapePos i) s, workTapePos := fun i (seekCfg w t ).workTapePos i + ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).2 }.state = (seekCfg w (t + 1) h).statew:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPos{ state := { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.q', inputPos := moveInputPos (seekCfg w t ).inputPos { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).1 with | none => (seekCfg w t ).workTapes i | some s => Function.update ((seekCfg w t ).workTapes i) ((seekCfg w t ).workTapePos i) s, workTapePos := fun i (seekCfg w t ).workTapePos i + ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).2 }.inputPos = (seekCfg w (t + 1) h).inputPosw:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPos{ state := { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.q', inputPos := moveInputPos (seekCfg w t ).inputPos { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).1 with | none => (seekCfg w t ).workTapes i | some s => Function.update ((seekCfg w t ).workTapes i) ((seekCfg w t ).workTapePos i) s, workTapePos := fun i (seekCfg w t ).workTapePos i + ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).2 }.workTapes = (seekCfg w (t + 1) h).workTapesw:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPos{ state := { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.q', inputPos := moveInputPos (seekCfg w t ).inputPos { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).1 with | none => (seekCfg w t ).workTapes i | some s => Function.update ((seekCfg w t ).workTapes i) ((seekCfg w t ).workTapePos i) s, workTapePos := fun i (seekCfg w t ).workTapePos i + ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).2 }.workTapePos = (seekCfg w (t + 1) h).workTapePos w:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPos{ state := { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.q', inputPos := moveInputPos (seekCfg w t ).inputPos { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).1 with | none => (seekCfg w t ).workTapes i | some s => Function.update ((seekCfg w t ).workTapes i) ((seekCfg w t ).workTapePos i) s, workTapePos := fun i (seekCfg w t ).workTapePos i + ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).2 }.state = (seekCfg w (t + 1) h).statew:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPos{ state := { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.q', inputPos := moveInputPos (seekCfg w t ).inputPos { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).1 with | none => (seekCfg w t ).workTapes i | some s => Function.update ((seekCfg w t ).workTapes i) ((seekCfg w t ).workTapePos i) s, workTapePos := fun i (seekCfg w t ).workTapePos i + ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).2 }.inputPos = (seekCfg w (t + 1) h).inputPosw:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPos{ state := { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.q', inputPos := moveInputPos (seekCfg w t ).inputPos { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).1 with | none => (seekCfg w t ).workTapes i | some s => Function.update ((seekCfg w t ).workTapes i) ((seekCfg w t ).workTapePos i) s, workTapePos := fun i (seekCfg w t ).workTapePos i + ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).2 }.workTapes = (seekCfg w (t + 1) h).workTapesw:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPos{ state := { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.q', inputPos := moveInputPos (seekCfg w t ).inputPos { inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).1 with | none => (seekCfg w t ).workTapes i | some s => Function.update ((seekCfg w t ).workTapes i) ((seekCfg w t ).workTapePos i) s, workTapePos := fun i (seekCfg w t ).workTapePos i + ({ inputMove := 1, workActions := fun x (none, 0), outS := none, q' := some stSeek }.workActions i).2 }.workTapePos = (seekCfg w (t + 1) h).workTapePos w:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPos(fun i (seekCfg w t ).workTapePos i + 0) = (seekCfg w (t + 1) h).workTapePos w:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPossome stSeek = (seekCfg w (t + 1) h).state All goals completed! 🐙 w:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPosmoveInputPos (seekCfg w t ).inputPos 1 = (seekCfg w (t + 1) h).inputPos All goals completed! 🐙 w:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPos(fun i (seekCfg w t ).workTapes i) = (seekCfg w (t + 1) h).workTapes w:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPosi:Fin 1(seekCfg w t ).workTapes i = (seekCfg w (t + 1) h).workTapes i All goals completed! 🐙 w:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPos(fun i (seekCfg w t ).workTapePos i + 0) = (seekCfg w (t + 1) h).workTapePos w:List Boolt:h:t + 1 w.lengthhpos:moveInputPos (seekCfg w t ).inputPos SignType.pos = (seekCfg w (t + 1) h).inputPosi:Fin 1(seekCfg w t ).workTapePos i + 0 = (seekCfg w (t + 1) h).workTapePos i All goals completed! 🐙

The seek phase's configuration and output at every step up to the input's length: the closed form of seekCfg, and nothing emitted. Both conjuncts run in one recursion, the output obligation being what the composition across the phase boundary needs alongside the configuration.

theorem configs_seek (w : List Bool) : t, h : t w.length, treeScanner.configs (treeScanner.initCfg (w.map boolEmb)) t = seekCfg w t h treeScanner.outputString (treeScanner.initCfg (w.map boolEmb)) t = [] := w:List Bool (t : ) (h : t w.length), configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = [] w:List Bool (h : Nat.zero w.length), configs (initCfg (List.map (⇑boolEmb) w)) Nat.zero = seekCfg w Nat.zero h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) Nat.zero = []w:List Bool (n : ), (∀ (h : n w.length), configs (initCfg (List.map (⇑boolEmb) w)) n = seekCfg w n h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) n = []) (h : n.succ w.length), configs (initCfg (List.map (⇑boolEmb) w)) n.succ = seekCfg w n.succ h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) n.succ = [] w:List Bool (h : Nat.zero w.length), configs (initCfg (List.map (⇑boolEmb) w)) Nat.zero = seekCfg w Nat.zero h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) Nat.zero = [] w:List Boolh✝:Nat.zero w.lengthconfigs (initCfg (List.map (⇑boolEmb) w)) Nat.zero = seekCfg w Nat.zero h✝ treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) Nat.zero = [] w:List Boolh✝:Nat.zero w.lengthconfigs (initCfg (List.map (⇑boolEmb) w)) Nat.zero = seekCfg w Nat.zero h✝ All goals completed! 🐙 w:List Bool (n : ), (∀ (h : n w.length), configs (initCfg (List.map (⇑boolEmb) w)) n = seekCfg w n h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) n = []) (h : n.succ w.length), configs (initCfg (List.map (⇑boolEmb) w)) n.succ = seekCfg w n.succ h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) n.succ = [] w:List Boolt:ih: (h : t w.length), configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = []h:t.succ w.lengthconfigs (initCfg (List.map (⇑boolEmb) w)) t.succ = seekCfg w t.succ h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t.succ = [] w:List Boolt:ih: (h : t w.length), configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = []h:t.succ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t ho:treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = []configs (initCfg (List.map (⇑boolEmb) w)) t.succ = seekCfg w t.succ h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t.succ = [] w:List Boolt:ih: (h : t w.length), configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = []h:t.succ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t ho:treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = []configs (initCfg (List.map (⇑boolEmb) w)) t.succ = seekCfg w t.succ hw:List Boolt:ih: (h : t w.length), configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = []h:t.succ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t ho:treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = []treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t.succ = [] w:List Boolt:ih: (h : t w.length), configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = []h:t.succ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t ho:treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = []configs (initCfg (List.map (⇑boolEmb) w)) t.succ = seekCfg w t.succ h w:List Boolt:ih: (h : t w.length), configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = []h:t.succ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t ho:treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = []step (seekCfg w t ) = seekCfg w t.succ h All goals completed! 🐙 w:List Boolt:ih: (h : t w.length), configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = []h:t.succ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t ho:treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = []treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t.succ = [] w:List Boolt:ih: (h : t w.length), configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t h treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = []h:t.succ w.lengthhc:configs (initCfg (List.map (⇑boolEmb) w)) t = seekCfg w t ho:treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) t = [][] ++ none.toList = [] All goals completed! 🐙

At the input's right end the seek step writes the first marker at cell 0, moves the work head right to cell 1 and the input head left.

theorem seekCfg_exit (w : List Bool) : treeScanner.step (seekCfg w w.length (Nat.le_refl _)) = plantCfg w := w:List Boolstep (seekCfg w w.length ) = plantCfg w w:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPosstep (seekCfg w w.length ) = plantCfg w w:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPos{ state := { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.q', inputPos := moveInputPos (seekCfg w w.length ).inputPos { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).1 with | none => (seekCfg w w.length ).workTapes i | some s => Function.update ((seekCfg w w.length ).workTapes i) ((seekCfg w w.length ).workTapePos i) s, workTapePos := fun i (seekCfg w w.length ).workTapePos i + ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).2 } = plantCfg w w:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPos{ state := { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.q', inputPos := moveInputPos (seekCfg w w.length ).inputPos { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).1 with | none => (seekCfg w w.length ).workTapes i | some s => Function.update ((seekCfg w w.length ).workTapes i) ((seekCfg w w.length ).workTapePos i) s, workTapePos := fun i (seekCfg w w.length ).workTapePos i + ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).2 }.state = (plantCfg w).statew:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPos{ state := { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.q', inputPos := moveInputPos (seekCfg w w.length ).inputPos { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).1 with | none => (seekCfg w w.length ).workTapes i | some s => Function.update ((seekCfg w w.length ).workTapes i) ((seekCfg w w.length ).workTapePos i) s, workTapePos := fun i (seekCfg w w.length ).workTapePos i + ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).2 }.inputPos = (plantCfg w).inputPosw:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPos{ state := { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.q', inputPos := moveInputPos (seekCfg w w.length ).inputPos { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).1 with | none => (seekCfg w w.length ).workTapes i | some s => Function.update ((seekCfg w w.length ).workTapes i) ((seekCfg w w.length ).workTapePos i) s, workTapePos := fun i (seekCfg w w.length ).workTapePos i + ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).2 }.workTapes = (plantCfg w).workTapesw:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPos{ state := { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.q', inputPos := moveInputPos (seekCfg w w.length ).inputPos { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).1 with | none => (seekCfg w w.length ).workTapes i | some s => Function.update ((seekCfg w w.length ).workTapes i) ((seekCfg w w.length ).workTapePos i) s, workTapePos := fun i (seekCfg w w.length ).workTapePos i + ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).2 }.workTapePos = (plantCfg w).workTapePos w:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPos{ state := { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.q', inputPos := moveInputPos (seekCfg w w.length ).inputPos { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).1 with | none => (seekCfg w w.length ).workTapes i | some s => Function.update ((seekCfg w w.length ).workTapes i) ((seekCfg w w.length ).workTapePos i) s, workTapePos := fun i (seekCfg w w.length ).workTapePos i + ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).2 }.state = (plantCfg w).statew:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPos{ state := { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.q', inputPos := moveInputPos (seekCfg w w.length ).inputPos { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).1 with | none => (seekCfg w w.length ).workTapes i | some s => Function.update ((seekCfg w w.length ).workTapes i) ((seekCfg w w.length ).workTapePos i) s, workTapePos := fun i (seekCfg w w.length ).workTapePos i + ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).2 }.inputPos = (plantCfg w).inputPosw:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPos{ state := { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.q', inputPos := moveInputPos (seekCfg w w.length ).inputPos { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).1 with | none => (seekCfg w w.length ).workTapes i | some s => Function.update ((seekCfg w w.length ).workTapes i) ((seekCfg w w.length ).workTapePos i) s, workTapePos := fun i (seekCfg w w.length ).workTapePos i + ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).2 }.workTapes = (plantCfg w).workTapesw:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPos{ state := { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.q', inputPos := moveInputPos (seekCfg w w.length ).inputPos { inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).1 with | none => (seekCfg w w.length ).workTapes i | some s => Function.update ((seekCfg w w.length ).workTapes i) ((seekCfg w w.length ).workTapePos i) s, workTapePos := fun i (seekCfg w w.length ).workTapePos i + ({ inputMove := -1, workActions := fun x (some (some 0), 1), outS := none, q' := some stPlant }.workActions i).2 }.workTapePos = (plantCfg w).workTapePos w:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPos(fun i (seekCfg w w.length ).workTapePos i + 1) = (plantCfg w).workTapePos w:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPossome stPlant = (plantCfg w).state All goals completed! 🐙 w:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPosmoveInputPos (seekCfg w w.length ).inputPos (-1) = (plantCfg w).inputPos All goals completed! 🐙 w:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPos(fun i Function.update ((seekCfg w w.length ).workTapes i) ((seekCfg w w.length ).workTapePos i) (some 0)) = (plantCfg w).workTapes w:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPosi:Fin 1z:Function.update ((seekCfg w w.length ).workTapes i) ((seekCfg w w.length ).workTapePos i) (some 0) z = (plantCfg w).workTapes i z All goals completed! 🐙 w:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPos(fun i (seekCfg w w.length ).workTapePos i + 1) = (plantCfg w).workTapePos w:List Boolhpos:moveInputPos (seekCfg w w.length ).inputPos SignType.neg = (plantCfg w).inputPosi:Fin 1(seekCfg w w.length ).workTapePos i + 1 = (plantCfg w).workTapePos i All goals completed! 🐙
end Seeksection Plant

The planting step writes the second marker at cell 1 and returns the work head to cell 0, leaving the input head where it stands.

theorem plantCfg_step (w : List Bool) : treeScanner.step (plantCfg w) = sweepCfg w w.length (Nat.le_refl _) := w:List Boolstep (plantCfg w) = sweepCfg w w.length w:List Boolhdepth:depth [] = 0step (plantCfg w) = sweepCfg w w.length w:List Boolhdepth:depth [] = 0{ state := { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (plantCfg w).inputPos { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).1 with | none => (plantCfg w).workTapes i | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s, workTapePos := fun i (plantCfg w).workTapePos i + ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).2 } = sweepCfg w w.length w:List Boolhdepth:depth [] = 0{ state := { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (plantCfg w).inputPos { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).1 with | none => (plantCfg w).workTapes i | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s, workTapePos := fun i (plantCfg w).workTapePos i + ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).2 }.state = (sweepCfg w w.length ).statew:List Boolhdepth:depth [] = 0{ state := { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (plantCfg w).inputPos { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).1 with | none => (plantCfg w).workTapes i | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s, workTapePos := fun i (plantCfg w).workTapePos i + ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).2 }.inputPos = (sweepCfg w w.length ).inputPosw:List Boolhdepth:depth [] = 0{ state := { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (plantCfg w).inputPos { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).1 with | none => (plantCfg w).workTapes i | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s, workTapePos := fun i (plantCfg w).workTapePos i + ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).2 }.workTapes = (sweepCfg w w.length ).workTapesw:List Boolhdepth:depth [] = 0{ state := { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (plantCfg w).inputPos { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).1 with | none => (plantCfg w).workTapes i | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s, workTapePos := fun i (plantCfg w).workTapePos i + ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).2 }.workTapePos = (sweepCfg w w.length ).workTapePos w:List Boolhdepth:depth [] = 0{ state := { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (plantCfg w).inputPos { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).1 with | none => (plantCfg w).workTapes i | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s, workTapePos := fun i (plantCfg w).workTapePos i + ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).2 }.state = (sweepCfg w w.length ).statew:List Boolhdepth:depth [] = 0{ state := { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (plantCfg w).inputPos { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).1 with | none => (plantCfg w).workTapes i | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s, workTapePos := fun i (plantCfg w).workTapePos i + ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).2 }.inputPos = (sweepCfg w w.length ).inputPosw:List Boolhdepth:depth [] = 0{ state := { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (plantCfg w).inputPos { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).1 with | none => (plantCfg w).workTapes i | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s, workTapePos := fun i (plantCfg w).workTapePos i + ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).2 }.workTapes = (sweepCfg w w.length ).workTapesw:List Boolhdepth:depth [] = 0{ state := { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (plantCfg w).inputPos { inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).1 with | none => (plantCfg w).workTapes i | some s => Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) s, workTapePos := fun i (plantCfg w).workTapePos i + ({ inputMove := 0, workActions := fun x (some (some 1), -1), outS := none, q' := some stLive }.workActions i).2 }.workTapePos = (sweepCfg w w.length ).workTapePos w:List Boolhdepth:depth [] = 0(fun i (plantCfg w).workTapePos i + (-1)) = (sweepCfg w w.length ).workTapePos w:List Boolhdepth:depth [] = 0some stLive = (sweepCfg w w.length ).state w:List Boolhdepth:depth [] = 0some stLive = if ok [] = true then some stLive else some stDead All goals completed! 🐙 w:List Boolhdepth:depth [] = 0moveInputPos (plantCfg w).inputPos 0 = (sweepCfg w w.length ).inputPos All goals completed! 🐙 w:List Boolhdepth:depth [] = 0(fun i Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) (some 1)) = (sweepCfg w w.length ).workTapes w:List Boolhdepth:depth [] = 0i:Fin 1z:Function.update ((plantCfg w).workTapes i) ((plantCfg w).workTapePos i) (some 1) z = (sweepCfg w w.length ).workTapes i z w:List Boolhdepth:depth [] = 0i:Fin 1z:(if z = 1 then some 1 else if z = 0 then some 0 else none) = if z = 0 then some 0 else if z = 1 then some 1 else none w:List Boolhdepth:depth [] = 0i:Fin 1z:h✝¹:z = 1h✝:z = 0some 1 = some 0w:List Boolhdepth:depth [] = 0i:Fin 1z:h✝¹:z = 1h✝:¬z = 0some 1 = some 1w:List Boolhdepth:depth [] = 0i:Fin 1z:h✝¹:¬z = 1h✝:z = 0some 0 = some 0w:List Boolhdepth:depth [] = 0i:Fin 1z:h✝¹:¬z = 1h✝:¬z = 0none = none w:List Boolhdepth:depth [] = 0i:Fin 1z:h✝¹:z = 1h✝:z = 0some 1 = some 0w:List Boolhdepth:depth [] = 0i:Fin 1z:h✝¹:z = 1h✝:¬z = 0some 1 = some 1w:List Boolhdepth:depth [] = 0i:Fin 1z:h✝¹:¬z = 1h✝:z = 0some 0 = some 0w:List Boolhdepth:depth [] = 0i:Fin 1z:h✝¹:¬z = 1h✝:¬z = 0none = none first | All goals completed! 🐙 | All goals completed! 🐙 w:List Boolhdepth:depth [] = 0(fun i (plantCfg w).workTapePos i + (-1)) = (sweepCfg w w.length ).workTapePos w:List Boolhdepth:depth [] = 0i:Fin 1(plantCfg w).workTapePos i + (-1) = (sweepCfg w w.length ).workTapePos i w:List Boolhdepth:depth [] = 0i:Fin 11 + -1 = 0 All goals completed! 🐙
end Plantsection Sweep

One sweep step consumes the bit to the input head's left: the state stays live exactly where the scan extended by that bit stays live, and the work head carries the extended scan's pending count.

theorem sweepCfg_step (w : List Bool) (k : ) (h : k + 1 w.length) : treeScanner.step (sweepCfg w (k + 1) h) = sweepCfg w k (w:List Boolk:h:k + 1 w.lengthk w.length All goals completed! 🐙) := w:List Boolk:h:k + 1 w.lengthstep (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) wstep (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPosstep (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truestep (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:¬ok (List.drop (k + 1) w) = truestep (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truestep (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivestep (sweepCfg w (k + 1) h) = sweepCfg w k cases hbit : w[k] with w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsestep (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truestep (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1step (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1{ state := { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).2 } = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1{ state := { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).2 }.state = (sweepCfg w k ).statew:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1{ state := { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).2 }.inputPos = (sweepCfg w k ).inputPosw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1{ state := { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).2 }.workTapes = (sweepCfg w k ).workTapesw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1{ state := { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).2 }.workTapePos = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1{ state := { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).2 }.state = (sweepCfg w k ).statew:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1{ state := { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).2 }.inputPos = (sweepCfg w k ).inputPosw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1{ state := { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).2 }.workTapes = (sweepCfg w k ).workTapesw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1{ state := { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 1), outS := none, q' := some stLive }.workActions i).2 }.workTapePos = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1(fun i (sweepCfg w (k + 1) h).workTapePos i + 1) = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1some stLive = (sweepCfg w k ).state All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1moveInputPos (sweepCfg w (k + 1) h).inputPos (-1) = (sweepCfg w k ).inputPos All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1(fun i (sweepCfg w (k + 1) h).workTapes i) = (sweepCfg w k ).workTapes w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1i:Fin 1(sweepCfg w (k + 1) h).workTapes i = (sweepCfg w k ).workTapes i All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1(fun i (sweepCfg w (k + 1) h).workTapePos i + 1) = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1i:Fin 1(sweepCfg w (k + 1) h).workTapePos i + 1 = (sweepCfg w k ).workTapePos i w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = falsehokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) + 1i:Fin 1(depth (List.drop (k + 1) w)) + 1 = (depth (List.drop (k + 1) w) + 1) All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truestep (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)step (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)step (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)step (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truestep (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1step (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1{ state := { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).2 } = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1{ state := { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).2 }.state = (sweepCfg w k ).statew:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1{ state := { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).2 }.inputPos = (sweepCfg w k ).inputPosw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1{ state := { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).2 }.workTapes = (sweepCfg w k ).workTapesw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1{ state := { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).2 }.workTapePos = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1{ state := { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).2 }.state = (sweepCfg w k ).statew:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1{ state := { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).2 }.inputPos = (sweepCfg w k ).inputPosw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1{ state := { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).2 }.workTapes = (sweepCfg w k ).workTapesw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1{ state := { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, -1), outS := none, q' := some stLive }.workActions i).2 }.workTapePos = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1(fun i (sweepCfg w (k + 1) h).workTapePos i + (-1)) = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1some stLive = (sweepCfg w k ).state All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1moveInputPos (sweepCfg w (k + 1) h).inputPos (-1) = (sweepCfg w k ).inputPos All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1(fun i (sweepCfg w (k + 1) h).workTapes i) = (sweepCfg w k ).workTapes w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1i:Fin 1(sweepCfg w (k + 1) h).workTapes i = (sweepCfg w k ).workTapes i All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1(fun i (sweepCfg w (k + 1) h).workTapePos i + (-1)) = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1i:Fin 1(sweepCfg w (k + 1) h).workTapePos i + (-1) = (sweepCfg w k ).workTapePos i w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:2 depth (List.drop (k + 1) w)hokk:ok (List.drop k w) = truehdk:depth (List.drop k w) = depth (List.drop (k + 1) w) - 1i:Fin 1(depth (List.drop (k + 1) w)) + -1 = (depth (List.drop (k + 1) w) - 1) All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)step (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2step (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsestep (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)step (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 } = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.state = (sweepCfg w k ).statew:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.inputPos = (sweepCfg w k ).inputPosw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.workTapes = (sweepCfg w k ).workTapesw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.workTapePos = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.state = (sweepCfg w k ).statew:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.inputPos = (sweepCfg w k ).inputPosw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.workTapes = (sweepCfg w k ).workTapesw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.workTapePos = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)(fun i (sweepCfg w (k + 1) h).workTapePos i + 0) = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)some stDead = (sweepCfg w k ).state w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)some stDead = if false = true then some stLive else some stDead All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)moveInputPos (sweepCfg w (k + 1) h).inputPos (-1) = (sweepCfg w k ).inputPos All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)(fun i (sweepCfg w (k + 1) h).workTapes i) = (sweepCfg w k ).workTapes w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)i:Fin 1(sweepCfg w (k + 1) h).workTapes i = (sweepCfg w k ).workTapes i All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)(fun i (sweepCfg w (k + 1) h).workTapePos i + 0) = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)i:Fin 1(sweepCfg w (k + 1) h).workTapePos i + 0 = (sweepCfg w k ).workTapePos i w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = truehst:(sweepCfg w (k + 1) h).state = some stLivehbit:w[k] = truehd:¬2 depth (List.drop (k + 1) w)hd2:depth (List.drop (k + 1) w) < 2hokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)i:Fin 1(depth (List.drop (k + 1) w)) + 0 = (depth (List.drop (k + 1) w)) All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:¬ok (List.drop (k + 1) w) = truestep (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsestep (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsestep (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)step (sweepCfg w (k + 1) h) = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 } = sweepCfg w k w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.state = (sweepCfg w k ).statew:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.inputPos = (sweepCfg w k ).inputPosw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.workTapes = (sweepCfg w k ).workTapesw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.workTapePos = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.state = (sweepCfg w k ).statew:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.inputPos = (sweepCfg w k ).inputPosw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.workTapes = (sweepCfg w k ).workTapesw:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w){ state := { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.q', inputPos := moveInputPos (sweepCfg w (k + 1) h).inputPos { inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).1 with | none => (sweepCfg w (k + 1) h).workTapes i | some s => Function.update ((sweepCfg w (k + 1) h).workTapes i) ((sweepCfg w (k + 1) h).workTapePos i) s, workTapePos := fun i (sweepCfg w (k + 1) h).workTapePos i + ({ inputMove := -1, workActions := fun x (none, 0), outS := none, q' := some stDead }.workActions i).2 }.workTapePos = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)(fun i (sweepCfg w (k + 1) h).workTapePos i + 0) = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)some stDead = (sweepCfg w k ).state w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)some stDead = if false = true then some stLive else some stDead All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)moveInputPos (sweepCfg w (k + 1) h).inputPos (-1) = (sweepCfg w k ).inputPos All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)(fun i (sweepCfg w (k + 1) h).workTapes i) = (sweepCfg w k ).workTapes w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)i:Fin 1(sweepCfg w (k + 1) h).workTapes i = (sweepCfg w k ).workTapes i All goals completed! 🐙 w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)(fun i (sweepCfg w (k + 1) h).workTapePos i + 0) = (sweepCfg w k ).workTapePos w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)i:Fin 1(sweepCfg w (k + 1) h).workTapePos i + 0 = (sweepCfg w k ).workTapePos i w:List Boolk:h:k + 1 w.lengthhdrop:List.drop k w = w[k] :: List.drop (k + 1) whpos:moveInputPos (sweepCfg w (k + 1) h).inputPos SignType.neg = (sweepCfg w k ).inputPoshok:ok (List.drop (k + 1) w) = falsehokk:ok (List.drop k w) = falsehdk:depth (List.drop k w) = depth (List.drop (k + 1) w)i:Fin 1(depth (List.drop (k + 1) w)) + 0 = (depth (List.drop (k + 1) w)) All goals completed! 🐙

The sweep phase's configuration and output at every step down to the input's left end: the closed form of sweepCfg, and nothing emitted. The family descends in its index while the step count ascends, so the motive carries the equation linking the two and nothing subtracts. Both conjuncts run in one recursion, the output obligation being what the composition across the phase boundary needs alongside the configuration.

theorem configs_sweep (w : List Bool) : j, k, h : k + j = w.length, treeScanner.configs (sweepCfg w w.length (Nat.le_refl _)) j = sweepCfg w k (w:List Boolj:k:h:k + j = w.lengthk w.length All goals completed! 🐙) treeScanner.outputString (sweepCfg w w.length (Nat.le_refl _)) j = [] := w:List Bool (j k : ) (h : k + j = w.length), configs (sweepCfg w w.length ) j = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) j = [] w:List Bool (k : ) (h : k + Nat.zero = w.length), configs (sweepCfg w w.length ) Nat.zero = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) Nat.zero = []w:List Bool (n : ), (∀ (k : ) (h : k + n = w.length), configs (sweepCfg w w.length ) n = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) n = []) (k : ) (h : k + n.succ = w.length), configs (sweepCfg w w.length ) n.succ = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) n.succ = [] w:List Bool (k : ) (h : k + Nat.zero = w.length), configs (sweepCfg w w.length ) Nat.zero = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) Nat.zero = [] w:List Boolk:hk:k + Nat.zero = w.lengthconfigs (sweepCfg w w.length ) Nat.zero = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) Nat.zero = [] w:List Boolk:hk:k + Nat.zero = w.lengthhkn:k = w.lengthconfigs (sweepCfg w w.length ) Nat.zero = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) Nat.zero = [] w:List Boolhk:w.length + Nat.zero = w.lengthconfigs (sweepCfg w w.length ) Nat.zero = sweepCfg w w.length treeScanner.outputString (sweepCfg w w.length ) Nat.zero = [] All goals completed! 🐙 w:List Bool (n : ), (∀ (k : ) (h : k + n = w.length), configs (sweepCfg w w.length ) n = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) n = []) (k : ) (h : k + n.succ = w.length), configs (sweepCfg w w.length ) n.succ = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) n.succ = [] w:List Boolj:ih: (k : ) (h : k + j = w.length), configs (sweepCfg w w.length ) j = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) j = []k:hk:k + j.succ = w.lengthconfigs (sweepCfg w w.length ) j.succ = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) j.succ = [] w:List Boolj:ih: (k : ) (h : k + j = w.length), configs (sweepCfg w w.length ) j = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) j = []k:hk:k + j.succ = w.lengthhc:configs (sweepCfg w w.length ) j = sweepCfg w (k + 1) ho:treeScanner.outputString (sweepCfg w w.length ) j = []configs (sweepCfg w w.length ) j.succ = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) j.succ = [] w:List Boolj:ih: (k : ) (h : k + j = w.length), configs (sweepCfg w w.length ) j = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) j = []k:hk:k + j.succ = w.lengthhc:configs (sweepCfg w w.length ) j = sweepCfg w (k + 1) ho:treeScanner.outputString (sweepCfg w w.length ) j = []configs (sweepCfg w w.length ) j.succ = sweepCfg w k w:List Boolj:ih: (k : ) (h : k + j = w.length), configs (sweepCfg w w.length ) j = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) j = []k:hk:k + j.succ = w.lengthhc:configs (sweepCfg w w.length ) j = sweepCfg w (k + 1) ho:treeScanner.outputString (sweepCfg w w.length ) j = []treeScanner.outputString (sweepCfg w w.length ) j.succ = [] w:List Boolj:ih: (k : ) (h : k + j = w.length), configs (sweepCfg w w.length ) j = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) j = []k:hk:k + j.succ = w.lengthhc:configs (sweepCfg w w.length ) j = sweepCfg w (k + 1) ho:treeScanner.outputString (sweepCfg w w.length ) j = []configs (sweepCfg w w.length ) j.succ = sweepCfg w k w:List Boolj:ih: (k : ) (h : k + j = w.length), configs (sweepCfg w w.length ) j = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) j = []k:hk:k + j.succ = w.lengthhc:configs (sweepCfg w w.length ) j = sweepCfg w (k + 1) ho:treeScanner.outputString (sweepCfg w w.length ) j = []step (sweepCfg w (k + 1) ) = sweepCfg w k exact sweepCfg_step w k (w:List Boolj:ih: (k : ) (h : k + j = w.length), configs (sweepCfg w w.length ) j = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) j = []k:hk:k + j.succ = w.lengthhc:configs (sweepCfg w w.length ) j = sweepCfg w (k + 1) ho:treeScanner.outputString (sweepCfg w w.length ) j = []k + 1 w.length All goals completed! 🐙) w:List Boolj:ih: (k : ) (h : k + j = w.length), configs (sweepCfg w w.length ) j = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) j = []k:hk:k + j.succ = w.lengthhc:configs (sweepCfg w w.length ) j = sweepCfg w (k + 1) ho:treeScanner.outputString (sweepCfg w w.length ) j = []treeScanner.outputString (sweepCfg w w.length ) j.succ = [] w:List Boolj:ih: (k : ) (h : k + j = w.length), configs (sweepCfg w w.length ) j = sweepCfg w k treeScanner.outputString (sweepCfg w w.length ) j = []k:hk:k + j.succ = w.lengthhc:configs (sweepCfg w w.length ) j = sweepCfg w (k + 1) ho:treeScanner.outputString (sweepCfg w w.length ) j = [][] ++ none.toList = [] All goals completed! 🐙
end Sweepsection Emission

At the input's left end the machine halts, live or dead.

theorem sweepCfg_zero_halts (w : List Bool) : (treeScanner.step (sweepCfg w 0 (Nat.zero_le _))).state = none := w:List Bool(step (sweepCfg w 0 )).state = none w:List Boolhok:ok w = true(step (sweepCfg w 0 )).state = nonew:List Boolhok:¬ok w = true(step (sweepCfg w 0 )).state = none w:List Boolhok:ok w = true(step (sweepCfg w 0 )).state = none w:List Boolhok:ok w = true{ state := (treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).q', inputPos := moveInputPos (sweepCfg w 0 ).inputPos (treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ((treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).workActions i).1 with | none => (sweepCfg w 0 ).workTapes i | some s => Function.update ((sweepCfg w 0 ).workTapes i) ((sweepCfg w 0 ).workTapePos i) s, workTapePos := fun i (sweepCfg w 0 ).workTapePos i + ((treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).workActions i).2 }.state = none w:List Boolhok:ok w = truehd:depth w = 1{ state := (treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).q', inputPos := moveInputPos (sweepCfg w 0 ).inputPos (treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ((treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).workActions i).1 with | none => (sweepCfg w 0 ).workTapes i | some s => Function.update ((sweepCfg w 0 ).workTapes i) ((sweepCfg w 0 ).workTapePos i) s, workTapePos := fun i (sweepCfg w 0 ).workTapePos i + ((treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).workActions i).2 }.state = nonew:List Boolhok:ok w = truehd:¬depth w = 1{ state := (treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).q', inputPos := moveInputPos (sweepCfg w 0 ).inputPos (treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ((treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).workActions i).1 with | none => (sweepCfg w 0 ).workTapes i | some s => Function.update ((sweepCfg w 0 ).workTapes i) ((sweepCfg w 0 ).workTapePos i) s, workTapePos := fun i (sweepCfg w 0 ).workTapePos i + ((treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).workActions i).2 }.state = none w:List Boolhok:ok w = truehd:depth w = 1{ state := (treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).q', inputPos := moveInputPos (sweepCfg w 0 ).inputPos (treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ((treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).workActions i).1 with | none => (sweepCfg w 0 ).workTapes i | some s => Function.update ((sweepCfg w 0 ).workTapes i) ((sweepCfg w 0 ).workTapePos i) s, workTapePos := fun i (sweepCfg w 0 ).workTapePos i + ((treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).workActions i).2 }.state = none All goals completed! 🐙 w:List Boolhok:ok w = truehd:¬depth w = 1{ state := (treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).q', inputPos := moveInputPos (sweepCfg w 0 ).inputPos (treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).inputMove, workTapes := fun i match (motive := Option (Option (Fin 2)) Option (Fin 2)) ((treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).workActions i).1 with | none => (sweepCfg w 0 ).workTapes i | some s => Function.update ((sweepCfg w 0 ).workTapes i) ((sweepCfg w 0 ).workTapePos i) s, workTapePos := fun i (sweepCfg w 0 ).workTapePos i + ((treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).workActions i).2 }.state = none All goals completed! 🐙 w:List Boolhok:¬ok w = true(step (sweepCfg w 0 )).state = none w:List Boolhok:ok w = false(step (sweepCfg w 0 )).state = none All goals completed! 🐙

The emitted symbol is the decision function's value: the machine's end-of-input cases — dead, live with the second marker under the work head, and live otherwise — are the cases of ok w && depth w == 1.

theorem outputSymbol_sweepCfg_zero (w : List Bool) : treeScanner.outputSymbol (sweepCfg w 0 (Nat.zero_le _)) = some (boolEmb (binRanked.validBool w)) := w:List BooloutputSymbol (sweepCfg w 0 ) = some (boolEmb (binRanked.validBool w)) w:List BooloutputSymbol (sweepCfg w 0 ) = some (boolEmb (ok w && depth w == 1)) w:List Bool(match (sweepCfg w 0 ).state with | none => none | some q => (treeScanner.tr q (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).outS) = some (boolEmb (ok w && depth w == 1)) w:List Boolhok:ok w = true(match (sweepCfg w 0 ).state with | none => none | some q => (treeScanner.tr q (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).outS) = some (boolEmb (ok w && depth w == 1))w:List Boolhok:¬ok w = true(match (sweepCfg w 0 ).state with | none => none | some q => (treeScanner.tr q (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).outS) = some (boolEmb (ok w && depth w == 1)) w:List Boolhok:ok w = true(match (sweepCfg w 0 ).state with | none => none | some q => (treeScanner.tr q (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).outS) = some (boolEmb (ok w && depth w == 1)) w:List Boolhok:ok w = true(treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).outS = some (boolEmb (ok w && depth w == 1)) w:List Boolhok:ok w = truehd:depth w = 1(treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).outS = some (boolEmb (ok w && depth w == 1))w:List Boolhok:ok w = truehd:¬depth w = 1(treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).outS = some (boolEmb (ok w && depth w == 1)) w:List Boolhok:ok w = truehd:depth w = 1(treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).outS = some (boolEmb (ok w && depth w == 1)) w:List Boolhok:ok w = truehd:depth w = 1{ inputMove := 0, workActions := fun x (none, 0), outS := some 1, q' := none }.outS = some (boolEmb (true && 1 == 1)) All goals completed! 🐙 w:List Boolhok:ok w = truehd:¬depth w = 1(treeScanner.tr stLive (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).outS = some (boolEmb (ok w && depth w == 1)) w:List Boolhok:ok w = truehd:¬depth w = 1{ inputMove := 0, workActions := fun x (none, 0), outS := some 0, q' := none }.outS = some (boolEmb (true && false)) All goals completed! 🐙 w:List Boolhok:¬ok w = true(match (sweepCfg w 0 ).state with | none => none | some q => (treeScanner.tr q (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).outS) = some (boolEmb (ok w && depth w == 1)) w:List Boolhok:ok w = false(match (sweepCfg w 0 ).state with | none => none | some q => (treeScanner.tr q (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).outS) = some (boolEmb (ok w && depth w == 1)) w:List Boolhok:ok w = false(treeScanner.tr stDead (sweepCfg w 0 ).inputSymbol (sweepCfg w 0 ).workTapeSymbols).outS = some (boolEmb (ok w && depth w == 1)) w:List Boolhok:ok w = false{ inputMove := 0, workActions := fun x (none, 0), outS := some 0, q' := none }.outS = some (boolEmb (false && depth w == 1)) All goals completed! 🐙

The machine halts after 2 * w.length + 3 steps: w.length seek steps, the seek's exit step, the planting step, w.length sweep steps, and the emitting step.

theorem halts_at (w : List Bool) : (treeScanner.configs (treeScanner.initCfg (w.map boolEmb)) (2 * w.length + 3)).state = none := w:List Bool(configs (initCfg (List.map (⇑boolEmb) w)) (2 * w.length + 3)).state = none w:List Bool(step (sweepCfg w 0 )).state = none All goals completed! 🐙

Over the same 2 * w.length + 3 steps the machine emits one symbol, the decision function's value at the input.

theorem outputString_eq (w : List Bool) : treeScanner.outputString (treeScanner.initCfg (w.map boolEmb)) (2 * w.length + 3) = [boolEmb (binRanked.validBool w)] := w:List BooltreeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (2 * w.length + 3) = [boolEmb (binRanked.validBool w)] w:List Boolhcfg:configs (initCfg (List.map (⇑boolEmb) w)) (w.length + 1 + 1) = sweepCfg w w.length treeScanner.outputString (initCfg (List.map (⇑boolEmb) w)) (2 * w.length + 3) = [boolEmb (binRanked.validBool w)] w:List Boolhcfg:configs (initCfg (List.map (⇑boolEmb) w)) (w.length + 1 + 1) = sweepCfg w w.length [] ++ none.toList ++ none.toList ++ [] ++ (some (boolEmb (binRanked.validBool w))).toList = [boolEmb (binRanked.validBool w)] All goals completed! 🐙
end Emissionend Geb.TreeScanner