Exact marked-input and output decoding identities

Copying a binary word in order builds the stack representation of its reverse. Reading a clean final stack tape in order likewise emits the reversed stack. Both identities include the single marker cell used for an empty stack.

theorem Complexity.MathlibTM2.binaryAdapter_input (tm : Turing.FinTM2) [(k : tm.K) → Fintype (tm.Γ k)] (input : tm.Γ tm.k₀ ≃ Bool) (output : tm.Γ tm.k₁ ≃ Bool) {Q : Type} [Fintype Q] [Inhabited Q] (G : Turing.TM0.Machine (Turing.TM2to1.Γ' tm.K tm.Γ) Q) (w : List Bool) : (binaryAdapter tm input output G).inputCells true w = Turing.TM2to1.trInit tm.k₀ (List.map (⇑input.symm) w.reverse)

theorem Complexity.MathlibTM2.decode_trInit {K α : Type} [DecidableEq K] {Γ : K → Type} (k : K) (e : Γ k ≃ α) (w : List (Γ k)) (j : ℕ) : Option.map (⇑e) (((Turing.Tape.mk₁ (Turing.TM2to1.trInit k w)).nth ↑j).2 k) = (List.map (⇑e) w.reverse)[j]?