Canonical binary count-up loops — internal proofs

Aggregation module for the comparison controller, certified loop induction, all-prefix space bound, and transducer proof.