Documentation

Complexitylib.Models.TuringMachine.Subroutines.BinaryRippleAdd.Internal.Out

Linear-time canonical binary addition -- output discipline #

The scan and its rewind wrapper leave the public output tape one-way, so both machines satisfy the transducer discipline required by space-bounded function computation.

source
theorem Complexity.TM.binaryRippleAddScanTM_isTransducer_internal {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) :
(binaryRippleAddScanTM lhsIdx rhsIdx resultIdx).IsTransducer

The ripple-add scan never moves the public output head left.

source
theorem Complexity.TM.binaryRippleAddTM_isTransducer_internal {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) :
(binaryRippleAddTM lhsIdx rhsIdx resultIdx).IsTransducer

The scan followed by all three rewinds remains a transducer.