(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************)
(*           The Calculus of Inductive Constructions            *)
(*                       COQ v5.10                              *)
(*                                                              *)
(* Laurent Arditi.  Laboratoire I3S. CNRS ura 1376.             *)
(* Universite de Nice - Sophia Antipolis                        *)
(* arditi@unice.fr, http://wwwi3s.unice.fr/~arditi/lolo.html    *)
(*                                                              *)
(* date: july 1995                                              *)
(* file: MultSeq.v                                              *)
(* contents: VERIFICATION OF A SEQUENTIAL MULTIPLIER.           *)
(* Proofs of the invariant and the final theorem                *)
(****************************************************************)

Require Import Definitions.
Require Import LemPrelim.
Require Import AdderProof.


(* L'invariant est :
si t<= size alors nat(R1(t)[size-t:size-1]@R2(t))=nat(V2)*nat(V1[0:t-1])
*)

(****************************************************************)
(* D'abord on prouve l'invariant pour t=O: *)

Lemma Invariant_t_O :
 BV_to_nat (appbv (stripbv (R1 0) size) (R2 0)) =
 BV_to_nat V2 * BV_to_nat (truncbv V1 0).
(* Goal: @eq nat (BV_to_nat (appbv (R1 size) (R2 size))) (Nat.mul (BV_to_nat V2) (BV_to_nat V1)) *)
intros. simpl in |- *.
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.add (S O) (Nat.sub size (S n))))) (Nat.mul (power2 (Nat.sub size (Nat.add (S O) (Nat.sub size (S n))))) (BV_to_nat (strip bool (abit (BV_full_adder_sum (R2 n) V2 false) O) (Nat.sub (Nat.sub size (S n)) (Nat.sub size (S O))))))) (Nat.add (Nat.mul (power2 (S n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (power2 (S n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (BV_to_nat (appbv (stripbv (R1 n) (Nat.sub size n)) (R2 n))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite BV_to_nat_app2. rewrite (trunc_O bool). rewrite <- length_V1_size.
(* Goal: @eq nat (Nat.add (BV_to_nat (stripbv V1 (lengthbv V1))) (Nat.mul (power2 (lengthbv (stripbv V1 (lengthbv V1)))) (BV_to_nat (BV_null (lengthbv V1))))) (Nat.mul (BV_to_nat V2) (BV_to_nat (@nil bool))) *)
rewrite (strip_all bool). rewrite length_V1_size.
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
simpl in |- *. elim plus_n_O. elim mult_n_O. rewrite BV_null_nat. trivial with arith.
Qed.

(****************************************************************)
(* Ensuite, lors de la preuve par induction pour t quelconque,
   on doit faire une preuve par cas selon R1[0].
   On fait la preuve pour R1[0]=false:  (assez long)
*)

Lemma inv_ind_false :
 forall t n : nat,
 (n <= size ->
  BV_to_nat (appbv (stripbv (R1 n) (size - n)) (R2 n)) =
  BV_to_nat V2 * BV_to_nat (truncbv V1 n)) ->
 S n <= size ->
 n <= size ->
 BV_to_nat
   (appbv
      (stripbv
         (appbv (highs (R1 n))
            (Mux false (abit (BV_full_adder_sum (R2 n) V2 false) 0)
               (consbv (lowbit (R2 n)) nilbv))) (size - S n))
      (appbv (highs (Mux false (BV_full_adder_sum (R2 n) V2 false) (R2 n)))
         (Mux false (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv)
            (consbv false nilbv)))) =
 BV_to_nat V2 * BV_to_nat (appbv (truncbv V1 n) (consbv false nilbv)).
(* Goal: @eq nat (BV_to_nat (appbv (R1 size) (R2 size))) (Nat.mul (BV_to_nat V2) (BV_to_nat V1)) *)
intros.
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
simpl in |- *.
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.add (S O) (Nat.sub size (S n))))) (Nat.mul (power2 (Nat.sub size (Nat.add (S O) (Nat.sub size (S n))))) (BV_to_nat (strip bool (abit (BV_full_adder_sum (R2 n) V2 false) O) (Nat.sub (Nat.sub size (S n)) (Nat.sub size (S O))))))) (Nat.add (Nat.mul (power2 (S n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (power2 (S n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (BV_to_nat (appbv (stripbv (R1 n) (Nat.sub size n)) (R2 n))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
do 3 rewrite BV_to_nat_app2.
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
simpl in |- *.
(* Goal: @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (R2 n))) (Nat.mul (BV_to_nat V2) (power2 n))) (Nat.add (Nat.add (Nat.mul (power2 n) (BV_to_nat (R2 n))) (Nat.mul (power2 n) (BV_to_nat V2))) (Nat.mul (power2 n) O)) *)
(* Goal: @eq BV (BV_full_adder (R2 n) V2 false) (appbv (BV_full_adder_sum (R2 n) V2 false) (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv)) *)
(* Goal: @eq nat (BV_to_nat (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv)) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)) *)
(* Goal: @eq nat (lengthbv (BV_full_adder_sum (R2 n) V2 false)) size *)
(* Goal: not (@eq nat (lengthbv (BV_full_adder_sum (R2 n) V2 false)) O) *)
(* Goal: not (@eq BV (BV_full_adder_sum (R2 n) V2 false) nilbv) *)
(* Goal: @eq nat (Nat.add n size) (S (Nat.add n (Nat.sub size (S O)))) *)
(* Goal: @eq nat (power2 n) (Nat.mul (power2 n) (S O)) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
elim mult_n_O.
(* Goal: @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (R2 n))) (Nat.mul (BV_to_nat V2) (power2 n))) (Nat.add (Nat.add (Nat.mul (power2 n) (BV_to_nat (R2 n))) (Nat.mul (power2 n) (BV_to_nat V2))) (Nat.mul (power2 n) O)) *)
(* Goal: @eq BV (BV_full_adder (R2 n) V2 false) (appbv (BV_full_adder_sum (R2 n) V2 false) (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv)) *)
(* Goal: @eq nat (BV_to_nat (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv)) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)) *)
(* Goal: @eq nat (lengthbv (BV_full_adder_sum (R2 n) V2 false)) size *)
(* Goal: not (@eq nat (lengthbv (BV_full_adder_sum (R2 n) V2 false)) O) *)
(* Goal: not (@eq BV (BV_full_adder_sum (R2 n) V2 false) nilbv) *)
(* Goal: @eq nat (Nat.add n size) (S (Nat.add n (Nat.sub size (S O)))) *)
(* Goal: @eq nat (power2 n) (Nat.mul (power2 n) (S O)) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
elim mult_n_O.
(* Goal: @eq nat (power2 n) (Nat.add (power2 n) O) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
elim plus_n_O.
(* Goal: @eq nat (power2 n) (Nat.add (power2 n) O) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
elim plus_n_O.
(* Goal: le (Nat.sub size (S n)) (Nat.add (@length bool (stripbv (R1 n) (S O))) (@length bool (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite (length_strip bool).
(* Goal: @eq nat (Nat.add (BV_to_nat (stripbv (appbv (highs (R1 n)) (abit (BV_full_adder_sum (R2 n) V2 false) O)) (Nat.sub size (S n)))) (Nat.add (Nat.mul (power2 (lengthbv (stripbv (appbv (highs (R1 n)) (abit (BV_full_adder_sum (R2 n) V2 false) O)) (Nat.sub size (S n))))) (BV_to_nat (highs (BV_full_adder_sum (R2 n) V2 false)))) (Nat.mul (power2 (lengthbv (stripbv (appbv (highs (R1 n)) (abit (BV_full_adder_sum (R2 n) V2 false) O)) (Nat.sub size (S n))))) (Nat.mul (power2 (lengthbv (highs (BV_full_adder_sum (R2 n) V2 false)))) (Nat.add (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)) O))))) (Nat.add (Nat.mul (BV_to_nat V2) (BV_to_nat (truncbv V1 n))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 (lengthbv (truncbv V1 n))) (S O)))) *)
rewrite <- H.
(* Goal: @eq nat (Nat.add (BV_to_nat (stripbv (appbv (highs (R1 n)) (abit (BV_full_adder_sum (R2 n) V2 false) O)) (Nat.sub size (S n)))) (Nat.add (Nat.mul (power2 (lengthbv (stripbv (appbv (highs (R1 n)) (abit (BV_full_adder_sum (R2 n) V2 false) O)) (Nat.sub size (S n))))) (BV_to_nat (highs (BV_full_adder_sum (R2 n) V2 false)))) (Nat.mul (power2 (lengthbv (stripbv (appbv (highs (R1 n)) (abit (BV_full_adder_sum (R2 n) V2 false) O)) (Nat.sub size (S n))))) (Nat.mul (power2 (lengthbv (highs (BV_full_adder_sum (R2 n) V2 false)))) (Nat.add (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)) O))))) (Nat.add (BV_to_nat (appbv (stripbv (R1 n) (Nat.sub size n)) (R2 n))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 (lengthbv (truncbv V1 n))) (S O)))) *)
(* Goal: le n size *)
clear H.
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite (length_app bool).
(* Goal: @eq nat (Nat.add (BV_to_nat (stripbv (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O)) (Nat.sub size (S n)))) (Nat.add (Nat.mul (power2 (lengthbv (stripbv (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O)) (Nat.sub size (S n))))) (BV_to_nat (highs (BV_full_adder_sum (R2 n) V2 false)))) (Nat.mul (power2 (lengthbv (stripbv (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O)) (Nat.sub size (S n))))) (Nat.mul (power2 (lengthbv (highs (BV_full_adder_sum (R2 n) V2 false)))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (BV_to_nat (appbv (stripbv (R1 n) (Nat.sub size n)) (R2 n))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 (lengthbv (truncbv V1 n))) (S O)))) *)
(* Goal: le n size *)
rewrite highs_is_strip.
(* Goal: le (Nat.sub size (S n)) (Nat.add (@length bool (stripbv (R1 n) (S O))) (@length bool (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite (length_strip bool).
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite length_R1.
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
simpl in |- *.
(* Goal: @eq nat (Nat.add (BV_to_nat (stripbv (appbv (stripbv (R1 n) (S O)) (consbv (lowbit (R2 n)) nilbv)) (Nat.sub size (S n)))) (Nat.mul (power2 (Nat.sub (Nat.add (Nat.sub size (S O)) (S O)) (Nat.sub size (S n)))) (BV_to_nat (highs (R2 n))))) (BV_to_nat (appbv (stripbv (R1 n) (Nat.sub size n)) (R2 n))) *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (highs (R1 n)) (consbv (lowbit (R2 n)) nilbv))) *)
replace (size - 1 + 1) with size.
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (abit (BV_full_adder_sum (R2 n) V2 false) O)))) (Nat.add (Nat.mul (Nat.add (power2 n) (power2 n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (Nat.add (power2 n) (power2 n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (Nat.add (BV_to_nat (stripbv (R1 n) (Nat.sub size n))) (Nat.mul (power2 (Nat.sub size (Nat.sub size n))) (BV_to_nat (R2 n)))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite minus_minus_lem2.
(* Goal: @eq nat (Nat.add (BV_to_nat (stripbv (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O)) (Nat.sub size (S n)))) (Nat.add (Nat.mul (power2 (S n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (power2 (S n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (BV_to_nat (appbv (stripbv (R1 n) (Nat.sub size n)) (R2 n))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite (strip_app bool).
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.add (S O) (Nat.sub size (S n))))) (Nat.mul (power2 (Nat.sub size (Nat.add (S O) (Nat.sub size (S n))))) (BV_to_nat (strip bool (abit (BV_full_adder_sum (R2 n) V2 false) O) (Nat.sub (Nat.sub size (S n)) (Nat.sub size (S O))))))) (Nat.add (Nat.mul (power2 (S n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (power2 (S n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (BV_to_nat (appbv (stripbv (R1 n) (Nat.sub size n)) (R2 n))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite BV_to_nat_app2.
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (stripbv (R1 n) (S O)) (Nat.sub size (S n)))) (Nat.mul (power2 (lengthbv (strip bool (stripbv (R1 n) (S O)) (Nat.sub size (S n))))) (BV_to_nat (strip bool (abit (BV_full_adder_sum (R2 n) V2 false) O) (Nat.sub (Nat.sub size (S n)) (@length bool (stripbv (R1 n) (S O)))))))) (Nat.add (Nat.mul (power2 (S n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (power2 (S n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (BV_to_nat (appbv (stripbv (R1 n) (Nat.sub size n)) (R2 n))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite (strip_strip bool).
(* Goal: le (Nat.sub size (S n)) (Nat.add (@length bool (stripbv (R1 n) (S O))) (@length bool (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite (length_strip bool).
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite length_R1.
(* Goal: le (Nat.sub size (S n)) (Nat.add (@length bool (stripbv (R1 n) (S O))) (@length bool (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite (length_strip bool).
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.add (S O) (Nat.sub size (S n))))) (Nat.mul (power2 (Nat.sub size (Nat.add (S O) (Nat.sub size (S n))))) (BV_to_nat (strip bool (abit (BV_full_adder_sum (R2 n) V2 false) O) (Nat.sub (Nat.sub size (S n)) (Nat.sub size (S O))))))) (Nat.add (Nat.mul (power2 (S n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (power2 (S n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (BV_to_nat (appbv (stripbv (R1 n) (Nat.sub size n)) (R2 n))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite BV_to_nat_app2.
(* Goal: le (Nat.sub size (S n)) (Nat.add (@length bool (stripbv (R1 n) (S O))) (@length bool (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite (length_strip bool).
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite length_R1.
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (abit (BV_full_adder_sum (R2 n) V2 false) O)))) (Nat.add (Nat.mul (Nat.add (power2 n) (power2 n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (Nat.add (power2 n) (power2 n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (Nat.add (BV_to_nat (stripbv (R1 n) (Nat.sub size n))) (Nat.mul (power2 (Nat.sub size (Nat.sub size n))) (BV_to_nat (R2 n)))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite minus_minus_lem2.
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.add (S O) (Nat.sub size (S n))))) (Nat.mul (power2 (Nat.sub size (Nat.add (S O) (Nat.sub size (S n))))) (BV_to_nat (strip bool (consbv (lowbit (R2 n)) nilbv) (Nat.sub (Nat.sub size (S n)) (Nat.sub size (S O))))))) (Nat.mul (power2 (S n)) (BV_to_nat (highs (R2 n))))) (Nat.add (BV_to_nat (stripbv (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (R2 n)))) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (Nat.sub size (S O)) (S O)) *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (highs (R1 n)) (consbv (lowbit (R2 n)) nilbv))) *)
replace (1 + (size - S n)) with (size - n).
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (abit (BV_full_adder_sum (R2 n) V2 false) O)))) (Nat.add (Nat.mul (Nat.add (power2 n) (power2 n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (Nat.add (power2 n) (power2 n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (Nat.add (BV_to_nat (stripbv (R1 n) (Nat.sub size n))) (Nat.mul (power2 (Nat.sub size (Nat.sub size n))) (BV_to_nat (R2 n)))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite minus_minus_lem2.
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.sub (S size) (S n)))) (Nat.mul (power2 (Nat.sub size (Nat.sub (S size) (S n)))) (BV_to_nat (strip bool (abit (BV_full_adder_sum (R2 n) V2 false) O) (Nat.sub (Nat.sub size (S n)) (Nat.sub size (S O))))))) (Nat.add (Nat.mul (Nat.add (power2 n) (power2 n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (Nat.add (power2 n) (power2 n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (Nat.add (BV_to_nat (stripbv (R1 n) (Nat.sub size n))) (Nat.mul (power2 (lengthbv (stripbv (R1 n) (Nat.sub size n)))) (BV_to_nat (R2 n)))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite (minus_le_O (size - S n) (size - 1)).
(* Goal: @eq BV (trunc bool (strip bool (BV_full_adder_sum (R2 n) V2 false) O) (S O)) (truncbv (BV_full_adder_sum (R2 n) V2 false) (S O)) *)
(* Goal: not (@eq BV (BV_full_adder_sum (R2 n) V2 false) nilbv) *)
(* Goal: not (@eq BV (R1 n) nilbv) *)
(* Goal: lt n size *)
(* Goal: @eq BV (abit V1 n) (elemlist bool V1 n) *)
(* Goal: le (S n) (@length bool V1) *)
rewrite (strip_O bool).
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (consbv (lowbit (R2 n)) nilbv)))) (Nat.mul (power2 (S n)) (BV_to_nat (highs (R2 n))))) (Nat.add (BV_to_nat (stripbv (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (R2 n)))) *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le n size *)
(* Goal: @eq nat (Nat.sub size n) (Nat.add (S O) (Nat.sub size (S n))) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (Nat.sub size (S O)) (S O)) *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (highs (R1 n)) (consbv (lowbit (R2 n)) nilbv))) *)
rewrite plus_assoc_reverse.
replace
 (power2 n * BV_to_nat (consbv (lowbit (R2 n)) nilbv) +
  power2 (S n) * BV_to_nat (highs (R2 n))) with (power2 n * BV_to_nat (R2 n)).
(* Goal: @eq nat (BV_to_nat V1) (BV_to_nat V1) *)
trivial with arith. symmetry  in |- *. apply BV_nat_lem1.
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: @eq nat (BV_to_nat (appbv (stripbv (appbv (highs (R1 n)) (Mux false (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) (consbv (lowbit (R2 n)) nilbv))) (Nat.sub size (S n))) (appbv (highs (Mux false (BV_full_adder_sum (R2 n) V2 false) (R2 n))) (Mux false (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv) (consbv false nilbv))))) (Nat.mul (BV_to_nat V2) (BV_to_nat (@app bool (trunc bool V1 n) (consbv false nilbv)))) *)
(* Goal: not (@eq BV (R1 n) nilbv) *)
(* Goal: lt n size *)
(* Goal: @eq BV (abit V1 n) (elemlist bool V1 n) *)
(* Goal: le (S n) (@length bool V1) *)
rewrite length_R2. exact size_not_O. exact H1. apply le_minus_minus; auto with arith.
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
exact H1. simpl in |- *. rewrite minus_Sn_m. auto with arith.
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
exact H0. exact H1. exact H1. rewrite length_R1. auto with arith. exact H1. 
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite length_R1. auto with arith. exact H1. exact H1. rewrite length_R1.
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
simpl in |- *. rewrite minus_Sn_m. simpl in |- *. auto with arith. exact H0. exact H1. 
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
exact H0. rewrite plus_comm. simpl in |- *. rewrite minus_Sn_m; auto with arith.
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
 exact H1. rewrite length_R1. auto with arith. exact H1. exact H1. 
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite (length_app bool). rewrite length_highs. rewrite length_R1.
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
simpl in |- *. rewrite plus_n_SO. replace (pred size) with (size - 1).
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite minus_Sn_m. simpl in |- *. elim minus_n_O. apply minus_le_lem2; auto with arith. auto with arith.
(* Goal: le n size *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: @eq BV (abit (BV_full_adder_sum (R2 n) V2 false) O) (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) *)
(* Goal: @eq nat (BV_to_nat (appbv (stripbv (appbv (highs (R1 n)) (Mux false (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) (consbv (lowbit (R2 n)) nilbv))) (Nat.sub size (S n))) (appbv (highs (Mux false (BV_full_adder_sum (R2 n) V2 false) (R2 n))) (Mux false (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv) (consbv false nilbv))))) (Nat.mul (BV_to_nat V2) (BV_to_nat (@app bool (trunc bool V1 n) (consbv false nilbv)))) *)
(* Goal: not (@eq BV (R1 n) nilbv) *)
(* Goal: lt n size *)
(* Goal: @eq BV (abit V1 n) (elemlist bool V1 n) *)
(* Goal: le (S n) (@length bool V1) *)
apply minus_n_SO. exact H1. apply (not_nil bool). rewrite length_R1; auto with arith.
Qed.

(****************************************************************)
(* Puis pour le cas ou R1[0]=true (tres tres long !!!!!)
*)

Lemma inv_ind_true :
 forall t n : nat,
 (n <= size ->
  BV_to_nat (appbv (stripbv (R1 n) (size - n)) (R2 n)) =
  BV_to_nat V2 * BV_to_nat (truncbv V1 n)) ->
 S n <= size ->
 n <= size ->
 BV_to_nat
   (appbv
      (stripbv
         (appbv (highs (R1 n))
            (Mux true (abit (BV_full_adder_sum (R2 n) V2 false) 0)
               (consbv (lowbit (R2 n)) nilbv))) (size - S n))
      (appbv (highs (Mux true (BV_full_adder_sum (R2 n) V2 false) (R2 n)))
         (Mux true (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv)
            (consbv false nilbv)))) =
 BV_to_nat V2 * BV_to_nat (appbv (truncbv V1 n) (consbv true nilbv)).

(* Goal: @eq nat (BV_to_nat (appbv (R1 size) (R2 size))) (Nat.mul (BV_to_nat V2) (BV_to_nat V1)) *)
intros. simpl in |- *. do 3 rewrite BV_to_nat_app2. simpl in |- *.
(* Goal: @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (R2 n))) (Nat.mul (BV_to_nat V2) (power2 n))) (Nat.add (Nat.mul (power2 n) (Nat.add (BV_to_nat (R2 n)) (BV_to_nat V2))) (Nat.mul (power2 n) (bool_to_nat false))) *)
(* Goal: @eq BV (BV_full_adder (R2 n) V2 false) (appbv (BV_full_adder_sum (R2 n) V2 false) (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv)) *)
(* Goal: @eq nat (BV_to_nat (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv)) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)) *)
(* Goal: @eq nat (lengthbv (BV_full_adder_sum (R2 n) V2 false)) size *)
(* Goal: not (@eq nat (lengthbv (BV_full_adder_sum (R2 n) V2 false)) O) *)
(* Goal: not (@eq BV (BV_full_adder_sum (R2 n) V2 false) nilbv) *)
(* Goal: @eq nat (Nat.add n size) (S (Nat.add n (Nat.sub size (S O)))) *)
(* Goal: @eq nat (power2 n) (Nat.mul (power2 n) (S O)) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite mult_plus_distr2.
rewrite
 (mult_plus_distr2 (BV_to_nat V2) (BV_to_nat (truncbv V1 n))
    (power2 (lengthbv (truncbv V1 n)) * 1)).
(* Goal: @eq nat (power2 n) (Nat.add (power2 n) O) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite <- H. clear H. elim plus_n_O.
(* Goal: @eq nat (Nat.add (BV_to_nat (stripbv (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O)) (Nat.sub size (S n)))) (Nat.add (Nat.mul (power2 (lengthbv (stripbv (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O)) (Nat.sub size (S n))))) (BV_to_nat (highs (BV_full_adder_sum (R2 n) V2 false)))) (Nat.mul (power2 (lengthbv (stripbv (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O)) (Nat.sub size (S n))))) (Nat.mul (power2 (lengthbv (highs (BV_full_adder_sum (R2 n) V2 false)))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (BV_to_nat (appbv (stripbv (R1 n) (Nat.sub size n)) (R2 n))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 (lengthbv (truncbv V1 n))) (S O)))) *)
(* Goal: le n size *)
rewrite highs_is_strip. rewrite highs_is_strip.
(* Goal: le (Nat.sub size (S n)) (Nat.add (@length bool (stripbv (R1 n) (S O))) (@length bool (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite (length_trunc bool). rewrite (length_strip bool).
(* Goal: le (Nat.sub size (S n)) (Nat.add (@length bool (stripbv (R1 n) (S O))) (@length bool (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
 rewrite (length_app bool). rewrite (length_strip bool).
(* Goal: le (Nat.sub size (S n)) (Nat.add (@length bool (stripbv (R1 n) (S O))) (@length bool (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
 rewrite (length_strip bool). rewrite length_abit.
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
 rewrite length_R1. rewrite (plus_comm (size - 1)).
(* Goal: @eq nat (Nat.add (BV_to_nat (stripbv (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O)) (Nat.sub size (S n)))) (Nat.add (Nat.mul (power2 (Nat.sub (PeanoNat.Nat.add (S O) (Nat.sub size (S O))) (Nat.sub size (S n)))) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (power2 (Nat.sub (PeanoNat.Nat.add (S O) (Nat.sub size (S O))) (Nat.sub size (S n)))) (Nat.mul (power2 (Nat.sub (@length bool (BV_full_adder_sum (R2 n) V2 false)) (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (BV_to_nat (appbv (stripbv (R1 n) (Nat.sub size n)) (R2 n))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
 replace (1 + (size - 1)) with size.
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (abit (BV_full_adder_sum (R2 n) V2 false) O)))) (Nat.add (Nat.mul (Nat.add (power2 n) (power2 n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (Nat.add (power2 n) (power2 n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (Nat.add (BV_to_nat (stripbv (R1 n) (Nat.sub size n))) (Nat.mul (power2 (Nat.sub size (Nat.sub size n))) (BV_to_nat (R2 n)))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite minus_minus_lem2. rewrite length_BV_full_adder_sum.
(* Goal: @eq nat (Nat.add (BV_to_nat (stripbv (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O)) (Nat.sub size (S n)))) (Nat.add (Nat.mul (power2 (S n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (power2 (S n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (BV_to_nat (appbv (stripbv (R1 n) (Nat.sub size n)) (R2 n))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite length_R2. rewrite (strip_app bool).
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.add (S O) (Nat.sub size (S n))))) (Nat.mul (power2 (Nat.sub size (Nat.add (S O) (Nat.sub size (S n))))) (BV_to_nat (strip bool (abit (BV_full_adder_sum (R2 n) V2 false) O) (Nat.sub (Nat.sub size (S n)) (Nat.sub size (S O))))))) (Nat.add (Nat.mul (power2 (S n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (power2 (S n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (BV_to_nat (appbv (stripbv (R1 n) (Nat.sub size n)) (R2 n))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
 rewrite BV_to_nat_app2. rewrite (strip_strip bool).
(* Goal: le (Nat.sub size (S n)) (Nat.add (@length bool (stripbv (R1 n) (S O))) (@length bool (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
 rewrite (length_strip bool). rewrite (length_strip bool).
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.add (S O) (Nat.sub size (S n))))) (Nat.mul (power2 (Nat.sub size (Nat.add (S O) (Nat.sub size (S n))))) (BV_to_nat (strip bool (abit (BV_full_adder_sum (R2 n) V2 false) O) (Nat.sub (Nat.sub size (S n)) (Nat.sub size (S O))))))) (Nat.add (Nat.mul (power2 (S n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (power2 (S n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (BV_to_nat (appbv (stripbv (R1 n) (Nat.sub size n)) (R2 n))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
 rewrite length_R1. rewrite BV_to_nat_app2.
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
simpl in |- *. rewrite minus_Sn_m.
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.sub (S size) (S n)))) (Nat.mul (power2 (Nat.sub size (Nat.sub (S size) (S n)))) (BV_to_nat (strip bool (abit (BV_full_adder_sum (R2 n) V2 false) O) (Nat.sub (Nat.sub size (S n)) (Nat.sub size (S O))))))) (Nat.add (Nat.mul (Nat.add (power2 n) (power2 n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (Nat.add (power2 n) (power2 n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (Nat.add (BV_to_nat (stripbv (R1 n) (Nat.sub size n))) (Nat.mul (power2 (lengthbv (stripbv (R1 n) (Nat.sub size n)))) (BV_to_nat (R2 n)))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
 rewrite (minus_le_O (size - S n) (size - 1)).
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
simpl in |- *. rewrite minus_minus_lem2.
(* Goal: le (Nat.sub size (S n)) (Nat.add (@length bool (stripbv (R1 n) (S O))) (@length bool (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
 rewrite (strip_O bool). rewrite (length_strip bool).
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
 rewrite length_R1. rewrite minus_minus_lem2.
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (abit (BV_full_adder_sum (R2 n) V2 false) O)))) (Nat.add (Nat.mul (Nat.add (power2 n) (power2 n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (Nat.add (power2 n) (power2 n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (Nat.add (BV_to_nat (stripbv (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (R2 n)))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
replace (power2 n + power2 n) with (power2 (S n)).
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (abit (BV_full_adder_sum (R2 n) V2 false) O)))) (Nat.add (Nat.mul (power2 (S n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (power2 (S n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (Nat.add (BV_to_nat (stripbv (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (R2 n)))) (Nat.mul (BV_to_nat V2) (Nat.mul (power2 n) (S O)))) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
replace (power2 n * 1) with (power2 n).
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (abit (BV_full_adder_sum (R2 n) V2 false) O)))) (Nat.add (Nat.mul (power2 (S n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (power2 (S n)) (Nat.mul (power2 (Nat.sub size (S O))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))))) (Nat.add (Nat.add (BV_to_nat (stripbv (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (R2 n)))) (Nat.mul (BV_to_nat V2) (power2 n))) *)
(* Goal: @eq nat (power2 n) (Nat.mul (power2 n) (S O)) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
 rewrite <- (mult_assoc_reverse (power2 (S n))).
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite <- power2_plus. simpl in |- *. rewrite <- power2_eq2. rewrite <- power2_eq2.
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (abit (BV_full_adder_sum (R2 n) V2 false) O)))) (Nat.add (Nat.mul (power2 (S n)) (BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (power2 (S (Nat.add n (Nat.sub size (S O))))) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false))))) (Nat.add (Nat.add (BV_to_nat (stripbv (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (R2 n)))) (Nat.mul (BV_to_nat V2) (power2 n))) *)
(* Goal: @eq nat (power2 n) (Nat.mul (power2 n) (S O)) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
replace (S (n + (size - 1))) with (n + size).
(* Goal: @eq nat (Nat.add (Nat.add (BV_to_nat (strip bool (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (consbv (lowbit (R2 n)) nilbv)))) (Nat.mul (power2 (S n)) (BV_to_nat (highs (R2 n))))) (Nat.add (BV_to_nat (stripbv (R1 n) (Nat.sub size n))) (Nat.mul (power2 n) (BV_to_nat (R2 n)))) *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le n size *)
(* Goal: @eq nat (Nat.sub size n) (Nat.add (S O) (Nat.sub size (S n))) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (Nat.sub size (S O)) (S O)) *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (highs (R1 n)) (consbv (lowbit (R2 n)) nilbv))) *)
repeat rewrite plus_assoc_reverse.
replace
 (power2 n * BV_to_nat (abit (BV_full_adder_sum (R2 n) V2 false) 0) +
  (power2 (S n) * BV_to_nat (stripbv (BV_full_adder_sum (R2 n) V2 false) 1) +
   power2 (n + size) * bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))
 with (power2 n * BV_to_nat (R2 n) + BV_to_nat V2 * power2 n).
(* Goal: @eq nat (BV_to_nat V1) (BV_to_nat V1) *)
trivial with arith. rewrite plus_assoc. rewrite <- highs_is_strip.
(* Goal: @eq BV (trunc bool (strip bool (BV_full_adder_sum (R2 n) V2 false) O) (S O)) (truncbv (BV_full_adder_sum (R2 n) V2 false) (S O)) *)
(* Goal: not (@eq BV (BV_full_adder_sum (R2 n) V2 false) nilbv) *)
(* Goal: not (@eq BV (R1 n) nilbv) *)
(* Goal: lt n size *)
(* Goal: @eq BV (abit V1 n) (elemlist bool V1 n) *)
(* Goal: le (S n) (@length bool V1) *)
 unfold abit in |- *. unfold elemlist in |- *. rewrite (strip_O bool).
(* Goal: @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (R2 n))) (Nat.mul (BV_to_nat V2) (power2 n))) (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.mul (power2 n) (BV_to_nat (trunc bool (BV_full_adder_sum (R2 n) V2 false) (S O)))) (Nat.mul (power2 (S n)) (BV_to_nat (highs (BV_full_adder_sum (R2 n) V2 false))))) (Nat.mul (power2 (Nat.add n size)) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))) *)
(* Goal: @eq nat (Nat.add n size) (S (Nat.add n (Nat.sub size (S O)))) *)
(* Goal: @eq nat (power2 n) (Nat.mul (power2 n) (S O)) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite <- lowbit_is_trunc. rewrite BV_nat_lem1. rewrite power2_plus.
(* Goal: @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (R2 n))) (Nat.mul (BV_to_nat V2) (power2 n))) (PeanoNat.Nat.add (Nat.mul (power2 n) (BV_to_nat (BV_full_adder_sum (R2 n) V2 false))) (Nat.mul (Nat.mul (power2 n) (power2 size)) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)))) *)
(* Goal: not (@eq nat (lengthbv (BV_full_adder_sum (R2 n) V2 false)) O) *)
(* Goal: not (@eq BV (BV_full_adder_sum (R2 n) V2 false) nilbv) *)
(* Goal: @eq nat (Nat.add n size) (S (Nat.add n (Nat.sub size (S O)))) *)
(* Goal: @eq nat (power2 n) (Nat.mul (power2 n) (S O)) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
 rewrite (mult_assoc_reverse (power2 n)). rewrite <- mult_plus_distr2.
(* Goal: @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (R2 n))) (Nat.mul (BV_to_nat V2) (power2 n))) (Nat.mul (power2 n) (Nat.add (BV_to_nat (BV_full_adder_sum (R2 n) V2 false)) (Nat.mul (power2 size) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false))))) *)
(* Goal: not (@eq nat (lengthbv (BV_full_adder_sum (R2 n) V2 false)) O) *)
(* Goal: not (@eq BV (BV_full_adder_sum (R2 n) V2 false) nilbv) *)
(* Goal: @eq nat (Nat.add n size) (S (Nat.add n (Nat.sub size (S O)))) *)
(* Goal: @eq nat (power2 n) (Nat.mul (power2 n) (S O)) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
replace size with (lengthbv (BV_full_adder_sum (R2 n) V2 false)).
replace (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)) with
 (BV_to_nat (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv)).
(* Goal: @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (R2 n))) (Nat.mul (BV_to_nat V2) (power2 n))) (Nat.mul (power2 n) (Nat.add (BV_to_nat (BV_full_adder_sum (R2 n) V2 false)) (Nat.mul (power2 (lengthbv (BV_full_adder_sum (R2 n) V2 false))) (BV_to_nat (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv))))) *)
(* Goal: @eq nat (BV_to_nat (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv)) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)) *)
(* Goal: @eq nat (lengthbv (BV_full_adder_sum (R2 n) V2 false)) size *)
(* Goal: not (@eq nat (lengthbv (BV_full_adder_sum (R2 n) V2 false)) O) *)
(* Goal: not (@eq BV (BV_full_adder_sum (R2 n) V2 false) nilbv) *)
(* Goal: @eq nat (Nat.add n size) (S (Nat.add n (Nat.sub size (S O)))) *)
(* Goal: @eq nat (power2 n) (Nat.mul (power2 n) (S O)) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite <- BV_to_nat_app2.
replace
 (appbv (BV_full_adder_sum (R2 n) V2 false)
    (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv)) with
 (BV_full_adder (R2 n) V2 false).
(* Goal: @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (R2 n))) (Nat.mul (BV_to_nat V2) (power2 n))) (Nat.mul (power2 n) (BV_to_nat (BV_full_adder (R2 n) V2 false))) *)
(* Goal: @eq BV (BV_full_adder (R2 n) V2 false) (appbv (BV_full_adder_sum (R2 n) V2 false) (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv)) *)
(* Goal: @eq nat (BV_to_nat (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv)) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)) *)
(* Goal: @eq nat (lengthbv (BV_full_adder_sum (R2 n) V2 false)) size *)
(* Goal: not (@eq nat (lengthbv (BV_full_adder_sum (R2 n) V2 false)) O) *)
(* Goal: not (@eq BV (BV_full_adder_sum (R2 n) V2 false) nilbv) *)
(* Goal: @eq nat (Nat.add n size) (S (Nat.add n (Nat.sub size (S O)))) *)
(* Goal: @eq nat (power2 n) (Nat.mul (power2 n) (S O)) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite BV_full_adder_ok.
(* Goal: @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (R2 n))) (Nat.mul (BV_to_nat V2) (power2 n))) (Nat.add (Nat.mul (power2 n) (Nat.add (BV_to_nat (R2 n)) (BV_to_nat V2))) (Nat.mul (power2 n) (bool_to_nat false))) *)
(* Goal: @eq BV (BV_full_adder (R2 n) V2 false) (appbv (BV_full_adder_sum (R2 n) V2 false) (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv)) *)
(* Goal: @eq nat (BV_to_nat (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv)) (bool_to_nat (BV_full_adder_carry (R2 n) V2 false)) *)
(* Goal: @eq nat (lengthbv (BV_full_adder_sum (R2 n) V2 false)) size *)
(* Goal: not (@eq nat (lengthbv (BV_full_adder_sum (R2 n) V2 false)) O) *)
(* Goal: not (@eq BV (BV_full_adder_sum (R2 n) V2 false) nilbv) *)
(* Goal: @eq nat (Nat.add n size) (S (Nat.add n (Nat.sub size (S O)))) *)
(* Goal: @eq nat (power2 n) (Nat.mul (power2 n) (S O)) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
 rewrite mult_plus_distr2. rewrite mult_plus_distr2.
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
simpl in |- *. elim mult_n_O. elim plus_n_O. rewrite (mult_sym (BV_to_nat V2)).
(* Goal: @eq nat (BV_to_nat V1) (BV_to_nat V1) *)
 trivial with arith. unfold BV_full_adder in |- *. trivial with arith. 
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
simpl in |- *. elim plus_n_O. trivial with arith. rewrite length_BV_full_adder_sum; auto with arith.
(* Goal: le size size *)
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
rewrite length_R2; auto with arith. rewrite length_BV_full_adder_sum; auto with arith.
(* Goal: le size size *)
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
rewrite length_R2; auto with arith. rewrite length_R2; auto with arith. 
(* Goal: le size size *)
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
apply (not_nil bool); auto with arith. rewrite length_BV_full_adder_sum; auto with arith.
(* Goal: le size size *)
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
 rewrite length_R2; auto with arith. rewrite length_R2; auto with arith. 
(* Goal: @eq nat (Nat.add n size) (S (Nat.add n (Nat.sub size (S O)))) *)
(* Goal: @eq nat (power2 n) (Nat.mul (power2 n) (S O)) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
replace (S (n + (size - 1))) with (S n + (size - 1)).
(* Goal: @eq nat (Nat.add n size) (Nat.add (S n) (Nat.sub size (S O))) *)
(* Goal: @eq nat (Nat.add (S n) (Nat.sub size (S O))) (S (Nat.add n (Nat.sub size (S O)))) *)
(* Goal: @eq nat (power2 n) (Nat.mul (power2 n) (S O)) *)
(* Goal: @eq nat (power2 (S n)) (Nat.add (power2 n) (power2 n)) *)
(* Goal: le n size *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size n) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: le (Nat.sub size (S n)) (Nat.sub size (S O)) *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
replace (S n + (size - 1)) with (n + S (size - 1)).
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite minus_Sn_m. simpl in |- *. elim minus_n_O. trivial with arith. 
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
auto with arith. rewrite plus_comm. simpl in |- *. rewrite plus_comm. trivial with arith.
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
simpl in |- *. trivial with arith. rewrite mult_sym. simpl in |- *. elim plus_n_O.
(* Goal: @eq nat (BV_to_nat V1) (BV_to_nat V1) *)
trivial with arith. auto with arith. exact H1. exact H1. rewrite length_R1; auto with arith.
(* Goal: le n size *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: @eq BV (abit (BV_full_adder_sum (R2 n) V2 false) O) (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) *)
(* Goal: @eq nat (BV_to_nat (appbv (stripbv (appbv (highs (R1 n)) (Mux false (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) (consbv (lowbit (R2 n)) nilbv))) (Nat.sub size (S n))) (appbv (highs (Mux false (BV_full_adder_sum (R2 n) V2 false) (R2 n))) (Mux false (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv) (consbv false nilbv))))) (Nat.mul (BV_to_nat V2) (BV_to_nat (@app bool (trunc bool V1 n) (consbv false nilbv)))) *)
(* Goal: not (@eq BV (R1 n) nilbv) *)
(* Goal: lt n size *)
(* Goal: @eq BV (abit V1 n) (elemlist bool V1 n) *)
(* Goal: le (S n) (@length bool V1) *)
 exact H1. apply le_minus_minus. auto with arith. exact H0. exact H1.
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.add (S O) (Nat.sub size (S n))) (@length bool (R1 n)) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: le (S n) size *)
(* Goal: @eq nat size (Nat.add (S O) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le (Nat.sub size (S n)) (@length bool (appbv (stripbv (R1 n) (S O)) (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite length_R1. auto with arith. exact H1. rewrite length_R1; auto with arith.
(* Goal: le n size *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: @eq BV (abit (BV_full_adder_sum (R2 n) V2 false) O) (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) *)
(* Goal: @eq nat (BV_to_nat (appbv (stripbv (appbv (highs (R1 n)) (Mux false (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) (consbv (lowbit (R2 n)) nilbv))) (Nat.sub size (S n))) (appbv (highs (Mux false (BV_full_adder_sum (R2 n) V2 false) (R2 n))) (Mux false (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv) (consbv false nilbv))))) (Nat.mul (BV_to_nat V2) (BV_to_nat (@app bool (trunc bool V1 n) (consbv false nilbv)))) *)
(* Goal: not (@eq BV (R1 n) nilbv) *)
(* Goal: lt n size *)
(* Goal: @eq BV (abit V1 n) (elemlist bool V1 n) *)
(* Goal: le (S n) (@length bool V1) *)
exact H1.
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite length_R2; auto with arith. exact H0. simpl in |- *. rewrite minus_Sn_m.
(* Goal: le n size *)
(* Goal: le (S n) size *)
(* Goal: le n size *)
(* Goal: @eq BV (abit (BV_full_adder_sum (R2 n) V2 false) O) (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) *)
(* Goal: @eq nat (BV_to_nat (appbv (stripbv (appbv (highs (R1 n)) (Mux false (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) (consbv (lowbit (R2 n)) nilbv))) (Nat.sub size (S n))) (appbv (highs (Mux false (BV_full_adder_sum (R2 n) V2 false) (R2 n))) (Mux false (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv) (consbv false nilbv))))) (Nat.mul (BV_to_nat V2) (BV_to_nat (@app bool (trunc bool V1 n) (consbv false nilbv)))) *)
(* Goal: not (@eq BV (R1 n) nilbv) *)
(* Goal: lt n size *)
(* Goal: @eq BV (abit V1 n) (elemlist bool V1 n) *)
(* Goal: le (S n) (@length bool V1) *)
auto with arith. auto with arith. exact H1. rewrite length_BV_full_adder_sum; auto with arith.
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: @eq nat (BV_to_nat (appbv (stripbv (appbv (highs (R1 n)) (Mux false (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) (consbv (lowbit (R2 n)) nilbv))) (Nat.sub size (S n))) (appbv (highs (Mux false (BV_full_adder_sum (R2 n) V2 false) (R2 n))) (Mux false (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv) (consbv false nilbv))))) (Nat.mul (BV_to_nat V2) (BV_to_nat (@app bool (trunc bool V1 n) (consbv false nilbv)))) *)
(* Goal: not (@eq BV (R1 n) nilbv) *)
(* Goal: lt n size *)
(* Goal: @eq BV (abit V1 n) (elemlist bool V1 n) *)
(* Goal: le (S n) (@length bool V1) *)
unfold lt in |- *. rewrite length_R2. auto with arith. exact H1. transitivity size; auto with arith. 
(* Goal: le size size *)
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
rewrite length_BV_full_adder_sum; auto with arith. rewrite length_R2; auto with arith.
(* Goal: le size size *)
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
 rewrite length_R2; auto with arith. rewrite length_R1; auto with arith. 
(* Goal: le (Nat.sub size (S n)) (Nat.add (@length bool (stripbv (R1 n) (S O))) (@length bool (abit (BV_full_adder_sum (R2 n) V2 false) O))) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
rewrite (length_app bool). rewrite (length_strip bool).
(* Goal: le size size *)
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
rewrite length_R1; auto with arith. rewrite length_abit. rewrite plus_comm.
(* Goal: le (Nat.sub size (S n)) (Nat.sub (S size) (S O)) *)
(* Goal: le (S O) size *)
(* Goal: lt O (lengthbv (BV_full_adder_sum (R2 n) V2 false)) *)
(* Goal: le (S O) (@length bool (R1 n)) *)
(* Goal: le n (@length bool V1) *)
(* Goal: le n size *)
simpl in |- *. rewrite minus_Sn_m. simpl in |- *. elim minus_n_O. apply minus_le_lem2. auto with arith.
(* Goal: le size size *)
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
rewrite length_BV_full_adder_sum; auto with arith. rewrite length_R2; auto with arith.
(* Goal: le size size *)
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
 rewrite length_R2; auto with arith. rewrite length_R1; auto with arith. 
(* Goal: le size size *)
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
replace (length V1) with (lengthbv V1); auto with arith.
(* Goal: le (S n) (lengthbv V1) *)
(* Goal: @eq nat (lengthbv V1) (@length bool V1) *)
rewrite length_V1_size. exact H1. exact H1. 

Qed.

(****************************************************************)
(* Finalement on prouve le cas general de l'invariant:
*)

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).

(* Goal: @eq nat (BV_to_nat (appbv (R1 size) (R2 size))) (Nat.mul (BV_to_nat V2) (BV_to_nat V1)) *)
simple induction t. intros. elim minus_n_O. apply Invariant_t_O.
(* Goal: @eq nat (BV_to_nat (appbv (R1 size) (R2 size))) (Nat.mul (BV_to_nat V2) (BV_to_nat V1)) *)
intros. rewrite <- (app_trunc_elemlist bool).
(* Goal: @eq nat (BV_to_nat (appbv (stripbv (R1 (S n)) (Nat.sub size (S n))) (R2 (S n)))) (Nat.mul (BV_to_nat V2) (BV_to_nat (@app bool (trunc bool V1 n) (elemlist bool V1 n)))) *)
(* Goal: le (S n) (@length bool V1) *)
replace (elemlist bool V1 n) with (abit V1 n).
(* Goal: @eq nat (BV_to_nat (appbv (stripbv (R1 (S n)) (Nat.sub size (S n))) (R2 (S n)))) (Nat.mul (BV_to_nat V2) (BV_to_nat (@app bool (trunc bool V1 n) (abit V1 n)))) *)
(* Goal: @eq BV (abit V1 n) (elemlist bool V1 n) *)
(* Goal: le (S n) (@length bool V1) *)
rewrite <- (R1_lem3 n). rewrite R1_eq2. rewrite R2_eq2.
(* Goal: @eq nat (BV_to_nat (appbv (stripbv (appbv (highs (R1 n)) (Mux (lowbit (R1 n)) (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) (consbv (lowbit (R2 n)) nilbv))) (Nat.sub size (S n))) (appbv (highs (Mux (lowbit (R1 n)) (BV_full_adder_sum (R2 n) V2 false) (R2 n))) (Mux (lowbit (R1 n)) (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv) (consbv false nilbv))))) (Nat.mul (BV_to_nat V2) (BV_to_nat (@app bool (trunc bool V1 n) (abit (R1 n) O)))) *)
(* Goal: lt n size *)
(* Goal: @eq BV (abit V1 n) (elemlist bool V1 n) *)
(* Goal: le (S n) (@length bool V1) *)
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).
(* Goal: le size size *)
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
apply inv_ind_true. auto with arith.
(* Goal: @eq nat (BV_to_nat (appbv (R1 size) (R2 size))) (Nat.mul (BV_to_nat V2) (BV_to_nat V1)) *)
intros. apply H. exact H1. exact H0.
(* Goal: le (S n) size *)
(* Goal: @eq nat (lengthbv V1) (@length bool V1) *)
apply le_Sn_le; exact H0. unfold abit in |- *. rewrite lowbit_is_trunc.
(* Goal: @eq nat (BV_to_nat V1) (BV_to_nat V1) *)
unfold elemlist in |- *. rewrite (strip_O bool). trivial with arith.
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: @eq nat (BV_to_nat (appbv (stripbv (appbv (highs (R1 n)) (Mux false (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) (consbv (lowbit (R2 n)) nilbv))) (Nat.sub size (S n))) (appbv (highs (Mux false (BV_full_adder_sum (R2 n) V2 false) (R2 n))) (Mux false (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv) (consbv false nilbv))))) (Nat.mul (BV_to_nat V2) (BV_to_nat (@app bool (trunc bool V1 n) (consbv false nilbv)))) *)
(* Goal: not (@eq BV (R1 n) nilbv) *)
(* Goal: lt n size *)
(* Goal: @eq BV (abit V1 n) (elemlist bool V1 n) *)
(* Goal: le (S n) (@length bool V1) *)
apply (not_nil bool). rewrite length_BV_full_adder_sum. rewrite length_R2.
(* Goal: not (@eq nat size O) *)
(* Goal: le n size *)
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: @eq nat (BV_to_nat (appbv (stripbv (appbv (highs (R1 n)) (Mux false (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) (consbv (lowbit (R2 n)) nilbv))) (Nat.sub size (S n))) (appbv (highs (Mux false (BV_full_adder_sum (R2 n) V2 false) (R2 n))) (Mux false (consbv (BV_full_adder_carry (R2 n) V2 false) nilbv) (consbv false nilbv))))) (Nat.mul (BV_to_nat V2) (BV_to_nat (@app bool (trunc bool V1 n) (consbv false nilbv)))) *)
(* Goal: not (@eq BV (R1 n) nilbv) *)
(* Goal: lt n size *)
(* Goal: @eq BV (abit V1 n) (elemlist bool V1 n) *)
(* Goal: le (S n) (@length bool V1) *)
exact size_not_O. apply le_Sn_le; exact H0.
(* Goal: @eq nat (BV_to_nat V1) (BV_to_nat V1) *)
rewrite length_R2. rewrite length_V2_size. trivial with arith.
(* Goal: le (S n) size *)
(* Goal: @eq nat (lengthbv V1) (@length bool V1) *)
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).
(* Goal: @eq nat (BV_to_nat V1) (BV_to_nat V1) *)
apply inv_ind_false. trivial with arith.
(* Goal: le (S n) size *)
(* Goal: @eq nat (lengthbv V1) (@length bool V1) *)
exact H. exact H0. apply le_Sn_le; exact H0. rewrite lowbit_is_trunc.
(* Goal: @eq nat (BV_to_nat V1) (BV_to_nat V1) *)
unfold abit in |- *. unfold elemlist in |- *. rewrite (strip_O bool). trivial with arith.
(* Goal: not (@eq BV (R1 n) nilbv) *)
(* Goal: lt n size *)
(* Goal: @eq BV (abit V1 n) (elemlist bool V1 n) *)
(* Goal: le (S n) (@length bool V1) *)
apply (not_nil bool).
(* Goal: le size size *)
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
rewrite length_BV_full_adder_sum. rewrite length_R2; auto with arith.
(* Goal: @eq nat (lengthbv (R2 n)) (lengthbv V2) *)
(* Goal: not (@eq BV (R1 n) nilbv) *)
(* Goal: lt n size *)
(* Goal: @eq BV (abit V1 n) (elemlist bool V1 n) *)
(* Goal: le (S n) (@length bool V1) *)
transitivity size.
(* Goal: @eq nat (BV_to_nat V1) (BV_to_nat V1) *)
rewrite length_R2; trivial with arith. apply le_Sn_le; exact H0. auto with arith.
(* Goal: le size size *)
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
apply (not_nil bool). rewrite length_R1; auto with arith. auto with arith. auto with arith.
(* Goal: le (S n) (lengthbv V1) *)
(* Goal: @eq nat (lengthbv V1) (@length bool V1) *)
replace (length V1) with (lengthbv V1). rewrite length_V1_size. exact H0.
(* Goal: le size size *)
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
auto with arith.

Qed.

(****************************************************************)
(* Et le theoreme final qui est une specialisation de l'invariant
   avec t=size *)

Theorem Correct :
 BV_to_nat (appbv (R1 size) (R2 size)) = BV_to_nat V2 * BV_to_nat V1.

(* Goal: @eq nat (BV_to_nat (appbv (R1 size) (R2 size))) (Nat.mul (BV_to_nat V2) (BV_to_nat V1)) *)
intros. rewrite <- (strip_O bool (R1 size)).
(* Goal: @eq nat (BV_to_nat (appbv (strip bool (R1 size) O) (R2 size))) (Nat.mul (BV_to_nat V2) (BV_to_nat V1)) *)
replace (BV_to_nat V1) with (BV_to_nat (truncbv V1 size)).
(* Goal: le size size *)
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
rewrite (minus_n_n size). apply Invariant. auto with arith.
(* Goal: @eq nat (BV_to_nat (truncbv V1 size)) (BV_to_nat V1) *)
rewrite <- length_V1_size. rewrite (trunc_all bool). trivial with arith.
Qed.