Documentation

Complexitylib.Models.TuringMachine.Subroutines.BinaryRippleAdd.Internal.Sem

Linear-time canonical binary addition -- composed semantics #

This file composes the one-pass full-adder scan with the three checked rewind contracts. The resulting machine restores both operands, returns a canonical sum, preserves the complete external tape frame, and carries explicit time and all-prefix auxiliary-space bounds.

source
def Complexity.TM.binaryRippleAddPost {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) (lhs rhs : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) :
TapePred n

Postcondition for completed binary ripple addition.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.TM.binaryRippleAddTM_hoareTime_frame_internal {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) (hdistinct : BinaryRippleAddDistinct lhsIdx rhsIdx resultIdx) (lhs rhs : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hlhs : (work₀ lhsIdx).HasBinaryNat lhs) (hrhs : (work₀ rhsIdx).HasBinaryNat rhs) (hresult : (work₀ resultIdx).HasBinaryNat 0) (hinput : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → Parked (work₀ i)) (houtput : Parked out₀) :
    (binaryRippleAddTM lhsIdx rhsIdx resultIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (binaryRippleAddPost lhsIdx rhsIdx resultIdx lhs rhs inp₀ work₀ out₀) (binaryRippleAddTime lhs rhs)
    source
    theorem Complexity.TM.binaryRippleAddTM_hoareTimeSpace_frame_internal {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) (hdistinct : BinaryRippleAddDistinct lhsIdx rhsIdx resultIdx) (lhs rhs inputLength initialSpace : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hlhs : (work₀ lhsIdx).HasBinaryNat lhs) (hrhs : (work₀ rhsIdx).HasBinaryNat rhs) (hresult : (work₀ resultIdx).HasBinaryNat 0) (hinput : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → Parked (work₀ i)) (houtput : Parked out₀) (hinitial : { state := (binaryRippleAddTM lhsIdx rhsIdx resultIdx).qstart, input := inp₀, work := work₀, output := out₀ }.WithinAuxSpace inputLength initialSpace) :
    (binaryRippleAddTM lhsIdx rhsIdx resultIdx).HoareTimeSpace (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (binaryRippleAddPost lhsIdx rhsIdx resultIdx lhs rhs inp₀ work₀ out₀) (binaryRippleAddTime lhs rhs) inputLength (initialSpace + binaryRippleAddTime lhs rhs)