proposition: Lemma R1_eq2 : forall t : nat, R1 (S t) = appbv (highs (R1 t)) (Mux (lowbit (R1 t)) (consbv (lowbit (BV_full_adder_sum (R2 t) V2 false)) nilbv) (consbv (lowbit (R2 t)) nilbv)).
proof: Proof. auto with arith. Qed.
imports: BV Adder Gt