Direct work-symbol branch combinator — proof internals

def Complexity.TM.workSymbolEqualWrap {n : ℕ} (idx : Fin n) (symbol : Γ) (onEqual onDifferent : TM n) (c : Cfg n onEqual.Q) : Cfg n (branchWorkSymbolTM idx symbol onEqual onDifferent).Q

Embed an equal-branch configuration in the direct-symbol controller.

Equations

• Complexity.TM.workSymbolEqualWrap idx symbol onEqual onDifferent c = { state := onEqual.workBranchBlankState onDifferent c.state, input := c.input, work := c.work, output := c.output }

def Complexity.TM.workSymbolDifferentWrap {n : ℕ} (idx : Fin n) (symbol : Γ) (onEqual onDifferent : TM n) (c : Cfg n onDifferent.Q) : Cfg n (branchWorkSymbolTM idx symbol onEqual onDifferent).Q

Embed a different-branch configuration in the direct-symbol controller.

Equations

• Complexity.TM.workSymbolDifferentWrap idx symbol onEqual onDifferent c = { state := onEqual.workBranchNonblankState onDifferent c.state, input := c.input, work := c.work, output := c.output }

theorem Complexity.TM.branchWorkSymbolTM_reachesIn_equal_frame_internal {n : ℕ} (idx : Fin n) (symbol : Γ) (onEqual onDifferent : TM n) (inp : Tape) (work : Fin n → Tape) (out : Tape) {t : ℕ} {c' : Cfg n onEqual.Q} (hequal : (work idx).read = symbol) (hinp : inp.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (work i).read ≠ Γ.start) (hout : out.read ≠ Γ.start) (hreach : onEqual.reachesIn t { state := onEqual.qstart, input := inp, work := work, output := out } c') (hhalt : onEqual.halted c') : ∃ (C : Cfg n (branchWorkSymbolTM idx symbol onEqual onDifferent).Q), (branchWorkSymbolTM idx symbol onEqual onDifferent).reachesIn (t + 1) { state := (branchWorkSymbolTM idx symbol onEqual onDifferent).qstart, input := inp, work := work, output := out } C ∧ (branchWorkSymbolTM idx symbol onEqual onDifferent).halted C ∧ C.input = c'.input ∧ C.work = c'.work ∧ C.output = c'.output

theorem Complexity.TM.branchWorkSymbolTM_reachesIn_different_frame_internal {n : ℕ} (idx : Fin n) (symbol : Γ) (onEqual onDifferent : TM n) (inp : Tape) (work : Fin n → Tape) (out : Tape) {t : ℕ} {c' : Cfg n onDifferent.Q} (hdifferent : (work idx).read ≠ symbol) (hinp : inp.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (work i).read ≠ Γ.start) (hout : out.read ≠ Γ.start) (hreach : onDifferent.reachesIn t { state := onDifferent.qstart, input := inp, work := work, output := out } c') (hhalt : onDifferent.halted c') : ∃ (C : Cfg n (branchWorkSymbolTM idx symbol onEqual onDifferent).Q), (branchWorkSymbolTM idx symbol onEqual onDifferent).reachesIn (t + 1) { state := (branchWorkSymbolTM idx symbol onEqual onDifferent).qstart, input := inp, work := work, output := out } C ∧ (branchWorkSymbolTM idx symbol onEqual onDifferent).halted C ∧ C.input = c'.input ∧ C.work = c'.work ∧ C.output = c'.output

theorem Complexity.TM.IsTransducer.branchWorkSymbolTM_internal {n : ℕ} {idx : Fin n} {symbol : Γ} {onEqual onDifferent : TM n} (hequal : onEqual.IsTransducer) (hdifferent : onDifferent.IsTransducer) : (branchWorkSymbolTM idx symbol onEqual onDifferent).IsTransducer