proposition: Lemma Invariant : forall t : nat, t <= size -> BV_to_nat (appbv (stripbv (R1 t) (size - t)) (R2 t)) = BV_to_nat V2 * BV_to_nat (truncbv V1 t).
proof: Proof. simple induction t. intros. elim minus_n_O. apply Invariant_t_O. intros. rewrite <- (app_trunc_elemlist bool). replace (elemlist bool V1 n) with (abit V1 n). rewrite <- (R1_lem3 n). rewrite R1_eq2. rewrite R2_eq2. rewrite <- lowbit_is_abit. case (lowbit (R1 n)). replace (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) with (abit (BV_full_adder_sum (R2 n) V2 false) 0). apply inv_ind_true. auto with arith. intros. apply H. exact H1. exact H0. apply le_Sn_le; exact H0. unfold abit in |- *. rewrite lowbit_is_trunc. unfold elemlist in |- *. rewrite (strip_O bool). trivial with arith. apply (not_nil bool). rewrite length_BV_full_adder_sum. rewrite length_R2. exact size_not_O. apply le_Sn_le; exact H0. rewrite length_R2. rewrite length_V2_size. trivial with arith. apply le_Sn_le; exact H0. replace (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) with (abit (BV_full_adder_sum (R2 n) V2 false) 0). apply inv_ind_false. trivial with arith. exact H. exact H0. apply le_Sn_le; exact H0. rewrite lowbit_is_trunc. unfold abit in |- *. unfold elemlist in |- *. rewrite (strip_O bool). trivial with arith. apply (not_nil bool). rewrite length_BV_full_adder_sum. rewrite length_R2; auto with arith. transitivity size. rewrite length_R2; trivial with arith. apply le_Sn_le; exact H0. auto with arith. apply (not_nil bool). rewrite length_R1; auto with arith. auto with arith. auto with arith. replace (length V1) with (lengthbv V1). rewrite length_V1_size. exact H0. auto with arith. Qed.
imports: Definitions LemPrelim AdderProof