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