(* 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: may 1995                                               *)
(* file: AdderProof                                             *)
(* contents: verification of the adder defined in Adder.v       *)
(*                                                              *)
(****************************************************************)

Require Export Adder.

(****************************************************************)

Lemma BV_full_adder_nil_true_ok :
 forall v : BV, BV_to_nat (BV_full_adder v nilbv true) = S (BV_to_nat v).
(* Goal: forall v : BV, @eq nat (BV_to_nat (BV_full_adder v nilbv true)) (S (BV_to_nat v)) *)
unfold nilbv in |- *. simple induction v; auto with arith. unfold BV_full_adder in |- *. intros.
(* Goal: @eq nat (BV_to_nat (appbv (BV_full_adder_sum (@cons bool a l) (@nil bool) true) (consbv (BV_full_adder_carry (@cons bool a l) (@nil bool) true) nilbv))) (S (BV_to_nat (@cons bool a l))) *)
rewrite BV_full_adder_sum_eq3. rewrite BV_full_adder_carry_eq3.
(* Goal: @eq nat (BV_to_nat (appbv (consbv (half_adder_sum a true) (BV_full_adder_sum l (@nil bool) (half_adder_carry a true))) (consbv (BV_full_adder_carry l (@nil bool) (half_adder_carry a true)) nilbv))) (S (BV_to_nat (@cons bool a l))) *)
rewrite (app_eq2 bool). rewrite half_adder_carry_true.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simpl in |- *. elim a. unfold appbv in H. rewrite H. simpl in |- *. auto with arith.
(* Goal: @eq nat (BV_to_nat (appbv (BV_full_adder_sum (@cons bool a l) nilbv false) (consbv (BV_full_adder_carry (@cons bool a l) nilbv false) nilbv))) (Nat.add (BV_to_nat (@cons bool a l)) (bool_to_nat false)) *)
rewrite BV_full_adder_sum_v_nil_false.
(* Goal: @eq nat (BV_to_nat (appbv (@cons bool a l) (consbv (BV_full_adder_carry (@cons bool a l) nilbv false) nilbv))) (Nat.add (BV_to_nat (@cons bool a l)) (bool_to_nat false)) *)
rewrite BV_full_adder_carry_v_nil_false. rewrite BV_to_nat_app2.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simpl in |- *. elim mult_n_O. elim plus_n_O. trivial with arith.
Qed.


Lemma BV_full_adder_nil_ok :
 forall (v : BV) (cin : bool),
 BV_to_nat (BV_full_adder v nilbv cin) = BV_to_nat v + bool_to_nat cin.

(* Goal: @eq nat (Nat.add (BV_to_nat w) (bool_to_nat cin)) (Nat.add (BV_to_nat w) (bool_to_nat cin)) *)
(* Goal: forall (a : bool) (l : list bool) (_ : forall (w : BV) (cin : bool), @eq nat (BV_to_nat (BV_full_adder l w cin)) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat w)) (bool_to_nat cin))) (w : BV) (cin : bool), @eq nat (BV_to_nat (BV_full_adder (@cons bool a l) w cin)) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat w)) (bool_to_nat cin)) *)
simple induction v. simple induction cin; auto with arith.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simple induction cin. rewrite BV_full_adder_nil_true_ok. simpl in |- *. auto with arith.
(* Goal: forall (a : bool) (l : list bool) (_ : forall (w : BV) (cin : bool), @eq nat (BV_to_nat (BV_full_adder l w cin)) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat w)) (bool_to_nat cin))) (w : BV) (cin : bool), @eq nat (BV_to_nat (BV_full_adder (@cons bool a l) w cin)) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat w)) (bool_to_nat cin)) *)
unfold BV_full_adder in |- *. rewrite BV_full_adder_sum_v_nil_false.
(* Goal: @eq nat (BV_to_nat (appbv (@cons bool a l) (consbv (BV_full_adder_carry (@cons bool a l) nilbv false) nilbv))) (Nat.add (BV_to_nat (@cons bool a l)) (bool_to_nat false)) *)
rewrite BV_full_adder_carry_v_nil_false. rewrite BV_to_nat_app2.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simpl in |- *. elim mult_n_O. elim plus_n_O. trivial with arith.
Qed.

(****************************************************************)

Theorem BV_full_adder_ok :
 forall (v w : BV) (cin : bool),
 BV_to_nat (BV_full_adder v w cin) =
 BV_to_nat v + BV_to_nat w + bool_to_nat cin.
(* Goal: forall (v w : BV) (cin : bool), @eq nat (BV_to_nat (BV_full_adder v w cin)) (Nat.add (Nat.add (BV_to_nat v) (BV_to_nat w)) (bool_to_nat cin)) *)
simple induction v.
(* Goal: forall (a0 : bool) (l0 : list bool) (_ : forall cin : bool, @eq nat (BV_to_nat (appbv (BV_full_adder_sum (@cons bool a l) l0 cin) (consbv (BV_full_adder_carry (@cons bool a l) l0 cin) nilbv))) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat l0)) (bool_to_nat cin))) (cin : bool), @eq nat (BV_to_nat (appbv (BV_full_adder_sum (@cons bool a l) (@cons bool a0 l0) cin) (consbv (BV_full_adder_carry (@cons bool a l) (@cons bool a0 l0) cin) nilbv))) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat (@cons bool a0 l0))) (bool_to_nat cin)) *)
intros.
(* Goal: @eq nat (BV_to_nat (BV_full_adder (@nil bool) w cin)) (Nat.add (Nat.add (BV_to_nat (@nil bool)) (BV_to_nat w)) (bool_to_nat cin)) *)
(* Goal: forall (a : bool) (l : list bool) (_ : forall (w : BV) (cin : bool), @eq nat (BV_to_nat (BV_full_adder l w cin)) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat w)) (bool_to_nat cin))) (w : BV) (cin : bool), @eq nat (BV_to_nat (BV_full_adder (@cons bool a l) w cin)) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat w)) (bool_to_nat cin)) *)
rewrite BV_full_adder_sym.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simpl in |- *.
(* Goal: @eq nat (BV_to_nat (BV_full_adder w (@nil bool) cin)) (Nat.add (BV_to_nat w) (bool_to_nat cin)) *)
(* Goal: forall (a : bool) (l : list bool) (_ : forall (w : BV) (cin : bool), @eq nat (BV_to_nat (BV_full_adder l w cin)) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat w)) (bool_to_nat cin))) (w : BV) (cin : bool), @eq nat (BV_to_nat (BV_full_adder (@cons bool a l) w cin)) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat w)) (bool_to_nat cin)) *)
rewrite BV_full_adder_nil_ok.
(* Goal: @eq nat (Nat.add (BV_to_nat w) (bool_to_nat cin)) (Nat.add (BV_to_nat w) (bool_to_nat cin)) *)
(* Goal: forall (a : bool) (l : list bool) (_ : forall (w : BV) (cin : bool), @eq nat (BV_to_nat (BV_full_adder l w cin)) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat w)) (bool_to_nat cin))) (w : BV) (cin : bool), @eq nat (BV_to_nat (BV_full_adder (@cons bool a l) w cin)) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat w)) (bool_to_nat cin)) *)
auto with arith.

(* Goal: forall (a : bool) (l : list bool) (_ : forall (w : BV) (cin : bool), @eq nat (BV_to_nat (BV_full_adder l w cin)) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat w)) (bool_to_nat cin))) (w : BV) (cin : bool), @eq nat (BV_to_nat (BV_full_adder (@cons bool a l) w cin)) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat w)) (bool_to_nat cin)) *)
unfold BV_full_adder in |- *.
(* Goal: forall (a : bool) (l : list bool) (_ : forall (w : BV) (cin : bool), @eq nat (BV_to_nat (appbv (BV_full_adder_sum l w cin) (consbv (BV_full_adder_carry l w cin) nilbv))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat w)) (bool_to_nat cin))) (w : BV) (cin : bool), @eq nat (BV_to_nat (appbv (BV_full_adder_sum (@cons bool a l) w cin) (consbv (BV_full_adder_carry (@cons bool a l) w cin) nilbv))) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat w)) (bool_to_nat cin)) *)
simple induction w.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simpl in |- *.
(* Goal: forall cin : bool, @eq nat (Nat.add (bool_to_nat (half_adder_sum a cin)) (Nat.add (BV_to_nat (appbv (BV_full_adder_sum l (@nil bool) (half_adder_carry a cin)) (consbv (BV_full_adder_carry l (@nil bool) (half_adder_carry a cin)) nilbv))) (BV_to_nat (appbv (BV_full_adder_sum l (@nil bool) (half_adder_carry a cin)) (consbv (BV_full_adder_carry l (@nil bool) (half_adder_carry a cin)) nilbv))))) (Nat.add (Nat.add (Nat.add (bool_to_nat a) (Nat.add (BV_to_nat l) (BV_to_nat l))) O) (bool_to_nat cin)) *)
(* Goal: forall (a0 : bool) (l0 : list bool) (_ : forall cin : bool, @eq nat (BV_to_nat (appbv (BV_full_adder_sum (@cons bool a l) l0 cin) (consbv (BV_full_adder_carry (@cons bool a l) l0 cin) nilbv))) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat l0)) (bool_to_nat cin))) (cin : bool), @eq nat (BV_to_nat (appbv (BV_full_adder_sum (@cons bool a l) (@cons bool a0 l0) cin) (consbv (BV_full_adder_carry (@cons bool a l) (@cons bool a0 l0) cin) nilbv))) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat (@cons bool a0 l0))) (bool_to_nat cin)) *)
intro.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum a a0 cin)) (Nat.add (BV_to_nat (appbv (BV_full_adder_sum l l0 (full_adder_carry a a0 cin)) (consbv (BV_full_adder_carry l l0 (full_adder_carry a a0 cin)) nilbv))) (BV_to_nat (appbv (BV_full_adder_sum l l0 (full_adder_carry a a0 cin)) (consbv (BV_full_adder_carry l l0 (full_adder_carry a a0 cin)) nilbv))))) (Nat.add (Nat.add (Nat.add (bool_to_nat a) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat cin)) *)
rewrite H.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simpl in |- *.
(* Goal: @eq nat (S (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0))))) (S (Nat.add (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false false true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
elim plus_n_O.
(* Goal: @eq nat (S (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0))))) (S (Nat.add (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false false true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
elim plus_n_O.
replace
 (BV_to_nat l + bool_to_nat (half_adder_carry a cin) +
  (BV_to_nat l + bool_to_nat (half_adder_carry a cin))) with
 (bool_to_nat (half_adder_carry a cin) + bool_to_nat (half_adder_carry a cin) +
  (BV_to_nat l + BV_to_nat l)).
(* Goal: @eq nat (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0)))) (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
repeat rewrite plus_assoc.
replace
 (bool_to_nat (half_adder_sum a cin) + bool_to_nat (half_adder_carry a cin) +
  bool_to_nat (half_adder_carry a cin)) with
 (bool_to_nat (half_adder_sum a cin) +
  (bool_to_nat (half_adder_carry a cin) +
   bool_to_nat (half_adder_carry a cin))).
(* Goal: @eq nat (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (bool_to_nat (half_adder_sum a cin)) (Nat.add (bool_to_nat (half_adder_carry a cin)) (bool_to_nat (half_adder_carry a cin)))) (BV_to_nat l)) (BV_to_nat l)) (Nat.add (PeanoNat.Nat.add (PeanoNat.Nat.add (bool_to_nat a) (BV_to_nat l)) (BV_to_nat l)) (bool_to_nat cin)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (half_adder_sum a cin)) (Nat.add (bool_to_nat (half_adder_carry a cin)) (bool_to_nat (half_adder_carry a cin)))) (Nat.add (Nat.add (bool_to_nat (half_adder_sum a cin)) (bool_to_nat (half_adder_carry a cin))) (bool_to_nat (half_adder_carry a cin))) *)
(* Goal: @eq nat (Nat.add (Nat.add (bool_to_nat (half_adder_carry a cin)) (bool_to_nat (half_adder_carry a cin))) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (Nat.add (BV_to_nat l) (bool_to_nat (half_adder_carry a cin))) (Nat.add (BV_to_nat l) (bool_to_nat (half_adder_carry a cin)))) *)
(* Goal: forall (a0 : bool) (l0 : list bool) (_ : forall cin : bool, @eq nat (BV_to_nat (appbv (BV_full_adder_sum (@cons bool a l) l0 cin) (consbv (BV_full_adder_carry (@cons bool a l) l0 cin) nilbv))) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat l0)) (bool_to_nat cin))) (cin : bool), @eq nat (BV_to_nat (appbv (BV_full_adder_sum (@cons bool a l) (@cons bool a0 l0) cin) (consbv (BV_full_adder_carry (@cons bool a l) (@cons bool a0 l0) cin) nilbv))) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat (@cons bool a0 l0))) (bool_to_nat cin)) *)
rewrite half_adder_ok.
(* Goal: @eq nat (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (bool_to_nat a) (bool_to_nat cin)) (BV_to_nat l)) (BV_to_nat l)) (Nat.add (PeanoNat.Nat.add (PeanoNat.Nat.add (bool_to_nat a) (BV_to_nat l)) (BV_to_nat l)) (bool_to_nat cin)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (half_adder_sum a cin)) (Nat.add (bool_to_nat (half_adder_carry a cin)) (bool_to_nat (half_adder_carry a cin)))) (Nat.add (Nat.add (bool_to_nat (half_adder_sum a cin)) (bool_to_nat (half_adder_carry a cin))) (bool_to_nat (half_adder_carry a cin))) *)
(* Goal: @eq nat (Nat.add (Nat.add (bool_to_nat (half_adder_carry a cin)) (bool_to_nat (half_adder_carry a cin))) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (Nat.add (BV_to_nat l) (bool_to_nat (half_adder_carry a cin))) (Nat.add (BV_to_nat l) (bool_to_nat (half_adder_carry a cin)))) *)
(* Goal: forall (a0 : bool) (l0 : list bool) (_ : forall cin : bool, @eq nat (BV_to_nat (appbv (BV_full_adder_sum (@cons bool a l) l0 cin) (consbv (BV_full_adder_carry (@cons bool a l) l0 cin) nilbv))) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat l0)) (bool_to_nat cin))) (cin : bool), @eq nat (BV_to_nat (appbv (BV_full_adder_sum (@cons bool a l) (@cons bool a0 l0) cin) (consbv (BV_full_adder_carry (@cons bool a l) (@cons bool a0 l0) cin) nilbv))) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat (@cons bool a0 l0))) (bool_to_nat cin)) *)
rewrite (plus_permute2 (bool_to_nat a) (bool_to_nat cin) (BV_to_nat l)).
rewrite
 (plus_permute2 (bool_to_nat a + BV_to_nat l) (bool_to_nat cin) (BV_to_nat l))
 .
(* Goal: @eq nat (S (PeanoNat.Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
trivial with arith.

(* Goal: @eq nat (S (PeanoNat.Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
trivial with arith.

(* Goal: @eq nat (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0)))) (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
repeat rewrite plus_assoc.
rewrite
 (plus_permute2 (bool_to_nat (half_adder_carry a cin))
    (bool_to_nat (half_adder_carry a cin)) (BV_to_nat l))
 .
(* Goal: @eq nat (PeanoNat.Nat.add (Nat.add (Nat.add (bool_to_nat (half_adder_carry a cin)) (BV_to_nat l)) (bool_to_nat (half_adder_carry a cin))) (BV_to_nat l)) (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (bool_to_nat (half_adder_carry a cin))) (BV_to_nat l)) (bool_to_nat (half_adder_carry a cin))) *)
(* Goal: forall (a0 : bool) (l0 : list bool) (_ : forall cin : bool, @eq nat (BV_to_nat (appbv (BV_full_adder_sum (@cons bool a l) l0 cin) (consbv (BV_full_adder_carry (@cons bool a l) l0 cin) nilbv))) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat l0)) (bool_to_nat cin))) (cin : bool), @eq nat (BV_to_nat (appbv (BV_full_adder_sum (@cons bool a l) (@cons bool a0 l0) cin) (consbv (BV_full_adder_carry (@cons bool a l) (@cons bool a0 l0) cin) nilbv))) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat (@cons bool a0 l0))) (bool_to_nat cin)) *)
rewrite (plus_comm (bool_to_nat (half_adder_carry a cin)) (BV_to_nat l)).
rewrite
 (plus_permute2 (BV_to_nat l + bool_to_nat (half_adder_carry a cin))
    (bool_to_nat (half_adder_carry a cin)) (BV_to_nat l))
 .
(* Goal: @eq nat (S (PeanoNat.Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
trivial with arith.

(* Goal: forall (a0 : bool) (l0 : list bool) (_ : forall cin : bool, @eq nat (BV_to_nat (appbv (BV_full_adder_sum (@cons bool a l) l0 cin) (consbv (BV_full_adder_carry (@cons bool a l) l0 cin) nilbv))) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat l0)) (bool_to_nat cin))) (cin : bool), @eq nat (BV_to_nat (appbv (BV_full_adder_sum (@cons bool a l) (@cons bool a0 l0) cin) (consbv (BV_full_adder_carry (@cons bool a l) (@cons bool a0 l0) cin) nilbv))) (Nat.add (Nat.add (BV_to_nat (@cons bool a l)) (BV_to_nat (@cons bool a0 l0))) (bool_to_nat cin)) *)
intros.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simpl in |- *.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum a a0 cin)) (Nat.add (BV_to_nat (appbv (BV_full_adder_sum l l0 (full_adder_carry a a0 cin)) (consbv (BV_full_adder_carry l l0 (full_adder_carry a a0 cin)) nilbv))) (BV_to_nat (appbv (BV_full_adder_sum l l0 (full_adder_carry a a0 cin)) (consbv (BV_full_adder_carry l l0 (full_adder_carry a a0 cin)) nilbv))))) (Nat.add (Nat.add (Nat.add (bool_to_nat a) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat cin)) *)
rewrite H.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum a a0 cin)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry a a0 cin))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry a a0 cin))))) (Nat.add (Nat.add (Nat.add (bool_to_nat a) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat cin)) *)
clear H.
(* Goal: @eq nat (Nat.add (bool_to_nat (half_adder_sum a true)) (Nat.add (BV_to_nat (@app bool (BV_full_adder_sum l (@nil bool) a) (consbv (BV_full_adder_carry l (@nil bool) a) nilbv))) (BV_to_nat (@app bool (BV_full_adder_sum l (@nil bool) a) (consbv (BV_full_adder_carry l (@nil bool) a) nilbv))))) (S (Nat.add (bool_to_nat a) (Nat.add (BV_to_nat l) (BV_to_nat l)))) *)
elim cin; elim a.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
rewrite full_adder_carry_sym1.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry a0 true true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry a0 true true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
rewrite full_adder_carry_true.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat true)) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat true)))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
rewrite full_adder_sum_sym1.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum a0 true true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat true)) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat true)))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
rewrite full_adder_sum_true.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simpl in |- *.
(* Goal: @eq nat (Nat.add (bool_to_nat a0) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (S O)) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (S O)))) (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (S O))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
repeat rewrite plus_n_SO.
(* Goal: @eq nat (S (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0))))) (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (S (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false false true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
elim plus_n_Sm.
(* Goal: @eq nat (S (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0))))) (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (S (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false false true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
elim plus_n_Sm.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simpl in |- *.
(* Goal: @eq nat (S (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0))))) (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (S (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false false true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
elim plus_n_Sm.
(* Goal: @eq nat (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0)))) (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
repeat rewrite plus_assoc.
rewrite
 (plus_permute2 (bool_to_nat a0 + BV_to_nat l) (BV_to_nat l0) (BV_to_nat l))
 .
(* Goal: @eq nat (S (S (PeanoNat.Nat.add (Nat.add (Nat.add (Nat.add (bool_to_nat a0) (BV_to_nat l)) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0)))) (S (S (PeanoNat.Nat.add (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (bool_to_nat a0)) (BV_to_nat l0)) (BV_to_nat l0)))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
rewrite (plus_comm (bool_to_nat a0) (BV_to_nat l)).
(* Goal: @eq nat (S (S (PeanoNat.Nat.add (Nat.add (Nat.add (PeanoNat.Nat.add (BV_to_nat l) (bool_to_nat a0)) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0)))) (S (S (PeanoNat.Nat.add (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (bool_to_nat a0)) (BV_to_nat l0)) (BV_to_nat l0)))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
rewrite (plus_permute2 (BV_to_nat l) (bool_to_nat a0) (BV_to_nat l)).
(* Goal: @eq nat (S (PeanoNat.Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
trivial with arith.

(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
elim a0.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simpl in |- *.
(* Goal: @eq nat (S (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0))))) (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (S (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false false true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
elim plus_n_Sm.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simpl in |- *.
(* Goal: @eq nat (S (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0))))) (S (Nat.add (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false false true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
elim plus_n_O.
(* Goal: @eq nat (S (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0))))) (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (S (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false false true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
elim plus_n_Sm.
(* Goal: @eq nat (S (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0))))) (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (S (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false false true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
elim plus_n_Sm.
(* Goal: @eq nat (S (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0))))) (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (S (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false false true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
elim plus_n_Sm.
(* Goal: @eq nat (S (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0))))) (S (Nat.add (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false false true)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false false true))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat true)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
elim plus_n_O.
(* Goal: @eq nat (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0)))) (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
repeat rewrite plus_assoc.
(* Goal: @eq nat (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (BV_to_nat l)) (BV_to_nat l0))) (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
rewrite (plus_permute2 (BV_to_nat l) (BV_to_nat l0) (BV_to_nat l)).
(* Goal: @eq nat (S (PeanoNat.Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
trivial with arith.

(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simpl in |- *.
(* Goal: @eq nat (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (S O)) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (S O))) (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (S (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
repeat rewrite <- plus_n_Sm.
(* Goal: @eq nat (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) O) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) O))) (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (Nat.add (BV_to_nat l0) (BV_to_nat l0))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
repeat rewrite <- plus_n_O.
(* Goal: @eq nat (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0)))) (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
repeat rewrite plus_assoc.
(* Goal: @eq nat (S (PeanoNat.Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
try trivial with arith.
(* Goal: @eq nat (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (BV_to_nat l)) (BV_to_nat l0))) (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
rewrite (plus_permute2 (BV_to_nat l) (BV_to_nat l0) (BV_to_nat l)).
(* Goal: @eq nat (S (PeanoNat.Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
try trivial with arith.

(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
elim a0.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simpl in |- *.
(* Goal: @eq nat (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (S O)) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (S O))) (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (S (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
repeat rewrite <- plus_n_Sm.
(* Goal: @eq nat (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) O) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) O))) (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (Nat.add (BV_to_nat l0) (BV_to_nat l0))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
repeat rewrite <- plus_n_O.
(* Goal: @eq nat (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0)))) (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
repeat rewrite plus_assoc.
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simpl in |- *.
(* Goal: @eq nat (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (BV_to_nat l)) (BV_to_nat l0))) (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
rewrite (plus_permute2 (BV_to_nat l) (BV_to_nat l0) (BV_to_nat l)).
(* Goal: @eq nat (S (PeanoNat.Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
trivial with arith.

(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum true false false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry true false false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat true) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
simpl in |- *.
(* Goal: @eq nat (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) O) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) O))) (S (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (Nat.add (BV_to_nat l0) (BV_to_nat l0))) O)) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
repeat rewrite <- plus_n_O.
(* Goal: @eq nat (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (Nat.add (BV_to_nat l) (BV_to_nat l0)))) (S (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
repeat rewrite plus_assoc.
(* Goal: @eq nat (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (BV_to_nat l)) (BV_to_nat l0))) (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
rewrite (plus_permute2 (BV_to_nat l) (BV_to_nat l0) (BV_to_nat l)).
(* Goal: @eq nat (S (PeanoNat.Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
trivial with arith.

elim a0; simpl in |- *; repeat rewrite <- plus_n_Sm;
 repeat rewrite <- plus_n_O; repeat rewrite plus_assoc;
 rewrite (plus_permute2 (BV_to_nat l) (BV_to_nat l0) (BV_to_nat l));
(* Goal: @eq nat (S (PeanoNat.Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) (S (PeanoNat.Nat.add (PeanoNat.Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l)) (BV_to_nat l0)) (BV_to_nat l0))) *)
(* Goal: @eq nat (Nat.add (bool_to_nat (full_adder_sum false a0 false)) (Nat.add (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))) (Nat.add (Nat.add (BV_to_nat l) (BV_to_nat l0)) (bool_to_nat (full_adder_carry false a0 false))))) (Nat.add (Nat.add (Nat.add (bool_to_nat false) (Nat.add (BV_to_nat l) (BV_to_nat l))) (Nat.add (bool_to_nat a0) (Nat.add (BV_to_nat l0) (BV_to_nat l0)))) (bool_to_nat false)) *)
 trivial with arith.

Qed.
(****************************************************************)