Require Import Arith Div2 List.
Require Import BellantoniCook.Lib BellantoniCook.Bitstring BellantoniCook.Cobham BellantoniCook.CobhamLib.

Opaque bs2nat.
Opaque Cond.

Lemma bs2nat_smash' : forall u v n,
  bs2nat v = power 2 n ->
  bs2nat (smash' u v) = power 2 (length u + n).
Proof.
(* Goal: forall u v : list bool, @eq nat (bs2nat (smash_bs u v)) (power (S (S O)) (Init.Nat.mul (@length bool u) (@length bool v))) *)
  induction u; simpl; intros; auto.
(* Goal: @eq nat (bs2nat (@cons bool false (smash' u v))) (Init.Nat.add (power (S (S O)) (Init.Nat.add (@length bool u) n)) (Init.Nat.add (power (S (S O)) (Init.Nat.add (@length bool u) n)) O)) *)
  rewrite bs2nat_false, (IHu v n); trivial.
Qed.

Lemma bs2nat_smash_bs : forall u v,
  bs2nat (smash_bs u v) = power 2 (length u * length v).
Proof.
(* Goal: forall u v : list bool, @eq nat (bs2nat (smash_bs u v)) (power (S (S O)) (Init.Nat.mul (@length bool u) (@length bool v))) *)
  induction u; simpl; intros; auto.
(* Goal: @eq nat (bs2nat (smash' v (smash_bs u v))) (power (S (S O)) (Init.Nat.add (@length bool v) (Init.Nat.mul (@length bool u) (@length bool v)))) *)
  rewrite bs2nat_smash' with (n := length u * length v); trivial.
Qed.

Lemma Smash_correct : forall l,
  bs2nat (Sem Smash l) = power 2 (length (hd nil l) * length (hd nil (tl l))).
Proof.
(* Goal: forall l : list (list bool), @eq nat (bs2nat (Sem Smash l)) (power (S (S O)) (Init.Nat.mul (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
  intros [ | u [ | v l] ]; trivial; simpl.
(* Goal: @eq nat (bs2nat (smash_bs u (@nil bool))) (power (S (S O)) (Init.Nat.mul (@length bool u) O)) *)
(* Goal: @eq nat (bs2nat (smash_bs u v)) (power (S (S O)) (Init.Nat.mul (@length bool u) (@length bool v))) *)
  rewrite mult_0_r; simpl.
(* Goal: @eq nat (bs2nat (smash_bs u (@nil bool))) (S O) *)
(* Goal: @eq nat (bs2nat (smash_bs u v)) (power (S (S O)) (Init.Nat.mul (@length bool u) (@length bool v))) *)
  induction u as [ | [ | ] u IH]; trivial.
(* Goal: @eq nat (bs2nat (smash_bs u v)) (power (S (S O)) (Init.Nat.mul (@length bool u) (@length bool v))) *)
  apply bs2nat_smash_bs.
Qed.

Lemma Zero_correct_bs n l: 
  Sem (Zero_e n) l = nil.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
Qed.

Lemma Zero_correct n l: 
  bs2nat (Sem (Zero_e n) l) = 0.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
Qed.

Definition False_e n :=
  Comp n (Succ false) [Zero_e n].

Lemma arity_False: forall n : nat, arity (False_e n) = ok_arity n.
Proof.
(* Goal: forall n : nat, @eq Arity (arity (False_e n)) (ok_arity n) *)
  simpl; simpl.
(* Goal: forall (b : bool) (l1 l2 : list bool) (_ : @eq nat (bs2nat l1) (bs2nat l2)), @eq nat (bs2nat (@cons bool b l1)) (bs2nat (@cons bool b l2)) *)
  intros.
(* Goal: @eq Arity (if andb (Nat.eqb n n) true then ok_arity n else error_Comp (ok_arity (S O)) (@cons Arity (ok_arity n) (@nil Arity))) (ok_arity n) *)
  rewrite <- beq_nat_refl.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  simpl.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
Qed.

Lemma rec_bounded_False: forall n : nat, rec_bounded (False_e n).
Proof.
(* Goal: forall n : nat, rec_bounded (False_e n) *)
 intros; simpl; intuition.
Qed.

Lemma False_correct: forall (n : nat) (l : list bs), bs2nat (Sem (False_e n) l) = 0.
Proof.
(* Goal: forall (n : nat) (l : list (list bool)), @eq (list bool) (Sem (False_e n) l) (@cons bool false (@nil bool)) *)
 intros; simpl; auto.
Qed.

Lemma False_correct_bs: forall (n : nat) (l : list bs), Sem (False_e n) l = [false].
Proof.
(* Goal: forall (n : nat) (l : list (list bool)), @eq (list bool) (Sem (False_e n) l) (@cons bool false (@nil bool)) *)
 intros; simpl; auto.
Qed.

Lemma One_correct n l: 
  bs2nat (Sem (One_e n) l) = 1.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
Qed.

Lemma One_correct_bs n l:
  Sem (One_e n) l = [true].
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
Qed.

Opaque Zero_e One_e False_e Rev_e RemoveLSZ_e.

Definition Normalize_e : Cobham :=
  Comp 1 Rev_e [Comp 1 RemoveLSZ_e [Rev_e]].

Lemma arity_Normalize :
  arity Normalize_e = ok_arity 1.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
Qed.

Lemma rec_bounded_Normalize :
  rec_bounded Normalize_e.
Proof.
(* Goal: rec_bounded Normalize_e *)
  simpl; intuition.
(* Goal: rec_bounded Rev_e *)
  apply rec_bounded_Rev.
(* Goal: rec_bounded RemoveLSZ_e *)
(* Goal: rec_bounded Rev_e *)
  apply rec_bounded_RemoveLSZ.
(* Goal: rec_bounded Rev_e *)
  apply rec_bounded_Rev.
Qed.

Lemma Normalize_correct : forall l,
  bs2nat (Sem Normalize_e l) = bs2nat (Sem (Proj 1 0) l).
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  destruct l as [ | v l]; trivial;simpl.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  induction v as [ | [ | ] v IH]; trivial.
  
(* Goal: @eq nat (Init.Nat.add (bs2nat u) match bs2nat v with | O => S O | S l => O end) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool true w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) O))))) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool false w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) O))))) *)
  rewrite bs2nat_true.
(* Goal: @eq nat (bs2nat (Sem Rev_e (@cons (list bool) (Sem RemoveLSZ_e (@cons (list bool) (Sem Rev_e (@cons (list bool) (@cons bool false v) l)) (@nil (list bool)))) (@nil (list bool))))) (Init.Nat.mul (S (S O)) (bs2nat v)) *)
  do 2 rewrite Rev_correct in *; simpl in *.
(* Goal: @eq nat (bs2nat (@rev bool (Sem RemoveLSZ_e (@cons (list bool) (@app bool (@rev bool v) (@cons bool false (@nil bool))) (@nil (list bool)))))) (Init.Nat.add (bs2nat v) (Init.Nat.add (bs2nat v) O)) *)
  rewrite RemoveLSZ_app, <- IH.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  destruct (Sem RemoveLSZ_e [rev v]); trivial; simpl.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  rewrite rev_unit; trivial.

(* Goal: @eq nat (bs2nat (@cons bool false (@firstn bool n l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub n O) l))) *)
  rewrite bs2nat_false.
(* Goal: @eq nat (bs2nat (Sem Rev_e (@cons (list bool) (Sem RemoveLSZ_e (@cons (list bool) (Sem Rev_e (@cons (list bool) (@cons bool false v) l)) (@nil (list bool)))) (@nil (list bool))))) (Init.Nat.mul (S (S O)) (bs2nat v)) *)
  do 2 rewrite Rev_correct in *; simpl in *.
(* Goal: @eq nat (bs2nat (@rev bool (Sem RemoveLSZ_e (@cons (list bool) (@app bool (@rev bool v) (@cons bool false (@nil bool))) (@nil (list bool)))))) (Init.Nat.add (bs2nat v) (Init.Nat.add (bs2nat v) O)) *)
  rewrite RemoveLSZ_app, <- IH.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  destruct (Sem RemoveLSZ_e [rev v]); trivial; simpl.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  rewrite rev_unit; trivial.
Qed.

Lemma Normalize_normal : forall l,
  Sem Normalize_e l = nil \/ bs2nat (Sem Normalize_e l) <> 0.
Proof.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) O vl (@nil bool))) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@cons bool true (@nth (list bool) O l (@nil bool))))) *)
  destruct l as [ | v l].
(* Goal: @eq nat O (Init.Nat.add (Init.Nat.mul (S O) (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul O O)) *)
(* Goal: @eq nat (S n) (Init.Nat.add (Init.Nat.mul O (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (S n) (S O))) *)
  tauto.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  simpl.
(* Goal: @eq nat (bs2nat (Sem Length_e (@cons (list bool) v l))) (@length bool v) *)
  induction v as [ | [ | ] v IH].
  
(* Goal: @eq nat O (Init.Nat.add (Init.Nat.mul (S O) (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul O O)) *)
(* Goal: @eq nat (S n) (Init.Nat.add (Init.Nat.mul O (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (S n) (S O))) *)
  tauto.

(* Goal: or (@eq (list bool) (Sem Rev_e (@cons (list bool) (Sem RemoveLSZ_e (@cons (list bool) (Sem Rev_e (@cons (list bool) (@cons bool false v) l)) (@nil (list bool)))) (@nil (list bool)))) (@nil bool)) (not (@eq nat (bs2nat (Sem Rev_e (@cons (list bool) (Sem RemoveLSZ_e (@cons (list bool) (Sem Rev_e (@cons (list bool) (@cons bool false v) l)) (@nil (list bool)))) (@nil (list bool))))) O)) *)
  do 2 rewrite Rev_correct in *.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
  simpl in *.
(* Goal: or (@eq (list bool) (@rev bool (Sem RemoveLSZ_e (@cons (list bool) (@app bool (@rev bool v) (@cons bool false (@nil bool))) (@nil (list bool))))) (@nil bool)) (not (@eq nat (bs2nat (@rev bool (Sem RemoveLSZ_e (@cons (list bool) (@app bool (@rev bool v) (@cons bool false (@nil bool))) (@nil (list bool)))))) O)) *)
  rewrite RemoveLSZ_app.
(* Goal: or (@eq (list bool) (@rev bool match Sem RemoveLSZ_e (@cons (list bool) (@rev bool v) (@nil (list bool))) with | nil => Sem RemoveLSZ_e (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))) | cons b l => @app bool (@cons bool b l) (@cons bool false (@nil bool)) end) (@nil bool)) (not (@eq nat (bs2nat (@rev bool match Sem RemoveLSZ_e (@cons (list bool) (@rev bool v) (@nil (list bool))) with | nil => Sem RemoveLSZ_e (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))) | cons b l => @app bool (@cons bool b l) (@cons bool false (@nil bool)) end)) O)) *)
  destruct (Sem RemoveLSZ_e [rev v]).
(* Goal: or (@eq (list bool) v (@nil bool)) (not (@eq nat (bs2nat v) O)) *)
  right.
(* Goal: @eq bool b1 false *)
(* Goal: @eq bool (@hd bool false (@skipn bool match @length bool z with | O => S (@length bool x) | S l => Init.Nat.sub (@length bool x) l end (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b x))) *)
(* Goal: le (@length bool z) (@length bool x) *)
  discriminate.
(* Goal: or (@eq (list bool) v (@nil bool)) (not (@eq nat (bs2nat v) O)) *)
  right.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  simpl.
(* Goal: or (@eq (list bool) (@app bool (@rev bool (@app bool l0 (@cons bool false (@nil bool)))) (@cons bool b (@nil bool))) (@nil bool)) (not (@eq nat (bs2nat (@app bool (@rev bool (@app bool l0 (@cons bool false (@nil bool)))) (@cons bool b (@nil bool)))) O)) *)
  rewrite rev_unit.
(* Goal: @eq bool b1 false *)
(* Goal: @eq bool (@hd bool false (@skipn bool match @length bool z with | O => S (@length bool x) | S l => Init.Nat.sub (@length bool x) l end (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b x))) *)
(* Goal: le (@length bool z) (@length bool x) *)
  discriminate.

(* Goal: or (@eq (list bool) (Sem Rev_e (@cons (list bool) (Sem RemoveLSZ_e (@cons (list bool) (Sem Rev_e (@cons (list bool) (@cons bool false v) l)) (@nil (list bool)))) (@nil (list bool)))) (@nil bool)) (not (@eq nat (bs2nat (Sem Rev_e (@cons (list bool) (Sem RemoveLSZ_e (@cons (list bool) (Sem Rev_e (@cons (list bool) (@cons bool false v) l)) (@nil (list bool)))) (@nil (list bool))))) O)) *)
  do 2 rewrite Rev_correct in *.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
  simpl in *.
(* Goal: or (@eq (list bool) (@rev bool (Sem RemoveLSZ_e (@cons (list bool) (@app bool (@rev bool v) (@cons bool false (@nil bool))) (@nil (list bool))))) (@nil bool)) (not (@eq nat (bs2nat (@rev bool (Sem RemoveLSZ_e (@cons (list bool) (@app bool (@rev bool v) (@cons bool false (@nil bool))) (@nil (list bool)))))) O)) *)
  rewrite RemoveLSZ_app.
(* Goal: or (@eq (list bool) (@rev bool match Sem RemoveLSZ_e (@cons (list bool) (@rev bool v) (@nil (list bool))) with | nil => Sem RemoveLSZ_e (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))) | cons b l => @app bool (@cons bool b l) (@cons bool false (@nil bool)) end) (@nil bool)) (not (@eq nat (bs2nat (@rev bool match Sem RemoveLSZ_e (@cons (list bool) (@rev bool v) (@nil (list bool))) with | nil => Sem RemoveLSZ_e (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))) | cons b l => @app bool (@cons bool b l) (@cons bool false (@nil bool)) end)) O)) *)
  destruct (Sem RemoveLSZ_e [rev v]).
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
  simpl in *.
(* Goal: or (@eq (list bool) (@app bool (@rev bool (@app bool l0 (@cons bool false (@nil bool)))) (@cons bool b (@nil bool))) (@nil bool)) (not (@eq nat (bs2nat (@app bool (@rev bool (@app bool l0 (@cons bool false (@nil bool)))) (@cons bool b (@nil bool)))) O)) *)
  rewrite rev_unit.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  simpl.
(* Goal: or (@eq (list bool) v (@nil bool)) (not (@eq nat (bs2nat v) O)) *)
  right.
(* Goal: @eq nat (bs2nat (@cons bool false (@firstn bool n l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub n O) l))) *)
  rewrite bs2nat_false.
(* Goal: not (@eq nat (Init.Nat.mul (S (S O)) (bs2nat (@app bool (@rev bool l0) (@cons bool b (@nil bool))))) O) *)
  destruct IH as [IH | IH].
(* Goal: not (@eq nat (Init.Nat.mul (S (S O)) (bs2nat (@app bool (@rev bool l0) (@cons bool b (@nil bool))))) O) *)
(* Goal: not (@eq nat (Init.Nat.mul (S (S O)) (bs2nat (@app bool (@rev bool l0) (@cons bool b (@nil bool))))) O) *)
  apply app_eq_nil in IH.
(* Goal: not (@eq nat (Init.Nat.mul (S (S O)) (bs2nat (@app bool (@rev bool l0) (@cons bool b (@nil bool))))) O) *)
(* Goal: not (@eq nat (Init.Nat.mul (S (S O)) (bs2nat (@app bool (@rev bool l0) (@cons bool b (@nil bool))))) O) *)
  destruct IH as [_ IH].
(* Goal: @eq nat (Nat.div2 (bs2nat (@fun_power (list bool) n (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l))))) (Nat.div2 (@fun_power nat n Nat.div2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
  congruence.
(* Goal: le (@length bool z) (@length bool x) *)
  omega.
Qed.

Opaque Normalize_e.

(** Def 1 of (Rose) *)

Definition Succ_e : Cobham :=
  Rec
    (Comp 0 (Succ true) [Zero])
    (Comp 2 (Succ true) [Proj 2 0])
    (Comp 2 (Succ false) [Proj 2 1])
    (Comp 1 (Succ true) [Proj 1 0]).

Lemma arity_Succ : arity Succ_e = ok_arity 1.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
Qed.

Lemma length_Succ : forall l,
  length (Sem Succ_e l) <= length (Sem (Comp 1 (Succ true) [Proj 1 0]) l).
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  destruct l as [ | v l]; trivial; simpl.
(* Goal: le (@length bool z) (@length bool x) *)
  induction v as [ | [ | ] v IH]; trivial; simpl; omega.
Qed.

Lemma le_1_length_Succ v : 
  1 <= length (Sem Succ_e [v]).
Proof.
(* Goal: le (@length bool z) (@length bool x) *)
  destruct v as [ | [ | ] v]; trivial; simpl; omega.
Qed.

Lemma le_length_Succ v :
  length v <= length (Sem Succ_e [v]).
Proof.
(* Goal: @eq nat (bs2nat (Sem Length_e (@cons (list bool) v l))) (@length bool v) *)
induction v as [ | [ | ] v IH].
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
simpl in *.
(* Goal: le (@length bool z) (@length bool x) *)
omega.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma Succ_length v :
  length (Sem Succ_e v) <= S (length (hd nil v)).
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
 intros; simpl.
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @cons bool true (@nil bool)) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) (@hd (list bool) (@nil bool) v) (@tl (list bool) v))) (S (@length bool (@hd (list bool) (@nil bool) v))) *)
 induction (hd nil v); simpl; auto.
(* Goal: le (@length bool z) (@length bool x) *)
 case a; simpl; omega.
Qed.  

Lemma rec_bounded_Succ :
  rec_bounded Succ_e.
Proof.
(* Goal: rec_bounded Normalize_e *)
 simpl; intuition.
 eapply le_trans.
 eapply le_trans.
 2:apply length_Succ.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
 simpl; trivial.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
 trivial.
Qed.

Lemma Succ_correct : forall l,
  bs2nat (Sem Succ_e l) = 1 + bs2nat (hd nil l).
Proof.
(* Goal: forall l : list (list bool), @eq nat (bs2nat (Sem Succ_e l)) (Init.Nat.add (S O) (bs2nat (@hd (list bool) (@nil bool) l))) *)
  destruct l as [ | v l]; trivial; simpl hd.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  induction v as [ | [ | ] v IH]; trivial.
(* Goal: @eq nat (bs2nat (Sem Mod2_e (@cons (list bool) (@cons bool false v) l))) (Init.Nat.sub (bs2nat (@cons bool false v)) (Init.Nat.mul (S (S O)) (Nat.div2 (bs2nat (@cons bool false v))))) *)
  simpl Sem in *.
(* Goal: @eq nat (bs2nat (@cons bool false (sem_Rec (fun _ : list (list bool) => @cons bool true (@nil bool)) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) v l))) (Init.Nat.add (S O) (bs2nat (@cons bool true v))) *)
  rewrite bs2nat_false, bs2nat_true, IH; ring.
Qed.

Opaque Succ_e.

(** Def 2 of (Rose) *)

Definition Pred'_e : Cobham :=
  Rec
    Zero
    (Comp 2 (Succ true) [Proj 2 1])
    (Comp 2 (Succ false) [Proj 2 0])
    (Proj 1 0).

Lemma arity_Pred' : arity Pred'_e = ok_arity 1.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
Qed.

Lemma rec_bounded_Pred' :
  rec_bounded Pred'_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
  intuition.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) O vl (@nil bool))) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@cons bool true (@nth (list bool) O l (@nil bool))))) *)
  destruct l as [ | v l].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  simpl.
(* Goal: @eq nat (bs2nat (Sem Length_e (@cons (list bool) v l))) (@length bool v) *)
  induction v as [ | [ | ] v IH].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
(* Goal: le (@length bool z) (@length bool x) *)
  simpl; omega.
Qed.

Lemma Pred'_correct : forall l,
  hd nil l = nil \/ bs2nat (hd nil l) <> 0 ->
  bs2nat (Sem Pred'_e l) =  bs2nat (hd nil l) - 1.
Proof.
(* Goal: forall (l : list (list bool)) (_ : or (@eq (list bool) (@hd (list bool) (@nil bool) l) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) l)) O))), @eq nat (bs2nat (Sem Pred'_e l)) (Init.Nat.sub (bs2nat (@hd (list bool) (@nil bool) l)) (S O)) *)
intros l H.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) O vl (@nil bool))) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@cons bool true (@nth (list bool) O l (@nil bool))))) *)
destruct l as [ | v l].
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (Sem Length_e (@cons (list bool) v l))) (@length bool (@hd (list bool) (@nil bool) (@cons (list bool) v l))) *)
simpl hd.
(* Goal: @eq nat (bs2nat (Sem Length_e (@cons (list bool) v l))) (@length bool v) *)
induction v as [ | [ | ] v IH].

(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.

(* Goal: @eq nat (bs2nat (Sem Mod2_e (@cons (list bool) (@cons bool false v) l))) (Init.Nat.sub (bs2nat (@cons bool false v)) (Init.Nat.mul (S (S O)) (Nat.div2 (bs2nat (@cons bool false v))))) *)
simpl Sem in *.
(* Goal: @eq nat (bs2nat (@cons bool false v)) (Init.Nat.sub (bs2nat (@cons bool true v)) (S O)) *)
(* Goal: @eq nat (bs2nat (Sem Pred'_e (@cons (list bool) (@cons bool false v) l))) (Init.Nat.sub (bs2nat (@cons bool false v)) (S O)) *)
rewrite bs2nat_false, bs2nat_true.
(* Goal: le (@length bool z) (@length bool x) *)
omega.

(* Goal: @eq nat (bs2nat (Sem Mod2_e (@cons (list bool) (@cons bool false v) l))) (Init.Nat.sub (bs2nat (@cons bool false v)) (Init.Nat.mul (S (S O)) (Nat.div2 (bs2nat (@cons bool false v))))) *)
simpl Sem in *.
(* Goal: @eq nat (bs2nat (@cons bool true (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @cons bool true (@nth (list bool) (S O) vl (@nil bool))) (fun vl : list (list bool) => @cons bool false (@nth (list bool) O vl (@nil bool))) v l))) (Init.Nat.sub (bs2nat (@cons bool false v)) (S O)) *)
rewrite bs2nat_false, bs2nat_true, IH.
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) match bs2nat (@cons bool false v) with | O => S O | S l => O end) *)
simpl in H.
(* Goal: @eq nat O match Init.Nat.mul (S (S O)) (bs2nat v) with | O => S O | S l => O end *)
destruct H as [H | H].
(* Goal: @eq nat (Nat.div2 (bs2nat (@fun_power (list bool) n (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l))))) (Nat.div2 (@fun_power nat n Nat.div2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
congruence.
(* Goal: or (@eq (list bool) v (@nil bool)) (not (@eq nat (bs2nat v) O)) *)
rewrite bs2nat_false in H.
(* Goal: le (@length bool z) (@length bool x) *)
omega.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
simpl in *.
(* Goal: @eq nat O match Init.Nat.mul (S (S O)) (bs2nat v) with | O => S O | S l => O end *)
destruct H as [H | H].
(* Goal: @eq nat (Nat.div2 (bs2nat (@fun_power (list bool) n (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l))))) (Nat.div2 (@fun_power nat n Nat.div2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
congruence.
(* Goal: or (@eq (list bool) v (@nil bool)) (not (@eq nat (bs2nat v) O)) *)
rewrite bs2nat_false in H.

(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) match bs2nat (@cons bool false v) with | O => S O | S l => O end) *)
simpl in H.
(* Goal: or (@eq (list bool) v (@nil bool)) (not (@eq nat (bs2nat v) O)) *)
right.
(* Goal: le (@length bool z) (@length bool x) *)
omega.
Qed.

Opaque Pred'_e.

Definition Pred_e : Cobham :=
  Comp 1 Pred'_e [Normalize_e].

Lemma arity_Pred : arity Pred_e = ok_arity 1.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_Pred :
  rec_bounded Pred_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded Pred'_e *)
(* Goal: rec_bounded Normalize_e *)
apply rec_bounded_Pred'.
(* Goal: rec_bounded Normalize_e *)
apply rec_bounded_Normalize.
Qed.

Lemma Pred_correct : forall l,
  bs2nat (Sem Pred_e l) =  bs2nat (hd nil l) - 1.
Proof.
(* Goal: forall l : list (list bool), @eq nat (@length bool (Sem DivTwoPower_e l)) (Init.Nat.sub (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
intro l.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (Sem Pred'_e (@cons (list bool) (Sem Normalize_e l) (@nil (list bool))))) (Init.Nat.sub (bs2nat (@hd (list bool) (@nil bool) l)) (S O)) *)
rewrite Pred'_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul match bs2nat (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) with | O => S O | S l => O end (bs2nat (@nth (list bool) (S O) l (@nil bool)))) (Init.Nat.mul (bs2nat (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) match match bs2nat (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) with | O => S O | S l => O end with | O => S O | S l => O end)) (Init.Nat.add (Init.Nat.mul match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (Init.Nat.mul (bs2nat (@hd (list bool) (@nil bool) l)) match match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
(* Goal: or (@eq (list bool) (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool))))) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))))) O)) *)
rewrite Normalize_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: le (@length bool match @nth (list bool) (S (S O)) l (@nil bool) with | nil => @nth (list bool) O l (@nil bool) | cons (true as b) l0 => Sem PlusOneMinus_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) | cons (false as b) l0 => @nth (list bool) O l (@nil bool) end) (S (@length bool (@hd (list bool) (@nil bool) l))) *)
rewrite hd_nth_0.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: or (@eq (list bool) (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool))))) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))))) O)) *)
apply Normalize_normal.
Qed.

Opaque Pred_e.

(** Def 3 of (Rose) *)

Definition OneMinus'_e : Cobham :=
  Rec2
    (One_e 0)
    (Zero_e 2)
    (One_e 1).

Lemma arity_OneMinus' : arity OneMinus'_e = ok_arity 1.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_OneMinus' :
  rec_bounded OneMinus'_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded (One_e (S (S O))) *)
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (Sem (False_e (S (S O)))) (Sem (One_e (S (S O)))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (Sem (One_e (S O)) l)) *)
apply rec_bounded_One.
(* Goal: rec_bounded (One_e (S (S O))) *)
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (Sem (False_e (S (S O)))) (Sem (One_e (S (S O)))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (Sem (One_e (S O)) l)) *)
apply rec_bounded_One.
(* Goal: rec_bounded (Zero_e n) *)
(* Goal: and True (and (rec_bounded (Repeat_e n len' b)) True) *)
apply rec_bounded_Zero.
(* Goal: rec_bounded (Zero_e n) *)
(* Goal: and True (and (rec_bounded (Repeat_e n len' b)) True) *)
apply rec_bounded_Zero.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) O vl (@nil bool))) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@cons bool true (@nth (list bool) O l (@nil bool))))) *)
destruct l as [ | v l].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (Sem Length_e (@cons (list bool) v l))) (@length bool v) *)
induction v as [ | [ | ] v IH].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat u) (Init.Nat.mul (bs2nat u) match bs2nat (@nil bool) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool true v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool true v) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool false v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool false v) with | O => S O | S l => O end) *)
auto with arith.
(* Goal: @eq nat (bs2nat u) (Init.Nat.mul (bs2nat u) match bs2nat (@nil bool) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool true v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool true v) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool false v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool false v) with | O => S O | S l => O end) *)
auto with arith.
Qed.

Lemma OneMinus'_correct : forall l,
  hd nil l = nil \/ bs2nat (hd nil l) <> 0 ->
  bs2nat (Sem OneMinus'_e l) = 1 - bs2nat (hd nil l).
Proof.
(* Goal: forall (l : list (list bool)) (_ : or (@eq (list bool) (@hd (list bool) (@nil bool) l) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) l)) O))), @eq nat (bs2nat (Sem OneMinusMultPlus'_e l)) (Init.Nat.add (Init.Nat.mul (Init.Nat.sub (S O) (bs2nat (@hd (list bool) (@nil bool) l))) (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (Init.Nat.mul (bs2nat (@hd (list bool) (@nil bool) l)) (Init.Nat.sub (S O) (Init.Nat.sub (S O) (bs2nat (@hd (list bool) (@nil bool) l)))))) *)
intros [ | v l] H.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (Sem Length_e (@cons (list bool) v l))) (@length bool (@hd (list bool) (@nil bool) (@cons (list bool) v l))) *)
simpl hd.
(* Goal: @eq nat (bs2nat match v with | nil => u | cons (true as b) l => Sem Succ_e (@cons (list bool) u (@nil (list bool))) | cons (false as b) l => u end) (Init.Nat.add (bs2nat u) (Init.Nat.sub (bs2nat v) (Init.Nat.add (Nat.div2 (bs2nat v)) (Init.Nat.add (Nat.div2 (bs2nat v)) O)))) *)
destruct v as [ | [ | ] v].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (Sem Mod2_e (@cons (list bool) (@cons bool false v) l))) (Init.Nat.sub (bs2nat (@cons bool false v)) (Init.Nat.mul (S (S O)) (Nat.div2 (bs2nat (@cons bool false v))))) *)
simpl Sem in *.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
simpl in *.
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool false v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool false v) with | O => S O | S l => O end) *)
rewrite Zero_correct.
(* Goal: @eq nat (bs2nat (@cons bool false v)) (Init.Nat.add (Init.Nat.mul match bs2nat (@cons bool false v) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (bs2nat (@cons bool false v)) match match bs2nat (@cons bool false v) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
rewrite bs2nat_false in *.
(* Goal: @eq nat O match Init.Nat.mul (S (S O)) (bs2nat v) with | O => S O | S l => O end *)
destruct H as [H | H].
(* Goal: @eq nat (Nat.div2 (bs2nat (@fun_power (list bool) n (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l))))) (Nat.div2 (@fun_power nat n Nat.div2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
congruence.
(* Goal: @eq nat (Init.Nat.mul (S (S O)) (bs2nat v)) (Init.Nat.add (Init.Nat.mul match Init.Nat.mul (S (S O)) (bs2nat v) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (Init.Nat.mul (S (S O)) (bs2nat v)) match match Init.Nat.mul (S (S O)) (bs2nat v) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
destruct (2 * bs2nat v).
(* Goal: @eq nat O (Init.Nat.add (Init.Nat.mul (S O) (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul O O)) *)
(* Goal: @eq nat (S n) (Init.Nat.add (Init.Nat.mul O (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (S n) (S O))) *)
tauto.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Opaque OneMinus'_e.

Definition OneMinus_e : Cobham :=
  Comp 1 OneMinus'_e [Normalize_e].

Lemma arity_OneMinus : arity OneMinus_e = ok_arity 1.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_OneMinus :
  rec_bounded OneMinus_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded OneMinus'_e *)
(* Goal: rec_bounded Normalize_e *)
apply rec_bounded_OneMinus'.
(* Goal: rec_bounded Normalize_e *)
apply rec_bounded_Normalize.
Qed.

Lemma OneMinus_correct : forall l,
  bs2nat (Sem OneMinus_e l) = 1 - bs2nat (hd nil l).
Proof.
(* Goal: forall l : list (list bool), @eq nat (@length bool (Sem DivTwoPower_e l)) (Init.Nat.sub (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
intro l.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (Sem OneMinus'_e (@cons (list bool) (Sem Normalize_e l) (@nil (list bool))))) match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end *)
rewrite OneMinus'_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul match bs2nat (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) with | O => S O | S l => O end (bs2nat (@nth (list bool) (S O) l (@nil bool)))) (Init.Nat.mul (bs2nat (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) match match bs2nat (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) with | O => S O | S l => O end with | O => S O | S l => O end)) (Init.Nat.add (Init.Nat.mul match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (Init.Nat.mul (bs2nat (@hd (list bool) (@nil bool) l)) match match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
(* Goal: or (@eq (list bool) (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool))))) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))))) O)) *)
rewrite Normalize_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: le (@length bool match @nth (list bool) (S (S O)) l (@nil bool) with | nil => @nth (list bool) O l (@nil bool) | cons (true as b) l0 => Sem PlusOneMinus_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) | cons (false as b) l0 => @nth (list bool) O l (@nil bool) end) (S (@length bool (@hd (list bool) (@nil bool) l))) *)
rewrite hd_nth_0.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: or (@eq (list bool) (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool))))) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))))) O)) *)
apply Normalize_normal.
Qed.

Opaque OneMinus_e.

(** Def 4 of (Rose) *)

Definition Div2_e : Cobham :=
  Rec2
    Zero
    (Proj 2 0)
    (Proj 1 0).

Lemma arity_Div2 : arity Div2_e = ok_arity 1.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma length_Div2 : forall l,
  length (Sem Div2_e l) = length (hd nil l) - 1.
Proof.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) O vl (@nil bool))) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@cons bool true (@nth (list bool) O l (@nil bool))))) *)
destruct l as [ | v l].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (Sem Length_e (@cons (list bool) v l))) (@length bool v) *)
induction v as [ | [ | ] v IH].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
Qed.

Lemma rec_bounded_Div2 :
  rec_bounded Div2_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) O vl (@nil bool))) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@cons bool true (@nth (list bool) O l (@nil bool))))) *)
destruct l as [ | v l].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat match v with | nil => u | cons (true as b) l => Sem Succ_e (@cons (list bool) u (@nil (list bool))) | cons (false as b) l => u end) (Init.Nat.add (bs2nat u) (Init.Nat.sub (bs2nat v) (Init.Nat.add (Nat.div2 (bs2nat v)) (Init.Nat.add (Nat.div2 (bs2nat v)) O)))) *)
destruct v as [ | [ | ] v].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
Qed.

Lemma Div2_correct_bs : forall l,
  Sem Div2_e l =
  tl (hd nil l).
Proof.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) O vl (@nil bool))) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@cons bool true (@nth (list bool) O l (@nil bool))))) *)
destruct l as [ | v l].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
destruct v as [ | [ | ] v]; trivial.
Qed.

Lemma Div2_correct : forall l,
  bs2nat (Sem Div2_e l) = div2 (bs2nat (hd nil l)).
Proof.
(* Goal: forall l : list (list bool), @eq nat (bs2nat (Sem Div2_e l)) (Nat.div2 (bs2nat (@hd (list bool) (@nil bool) l))) *)
intros [ | v l].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq (list bool) (Sem Div2_e (@cons (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@nil (list bool)))) (@tl bool (@fun_power (list bool) (@length bool u) (@tl bool) v)) *)
rewrite Div2_correct_bs.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (@tl bool v)) (Nat.div2 (bs2nat v)) *)
apply bs2nat_tl.
Qed.

Opaque Div2_e.

(** Def 5 of (Rose) *)

Definition Mod2_e : Cobham :=
  Rec
    Zero
    (False_e 2)
    (One_e 2)
    (One_e 1).

Lemma arity_Mod2 : arity Mod2_e = ok_arity 1.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_Mod2 :
  rec_bounded Mod2_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded (One_e (S (S O))) *)
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (Sem (False_e (S (S O)))) (Sem (One_e (S (S O)))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (Sem (One_e (S O)) l)) *)
apply rec_bounded_One.
(* Goal: rec_bounded (False_e (S (S O))) *)
(* Goal: rec_bounded (One_e (S (S O))) *)
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (Sem (False_e (S (S O)))) (Sem (One_e (S (S O)))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (Sem (One_e (S O)) l)) *)
apply rec_bounded_False.
(* Goal: rec_bounded (One_e (S (S O))) *)
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (Sem (False_e (S (S O)))) (Sem (One_e (S (S O)))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (Sem (One_e (S O)) l)) *)
apply rec_bounded_One.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) O vl (@nil bool))) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@cons bool true (@nth (list bool) O l (@nil bool))))) *)
destruct l as [ | v l].
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (Sem Length_e (@cons (list bool) v l))) (@length bool v) *)
induction v as [ | [ | ] v IH].
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
(* Goal: @eq nat (bs2nat u) (Init.Nat.mul (bs2nat u) match bs2nat (@nil bool) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool true v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool true v) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool false v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool false v) with | O => S O | S l => O end) *)
auto with arith.
(* Goal: @eq nat (bs2nat u) (Init.Nat.mul (bs2nat u) match bs2nat (@nil bool) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool true v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool true v) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool false v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool false v) with | O => S O | S l => O end) *)
auto with arith.
Qed.

Lemma Mod2_correct_bs : forall l, 
  (hd nil l) <> nil ->
  Sem Mod2_e l = [hd true (hd nil l)].
Proof.
(* Goal: forall (b : bool) (l1 l2 : list bool) (_ : @eq nat (bs2nat l1) (bs2nat l2)), @eq nat (bs2nat (@cons bool b l1)) (bs2nat (@cons bool b l2)) *)
  intros.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  simpl.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  destruct (hd nil l); simpl; trivial.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  elim H; trivial.
(* Goal: @eq nat (bs2nat (@cons bool b l1)) (bs2nat (@cons bool b l2)) *)
  case b.
(* Goal: @eq (list bool) (Sem (One_e (S (S O))) (@cons (list bool) l0 (@cons (list bool) (sem_Rec (fun _ : list (list bool) => @nil bool) (Sem (False_e (S (S O)))) (Sem (One_e (S (S O)))) l0 (@tl (list bool) l)) (@tl (list bool) l)))) (@cons bool true (@nil bool)) *)
(* Goal: @eq (list bool) (Sem (False_e (S (S O))) (@cons (list bool) l0 (@cons (list bool) (sem_Rec (fun _ : list (list bool) => @nil bool) (Sem (False_e (S (S O)))) (Sem (One_e (S (S O)))) l0 (@tl (list bool) l)) (@tl (list bool) l)))) (@cons bool false (@nil bool)) *)
  rewrite One_correct_bs.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
(* Goal: @eq (list bool) (Sem (False_e (S (S O))) (@cons (list bool) l0 (@cons (list bool) (sem_Rec (fun _ : list (list bool) => @nil bool) (Sem (False_e (S (S O)))) (Sem (One_e (S (S O)))) l0 (@tl (list bool) l)) (@tl (list bool) l)))) (@cons bool false (@nil bool)) *)
  rewrite False_correct_bs.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
Qed.

Lemma Mod2_correct : forall l,
  bs2nat (Sem Mod2_e l) = mod2 (bs2nat (hd nil l)).
Proof.
(* Goal: forall l : list (list bool), @eq nat (bs2nat (Sem PlusOneMinusMod2_e l)) (Init.Nat.add (bs2nat (@hd (list bool) (@nil bool) l)) (Init.Nat.mul (Init.Nat.sub (S O) (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (mod2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) (@tl (list bool) l))))))) *)
unfold mod2.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) O vl (@nil bool))) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@cons bool true (@nth (list bool) O l (@nil bool))))) *)
destruct l as [ | v l].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (Sem Length_e (@cons (list bool) v l))) (@length bool (@hd (list bool) (@nil bool) (@cons (list bool) v l))) *)
simpl hd.
(* Goal: @eq nat (bs2nat match v with | nil => u | cons (true as b) l => Sem Succ_e (@cons (list bool) u (@nil (list bool))) | cons (false as b) l => u end) (Init.Nat.add (bs2nat u) (Init.Nat.sub (bs2nat v) (Init.Nat.add (Nat.div2 (bs2nat v)) (Init.Nat.add (Nat.div2 (bs2nat v)) O)))) *)
destruct v as [ | [ | ] v].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (Sem Mod2_e (@cons (list bool) (@cons bool false v) l))) (Init.Nat.sub (bs2nat (@cons bool false v)) (Init.Nat.mul (S (S O)) (Nat.div2 (bs2nat (@cons bool false v))))) *)
simpl Sem in *.
(* Goal: @eq nat (bs2nat (Sem (One_e (S (S O))) (@cons (list bool) v (@cons (list bool) (sem_Rec (fun _ : list (list bool) => @nil bool) (Sem (False_e (S (S O)))) (Sem (One_e (S (S O)))) v l) l)))) (Init.Nat.sub (bs2nat (@cons bool true v)) (Init.Nat.mul (S (S O)) (Nat.div2 (bs2nat (@cons bool true v))))) *)
(* Goal: @eq nat (bs2nat (Sem Mod2_e (@cons (list bool) (@cons bool false v) l))) (Init.Nat.sub (bs2nat (@cons bool false v)) (Init.Nat.mul (S (S O)) (Nat.div2 (bs2nat (@cons bool false v))))) *)
rewrite One_correct, bs2nat_true.
(* Goal: @eq nat (Init.Nat.add (S O) (bs2nat (@hd (list bool) (@nil bool) (@cons (list bool) u (@nil (list bool)))))) (Init.Nat.add (bs2nat u) (Init.Nat.sub (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) (bs2nat v))) (Init.Nat.add (Nat.div2 (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) (bs2nat v)))) (Init.Nat.add (Nat.div2 (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) (bs2nat v)))) O)))) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.sub (bs2nat (@cons bool false v)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false v))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false v))) O)))) *)
change (1 + 2 * bs2nat v) with (S (2 * bs2nat v)).
(* Goal: @eq nat (Init.Nat.add (bs2nat u) match bs2nat v with | O => S O | S l => O end) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (S (Init.Nat.mul (S (S O)) (bs2nat w))) (Init.Nat.add (Nat.div2 (S (Init.Nat.mul (S (S O)) (bs2nat w)))) (Init.Nat.add (Nat.div2 (S (Init.Nat.mul (S (S O)) (bs2nat w)))) O))))) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool false w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) O))))) *)
rewrite div2_double_plus_one.
(* Goal: le (@length bool z) (@length bool x) *)
omega.
(* Goal: @eq nat (bs2nat (Sem Mod2_e (@cons (list bool) (@cons bool false v) l))) (Init.Nat.sub (bs2nat (@cons bool false v)) (Init.Nat.mul (S (S O)) (Nat.div2 (bs2nat (@cons bool false v))))) *)
simpl Sem in *.
(* Goal: @eq nat (bs2nat (@cons bool false (@firstn bool n l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub n O) l))) *)
rewrite bs2nat_false.
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (Init.Nat.mul (S (S O)) (bs2nat w)) (Init.Nat.add (Nat.div2 (Init.Nat.mul (S (S O)) (bs2nat w))) (Init.Nat.add (Nat.div2 (Init.Nat.mul (S (S O)) (bs2nat w))) O))))) *)
rewrite div2_double.
(* Goal: @eq nat (bs2nat u) (Init.Nat.mul (bs2nat u) match bs2nat (@nil bool) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool true v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool true v) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool false v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool false v) with | O => S O | S l => O end) *)
auto with arith.
Qed.

Opaque Mod2_e.

(** Def 6 of (Rose) *)

Definition Length_e : Cobham :=
  Rec2
    Zero
    (Comp 2 Succ_e [Proj 2 1])
    (Proj 1 0).

Lemma arity_Length : arity Length_e = ok_arity 1.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
Qed.

Lemma rec_bounded_Length :
  rec_bounded Length_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded Succ_e *)
apply rec_bounded_Succ.
(* Goal: rec_bounded Succ_e *)
apply rec_bounded_Succ.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) O vl (@nil bool))) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@cons bool true (@nth (list bool) O l (@nil bool))))) *)
destruct l as [ | v l].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (Sem Length_e (@cons (list bool) v l))) (@length bool v) *)
induction v as [ | [ | ] v IH].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
eapply le_trans.
apply length_Succ.
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
eapply le_trans.
apply length_Succ.
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
Qed.

Lemma Length_correct : forall l,
  bs2nat (Sem Length_e l) = length (hd nil l).
Proof.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) O vl (@nil bool))) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@cons bool true (@nth (list bool) O l (@nil bool))))) *)
destruct l as [ | v l].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (Sem Length_e (@cons (list bool) v l))) (@length bool (@hd (list bool) (@nil bool) (@cons (list bool) v l))) *)
simpl hd.
(* Goal: @eq nat (bs2nat (Sem Length_e (@cons (list bool) v l))) (@length bool v) *)
induction v as [ | [ | ] v IH].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (Sem Succ_e (@cons (list bool) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) v l) (@nil (list bool))))) (S (@length bool v)) *)
rewrite Succ_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq (list bool) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec x y z)) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
(* Goal: le (@length bool z) (@length bool x) *)
f_equal.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (Sem Succ_e (@cons (list bool) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) v l) (@nil (list bool))))) (S (@length bool v)) *)
rewrite Succ_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq (list bool) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec x y z)) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
(* Goal: le (@length bool z) (@length bool x) *)
f_equal.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Opaque Length_e.

(** Def 7 of (Rose) *)

Definition MultOneMinus'_e : Cobham :=
  Comp 2 Cond [
    Proj 2 1;
    Proj 2 0;
    Zero_e 2;
    Zero_e 2
  ].

Lemma arity_MultOneMinus' : arity MultOneMinus'_e = ok_arity 2.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_MultOneMinus' :
  rec_bounded MultOneMinus'_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded Cond *)
(* Goal: rec_bounded PlusOneMinus_e *)
apply rec_bounded'_spec with 4.
(* Goal: @eq Arity (arity Cond) (ok_arity (S (S (S (S O))))) *)
(* Goal: rec_bounded' Cond *)
(* Goal: rec_bounded PlusOneMinus_e *)
apply arity_Cond.
(* Goal: rec_bounded' Cond *)
(* Goal: rec_bounded PlusOneMinus_e *)
apply rec_bounded_Cond.
(* Goal: rec_bounded (Zero_e n) *)
(* Goal: and True (and (rec_bounded (Repeat_e n len' b)) True) *)
apply rec_bounded_Zero.
(* Goal: rec_bounded (Zero_e n) *)
(* Goal: and True (and (rec_bounded (Repeat_e n len' b)) True) *)
apply rec_bounded_Zero.
Qed.

Lemma MultOneMinus'_correct : forall l,
  hd nil (tl l) = nil \/ bs2nat (hd nil (tl l)) <> 0 ->
  bs2nat (Sem MultOneMinus'_e l) = bs2nat (hd nil l) * (1 - bs2nat (hd nil (tl l))).
Proof.
(* Goal: forall (l : list (list bool)) (_ : or (@eq (list bool) (@hd (list bool) (@nil bool) (@tl (list bool) l)) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))) O))), @eq nat (bs2nat (Sem PlusOneMinus'_e l)) (Init.Nat.add (bs2nat (@hd (list bool) (@nil bool) l)) (Init.Nat.sub (S O) (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
intros [ | u [ | v l] ] H.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat u) (Init.Nat.mul (bs2nat u) match bs2nat (@nil bool) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool true v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool true v) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool false v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool false v) with | O => S O | S l => O end) *)
auto with arith.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (Sem Cond (@cons (list bool) w (@cons (list bool) u (@cons (list bool) (Sem PlusOneMinus_e (@cons (list bool) u (@cons (list bool) v (@nil (list bool))))) (@cons (list bool) u (@nil (list bool)))))))) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat w) (Init.Nat.add (Nat.div2 (bs2nat w)) (Init.Nat.add (Nat.div2 (bs2nat w)) O))))) *)
rewrite Cond_correct.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
simpl in *.
(* Goal: @eq nat (bs2nat match v with | nil => u | cons (true as b) l => Sem Succ_e (@cons (list bool) u (@nil (list bool))) | cons (false as b) l => u end) (Init.Nat.add (bs2nat u) (Init.Nat.sub (bs2nat v) (Init.Nat.add (Nat.div2 (bs2nat v)) (Init.Nat.add (Nat.div2 (bs2nat v)) O)))) *)
destruct v as [ | [ | ] v].
(* Goal: @eq nat (bs2nat u) (Init.Nat.mul (bs2nat u) match bs2nat (@nil bool) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool true v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool true v) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool false v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool false v) with | O => S O | S l => O end) *)
auto with arith.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool false v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool false v) with | O => S O | S l => O end) *)
rewrite Zero_correct.
(* Goal: @eq nat (bs2nat (@cons bool false v)) (Init.Nat.add (Init.Nat.mul match bs2nat (@cons bool false v) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (bs2nat (@cons bool false v)) match match bs2nat (@cons bool false v) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
rewrite bs2nat_false in *.
(* Goal: @eq nat (Init.Nat.mul (S (S O)) (bs2nat v)) (Init.Nat.add (Init.Nat.mul match Init.Nat.mul (S (S O)) (bs2nat v) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (Init.Nat.mul (S (S O)) (bs2nat v)) match match Init.Nat.mul (S (S O)) (bs2nat v) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
destruct (2 * bs2nat v).
(* Goal: @eq nat O (Init.Nat.add (Init.Nat.mul (S O) (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul O O)) *)
(* Goal: @eq nat (S n) (Init.Nat.add (Init.Nat.mul O (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (S n) (S O))) *)
destruct H.
(* Goal: @eq nat (Nat.div2 (bs2nat (@fun_power (list bool) n (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l))))) (Nat.div2 (@fun_power nat n Nat.div2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
congruence.
(* Goal: @eq nat O (Init.Nat.add (Init.Nat.mul (S O) (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul O O)) *)
(* Goal: @eq nat (S n) (Init.Nat.add (Init.Nat.mul O (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (S n) (S O))) *)
tauto.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed. 

Opaque MultOneMinus'_e.

Definition MultOneMinus_e : Cobham :=
  Comp 2 MultOneMinus'_e [Proj 2 0; Comp 2 Normalize_e [Proj 2 1]].

Lemma arity_MultOneMinus : arity MultOneMinus_e = ok_arity 2.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_MultOneMinus :
  rec_bounded MultOneMinus_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded MultOneMinus'_e *)
(* Goal: rec_bounded Normalize_e *)
apply rec_bounded_MultOneMinus'.
(* Goal: rec_bounded Normalize_e *)
apply rec_bounded_Normalize.
Qed.

Lemma MultOneMinus_correct : forall l,
  bs2nat (Sem MultOneMinus_e l) = bs2nat (hd nil l) * (1 - bs2nat (hd nil (tl l))).
Proof.
(* Goal: forall l : list (list bool), @eq nat (@length bool (Sem DivTwoPower_e l)) (Init.Nat.sub (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
intro l.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (Sem MultOneMinus'_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@nil (list bool)))))) (Init.Nat.mul (bs2nat (@hd (list bool) (@nil bool) l)) match bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)) with | O => S O | S l => O end) *)
rewrite MultOneMinus'_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul match bs2nat (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) with | O => S O | S l => O end (bs2nat (@nth (list bool) (S O) l (@nil bool)))) (Init.Nat.mul (bs2nat (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) match match bs2nat (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) with | O => S O | S l => O end with | O => S O | S l => O end)) (Init.Nat.add (Init.Nat.mul match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (Init.Nat.mul (bs2nat (@hd (list bool) (@nil bool) l)) match match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
(* Goal: or (@eq (list bool) (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool))))) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))))) O)) *)
rewrite Normalize_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul match bs2nat (@nth (list bool) O l (@nil bool)) with | O => S O | S l => O end (bs2nat (@nth (list bool) (S O) l (@nil bool)))) (Init.Nat.mul (bs2nat (@nth (list bool) O l (@nil bool))) match match bs2nat (@nth (list bool) O l (@nil bool)) with | O => S O | S l => O end with | O => S O | S l => O end)) (Init.Nat.add (Init.Nat.mul match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (Init.Nat.mul (bs2nat (@hd (list bool) (@nil bool) l)) match match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
(* Goal: or (@eq (list bool) (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool))))) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))))) O)) *)
rewrite hd_nth_1, hd_nth_0.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: or (@eq (list bool) (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool))))) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))))) O)) *)
apply Normalize_normal.
Qed.

Opaque MultOneMinus_e.

(** Def 8 of (Rose) *)

Definition PlusOneMinus'_e : Cobham :=
  Comp 2 Cond [
    Proj 2 1;
    Comp 2 Succ_e [Proj 2 0];
    Proj 2 0;
    Proj 2 0
  ].

Lemma arity_PlusOneMinus' : arity PlusOneMinus'_e = ok_arity 2.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_PlusOneMinus' :
  rec_bounded PlusOneMinus'_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded Cond *)
(* Goal: rec_bounded PlusOneMinus_e *)
apply rec_bounded'_spec with 4.
(* Goal: @eq Arity (arity Cond) (ok_arity (S (S (S (S O))))) *)
(* Goal: rec_bounded' Cond *)
(* Goal: rec_bounded PlusOneMinus_e *)
apply arity_Cond.
(* Goal: rec_bounded' Cond *)
(* Goal: rec_bounded PlusOneMinus_e *)
apply rec_bounded_Cond.
(* Goal: rec_bounded Succ_e *)
apply rec_bounded_Succ.
Qed.

Lemma PlusOneMinus'_correct : forall l,
  hd nil (tl l) = nil \/ bs2nat (hd nil (tl l)) <> 0 ->
  bs2nat (Sem PlusOneMinus'_e l) = bs2nat (hd nil l) + (1 - bs2nat (hd nil (tl l))).
Proof.
(* Goal: forall (l : list (list bool)) (_ : or (@eq (list bool) (@hd (list bool) (@nil bool) (@tl (list bool) l)) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))) O))), @eq nat (bs2nat (Sem PlusOneMinus'_e l)) (Init.Nat.add (bs2nat (@hd (list bool) (@nil bool) l)) (Init.Nat.sub (S O) (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
intros [ | u [ | v l] ] H.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (Sem Cond (@cons (list bool) w (@cons (list bool) u (@cons (list bool) (Sem PlusOneMinus_e (@cons (list bool) u (@cons (list bool) v (@nil (list bool))))) (@cons (list bool) u (@nil (list bool)))))))) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat w) (Init.Nat.add (Nat.div2 (bs2nat w)) (Init.Nat.add (Nat.div2 (bs2nat w)) O))))) *)
rewrite Cond_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (Sem Succ_e (@cons (list bool) u (@nil (list bool))))) (Init.Nat.add (bs2nat u) match bs2nat (@nil bool) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) match bs2nat (@cons bool true v) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) match bs2nat (@cons bool false v) with | O => S O | S l => O end) *)
rewrite Succ_correct, bs2nat_nil.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.add (bs2nat l1) (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2))) (Init.Nat.add (Init.Nat.add (bs2nat l1) (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2))) O)) (Init.Nat.add (Init.Nat.add (bs2nat l1) (Init.Nat.add (bs2nat l1) O)) (Init.Nat.add (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2)) (Init.Nat.add (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2)) O))) *)
simpl; ring.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (Sem Cond (@cons (list bool) w (@cons (list bool) u (@cons (list bool) (Sem PlusOneMinus_e (@cons (list bool) u (@cons (list bool) v (@nil (list bool))))) (@cons (list bool) u (@nil (list bool)))))))) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat w) (Init.Nat.add (Nat.div2 (bs2nat w)) (Init.Nat.add (Nat.div2 (bs2nat w)) O))))) *)
rewrite Cond_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat match v with | nil => u | cons (true as b) l => Sem Succ_e (@cons (list bool) u (@nil (list bool))) | cons (false as b) l => u end) (Init.Nat.add (bs2nat u) (Init.Nat.sub (bs2nat v) (Init.Nat.add (Nat.div2 (bs2nat v)) (Init.Nat.add (Nat.div2 (bs2nat v)) O)))) *)
destruct v as [ | [ | ] v].
(* Goal: @eq nat (bs2nat (Sem Succ_e (@cons (list bool) u (@nil (list bool))))) (Init.Nat.add (bs2nat u) match bs2nat (@nil bool) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) match bs2nat (@cons bool true v) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) match bs2nat (@cons bool false v) with | O => S O | S l => O end) *)
rewrite Succ_correct, bs2nat_nil.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.add (bs2nat l1) (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2))) (Init.Nat.add (Init.Nat.add (bs2nat l1) (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2))) O)) (Init.Nat.add (Init.Nat.add (bs2nat l1) (Init.Nat.add (bs2nat l1) O)) (Init.Nat.add (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2)) (Init.Nat.add (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2)) O))) *)
simpl; ring.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) match bs2nat (@cons bool false v) with | O => S O | S l => O end) *)
simpl in H.
(* Goal: @eq nat (bs2nat (@cons bool false v)) (Init.Nat.add (Init.Nat.mul match bs2nat (@cons bool false v) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (bs2nat (@cons bool false v)) match match bs2nat (@cons bool false v) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
rewrite bs2nat_false in *.
(* Goal: @eq nat (Init.Nat.mul (S (S O)) (bs2nat v)) (Init.Nat.add (Init.Nat.mul match Init.Nat.mul (S (S O)) (bs2nat v) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (Init.Nat.mul (S (S O)) (bs2nat v)) match match Init.Nat.mul (S (S O)) (bs2nat v) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
destruct (2 * bs2nat v).
(* Goal: @eq nat O (Init.Nat.add (Init.Nat.mul (S O) (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul O O)) *)
(* Goal: @eq nat (S n) (Init.Nat.add (Init.Nat.mul O (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (S n) (S O))) *)
destruct H.
(* Goal: @eq nat (Nat.div2 (bs2nat (@fun_power (list bool) n (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l))))) (Nat.div2 (@fun_power nat n Nat.div2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
congruence.
(* Goal: @eq nat O (Init.Nat.add (Init.Nat.mul (S O) (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul O O)) *)
(* Goal: @eq nat (S n) (Init.Nat.add (Init.Nat.mul O (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (S n) (S O))) *)
tauto.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma PlusOneMinus'_length : forall l,
  length (Sem PlusOneMinus'_e [nth 0 l nil; Sem Normalize_e [nth 1 l nil]])
  <= S (length (hd nil l)).
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
 intros; simpl.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
 rewrite Cond_correct; simpl.
(* Goal: le (@length bool match @nth (list bool) (S (S O)) l (@nil bool) with | nil => @nth (list bool) O l (@nil bool) | cons (true as b) l0 => Sem PlusOneMinus_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) | cons (false as b) l0 => @nth (list bool) O l (@nil bool) end) (S (@length bool (@hd (list bool) (@nil bool) l))) *)
 rewrite hd_nth_0.
(* Goal: le (@length bool match Sem Normalize_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool))) with | nil => Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))) | cons (true as b) l0 => @nth (list bool) O l (@nil bool) | cons (false as b) l0 => @nth (list bool) O l (@nil bool) end) (S (@length bool (@nth (list bool) O l (@nil bool)))) *)
 destruct (Sem Normalize_e [nth 1 l nil]); auto.
(* Goal: le (@length bool (Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) (S (@length bool (@nth (list bool) O l (@nil bool)))) *)
(* Goal: le (@length bool (if b then @nth (list bool) O l (@nil bool) else @nth (list bool) O l (@nil bool))) (S (@length bool (@nth (list bool) O l (@nil bool)))) *)
 apply Succ_length.
(* Goal: le (@length bool (if b then Sem PlusOneMinus_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) else @nth (list bool) O l (@nil bool))) (S (@length bool (@nth (list bool) O l (@nil bool)))) *)
 case b; auto.
Qed.

Opaque PlusOneMinus'_e.

Definition PlusOneMinus_e : Cobham :=
  Comp 2 PlusOneMinus'_e [Proj 2 0; Comp 2 Normalize_e [Proj 2 1] ].

Lemma arity_PlusOneMinus : arity PlusOneMinus_e = ok_arity 2.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_PlusOneMinus :
  rec_bounded PlusOneMinus_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded PlusOneMinus'_e *)
(* Goal: rec_bounded Normalize_e *)
apply rec_bounded_PlusOneMinus'.
(* Goal: rec_bounded Normalize_e *)
apply rec_bounded_Normalize.
Qed.

Lemma PlusOneMinus_correct : forall l,
  bs2nat (Sem PlusOneMinus_e l) = bs2nat (hd nil l) + (1 - bs2nat (hd nil (tl l))).
Proof.
(* Goal: forall l : list (list bool), @eq nat (@length bool (Sem DivTwoPower_e l)) (Init.Nat.sub (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
intro l.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (Sem PlusOneMinus'_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@nil (list bool)))))) (Init.Nat.add (bs2nat (@hd (list bool) (@nil bool) l)) match bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)) with | O => S O | S l => O end) *)
rewrite PlusOneMinus'_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul match bs2nat (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) with | O => S O | S l => O end (bs2nat (@nth (list bool) (S O) l (@nil bool)))) (Init.Nat.mul (bs2nat (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) match match bs2nat (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) with | O => S O | S l => O end with | O => S O | S l => O end)) (Init.Nat.add (Init.Nat.mul match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (Init.Nat.mul (bs2nat (@hd (list bool) (@nil bool) l)) match match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
(* Goal: or (@eq (list bool) (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool))))) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))))) O)) *)
rewrite Normalize_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul match bs2nat (@nth (list bool) O l (@nil bool)) with | O => S O | S l => O end (bs2nat (@nth (list bool) (S O) l (@nil bool)))) (Init.Nat.mul (bs2nat (@nth (list bool) O l (@nil bool))) match match bs2nat (@nth (list bool) O l (@nil bool)) with | O => S O | S l => O end with | O => S O | S l => O end)) (Init.Nat.add (Init.Nat.mul match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (Init.Nat.mul (bs2nat (@hd (list bool) (@nil bool) l)) match match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
(* Goal: or (@eq (list bool) (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool))))) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))))) O)) *)
rewrite hd_nth_1, hd_nth_0.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: or (@eq (list bool) (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool))))) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))))) O)) *)
apply Normalize_normal.
Qed.

Lemma PlusOneMinus_length : forall l,
  length (Sem PlusOneMinus_e [nth 0 l nil; nth 1 l nil]) <= S (length (nth 0 l nil)).
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
 intros; simpl.
(* Goal: le (@length bool (Sem PlusOneMinus'_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@nil (list bool)))))) (S (@length bool (@nth (list bool) O l (@nil bool)))) *)
 rewrite <- hd_nth_0 at 2.
(* Goal: le (@length bool (Sem PlusOneMinus'_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@nil (list bool)))))) (S (@length bool (@hd (list bool) (@nil bool) l))) *)
 apply PlusOneMinus'_length.
Qed.

Opaque PlusOneMinus_e.

(** Def 9 of (Rose) *)

Definition OneMinusMultPlus'_e : Cobham :=
  Rec
    (Proj 1 0)
    (Comp 3 (Succ false) [Proj 3 0])
    (Comp 3 (Succ true) [Proj 3 0])
    (Comp 2 Smash [Comp 2 Succ_e [Proj 2 1]; Comp 2 (Succ true) [Proj 2 0]]).

Lemma arity_OneMinusMultPlus' : arity OneMinusMultPlus'_e = ok_arity 2.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_OneMinusMultPlus' :
  rec_bounded OneMinusMultPlus'_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded Succ_e *)
apply rec_bounded_Succ.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) O vl (@nil bool))) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) (@cons bool true (@nth (list bool) O l (@nil bool))))) *)
destruct l as [ | v l].
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
induction v as [ | [ | ] v IH]; simpl.
(* Goal: le (S (@length bool v)) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons bool true (@cons bool false v)))) *)
rewrite length_smash.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) u (@nil (list bool)))) (S (S (Init.Nat.mul (@length bool u) (S O)))) *)
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) u (@cons (list bool) v l))) (S (@length bool (smash' v (smash_bs u (@cons bool true v))))) *)
rewrite mult_1_r.
(* Goal: le (@length bool (@nth (list bool) O l (@nil bool))) (S (@length bool (Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))))) *)
(* Goal: le (S (@length bool v)) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons bool true (@cons bool true v)))) *)
(* Goal: le (S (@length bool v)) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons bool true (@cons bool false v)))) *)
eapply le_trans; [idtac | apply le_n_S; apply le_length_Succ].
(* Goal: le (@length bool z) (@length bool x) *)
omega.
(* Goal: le (S (@length bool v)) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons bool true (@cons bool false v)))) *)
rewrite length_smash.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: le (S (@length bool v)) (S (Init.Nat.mul (@length bool (Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) (S (S (@length bool v))))) *)
apply le_n_S.
(* Goal: le (@length bool v) (Init.Nat.mul (@length bool (Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) (S (S (@length bool v)))) *)
rewrite <- (mult_1_l (length v)).
(* Goal: le (Nat.mul (S O) (@length bool v)) (Init.Nat.mul (@length bool (Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) (S (S (Nat.mul (S O) (@length bool v))))) *)
apply mult_le_compat.
(* Goal: le (S O) (@length bool (Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) *)
(* Goal: le (@length bool v) (S (S (Nat.mul (S O) (@length bool v)))) *)
apply le_1_length_Succ.
(* Goal: le (@length bool z) (@length bool x) *)
omega.
(* Goal: le (S (@length bool v)) (@length bool (smash_bs (Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons bool true (@cons bool false v)))) *)
rewrite length_smash.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: le (S (@length bool v)) (S (Init.Nat.mul (@length bool (Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) (S (S (@length bool v))))) *)
apply le_n_S.
(* Goal: le (@length bool v) (Init.Nat.mul (@length bool (Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) (S (S (@length bool v)))) *)
rewrite <- (mult_1_l (length v)).
(* Goal: le (Nat.mul (S O) (@length bool v)) (Init.Nat.mul (@length bool (Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) (S (S (Nat.mul (S O) (@length bool v))))) *)
apply mult_le_compat.
(* Goal: le (S O) (@length bool (Sem Succ_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) *)
(* Goal: le (@length bool v) (S (S (Nat.mul (S O) (@length bool v)))) *)
apply le_1_length_Succ.
(* Goal: le (@length bool z) (@length bool x) *)
omega.
Qed.

Lemma OneMinusMultPlus'_correct : forall l,
  hd nil l = nil \/ bs2nat (hd nil l) <> 0 ->
  bs2nat (Sem OneMinusMultPlus'_e l) =
  (1 - bs2nat (hd nil l)) * bs2nat (hd nil (tl l)) +
  bs2nat (hd nil l) * (1 - (1 - bs2nat (hd nil l))).
Proof.
(* Goal: forall (l : list (list bool)) (_ : or (@eq (list bool) (@hd (list bool) (@nil bool) l) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) l)) O))), @eq nat (bs2nat (Sem OneMinusMultPlus'_e l)) (Init.Nat.add (Init.Nat.mul (Init.Nat.sub (S O) (bs2nat (@hd (list bool) (@nil bool) l))) (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (Init.Nat.mul (bs2nat (@hd (list bool) (@nil bool) l)) (Init.Nat.sub (S O) (Init.Nat.sub (S O) (bs2nat (@hd (list bool) (@nil bool) l)))))) *)
intros [ | v l] H.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
destruct v as [ | [ | ] v]; simpl.
(* Goal: @eq nat (bs2nat (@nth (list bool) O l (@nil bool))) (Init.Nat.add (Init.Nat.mul match bs2nat (@nil bool) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (bs2nat (@nil bool)) match match bs2nat (@nil bool) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
(* Goal: @eq nat (bs2nat (@cons bool true v)) (Init.Nat.add (Init.Nat.mul match bs2nat (@cons bool true v) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (bs2nat (@cons bool true v)) match match bs2nat (@cons bool true v) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
(* Goal: @eq nat (bs2nat (@cons bool false v)) (Init.Nat.add (Init.Nat.mul match bs2nat (@cons bool false v) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (bs2nat (@cons bool false v)) match match bs2nat (@cons bool false v) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
rewrite bs2nat_nil, hd_nth_0.
(* Goal: @eq nat (Init.Nat.mul (power (S (S O)) (@length bool (@nth (list bool) (S O) l (@nil bool)))) (bs2nat (@nth (list bool) O l (@nil bool)))) (Init.Nat.mul (bs2nat (@nth (list bool) O l (@nil bool))) (power (S (S O)) (@length bool (@nth (list bool) (S O) l (@nil bool))))) *)
ring.
(* Goal: @eq nat (Init.Nat.add (bs2nat u) match bs2nat v with | O => S O | S l => O end) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool true w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) O))))) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool false w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) O))))) *)
rewrite bs2nat_true.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.add (bs2nat l1) (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2))) (Init.Nat.add (Init.Nat.add (bs2nat l1) (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2))) O)) (Init.Nat.add (Init.Nat.add (bs2nat l1) (Init.Nat.add (bs2nat l1) O)) (Init.Nat.add (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2)) (Init.Nat.add (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2)) O))) *)
simpl; ring.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
simpl in *.
(* Goal: @eq nat (bs2nat (@cons bool false v)) (Init.Nat.add (Init.Nat.mul match bs2nat (@cons bool false v) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (bs2nat (@cons bool false v)) match match bs2nat (@cons bool false v) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
rewrite bs2nat_false in *.
(* Goal: @eq nat (Init.Nat.mul (S (S O)) (bs2nat v)) (Init.Nat.add (Init.Nat.mul match Init.Nat.mul (S (S O)) (bs2nat v) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (Init.Nat.mul (S (S O)) (bs2nat v)) match match Init.Nat.mul (S (S O)) (bs2nat v) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
destruct (2 * bs2nat v).
(* Goal: @eq nat O (Init.Nat.add (Init.Nat.mul (S O) (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul O O)) *)
(* Goal: @eq nat (S n) (Init.Nat.add (Init.Nat.mul O (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (S n) (S O))) *)
destruct H.
(* Goal: @eq nat (Nat.div2 (bs2nat (@fun_power (list bool) n (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l))))) (Nat.div2 (@fun_power nat n Nat.div2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
congruence.
(* Goal: @eq nat O (Init.Nat.add (Init.Nat.mul (S O) (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul O O)) *)
(* Goal: @eq nat (S n) (Init.Nat.add (Init.Nat.mul O (bs2nat (@hd (list bool) (@nil bool) l))) (Init.Nat.mul (S n) (S O))) *)
tauto.
(* Goal: @eq nat (Init.Nat.mul (power (S (S O)) (@length bool (@nth (list bool) (S O) l (@nil bool)))) (bs2nat (@nth (list bool) O l (@nil bool)))) (Init.Nat.mul (bs2nat (@nth (list bool) O l (@nil bool))) (power (S (S O)) (@length bool (@nth (list bool) (S O) l (@nil bool))))) *)
ring.
Qed.

Opaque OneMinusMultPlus'_e.

Definition OneMinusMultPlus_e : Cobham :=
  Comp 2 OneMinusMultPlus'_e [Comp 2 Normalize_e [Proj 2 0]; Proj 2 1].

Lemma arity_OneMinusMultPlus : arity OneMinusMultPlus_e = ok_arity 2.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_OneMinusMultPlus :
  rec_bounded OneMinusMultPlus_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded OneMinusMultPlus'_e *)
(* Goal: rec_bounded Normalize_e *)
apply rec_bounded_OneMinusMultPlus'.
(* Goal: rec_bounded Normalize_e *)
apply rec_bounded_Normalize.
Qed.

Lemma OneMinusMultPlus_correct : forall l,
  bs2nat (Sem OneMinusMultPlus_e l) =
  (1 - bs2nat (hd nil l)) * bs2nat (hd nil (tl l)) +
  bs2nat (hd nil l) * (1 - (1 - bs2nat (hd nil l))).
Proof.
(* Goal: forall l : list (list bool), @eq nat (@length bool (Sem DivTwoPower_e l)) (Init.Nat.sub (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
intro l.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (Sem OneMinusMultPlus'_e (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))))) (Init.Nat.add (Init.Nat.mul match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (Init.Nat.mul (bs2nat (@hd (list bool) (@nil bool) l)) match match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
rewrite OneMinusMultPlus'_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul match bs2nat (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) with | O => S O | S l => O end (bs2nat (@nth (list bool) (S O) l (@nil bool)))) (Init.Nat.mul (bs2nat (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) match match bs2nat (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) with | O => S O | S l => O end with | O => S O | S l => O end)) (Init.Nat.add (Init.Nat.mul match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (Init.Nat.mul (bs2nat (@hd (list bool) (@nil bool) l)) match match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
(* Goal: or (@eq (list bool) (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool))))) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))))) O)) *)
rewrite Normalize_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul match bs2nat (@nth (list bool) O l (@nil bool)) with | O => S O | S l => O end (bs2nat (@nth (list bool) (S O) l (@nil bool)))) (Init.Nat.mul (bs2nat (@nth (list bool) O l (@nil bool))) match match bs2nat (@nth (list bool) O l (@nil bool)) with | O => S O | S l => O end with | O => S O | S l => O end)) (Init.Nat.add (Init.Nat.mul match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (Init.Nat.mul (bs2nat (@hd (list bool) (@nil bool) l)) match match bs2nat (@hd (list bool) (@nil bool) l) with | O => S O | S l => O end with | O => S O | S l => O end)) *)
(* Goal: or (@eq (list bool) (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool))))) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))))) O)) *)
rewrite hd_nth_1, hd_nth_0.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: or (@eq (list bool) (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool))))) (@nil bool)) (not (@eq nat (bs2nat (@hd (list bool) (@nil bool) (@cons (list bool) (Sem Normalize_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))))) O)) *)
apply Normalize_normal.
Qed.

Opaque OneMinusMultPlus_e.

(** Def 10 of (Rose) *)

Definition PlusMod2_e : Cobham :=
  Comp 2 Cond [
     Proj 2 1;
     Proj 2 0;
     Comp 2 Succ_e [Proj 2 0];
     Proj 2 0
  ].

Lemma arity_PlusMod2 :
  arity PlusMod2_e = ok_arity 2.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_PlusMod2 :
  rec_bounded PlusMod2_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded Cond *)
(* Goal: rec_bounded PlusOneMinus_e *)
apply rec_bounded'_spec with 4.
(* Goal: @eq Arity (arity Cond) (ok_arity (S (S (S (S O))))) *)
(* Goal: rec_bounded' Cond *)
(* Goal: rec_bounded PlusOneMinus_e *)
apply arity_Cond.
(* Goal: rec_bounded' Cond *)
(* Goal: rec_bounded PlusOneMinus_e *)
apply rec_bounded_Cond.
(* Goal: rec_bounded Succ_e *)
apply rec_bounded_Succ.
Qed.

Lemma PlusMod2_correct : forall l,
  bs2nat (Sem PlusMod2_e l) =
  bs2nat (hd nil l) + mod2 (bs2nat (hd nil (tl l))).
Proof.
(* Goal: forall l : list (list bool), @eq nat (bs2nat (Sem PlusOneMinusMod2_e l)) (Init.Nat.add (bs2nat (@hd (list bool) (@nil bool) l)) (Init.Nat.mul (Init.Nat.sub (S O) (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (mod2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) (@tl (list bool) l))))))) *)
unfold mod2.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
intros [ | u [ | v l] ]; simpl.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
rewrite Cond_correct, bs2nat_nil; simpl.
(* Goal: le (@length bool z) (@length bool x) *)
omega.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
rewrite Cond_correct; simpl.
(* Goal: @eq nat (bs2nat match v with | nil => u | cons (true as b) l => Sem Succ_e (@cons (list bool) u (@nil (list bool))) | cons (false as b) l => u end) (Init.Nat.add (bs2nat u) (Init.Nat.sub (bs2nat v) (Init.Nat.add (Nat.div2 (bs2nat v)) (Init.Nat.add (Nat.div2 (bs2nat v)) O)))) *)
destruct v as [ | [ | ] v].
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@nil bool)) (Init.Nat.add (Nat.div2 (bs2nat (@nil bool))) (Init.Nat.add (Nat.div2 (bs2nat (@nil bool))) O))))) *)
(* Goal: @eq nat (bs2nat (Sem PlusOneMinus_e (@cons (list bool) u (@cons (list bool) v (@nil (list bool)))))) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool true w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) O))))) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool false w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) O))))) *)
rewrite bs2nat_nil.
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
(* Goal: @eq nat (bs2nat (Sem Succ_e (@cons (list bool) u (@nil (list bool))))) (Init.Nat.add (bs2nat u) (Init.Nat.sub (bs2nat (@cons bool true v)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true v))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true v))) O)))) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.sub (bs2nat (@cons bool false v)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false v))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false v))) O)))) *)
rewrite bs2nat_true, Succ_correct.
(* Goal: @eq nat (Init.Nat.add (S O) (bs2nat (@hd (list bool) (@nil bool) (@cons (list bool) u (@nil (list bool)))))) (Init.Nat.add (bs2nat u) (Init.Nat.sub (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) (bs2nat v))) (Init.Nat.add (Nat.div2 (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) (bs2nat v)))) (Init.Nat.add (Nat.div2 (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) (bs2nat v)))) O)))) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.sub (bs2nat (@cons bool false v)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false v))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false v))) O)))) *)
change (1 + 2 * bs2nat v) with (S (2 * bs2nat v)).
(* Goal: @eq nat (Init.Nat.add (bs2nat u) match bs2nat v with | O => S O | S l => O end) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (S (Init.Nat.mul (S (S O)) (bs2nat w))) (Init.Nat.add (Nat.div2 (S (Init.Nat.mul (S (S O)) (bs2nat w)))) (Init.Nat.add (Nat.div2 (S (Init.Nat.mul (S (S O)) (bs2nat w)))) O))))) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool false w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) O))))) *)
rewrite div2_double_plus_one.
(* Goal: le (@length bool z) (@length bool x) *)
simpl hd; omega.
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.sub (bs2nat (@cons bool false v)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false v))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false v))) O)))) *)
rewrite bs2nat_false, div2_double.
(* Goal: le (@length bool z) (@length bool x) *)
omega.
Qed.

Opaque PlusMod2_e.

(** Def 11 of (Rose) *)

Definition PlusOneMinusMod2_e : Cobham :=
  Comp 3 Cond [
    Proj 3 2;
    Proj 3 0;
    Comp 3 PlusOneMinus_e [Proj 3 0; Proj 3 1];
    Proj 3 0
  ].

Lemma arity_PlusOneMinusMod2 :
  arity PlusOneMinusMod2_e = ok_arity 3.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_PlusOneMinusMod2 :
  rec_bounded PlusOneMinusMod2_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded Cond *)
(* Goal: rec_bounded PlusOneMinus_e *)
apply rec_bounded'_spec with 4.
(* Goal: @eq Arity (arity Cond) (ok_arity (S (S (S (S O))))) *)
(* Goal: rec_bounded' Cond *)
(* Goal: rec_bounded PlusOneMinus_e *)
apply arity_Cond.
(* Goal: rec_bounded' Cond *)
(* Goal: rec_bounded PlusOneMinus_e *)
apply rec_bounded_Cond.
(* Goal: rec_bounded PlusOneMinus_e *)
apply rec_bounded_PlusOneMinus.
Qed.

Lemma PlusOneMinusMod2_correct : forall l,
  bs2nat (Sem PlusOneMinusMod2_e l) =
  bs2nat (hd nil l) +
  (1 - bs2nat (hd nil (tl l))) *
  mod2 (bs2nat (hd nil (tl (tl l)))).
Proof.
(* Goal: forall l : list (list bool), @eq nat (bs2nat (Sem PlusOneMinusMod2_e l)) (Init.Nat.add (bs2nat (@hd (list bool) (@nil bool) l)) (Init.Nat.mul (Init.Nat.sub (S O) (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (mod2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) (@tl (list bool) l))))))) *)
unfold mod2.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
intros [ | u [ | v [ | w l] ] ]; simpl.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (Sem Cond (@cons (list bool) w (@cons (list bool) u (@cons (list bool) (Sem PlusOneMinus_e (@cons (list bool) u (@cons (list bool) v (@nil (list bool))))) (@cons (list bool) u (@nil (list bool)))))))) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat w) (Init.Nat.add (Nat.div2 (bs2nat w)) (Init.Nat.add (Nat.div2 (bs2nat w)) O))))) *)
rewrite Cond_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@nil bool)) (Init.Nat.add (Nat.div2 (bs2nat (@nil bool))) (Init.Nat.add (Nat.div2 (bs2nat (@nil bool))) O))))) *)
(* Goal: @eq nat (bs2nat (Sem PlusOneMinus_e (@cons (list bool) u (@cons (list bool) v (@nil (list bool)))))) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool true w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) O))))) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool false w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) O))))) *)
rewrite bs2nat_nil.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.add (bs2nat l1) (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2))) (Init.Nat.add (Init.Nat.add (bs2nat l1) (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2))) O)) (Init.Nat.add (Init.Nat.add (bs2nat l1) (Init.Nat.add (bs2nat l1) O)) (Init.Nat.add (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2)) (Init.Nat.add (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2)) O))) *)
simpl; ring.
(* Goal: @eq nat (bs2nat (Sem Cond (@cons (list bool) w (@cons (list bool) u (@cons (list bool) (Sem PlusOneMinus_e (@cons (list bool) u (@cons (list bool) v (@nil (list bool))))) (@cons (list bool) u (@nil (list bool)))))))) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat w) (Init.Nat.add (Nat.div2 (bs2nat w)) (Init.Nat.add (Nat.div2 (bs2nat w)) O))))) *)
rewrite Cond_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat match w with | nil => u | cons (true as b) l => Sem PlusOneMinus_e (@cons (list bool) u (@cons (list bool) v (@nil (list bool)))) | cons (false as b) l => u end) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat w) (Init.Nat.add (Nat.div2 (bs2nat w)) (Init.Nat.add (Nat.div2 (bs2nat w)) O))))) *)
destruct w as [ | [ | ] w].
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@nil bool)) (Init.Nat.add (Nat.div2 (bs2nat (@nil bool))) (Init.Nat.add (Nat.div2 (bs2nat (@nil bool))) O))))) *)
(* Goal: @eq nat (bs2nat (Sem PlusOneMinus_e (@cons (list bool) u (@cons (list bool) v (@nil (list bool)))))) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool true w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) O))))) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool false w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) O))))) *)
rewrite bs2nat_nil.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.add (bs2nat l1) (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2))) (Init.Nat.add (Init.Nat.add (bs2nat l1) (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2))) O)) (Init.Nat.add (Init.Nat.add (bs2nat l1) (Init.Nat.add (bs2nat l1) O)) (Init.Nat.add (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2)) (Init.Nat.add (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2)) O))) *)
simpl; ring.
(* Goal: @eq nat (bs2nat (Sem PlusOneMinus_e (@cons (list bool) u (@cons (list bool) v (@nil (list bool)))))) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool true w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) O))))) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool false w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) O))))) *)
rewrite PlusOneMinus_correct.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (Init.Nat.add (bs2nat u) match bs2nat v with | O => S O | S l => O end) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool true w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) O))))) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool false w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) O))))) *)
rewrite bs2nat_true.
(* Goal: @eq nat (Init.Nat.add (bs2nat u) match bs2nat v with | O => S O | S l => O end) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) (bs2nat w))) (Init.Nat.add (Nat.div2 (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) (bs2nat w)))) (Init.Nat.add (Nat.div2 (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) (bs2nat w)))) O))))) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool false w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) O))))) *)
change (1 + 2 * bs2nat w) with (S (2 * bs2nat w)).
(* Goal: @eq nat (Init.Nat.add (bs2nat u) match bs2nat v with | O => S O | S l => O end) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (S (Init.Nat.mul (S (S O)) (bs2nat w))) (Init.Nat.add (Nat.div2 (S (Init.Nat.mul (S (S O)) (bs2nat w)))) (Init.Nat.add (Nat.div2 (S (Init.Nat.mul (S (S O)) (bs2nat w)))) O))))) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool false w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) O))))) *)
rewrite div2_double_plus_one.
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (Init.Nat.mul (S (S O)) (bs2nat w)) (Init.Nat.add (bs2nat w) (Init.Nat.add (bs2nat w) O))))) *)
case (bs2nat v).
(* Goal: le (@length bool z) (@length bool x) *)
omega.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@cons bool false (@firstn bool n l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub n O) l))) *)
rewrite bs2nat_false.
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (Init.Nat.mul (S (S O)) (bs2nat w)) (Init.Nat.add (Nat.div2 (Init.Nat.mul (S (S O)) (bs2nat w))) (Init.Nat.add (Nat.div2 (Init.Nat.mul (S (S O)) (bs2nat w))) O))))) *)
rewrite div2_double.
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (Init.Nat.mul (S (S O)) (bs2nat w)) (Init.Nat.add (bs2nat w) (Init.Nat.add (bs2nat w) O))))) *)
case (bs2nat v).
(* Goal: le (@length bool z) (@length bool x) *)
omega.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma PlusOneMinusMod2_length : forall l,
  length (Sem PlusOneMinusMod2_e l) <= S (length (hd nil l)).
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
 intros; simpl.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
 rewrite Cond_correct; simpl.
(* Goal: le (@length bool match @nth (list bool) (S (S O)) l (@nil bool) with | nil => @nth (list bool) O l (@nil bool) | cons (true as b) l0 => Sem PlusOneMinus_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) | cons (false as b) l0 => @nth (list bool) O l (@nil bool) end) (S (@length bool (@hd (list bool) (@nil bool) l))) *)
 rewrite hd_nth_0.
(* Goal: le (@length bool match @nth (list bool) (S (S O)) l (@nil bool) with | nil => @nth (list bool) O l (@nil bool) | cons (true as b) l0 => Sem PlusOneMinus_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) | cons (false as b) l0 => @nth (list bool) O l (@nil bool) end) (S (@length bool (@nth (list bool) O l (@nil bool)))) *)
 destruct (nth 2 l nil); auto.
(* Goal: le (@length bool (if b then Sem PlusOneMinus_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))) else @nth (list bool) O l (@nil bool))) (S (@length bool (@nth (list bool) O l (@nil bool)))) *)
 case b; auto.
(* Goal: le (@length bool (Sem PlusOneMinus_e (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@nil (list bool)))))) (S (@length bool (@nth (list bool) O l (@nil bool)))) *)
 apply PlusOneMinus_length.
Qed.

Opaque PlusOneMinusMod2_e.

(** Def 13 of (Rose) *)

Definition MultTwoPowerLength'_e : Cobham :=
  Rec2
    (Proj 1 0)
    (Comp 3 (Succ false) [Proj 3 1])
    (Comp 2 Smash [Comp 2 (Succ true) [Proj 2 0]; Comp 2 (Succ true) [Proj 2 1] ] ).

(* FIXME: According to Rose (Def 13), 'plus 1' in arguments of Smash are not necessary
 *)

Lemma arity_MultTwoPowerLength' :
  arity MultTwoPowerLength'_e = ok_arity 2.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_MultTwoPowerLength' :
  rec_bounded MultTwoPowerLength'_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
destruct l as [ | u [ | v l] ]; simpl.
(* Goal: le (@length bool z) (@length bool x) *)
omega.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
rewrite length_smash; simpl.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) u (@nil (list bool)))) (S (S (Init.Nat.mul (@length bool u) (S O)))) *)
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) u (@cons (list bool) v l))) (S (@length bool (smash' v (smash_bs u (@cons bool true v))))) *)
rewrite mult_1_r.
(* Goal: le (@length bool z) (@length bool x) *)
induction u as [ | [ | ] u IH]; simpl; omega.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
rewrite length_smash', length_smash; simpl.
(* Goal: le (@length bool z) (@length bool x) *)
induction u as [ | [ | ] u IH]; simpl; omega.
Qed.

Lemma MultTwoPowerLength'_correct : forall l,
  bs2nat (Sem MultTwoPowerLength'_e l) =
  power 2 (length (hd nil l)) * bs2nat (hd nil (tl l)).
Proof.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
destruct l as [ | u [ | v l] ].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) u (@nil (list bool)))) (Init.Nat.mul (power (S (S O)) (@length bool u)) (bs2nat (@nil bool))) *)
(* Goal: @eq nat (bs2nat (Sem MultTwoPowerLength'_e (@cons (list bool) u (@cons (list bool) v l)))) (Init.Nat.mul (power (S (S O)) (@length bool (@hd (list bool) (@nil bool) (@cons (list bool) u (@cons (list bool) v l))))) (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) (@cons (list bool) u (@cons (list bool) v l)))))) *)
rewrite bs2nat_nil, mult_0_r.
(* Goal: @eq (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@fun_power (list bool) (@length bool u) (@tl bool) v) *)
induction u as [ | [ | ] u IH].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (@cons bool false (@firstn bool n l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub n O) l))) *)
rewrite bs2nat_false.
(* Goal: le (@length bool z) (@length bool x) *)
omega.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (@cons bool false (@firstn bool n l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub n O) l))) *)
rewrite bs2nat_false.
(* Goal: le (@length bool z) (@length bool x) *)
omega.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
induction u as [ | [ | ] u IH]; simpl in *.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@cons bool false (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) u (@cons (list bool) v l)))) (Init.Nat.mul (Init.Nat.add (power (S (S O)) (@length bool u)) (Init.Nat.add (power (S (S O)) (@length bool u)) O)) (bs2nat v)) *)
rewrite bs2nat_false, plus_0_r, IH.
(* Goal: @eq nat (Init.Nat.mul (power (S (S O)) (@length bool (@nth (list bool) (S O) l (@nil bool)))) (bs2nat (@nth (list bool) O l (@nil bool)))) (Init.Nat.mul (bs2nat (@nth (list bool) O l (@nil bool))) (power (S (S O)) (@length bool (@nth (list bool) (S O) l (@nil bool))))) *)
ring.
(* Goal: @eq nat (bs2nat (@cons bool false (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) (fun vl : list (list bool) => @cons bool false (@nth (list bool) (S O) vl (@nil bool))) u (@cons (list bool) v l)))) (Init.Nat.mul (Init.Nat.add (power (S (S O)) (@length bool u)) (Init.Nat.add (power (S (S O)) (@length bool u)) O)) (bs2nat v)) *)
rewrite bs2nat_false, plus_0_r, IH.
(* Goal: @eq nat (Init.Nat.mul (power (S (S O)) (@length bool (@nth (list bool) (S O) l (@nil bool)))) (bs2nat (@nth (list bool) O l (@nil bool)))) (Init.Nat.mul (bs2nat (@nth (list bool) O l (@nil bool))) (power (S (S O)) (@length bool (@nth (list bool) (S O) l (@nil bool))))) *)
ring.
Qed.

Opaque MultTwoPowerLength'_e.

Definition MultTwoPowerLength_e : Cobham :=
  Comp 2 MultTwoPowerLength'_e [Proj 2 1; Proj 2 0].

Lemma arity_MultTwoPowerLength :
  arity MultTwoPowerLength_e = ok_arity 2.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_MultTwoPowerLength :
  rec_bounded MultTwoPowerLength_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded MultTwoPowerLength'_e *)
apply rec_bounded_MultTwoPowerLength'.
Qed.

Lemma MultTwoPowerLength_correct : forall l,
  bs2nat (Sem MultTwoPowerLength_e l) =
  bs2nat (hd nil l) * power 2 (length (hd nil (tl l))).
Proof.
(* Goal: forall l : list (list bool), @eq nat (@length bool (Sem DivTwoPower_e l)) (Init.Nat.sub (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
intro l.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
rewrite MultTwoPowerLength'_correct; simpl.
(* Goal: @eq nat (Init.Nat.mul (power (S (S O)) (@length bool (@nth (list bool) (S O) l (@nil bool)))) (bs2nat (@nth (list bool) O l (@nil bool)))) (Init.Nat.mul (bs2nat (@hd (list bool) (@nil bool) l)) (power (S (S O)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
rewrite hd_nth_0, hd_nth_1.
(* Goal: @eq nat (Init.Nat.mul (power (S (S O)) (@length bool (@nth (list bool) (S O) l (@nil bool)))) (bs2nat (@nth (list bool) O l (@nil bool)))) (Init.Nat.mul (bs2nat (@nth (list bool) O l (@nil bool))) (power (S (S O)) (@length bool (@nth (list bool) (S O) l (@nil bool))))) *)
ring.
Qed.

Opaque MultTwoPowerLength_e.

(** Def 14 of (Rose) *)

Definition DivTwoPower'_e : Cobham :=
  Rec2
    (Proj 1 0)
    (Comp 3 Div2_e [Proj 3 1])
    (Proj 2 1).

Lemma arity_DivTwoPower' :
  arity DivTwoPower'_e = ok_arity 2.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma length_DivTwoPower' : forall l,
  length (Sem DivTwoPower'_e l) = length (hd nil (tl l)) - length (hd nil l).
Proof.
(* Goal: forall l : list (list bool), @eq (list bool) (Sem DivTwoPower'_e l) (@fun_power (list bool) (@length bool (@hd (list bool) (@nil bool) l)) (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l))) *)
intros [ | u [ | v l] ].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@fun_power (list bool) (@length bool u) (@tl bool) v) *)
induction u as [ | [ | ] u IH].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: le (@length bool (Sem Div2_e (@cons (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@nil (list bool))))) (@length bool v) *)
rewrite length_Div2.
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: le (@length bool (Sem Div2_e (@cons (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@nil (list bool))))) (@length bool v) *)
rewrite length_Div2.
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
(* Goal: @eq (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@fun_power (list bool) (@length bool u) (@tl bool) v) *)
induction u as [ | [ | ] u IH].
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
simpl in *.
(* Goal: le (@length bool (Sem Div2_e (@cons (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@nil (list bool))))) (@length bool v) *)
rewrite length_Div2.
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
simpl in *.
(* Goal: le (@length bool (Sem Div2_e (@cons (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@nil (list bool))))) (@length bool v) *)
rewrite length_Div2.
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
Qed.

Lemma rec_bounded_DivTwoPower' :
  rec_bounded DivTwoPower'_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded Div2_e *)
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
apply rec_bounded_Div2.
(* Goal: rec_bounded Div2_e *)
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
apply rec_bounded_Div2.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
destruct l as [ | u [ | v l] ].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@fun_power (list bool) (@length bool u) (@tl bool) v) *)
induction u as [ | [ | ] u IH].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: le (@length bool (Sem Div2_e (@cons (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@nil (list bool))))) (@length bool v) *)
rewrite length_Div2.
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: le (@length bool (Sem Div2_e (@cons (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@nil (list bool))))) (@length bool v) *)
rewrite length_Div2.
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
(* Goal: @eq (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@fun_power (list bool) (@length bool u) (@tl bool) v) *)
induction u as [ | [ | ] u IH].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
simpl in *.
(* Goal: le (@length bool (Sem Div2_e (@cons (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@nil (list bool))))) (@length bool v) *)
rewrite length_Div2.
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
simpl in *.
(* Goal: le (@length bool (Sem Div2_e (@cons (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@nil (list bool))))) (@length bool v) *)
rewrite length_Div2.
(* Goal: le (@length bool z) (@length bool x) *)
simpl; omega.
Qed.

Lemma DivTwoPower'_correct_bs : forall l,
  Sem DivTwoPower'_e l =
  fun_power (length (hd nil l)) (@tl _) (hd nil (tl l)).
Proof.
(* Goal: forall l : list (list bool), @eq (list bool) (Sem DivTwoPower'_e l) (@fun_power (list bool) (@length bool (@hd (list bool) (@nil bool) l)) (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l))) *)
intros [ | u [ | v l] ].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@fun_power (list bool) (@length bool u) (@tl bool) v) *)
induction u as [ | [ | ] u IH].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq (list bool) (Sem Div2_e (@cons (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@nil (list bool)))) (@tl bool (@fun_power (list bool) (@length bool u) (@tl bool) v)) *)
rewrite Div2_correct_bs.
(* Goal: @eq nat (Nat.div2 (bs2nat (@fun_power (list bool) n (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l))))) (Nat.div2 (@fun_power nat n Nat.div2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
simpl; congruence.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq (list bool) (Sem Div2_e (@cons (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@nil (list bool)))) (@tl bool (@fun_power (list bool) (@length bool u) (@tl bool) v)) *)
rewrite Div2_correct_bs.
(* Goal: @eq nat (Nat.div2 (bs2nat (@fun_power (list bool) n (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l))))) (Nat.div2 (@fun_power nat n Nat.div2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
simpl; congruence.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@fun_power (list bool) (@length bool u) (@tl bool) v) *)
induction u as [ | [ | ] u IH].
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq (list bool) (Sem Div2_e (@cons (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@nil (list bool)))) (@tl bool (@fun_power (list bool) (@length bool u) (@tl bool) v)) *)
rewrite Div2_correct_bs.
(* Goal: @eq nat (Nat.div2 (bs2nat (@fun_power (list bool) n (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l))))) (Nat.div2 (@fun_power nat n Nat.div2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
simpl; congruence.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq (list bool) (Sem Div2_e (@cons (list bool) (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) (fun vl : list (list bool) => Sem Div2_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@nil (list bool)))) u (@cons (list bool) v l)) (@nil (list bool)))) (@tl bool (@fun_power (list bool) (@length bool u) (@tl bool) v)) *)
rewrite Div2_correct_bs.
(* Goal: @eq nat (Nat.div2 (bs2nat (@fun_power (list bool) n (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l))))) (Nat.div2 (@fun_power nat n Nat.div2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
simpl; congruence.
Qed.

Lemma DivTwoPower'_correct : forall l,
  bs2nat (Sem DivTwoPower'_e l) =
  fun_power (length (hd nil l)) div2 (bs2nat (hd nil (tl l))).
Proof.
(* Goal: forall l : list (list bool), @eq nat (@length bool (Sem DivTwoPower_e l)) (Init.Nat.sub (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
intro l.
(* Goal: @eq (list bool) (Sem DivTwoPower'_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) (@fun_power (list bool) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l))) (@tl bool) (@hd (list bool) (@nil bool) l)) *)
rewrite DivTwoPower'_correct_bs.
(* Goal: @eq nat (bs2nat (@fun_power (list bool) (@length bool (@hd (list bool) (@nil bool) l)) (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l)))) (@fun_power nat (@length bool (@hd (list bool) (@nil bool) l)) Nat.div2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
induction (length (hd nil l)).
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (bs2nat (@tl bool (@fun_power (list bool) n (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l))))) (Nat.div2 (@fun_power nat n Nat.div2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
rewrite bs2nat_tl.
(* Goal: @eq nat (Nat.div2 (bs2nat (@fun_power (list bool) n (@tl bool) (@hd (list bool) (@nil bool) (@tl (list bool) l))))) (Nat.div2 (@fun_power nat n Nat.div2 (bs2nat (@hd (list bool) (@nil bool) (@tl (list bool) l))))) *)
congruence.
Qed.

Opaque DivTwoPower'_e.

Definition DivTwoPower_e : Cobham :=
  Comp 2 DivTwoPower'_e [Proj 2 1; Proj 2 0].

Lemma arity_DivTwoPower :
  arity DivTwoPower_e = ok_arity 2.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_DivTwoPower :
  rec_bounded DivTwoPower_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded DivTwoPower'_e *)
apply rec_bounded_DivTwoPower'.
Qed.

Lemma DivTwoPower_correct_bs : forall l,
  Sem DivTwoPower_e l =
  fun_power (length (hd nil (tl l))) (@tl _) (hd nil l).
Proof.
(* Goal: forall l : list (list bool), @eq nat (@length bool (Sem DivTwoPower_e l)) (Init.Nat.sub (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
intro l.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq (list bool) (Sem DivTwoPower'_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool))))) (@fun_power (list bool) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l))) (@tl bool) (@hd (list bool) (@nil bool) l)) *)
rewrite DivTwoPower'_correct_bs.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (Init.Nat.sub (@length bool (@nth (list bool) O l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool)))) (Init.Nat.sub (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
rewrite <- hd_nth_0, <- hd_nth_1.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma length_DivTwoPower : forall l,
  length (Sem DivTwoPower_e l) = length (hd nil l) - length (hd nil (tl l)).
Proof.
(* Goal: forall l : list (list bool), @eq nat (@length bool (Sem DivTwoPower_e l)) (Init.Nat.sub (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
intro l.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (@length bool (Sem DivTwoPower'_e (@cons (list bool) (@nth (list bool) (S O) l (@nil bool)) (@cons (list bool) (@nth (list bool) O l (@nil bool)) (@nil (list bool)))))) (Init.Nat.sub (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
rewrite length_DivTwoPower'.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: @eq nat (Init.Nat.sub (@length bool (@nth (list bool) O l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool)))) (Init.Nat.sub (@length bool (@hd (list bool) (@nil bool) l)) (@length bool (@hd (list bool) (@nil bool) (@tl (list bool) l)))) *)
rewrite <- hd_nth_0, <- hd_nth_1.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma skipn_tl : forall n (l : bs),
  skipn (S n) l = tl (skipn n l).
Proof.
(* Goal: forall (b : bool) (l1 l2 : list bool) (_ : @eq nat (bs2nat l1) (bs2nat l2)), @eq nat (bs2nat (@cons bool b l1)) (bs2nat (@cons bool b l2)) *)
  intros.
(* Goal: @eq (list bool) (@skipn bool (S n) l) (@tl bool (@skipn bool n l)) *)
  destruct (le_lt_dec (length l) n).
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  rewrite skipn_nil; simpl.
(* Goal: @eq (list bool) (@tl bool (@skipn bool (@length bool l0) (@nil bool))) (@nil bool) *)
(* Goal: @eq (list bool) (@tl bool (@skipn bool (@length bool l0) (@cons bool b l1))) (@skipn bool (@length bool l0) l1) *)
  rewrite skipn_nil; simpl; auto.
(* Goal: le (@length bool z) (@length bool x) *)
  omega.
(* Goal: @eq (list bool) (@skipn bool (S n) l) (@tl bool (@skipn bool n l)) *)
  rewrite (skipn_hd n l true).
(* Goal: @eq (list bool) (@skipn bool (S n) l) (@tl bool (@cons bool (@nth bool n l true) (@skipn bool (S n) l))) *)
(* Goal: lt n (@length bool l) *)
  reflexivity.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
Qed.   
  
Lemma DivTwoPower_correct : forall l,
  Sem DivTwoPower_e l =
  skipn (length (nth 1 l nil)) (nth 0 l nil).
Proof.
(* Goal: forall l : list (list bool), @eq (list bool) (Sem DivDivTwoPower_e l) (@skipn bool (Init.Nat.sub (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (@nth (list bool) O l (@nil bool))) *)
  intros l.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  simpl.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  rewrite DivTwoPower'_correct_bs; simpl.
(* Goal: @eq (list bool) (@fun_power (list bool) (@length bool (@nth (list bool) (S O) l (@nil bool))) (@tl bool) (@nth (list bool) O l (@nil bool))) (@skipn bool (@length bool (@nth (list bool) (S O) l (@nil bool))) (@nth (list bool) O l (@nil bool))) *)
  induction (nth 1 l nil); simpl; auto.
(* Goal: @eq (list bool) (@tl bool (@fun_power (list bool) (@length bool l0) (@tl bool) (@nth (list bool) O l (@nil bool)))) match @nth (list bool) O l (@nil bool) with | nil => @nil bool | cons a l => @skipn bool (@length bool l0) l end *)
  rewrite IHl0.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  destruct (nth 0 l nil); simpl.
(* Goal: @eq (list bool) (@tl bool (@skipn bool (@length bool l0) (@nil bool))) (@nil bool) *)
(* Goal: @eq (list bool) (@tl bool (@skipn bool (@length bool l0) (@cons bool b l1))) (@skipn bool (@length bool l0) l1) *)
  rewrite skipn_nil; simpl; auto.
(* Goal: le (@length bool z) (@length bool x) *)
  omega.
(* Goal: @eq (list bool) (@tl bool (@skipn bool (@length bool l0) (@cons bool b l1))) (@skipn bool (@length bool l0) l1) *)
  rewrite <- skipn_tl.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  simpl.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  trivial.
Qed.

Opaque DivTwoPower_e.

(** Def 15 of (Rose) *)

Definition DivDivTwoPower_e : Cobham :=
  Comp 3 DivTwoPower_e [Proj 3 0; Comp 3 DivTwoPower_e [Proj 3 1; Proj 3 2] ].

Lemma arity_DivDivTwoPower :
  arity DivDivTwoPower_e = ok_arity 3.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_DivDivTwoPower :
  rec_bounded DivDivTwoPower_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded DivTwoPower_e *)
apply rec_bounded_DivTwoPower.
(* Goal: rec_bounded DivTwoPower_e *)
apply rec_bounded_DivTwoPower.
Qed.

Lemma DivDivTwoPower_correct : forall l,
  Sem DivDivTwoPower_e l =
  skipn (length (nth 1 l nil) - length (nth 2 l nil)) (nth 0 l nil).
Proof.
(* Goal: forall l : list (list bool), @eq (list bool) (Sem DivDivTwoPower_e l) (@skipn bool (Init.Nat.sub (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (@nth (list bool) O l (@nil bool))) *)
  intros l.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  simpl.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  rewrite DivTwoPower_correct; simpl.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  rewrite DivTwoPower_correct; simpl.
(* Goal: @eq (list bool) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec x y z)) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
(* Goal: le (@length bool z) (@length bool x) *)
  f_equal.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  rewrite length_skipn; trivial.
Qed.

Opaque DivDivTwoPower_e.

(** Def 16 of (Rose) *)

Fixpoint Repeat_e (n l : nat) (b : bool) : Cobham :=
  match l with
    | 0 => Zero_e n
    | S l' => Comp n (Succ b) [Repeat_e n l' b]
  end.

Lemma arity_Repeat : forall n len b,
  arity (Repeat_e n len b) = ok_arity n.
Proof.
induction len as [ | len' IH]; simpl; trivial; intros [ | ];
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  rewrite IH; simpl; rewrite <- beq_nat_refl; trivial.
Qed.

Lemma rec_bounded_Repeat : forall n len b,
  rec_bounded (Repeat_e n len b).
Proof.
(* Goal: forall (n len : nat) (b : bool), rec_bounded (Repeat_e n len b) *)
intros n len b.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
induction len as [ | len' IH]; simpl.
(* Goal: rec_bounded (Zero_e n) *)
(* Goal: and True (and (rec_bounded (Repeat_e n len' b)) True) *)
apply rec_bounded_Zero.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
Qed.

Lemma length_Repeat : forall n l b l',
  length (Sem (Repeat_e n l b) l') = l.
Proof.
(* Goal: forall (n l : nat) (b : bool) (l' : list (list bool)), @eq nat (@length bool (Sem (Repeat_e n l b) l')) l *)
  induction l; simpl; auto.
Qed.

Opaque Repeat_e.

Definition RoseS'_e : Cobham :=
  Rec2
    (Zero_e 2)
    (Comp 4 PlusOneMinusMod2_e [
      Comp 4 (Succ false) [Proj 4 1];
      Comp 4 DivTwoPower_e [Comp 4 DivTwoPower_e [Proj 4 2; Proj 4 0]; Proj 4 3];
      Comp 4 DivDivTwoPower_e [Proj 4 2; Proj 4 2; Comp 4 (Succ false) [Proj 4 0]]
    ])
    (Comp 3 Smash [Proj 3 0; Repeat_e 3 2 true]).

Definition arity_RoseS' :
  arity RoseS'_e = ok_arity 3.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Lemma rec_bounded_RoseS' :
  rec_bounded RoseS'_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
apply rec_bounded_Repeat.
(* Goal: rec_bounded (Zero_e n) *)
(* Goal: and True (and (rec_bounded (Repeat_e n len' b)) True) *)
apply rec_bounded_Zero.
apply rec_bounded_PlusOneMinusMod2.
(* Goal: rec_bounded DivTwoPower_e *)
apply rec_bounded_DivTwoPower.
(* Goal: rec_bounded DivTwoPower_e *)
apply rec_bounded_DivTwoPower.
apply rec_bounded_DivDivTwoPower.
apply rec_bounded_PlusOneMinusMod2.
(* Goal: rec_bounded DivTwoPower_e *)
apply rec_bounded_DivTwoPower.
(* Goal: rec_bounded DivTwoPower_e *)
apply rec_bounded_DivTwoPower.
apply rec_bounded_DivDivTwoPower.
rewrite <- hd_nth_0.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
induction (hd nil l); simpl.
(* Goal: @eq nat (bs2nat u) (Init.Nat.mul (bs2nat u) match bs2nat (@nil bool) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool true v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool true v) with | O => S O | S l => O end) *)
(* Goal: @eq nat (bs2nat (Sem (Zero_e (S (S O))) (@cons (list bool) u (@cons (list bool) (@cons bool false v) l)))) (Init.Nat.mul (bs2nat u) match bs2nat (@cons bool false v) with | O => S O | S l => O end) *)
rewrite Zero_correct_bs; simpl; auto with arith.
case a.
eapply le_trans.
apply PlusOneMinusMod2_length.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
rewrite length_smash'.
rewrite length_Repeat.
(* Goal: le (@length bool z) (@length bool x) *)
omega.
eapply le_trans.
apply PlusOneMinusMod2_length.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
rewrite length_smash'.
rewrite length_Repeat.
(* Goal: le (@length bool z) (@length bool x) *)
omega.
Qed.

Definition RoseS_e : Cobham :=
  Comp 3 RoseS'_e [Proj 3 2; Proj 3 0; Proj 3 1].

Lemma arity_RoseS :
  arity RoseS_e = ok_arity 3.
Proof.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
trivial.
Qed.

Opaque RoseS'_e.

Lemma rec_bounded_RoseS :
  rec_bounded RoseS_e.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
simpl.
(* Goal: and (rec_bounded RoseS'_e) (and True (and True (and True True))) *)
intuition.
(* Goal: rec_bounded RoseS'_e *)
apply rec_bounded_RoseS'.
Qed.

Transparent RoseS'_e.

Lemma bs2nat_firstn_false : forall n l,
  bs2nat (firstn n (false :: l)) = 2 * bs2nat (firstn (n-1) l).
Proof.
(* Goal: forall (b : bool) (l1 l2 : list bool) (_ : @eq nat (bs2nat l1) (bs2nat l2)), @eq nat (bs2nat (@cons bool b l1)) (bs2nat (@cons bool b l2)) *)
  intros.
(* Goal: @eq nat (bs2nat (@firstn bool n (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub n (S O)) l))) *)
  destruct n.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  simpl.
(* Goal: @eq nat (Init.Nat.mul (power (S (S O)) (@length bool (@nth (list bool) (S O) l (@nil bool)))) (bs2nat (@nth (list bool) O l (@nil bool)))) (Init.Nat.mul (bs2nat (@nth (list bool) O l (@nil bool))) (power (S (S O)) (@length bool (@nth (list bool) (S O) l (@nil bool))))) *)
  rewrite bs2nat_nil; ring.
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  simpl firstn.
(* Goal: @eq nat (bs2nat (@cons bool false (@firstn bool n l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub n O) l))) *)
  rewrite bs2nat_false.
(* Goal: @eq (list bool) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec x y z)) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
(* Goal: le (@length bool z) (@length bool x) *)
  f_equal.
(* Goal: @eq (list bool) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec x y z)) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
(* Goal: le (@length bool z) (@length bool x) *)
  f_equal.
(* Goal: @eq (list bool) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec x y z)) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
(* Goal: le (@length bool z) (@length bool x) *)
  f_equal.
(* Goal: le (@length bool z) (@length bool x) *)
  omega.
Qed.


Lemma bs2nat_app : forall l1 l2,
  bs2nat (l1 ++ l2) = bs2nat l1 + bs2nat (repeat (length l1) false ++ l2).
Proof.
(* Goal: forall (b : bool) (l1 l2 : list bool) (_ : @eq nat (bs2nat l1) (bs2nat l2)), @eq nat (bs2nat (@cons bool b l1)) (bs2nat (@cons bool b l2)) *)
 intros.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
 induction l1; simpl.
(* Goal: @eq nat (bs2nat (@nil bool)) O *)
(* Goal: @eq nat (bs2nat match (if match Init.Nat.sub (@length bool x) (@length bool y) with | O => false | S m' => Nat.leb (@length bool z) m' end then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) with | nil => @nil bool | cons a l => @skipn bool (@length bool z) l end) O *)
 rewrite bs2nat_nil; auto.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
 rewrite bs2nat_false; simpl.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
 destruct a; simpl.
(* Goal: @eq nat (Init.Nat.add (bs2nat u) match bs2nat v with | O => S O | S l => O end) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool true w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool true w))) O))))) *)
(* Goal: @eq nat (bs2nat u) (Init.Nat.add (bs2nat u) (Init.Nat.mul match bs2nat v with | O => S O | S l => O end (Init.Nat.sub (bs2nat (@cons bool false w)) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) (Init.Nat.add (Nat.div2 (bs2nat (@cons bool false w))) O))))) *)
 repeat rewrite bs2nat_true.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
 rewrite IHl1; simpl.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.add (bs2nat l1) (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2))) (Init.Nat.add (Init.Nat.add (bs2nat l1) (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2))) O)) (Init.Nat.add (Init.Nat.add (bs2nat l1) (Init.Nat.add (bs2nat l1) O)) (Init.Nat.add (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2)) (Init.Nat.add (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2)) O))) *)
 simpl; ring.
(* Goal: @eq nat (bs2nat (@cons bool false (@firstn bool n l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub n O) l))) *)
 repeat rewrite bs2nat_false.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
 rewrite IHl1; simpl.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.add (bs2nat l1) (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2))) (Init.Nat.add (Init.Nat.add (bs2nat l1) (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2))) O)) (Init.Nat.add (Init.Nat.add (bs2nat l1) (Init.Nat.add (bs2nat l1) O)) (Init.Nat.add (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2)) (Init.Nat.add (bs2nat (@app bool (@repeat bool (@length bool l1) false) l2)) O))) *)
 simpl; ring.
Qed.

Lemma bs2nat_power : forall l n,
  bs2nat (repeat n false ++ l) = (power 2 n) * (bs2nat l).
Proof.
(* Goal: forall (l : list bool) (n : nat), @eq nat (bs2nat (@app bool (@repeat bool n false) l)) (Init.Nat.mul (power (S (S O)) n) (bs2nat l)) *)
 induction n; simpl; auto.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
 rewrite bs2nat_false; simpl.
(* Goal: @eq nat (Init.Nat.mul (power (S (S O)) (@length bool (@nth (list bool) (S O) l (@nil bool)))) (bs2nat (@nth (list bool) O l (@nil bool)))) (Init.Nat.mul (bs2nat (@nth (list bool) O l (@nil bool))) (power (S (S O)) (@length bool (@nth (list bool) (S O) l (@nil bool))))) *)
 rewrite IHn; ring.
Qed.

Fixpoint RoseS_spec (x y z : bs) :=
  match z with
    | nil => nil
    | _ :: z' =>
      if leb (length z) (length x - length y)
        then false :: RoseS_spec x y z'
        else hd false (skipn (length x - length z) x) :: RoseS_spec x y z'
  end.

Lemma RoseS_spec2_false : forall x y z,
  length z <= length x - length y ->
  bs2nat (RoseS_spec x y z) = 0.
Proof.
(* Goal: forall (b : bool) (l1 l2 : list bool) (_ : @eq nat (bs2nat l1) (bs2nat l2)), @eq nat (bs2nat (@cons bool b l1)) (bs2nat (@cons bool b l2)) *)
 induction z; simpl; intros.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
 rewrite bs2nat_nil; trivial.
(* Goal: forall (b : bool) (l1 l2 : list bool) (_ : @eq nat (bs2nat l1) (bs2nat l2)), @eq nat (bs2nat (@cons bool b l1)) (bs2nat (@cons bool b l2)) *)
 case_eq (length x - length y); intros.
(* Goal: @eq nat (bs2nat (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z))) O *)
(* Goal: @eq nat (bs2nat (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z))) O *)
 rewrite H0 in H.
(* Goal: le (@length bool z) (@length bool x) *)
 elimtype False; omega.
(* Goal: forall (b : bool) (l1 l2 : list bool) (_ : @eq nat (bs2nat l1) (bs2nat l2)), @eq nat (bs2nat (@cons bool b l1)) (bs2nat (@cons bool b l2)) *)
 case_eq (leb (length z) n); intros.
(* Goal: @eq nat (bs2nat (@cons bool false (RoseS_spec x y z))) O *)
(* Goal: @eq nat (bs2nat (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z))) O *)
 apply leb_complete in H1.
(* Goal: @eq nat (bs2nat (@cons bool false (RoseS_spec x y z))) O *)
(* Goal: @eq nat (bs2nat (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z))) O *)
 rewrite bs2nat_false, IHz; auto.
(* Goal: le (@length bool z) (@length bool x) *)
 omega.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) *)
(* Goal: le (@length bool z) (@length bool x) *)
 apply leb_complete_conv in H1.
(* Goal: le (@length bool z) (@length bool x) *)
 elimtype False; omega.
Qed.

Lemma skipn_roseS : forall x y z,
  bs2nat (skipn (length z) (RoseS_spec x y z)) = 0.
Proof.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  induction z; simpl.
(* Goal: @eq nat (bs2nat (@nil bool)) O *)
(* Goal: @eq nat (bs2nat match (if match Init.Nat.sub (@length bool x) (@length bool y) with | O => false | S m' => Nat.leb (@length bool z) m' end then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) with | nil => @nil bool | cons a l => @skipn bool (@length bool z) l end) O *)
  rewrite bs2nat_nil; auto.
(* Goal: @eq nat (bs2nat match (if match Init.Nat.sub (@length bool x) (@length bool y) with | O => false | S m' => Nat.leb (@length bool z) m' end then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) with | nil => @nil bool | cons a l => @skipn bool (@length bool z) l end) O *)
  case_eq (length x - length y); intros; auto.
(* Goal: @eq nat (bs2nat match (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) with | nil => @nil bool | cons a l => @skipn bool (@length bool z) l end) O *)
  case_eq (leb (length z) n); intros; auto.
Qed.

Lemma RoseS_cons : forall x y z b1 b2,
  length z <= length x ->
  RoseS_spec (b1 :: x) (b2 :: y) z = RoseS_spec x y z.
Proof.
(* Goal: forall (b : bool) (l1 l2 : list bool) (_ : @eq nat (bs2nat l1) (bs2nat l2)), @eq nat (bs2nat (@cons bool b l1)) (bs2nat (@cons bool b l2)) *)
  induction z; simpl; trivial; intros.
(* Goal: forall (b : bool) (l1 l2 : list bool) (_ : @eq nat (bs2nat l1) (bs2nat l2)), @eq nat (bs2nat (@cons bool b l1)) (bs2nat (@cons bool b l2)) *)
  case_eq (length x - length y); intros.
(* Goal: @eq (list bool) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
  rewrite IHz;[ | omega ]; clear IHz.
(* Goal: @eq (list bool) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec x y z)) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
(* Goal: le (@length bool z) (@length bool x) *)
  f_equal.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
  destruct x; simpl in *.
(* Goal: le (@length bool z) (@length bool x) *)
  elimtype False; omega.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
  destruct y; simpl in *.
(* Goal: @eq bool b1 false *)
(* Goal: @eq bool (@hd bool false (@skipn bool match @length bool z with | O => S (@length bool x) | S l => Init.Nat.sub (@length bool x) l end (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b x))) *)
(* Goal: le (@length bool z) (@length bool x) *)
  discriminate.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  destruct z; simpl.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  rewrite <- minus_n_O; trivial.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
  simpl in *.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: le (@length bool z) (@length bool x) *)
  cutrewrite (length x - length z = S (length x - S (length z))).
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  simpl; trivial.
(* Goal: le (@length bool z) (@length bool x) *)
  omega.
(* Goal: forall (b : bool) (l1 l2 : list bool) (_ : @eq nat (bs2nat l1) (bs2nat l2)), @eq nat (bs2nat (@cons bool b l1)) (bs2nat (@cons bool b l2)) *)
  case_eq (leb (length z) n); intros.
(* Goal: @eq (list bool) (@cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (@cons bool false (RoseS_spec x y z)) *)
(* Goal: @eq (list bool) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
  rewrite IHz; auto.
(* Goal: le (@length bool z) (@length bool x) *)
  omega.
(* Goal: @eq (list bool) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
  rewrite IHz.
(* Goal: @eq (list bool) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec x y z)) (@cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
(* Goal: le (@length bool z) (@length bool x) *)
  f_equal.  
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) *)
(* Goal: le (@length bool z) (@length bool x) *)
  apply leb_complete_conv in H1.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
  destruct x; simpl in *.
(* Goal: @eq bool b1 false *)
(* Goal: @eq bool (@hd bool false (@skipn bool match @length bool z with | O => S (@length bool x) | S l => Init.Nat.sub (@length bool x) l end (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b x))) *)
(* Goal: le (@length bool z) (@length bool x) *)
  discriminate.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: @eq (list bool) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 x))) (RoseS_spec (@cons bool b1 x) (@cons bool b2 y) z)) (if Nat.leb (@length bool z) n then @cons bool false (RoseS_spec x y z) else @cons bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) x)) (RoseS_spec x y z)) *)
  destruct y; simpl in *.
(* Goal: le (@length bool z) (@length bool x) *)
  elimtype False; omega.
(* Goal: @eq nat (bs2nat (@firstn bool O (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub O (S O)) l))) *)
(* Goal: @eq nat (bs2nat (@firstn bool (S n) (@cons bool false l))) (Init.Nat.mul (S (S O)) (bs2nat (@firstn bool (Init.Nat.sub (S n) (S O)) l))) *)
  destruct z; simpl.
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  rewrite <- minus_n_O; trivial.
(* Goal: @eq bool (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (@length bool z)) (@cons bool b1 (@cons bool b x)))) (@hd bool false (@skipn bool (Init.Nat.sub (@length bool x) (S (@length bool z))) (@cons bool b x))) *)
(* Goal: le (@length bool z) (@length bool x) *)
  cutrewrite (length x - length z = S (length x - S (length z))).
(* Goal: @eq Arity (arity RoseS_e) (ok_arity (S (S (S O)))) *)
  simpl; trivial.
(* Goal: le (@length bool z) (@length bool x) *)
  simpl in *; omega.
(* Goal: le (@length bool z) (@length bool x) *)
  omega.
Qed.

Lemma bs2nat_cons_eq : forall b l1 l2,
  bs2nat l1 = bs2nat l2 ->
  bs2nat (b :: l1) = bs2nat (b :: l2).
Proof.
(* Goal: forall (b : bool) (l1 l2 : list bool) (_ : @eq nat (bs2nat l1) (bs2nat l2)), @eq nat (bs2nat (@cons bool b l1)) (bs2nat (@cons bool b l2)) *)
  intros.
(* Goal: @eq nat (bs2nat (@cons bool b l1)) (bs2nat (@cons bool b l2)) *)
  case b.
(* Goal: @eq nat (bs2nat (@cons bool true l1)) (bs2nat (@cons bool true l2)) *)
(* Goal: @eq nat (bs2nat (@cons bool false l1)) (bs2nat (@cons bool false l2)) *)
  repeat rewrite bs2nat_true; ring [H].
(* Goal: @eq nat (bs2nat (@cons bool false l1)) (bs2nat (@cons bool false l2)) *)
  repeat rewrite bs2nat_false; ring [H].
Qed.

Fixpoint RoseS_spec' (x : bs) (y z : nat) :=
  match z with
    | 0 => nil
    | S z' =>
      if leb z (length x - y)
        then false :: RoseS_spec' x y z'
        else hd false (skipn (length x - z) x) :: RoseS_spec' x y z'
  end.
