Linear-time canonical binary subtraction -- operand rewind internals

The subtraction core already returns its result to cell one. This module packages the two remaining operand rewinds into one exact framed contract.

def Complexity.TM.binaryRippleSubCanonicalTape (bits : List Bool) : Tape

Canonical parked tape containing the supplied little-endian binary digits.

Equations

• Complexity.TM.binaryRippleSubCanonicalTape bits = (Complexity.Tape.init (List.map Complexity.Γ.ofBool bits)).move Complexity.Dir3.right

theorem Complexity.TM.binaryRippleSubRewindTM_hoareTime_frame_internal {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) (hdistinct : BinaryRippleSubDistinct lhsIdx rhsIdx resultIdx) (lhsBits rhsBits : List Bool) (lhsBound rhsBound : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hlhs : (work₀ lhsIdx).HasBinaryContent lhsBits) (hlhsStart : (work₀ lhsIdx).cells 0 = Γ.start) (hlhsHead : 1 ≤ (work₀ lhsIdx).head ∧ (work₀ lhsIdx).head ≤ lhsBound) (hrhs : (work₀ rhsIdx).HasBinaryContent rhsBits) (hrhsStart : (work₀ rhsIdx).cells 0 = Γ.start) (hrhsHead : 1 ≤ (work₀ rhsIdx).head ∧ (work₀ rhsIdx).head ≤ rhsBound) (hresult : Parked (work₀ resultIdx)) (hinput : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → Parked (work₀ i)) (houtput : Parked out₀) : ((rewindWorkTM lhsIdx).seqTM (rewindWorkTM rhsIdx)).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work lhsIdx = binaryRippleSubCanonicalTape lhsBits ∧ work rhsIdx = binaryRippleSubCanonicalTape rhsBits ∧ work resultIdx = work₀ resultIdx ∧ (∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → work i = work₀ i) ∧ out = out₀) (lhsBound + rhsBound + 5)