Finite composition of proof-carrying binary routines -- definitions

def Complexity.BinaryRoutine.seqList {n : ℕ} : List (BinaryRoutine n) → BinaryRoutine n

Sequentially compose a fixed finite list of binary routines.

Equations

• Complexity.BinaryRoutine.seqList [] = Complexity.BinaryRoutine.identity
• Complexity.BinaryRoutine.seqList (routine :: routines) = routine.seq (Complexity.BinaryRoutine.seqList routines)

def Complexity.BinaryRoutine.repeatRoutine {n : ℕ} (count : ℕ) (routine : BinaryRoutine n) : BinaryRoutine n

Repeat one binary routine a fixed finite number of times.

Equations

• Complexity.BinaryRoutine.repeatRoutine count routine = Complexity.BinaryRoutine.seqList (List.replicate count routine)