Require Import Arith List.
Require Import BellantoniCook.Lib BellantoniCook.Cobham.

Definition Zero_e (n:nat) : Cobham :=
  Comp n Zero nil.

Lemma arity_Zero n : arity (Zero_e n) = ok_arity n.
Proof.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  trivial.
Qed.

Lemma rec_bounded_Zero n : 
  rec_bounded (Zero_e n).
Proof.
(* Goal: rec_bounded (One_e n) *)
simpl; tauto.
Qed.

Definition One_e (n:nat) : Cobham :=
  Comp n (Comp 0 (Succ true) [Zero]) nil.

Lemma arity_One n : arity (One_e n) = ok_arity n.
Proof.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  trivial.
Qed.

Lemma rec_bounded_One n :
  rec_bounded (One_e n).
Proof.
(* Goal: rec_bounded (One_e n) *)
simpl; tauto.
Qed.

(** Def 12 of (Rose) *)

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

Lemma arity_App : arity App_e = ok_arity 2.
Proof.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  trivial.
Qed.

Lemma rec_bounded_App : rec_bounded App_e.
Proof.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
simpl.
(* Goal: and True (and True (and True (and (and True (and True True)) (forall l : list (list bool), le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) (S 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 (@nth (list bool) O l (@nil bool))))))) *)
intuition.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
destruct l as [ | u [ | v l] ]; simpl.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S O) l (@nil bool)))) (S O))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S O) l (@nil bool)))) (S O))) (S (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
omega.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
rewrite length_smash, mult_1_r; simpl.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S O) l (@nil bool)))) (S O))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S O) l (@nil bool)))) (S O))) (S (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
induction u as [ | [ | ] u IH]; simpl; omega.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
rewrite length_smash', length_smash; simpl.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S O) l (@nil bool)))) (S O))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S O) l (@nil bool)))) (S O))) (S (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
induction u as [ | [ | ] u IH]; simpl; omega.
Qed.

Lemma App_correct : forall l,
  Sem App_e l = hd nil l ++ hd nil (tl l).
Proof.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
  intros; simpl.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  destruct l; simpl; trivial.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
  induction l; simpl.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  destruct l0; simpl; trivial.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  rewrite IHl; case a; trivial.
Qed.

Opaque App_e.

Definition Rev_e : Cobham :=
  Rec
    Zero
    (Comp 2 App_e [Proj 2 1; Comp 2 (Succ false) [Zero_e 2]])
    (Comp 2 App_e [Proj 2 1; Comp 2 (Succ true) [Zero_e 2]])
    (Proj 1 0).

Lemma arity_Rev : 
  arity Rev_e = ok_arity 1.
Proof.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
trivial.
Qed.

Lemma rec_bounded_Rev :
  rec_bounded Rev_e.
Proof.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
simpl.
(* Goal: and True (and True (and True (and (and True (and True True)) (forall l : list (list bool), le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) (S 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 (@nth (list bool) O l (@nil bool))))))) *)
intuition.
(* Goal: rec_bounded App_e *)
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool true (@nil bool)) (@nil (list bool))))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (@nth (list bool) O l (@nil bool))) *)
apply rec_bounded_App.
(* Goal: rec_bounded App_e *)
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool true (@nil bool)) (@nil (list bool))))) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (@length bool (@nth (list bool) O l (@nil bool))) *)
apply rec_bounded_App.
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) (S 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 (@nth (list bool) O l (@nil bool))) *)
destruct l as [ | v l].
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
trivial.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
simpl.
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) (S O) vl (@nil bool)) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) v l)) (@length bool v) *)
induction v as [ | [ | ] v IH].
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
trivial.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
simpl.
(* Goal: @eq (list bool) (Sem App_e (@cons (list bool) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool true (@nil bool)) (@nil (list bool))))) v l) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (@app bool (@rev bool v) (@cons bool false (@nil bool))) *)
rewrite App_correct.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
simpl.
(* Goal: le (@length bool (@app bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool true (@nil bool)) (@nil (list bool))))) v l) (@cons bool false (@nil bool)))) (S (@length bool v)) *)
rewrite app_length.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S O) l (@nil bool)))) (S O))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S O) l (@nil bool)))) (S O))) (S (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
simpl; omega.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
simpl.
(* Goal: @eq (list bool) (Sem App_e (@cons (list bool) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool true (@nil bool)) (@nil (list bool))))) v l) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (@app bool (@rev bool v) (@cons bool false (@nil bool))) *)
rewrite App_correct.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
simpl.
(* Goal: le (@length bool (@app bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool true (@nil bool)) (@nil (list bool))))) v l) (@cons bool false (@nil bool)))) (S (@length bool v)) *)
rewrite app_length.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S O) l (@nil bool)))) (S O))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S O) l (@nil bool)))) (S O))) (S (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
simpl; omega.
Qed. 

Lemma Rev_correct l :
  Sem Rev_e l = List.rev (hd nil l).
Proof.
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) (S 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 (@nth (list bool) O l (@nil bool))) *)
destruct l as [ | v l].
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
trivial.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
simpl.
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) (S O) vl (@nil bool)) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) v l)) (@length bool v) *)
induction v as [ | [ | ] v IH].
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
trivial.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
simpl.
(* Goal: @eq (list bool) (Sem App_e (@cons (list bool) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool true (@nil bool)) (@nil (list bool))))) v l) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (@app bool (@rev bool v) (@cons bool false (@nil bool))) *)
rewrite App_correct.
(* Goal: @eq (list bool) (@app bool (@hd (list bool) (@nil bool) (@cons (list bool) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool true (@nil bool)) (@nil (list bool))))) v l) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (@hd (list bool) (@nil bool) (@tl (list bool) (@cons (list bool) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool true (@nil bool)) (@nil (list bool))))) v l) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))))) (@app bool (@rev bool v) (@cons bool false (@nil bool))) *)
simpl; congruence.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
simpl.
(* Goal: @eq (list bool) (Sem App_e (@cons (list bool) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool true (@nil bool)) (@nil (list bool))))) v l) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (@app bool (@rev bool v) (@cons bool false (@nil bool))) *)
rewrite App_correct.
(* Goal: @eq (list bool) (@app bool (@hd (list bool) (@nil bool) (@cons (list bool) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool true (@nil bool)) (@nil (list bool))))) v l) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (@hd (list bool) (@nil bool) (@tl (list bool) (@cons (list bool) (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))) (fun vl : list (list bool) => Sem App_e (@cons (list bool) (@nth (list bool) (S O) vl (@nil bool)) (@cons (list bool) (@cons bool true (@nil bool)) (@nil (list bool))))) v l) (@cons (list bool) (@cons bool false (@nil bool)) (@nil (list bool))))))) (@app bool (@rev bool v) (@cons bool false (@nil bool))) *)
simpl; congruence.
Qed.

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

Lemma arity_RemoveLSZ : 
  arity RemoveLSZ_e = ok_arity 1.
Proof.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
trivial.
Qed.

Lemma rec_bounded_RemoveLSZ :
  rec_bounded RemoveLSZ_e.
Proof.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
simpl.
(* Goal: and True (and True (and True (and (and True (and True True)) (forall l : list (list bool), le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) (S 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 (@nth (list bool) O l (@nil bool))))))) *)
intuition.
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) (S 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 (@nth (list bool) O l (@nil bool))) *)
destruct l as [ | v l].
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
trivial.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
simpl.
(* Goal: le (@length bool (sem_Rec (fun _ : list (list bool) => @nil bool) (fun vl : list (list bool) => @nth (list bool) (S O) vl (@nil bool)) (fun vl : list (list bool) => @cons bool true (@nth (list bool) O vl (@nil bool))) v l)) (@length bool v) *)
induction v as [ | [ | ] v IH].
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
trivial.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
trivial.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S O) l (@nil bool)))) (S O))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S O) l (@nil bool)))) (S O))) (S (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
simpl; omega.
Qed.

Lemma RemoveLSZ_app u v l :
  Sem RemoveLSZ_e ((u++v)::l) =
  match Sem RemoveLSZ_e (u::l) with
  | nil => Sem RemoveLSZ_e (v::l)
  | u' => u'++v
  end.
Proof.
(* Goal: @eq (list bool) (Sem RemoveLSZ_e (@cons (list bool) (@app bool u v) l)) match Sem RemoveLSZ_e (@cons (list bool) u l) with | nil => Sem RemoveLSZ_e (@cons (list bool) v l) | cons b l => @app bool (@cons bool b l) v end *)
simpl.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
induction u as [ | [ | ] u IH]; trivial.
Qed.

Definition Cond : Cobham :=
  Rec (Proj 3 0) (Proj 5 4) (Proj 5 3) (
    Comp 4 Smash [
      Comp 4 (Succ true) [Proj 4 1];
      Comp 4 Smash [
        Comp 4 (Succ true) [Proj 4 2];
        Comp 4 (Succ true) [Proj 4 3]
      ]
    ]
  ).

Lemma arity_Cond : arity Cond = ok_arity 4.
Proof.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
trivial.
Qed.

Lemma rec_bounded_Cond : rec_bounded' Cond.
Proof.
  simpl; repeat (split; auto);  intros.
(* Goal: le (@length bool (sem_Rec (fun vl : list (list bool) => @nth (list bool) O vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (@length bool (smash' (@nth (list bool) (S (S (S O))) l (@nil bool)) (smash_bs (@nth (list bool) (S (S O)) l (@nil bool)) (@cons bool true (@nth (list bool) (S (S (S O))) l (@nil bool))))))))))) *)
  repeat (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) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (@length bool (smash_bs (@nth (list bool) (S (S O)) l (@nil bool)) (@cons bool true (@nth (list bool) (S (S (S O))) l (@nil bool))))))))))) *)
  repeat (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) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (@length bool (smash' (@nth (list bool) (S (S (S O))) l (@nil bool)) (smash_bs (@nth (list bool) (S (S O)) l (@nil bool)) (@cons bool true (@nth (list bool) (S (S (S O))) l (@nil bool))))))))))) *)
  repeat (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) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (@length bool (smash_bs (@nth (list bool) (S (S O)) l (@nil bool)) (@cons bool true (@nth (list bool) (S (S (S O))) l (@nil bool))))))))))) *)
  repeat (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) => @nth (list bool) (S (S (S (S O)))) vl (@nil bool)) (fun vl : list (list bool) => @nth (list bool) (S (S (S O))) vl (@nil bool)) (@hd (list bool) (@nil bool) l) (@tl (list bool) l))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  destruct (hd nil l); simpl; repeat rewrite nth_S_tl.

(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  rewrite plus_n_Sm.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  rewrite plus_comm.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (Nat.add (S (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))))))) (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  apply le_plus_trans.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  apply le_trans with ( S (S (length (nth 1 l nil)) * 1)).
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S O) l (@nil bool)))) (S O))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S O) l (@nil bool)))) (S O))) (S (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  omega.
(* Goal: le (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  apply le_n_S.
(* Goal: le (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  apply le_n_S.
(* Goal: le ((fix mul (n m : nat) {struct n} : nat := match n with | O => O | S p => Init.Nat.add m (mul p m) end) (@length bool (@nth (list bool) (S O) l (@nil bool))) (S O)) (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  apply mult_le_compat.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  trivial.
(* Goal: le (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  apply le_n_S.
(* Goal: le (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R1)) (Init.Nat.mul R3 R1)) (Init.Nat.mul (S (S O)) R1)) (S O))) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R3)) (Init.Nat.mul R2 R1)) R2) (Init.Nat.mul R3 R1)) R3) (Init.Nat.mul (S (S O)) R1)) (S (S (S O)))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R1)) (Init.Nat.mul R3 R1)) (Init.Nat.mul (S (S O)) R1)) (S O))) *)
  auto with arith.

(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  apply le_trans with ( S (length (if b then nth 2 l nil else nth 3 l nil)) * 1).
(* Goal: le (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R1)) (Init.Nat.mul R3 R1)) (Init.Nat.mul (S (S O)) R1)) (S O))) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R3)) (Init.Nat.mul R2 R1)) R2) (Init.Nat.mul R3 R1)) R3) (Init.Nat.mul (S (S O)) R1)) (S (S (S O)))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R1)) (Init.Nat.mul R3 R1)) (Init.Nat.mul (S (S O)) R1)) (S O))) *)
  rewrite mult_1_r; auto with arith.

(* Goal: le (Init.Nat.mul (S (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool)))) (S O)) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  apply le_trans with (S (S (length (nth 2 l nil)) * S (length (nth 3 l nil)))).
(* Goal: le (Init.Nat.mul (S (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool)))) (S O)) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  case b.
(* Goal: le (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))) (S O)) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  rewrite mult_1_r.
(* Goal: le (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  apply le_n_S.
(* Goal: le (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))) *)
(* Goal: le (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))) (S O)) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  rewrite <- mult_1_r at 1.
(* Goal: le (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R1)) (Init.Nat.mul R3 R1)) (Init.Nat.mul (S (S O)) R1)) (S O))) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R3)) (Init.Nat.mul R2 R1)) R2) (Init.Nat.mul R3 R1)) R3) (Init.Nat.mul (S (S O)) R1)) (S (S (S O)))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R1)) (Init.Nat.mul R3 R1)) (Init.Nat.mul (S (S O)) R1)) (S O))) *)
  apply mult_le_compat; auto with arith.
(* Goal: le (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))) (S O)) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  rewrite mult_1_r.
(* Goal: le (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))) (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  apply le_n_S.
(* Goal: le (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))) *)
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  rewrite <- mult_1_l at 1.
(* Goal: le (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R1)) (Init.Nat.mul R3 R1)) (Init.Nat.mul (S (S O)) R1)) (S O))) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R3)) (Init.Nat.mul R2 R1)) R2) (Init.Nat.mul R3 R1)) R3) (Init.Nat.mul (S (S O)) R1)) (S (S (S O)))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R1)) (Init.Nat.mul R3 R1)) (Init.Nat.mul (S (S O)) R1)) (S O))) *)
  apply mult_le_compat; auto with arith.
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  set (R1 := length (nth 1 l nil)).
(* Goal: le (S (Init.Nat.mul (S (@length bool (@nth (list bool) (S (S O)) l (@nil bool)))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul R1 (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  set (R2 := length (nth 2 l nil)).
(* Goal: le (S (Init.Nat.mul (S R2) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul R2 (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul R1 (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul R2 (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
  set (R3 := length (nth 3 l nil)).
(* Goal: le (S (Init.Nat.mul (S R2) (S R3))) (S (Init.Nat.add (Init.Nat.add R3 (S (Init.Nat.mul R2 (S R3)))) (S (Init.Nat.mul R1 (S (Init.Nat.add R3 (S (Init.Nat.mul R2 (S R3))))))))) *)
  set (R4 := length (nth 4 l nil)).
(* Goal: le (S (Init.Nat.mul (S R2) (S R3))) (S (Init.Nat.add (Init.Nat.add R3 (S (Init.Nat.mul R2 (S R3)))) (S (Init.Nat.mul R1 (S (Init.Nat.add R3 (S (Init.Nat.mul R2 (S R3))))))))) *)
  ring_simplify.
  cutrewrite (R2 * R3 * R1 + R2 * R3 + R2 * R1 + R2 + R3 * R1 + R3 + 2 * R1 + 3 =
    (R2 * R3 + R2 + R3 + 2) + (R2 * R3 * R1 + R2 * R1 + R3 * R1 + 2 * R1 + 1)).
(* Goal: le (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R1)) (Init.Nat.mul R3 R1)) (Init.Nat.mul (S (S O)) R1)) (S O))) *)
(* Goal: @eq nat (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R3)) (Init.Nat.mul R2 R1)) R2) (Init.Nat.mul R3 R1)) R3) (Init.Nat.mul (S (S O)) R1)) (S (S (S O)))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R1)) (Init.Nat.mul R3 R1)) (Init.Nat.mul (S (S O)) R1)) (S O))) *)
  auto with arith.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R3)) (Init.Nat.mul R2 R1)) R2) (Init.Nat.mul R3 R1)) R3) (Init.Nat.mul (S (S O)) R1)) (S (S (S O)))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul R2 R3) R2) R3) (S (S O))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.add (Init.Nat.mul (Init.Nat.mul R2 R3) R1) (Init.Nat.mul R2 R1)) (Init.Nat.mul R3 R1)) (Init.Nat.mul (S (S O)) R1)) (S O))) *)
  ring.
Qed.

Lemma Cond_correct : forall l,
  Sem Cond l =
  match hd nil l with
  | nil => hd nil (tl l)
  | true::_ => hd nil (tl (tl l))
  | false::_ => hd nil (tl (tl (tl l)))
  end.
Proof.
(* Goal: le (@length bool (@nth (list bool) (S O) l (@nil bool))) (@length bool (@nth (list bool) (S O) l (@nil bool))) *)
(* Goal: le (S O) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))) *)
(* Goal: le (@length bool (if b then @nth (list bool) (S (S O)) l (@nil bool) else @nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.add (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))))))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S O) l (@nil bool))) (S (Init.Nat.add (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool))) (S (Init.Nat.mul (@length bool (@nth (list bool) (S (S O)) l (@nil bool))) (S (@length bool (@nth (list bool) (S (S (S O))) l (@nil bool)))))))))))) *)
destruct l as [ | [ | [ | ] v1] [ | v2 [ | v3 [ | v4 l] ] ] ]; trivial.
Qed.
