Documentation

Complexitylib.Models.TuringMachine.Subroutines.BinaryShiftMul.Internal.Out

Width-driven binary shift-and-add multiplication -- output safety #

This file composes the transducer certificates of every multiplication phase.

source
theorem Complexity.TM.binaryShiftMulTM_isTransducer_internal {n : ℕ} (abi : BinaryShiftMulABI n) :
(binaryShiftMulTM abi).IsTransducer

Shift-and-add multiplication never moves the public output head left.