proposition: Lemma BV_increment_adder : forall v : BV, appbv (BV_increment v) (consbv (BV_increment_carry v) nilbv) = BV_full_adder v nilbv true.
proof: Proof. simple induction v. simpl in |- *. unfold BV_full_adder in |- *. unfold nilbv, consbv, appbv in |- *. simpl in |- *. trivial. simple induction a. intros. unfold consbv, nilbv, appbv in |- *. simpl in |- *. unfold consbv, nilbv, appbv in H. rewrite H. unfold BV_full_adder in |- *. simpl in |- *. replace (half_adder_sum true true) with false. trivial. auto. unfold BV_full_adder in |- *. unfold consbv, nilbv, appbv in |- *. intros. simpl in |- *. replace (half_adder_sum false true) with true. replace (BV_full_adder_sum l nil false) with l. replace (BV_full_adder_carry l nil false) with false. trivial. auto. auto. auto. Qed.
imports: AdderProof