Require Import Arith NPeano List Bool Psatz.
Require Import Cecoa.Lib Cecoa.Syntax Cecoa.CBV_cache.
Require Import Omega.

Import List.ListNotations.
Infix "∈" := In (at level 70).

Section Ordering.

Set Implicit Arguments.

Variables variable function constructor : Type.

Notation value := (Syntax.value constructor).
Notation term := (Syntax.term variable function constructor).
Notation pattern := (Syntax.pattern variable constructor).
Notation rule := (Syntax.rule variable function constructor).
Notation cbv := (CBV_cache.cbv variable function constructor).
Notation cache := (CBV_cache.cache variable function constructor).

Variable variable_eq_dec : forall (x1 x2 : variable), {x1=x2}+{x1<>x2}.

Variable function_eq_dec : forall (x1 x2 : function), {x1=x2}+{x1<>x2}.

Variable constructor_eq_dec : forall (x1 x2 : constructor), {x1=x2}+{x1<>x2}.

Variable rule_default : rule.

Variable prog : list rule.

Variable max_arity : nat.

Notation wf :=
  (CBV_cache.wf variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity).

(* Function ranks and compatibility *)

Variable rank: function -> nat.

(* PPO *)

Inductive product {A: Type} (R : A -> A -> Prop) : list A -> list A -> Prop :=
| product_conseq : forall x y xs ys, x = y -> product R xs ys   -> product R (x::xs) (y::ys)
| product_consst : forall x y xs ys, R x y -> Forall2 (clos_refl R) xs ys -> product R (x::xs) (y::ys).

Inductive PPO: term -> term -> Prop :=
| ppo_constr_in    : forall s c lt,    In s lt            -> PPO s (capply c lt)
| ppo_fun_in       : forall s f lt,    In s lt            -> PPO s (fapply f lt)
| ppo_constr_sub   : forall s t c lt,  In t lt -> PPO s t -> PPO s (capply c lt)
| ppo_fun_sub      : forall s t f lt,  In t lt -> PPO s t -> PPO s (fapply f lt)
| ppo_constr_split : forall c ls f lt, (forall s, In s ls -> PPO s (fapply f lt))
                                       -> PPO (capply c ls) (fapply f lt)
| ppo_funlt_split  : forall g ls f lt, rank g < rank f
                                       -> (forall s, In s ls -> PPO s (fapply f lt))
                                       -> PPO (fapply g ls) (fapply f lt)
| ppo_funeqv_split : forall g ls f lt, rank g = rank f
                                       -> product PPO ls lt
                                       -> PPO (fapply g ls) (fapply f lt).

Infix "≺ppo" := PPO (at level 80).
Infix "≼ppo" := (clos_refl PPO) (at level 80).

Hint Constructors product PPO.

Definition lt_wf_rect (n : nat) (P : nat -> Type)
  (F : forall n, (forall m, m < n -> P m) -> P n) : P n :=
  well_founded_induction_type (well_founded_ltof nat (fun m => m)) P F n.

Definition term_dec (t1 t2 : term) : {t1=t2}+{t1<>t2}.
Proof.
case_eq (term_beq variable_eq_dec function_eq_dec constructor_eq_dec t1 t2); intro H; [ left | right];
rewrite <- (term_beq_eq variable_eq_dec function_eq_dec constructor_eq_dec); [exact H | congruence ].
Defined.

Lemma Exists_dec_gen :
  forall {A : Type} (P : A -> Prop) (l : list A),
  (forall x : A, In x l -> {P x} + {~ P x}) -> {Exists P l} + {~ Exists P l}.
Proof.
(* Goal: forall (A : Type) (P : forall _ : A, Prop) (l : list A) (_ : forall (x : A) (_ : @In A x l), sumbool (P x) (not (P x))), sumbool (@Exists A P l) (not (@Exists A P l)) *)
intros A P l P_dec.
(* Goal: sumbool (@Exists A P l) (not (@Exists A P l)) *)
induction l as [ | x l IH ].

- right.
(* Goal: not (@Exists A P (@cons A x l)) *)
  intro Hex.
(* Goal: False *)
  inversion Hex.

- elim (P_dec x); [ | | simpl; tauto ].

  + intro HP.
(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
    left.
(* Goal: @Exists A P (@cons A x l) *)
    apply Exists_cons_hd; assumption.

  + intro HnotP.
(* Goal: sumbool (@Exists A P (@cons A x l)) (not (@Exists A P (@cons A x l))) *)
    elim IH.

(* Goal: not (@Exists A P (@cons A x l)) *)
    * intro Hex.
(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
      left.
(* Goal: @Exists A P (@cons A x l) *)
      apply Exists_cons_tl; assumption.

    * intro Hnotex.
(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
      right.
(* Goal: not (@Exists A P (@cons A x l)) *)
      intro Hex.
(* Goal: False *)
      inversion Hex; tauto.

    * intros x' Hx'.
(* Goal: sumbool (P x') (not (P x')) *)
      apply P_dec.
(* Goal: @In A x' (@cons A x l) *)
      simpl; tauto.
Defined.

Lemma Forall_dec_gen :
  forall {A : Type} (P : A -> Prop) (l : list A),
  (forall x : A, In x l -> {P x} + {~ P x}) -> {Forall P l} + {~ Forall P l}.
Proof.
(* Goal: forall (A : Type) (P : forall _ : A, Prop) (l : list A) (_ : forall (x : A) (_ : @In A x l), sumbool (P x) (not (P x))), sumbool (@Forall A P l) (not (@Forall A P l)) *)
  intros A P l.
  induction l as [ | x' l' IH ];
    [ intros; left; constructor | ].
(* Goal: forall _ : forall (x : A) (_ : @In A x (@cons A x' l')), sumbool (P x) (not (P x)), sumbool (@Forall A P (@cons A x' l')) (not (@Forall A P (@cons A x' l'))) *)
  intros Hx'l'.
  assert (Hx' : {P x'} + {~ P x'}) by now apply Hx'l'; left.
  assert (Hl' : forall x : A, In x l' -> {P x} + {~ P x}) by now intros; apply Hx'l'; right.
(* Goal: sumbool (@Forall A P (@cons A x' l')) (not (@Forall A P (@cons A x' l'))) *)
  clear Hx'l'.
(* Goal: sumbool (@Forall A P (@cons A x' l')) (not (@Forall A P (@cons A x' l'))) *)
  apply IH in Hl'.
  elim Hx'; elim Hl'; intros H'x' H'l';
  [ now left; constructor | | | ];
  now right; intros Hfor; inversion Hfor.
Defined.

Lemma Forall2_dec_gen :
  forall {A B : Type} (R : A -> B -> Prop) (xs : list A) (ys : list B),
  (forall x y, In x xs -> In y ys -> {R x y}+{~R x y}) ->
  {Forall2 R xs ys}+{~Forall2 R xs ys}.
Proof.
(* Goal: forall (A B : Type) (R : forall (_ : A) (_ : B), Prop) (xs : list A) (ys : list B) (_ : forall (x : A) (y : B) (_ : @In A x xs) (_ : @In B y ys), sumbool (R x y) (not (R x y))), sumbool (@Forall2 A B R xs ys) (not (@Forall2 A B R xs ys)) *)
  intros A B R xs.
(* Goal: forall (ys : list B) (_ : forall (x : A) (y : B) (_ : @In A x xs) (_ : @In B y ys), sumbool (R x y) (not (R x y))), sumbool (@Forall2 A B R xs ys) (not (@Forall2 A B R xs ys)) *)
  induction xs as [ | x xs IH ].

  - intros ys.
    case ys; intros;
      [ left; constructor
      | right; intros Hfor; inversion Hfor ].

  - intros ys; case ys; clear ys;
    [ now intros; right; intros Hfor; inversion Hfor | ].
(* Goal: forall (b : B) (l : list B) (_ : forall (x0 : A) (y : B) (_ : @In A x0 (@cons A x xs)) (_ : @In B y (@cons B b l)), sumbool (R x0 y) (not (R x0 y))), sumbool (@Forall2 A B R (@cons A x xs) (@cons B b l)) (not (@Forall2 A B R (@cons A x xs) (@cons B b l))) *)
    intros y ys Hxxsyys.

    assert (Hxy : {R x y} + {~ R x y}) by now apply Hxxsyys; left.
    assert (Hxsys : {Forall2 R xs ys} + {~ Forall2 R xs ys})
(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
      by now apply IH; intros; apply Hxxsyys; right.
(* Goal: sumbool (@Forall2 A B R (@cons A x xs) (@cons B y ys)) (not (@Forall2 A B R (@cons A x xs) (@cons B y ys))) *)
    clear Hxxsyys.
    elim Hxy; elim Hxsys; intros H'xsys H'xy;
    [ now left; constructor | | | ] ;
    now right; intros Hfor; inversion Hfor.
Defined.

Lemma clos_refl_dec {A : Type} (A_dec : forall x y:A, {x=y}+{x<>y})
  (R : A -> A -> Prop) (x y : A) (R_dec : {R x y}+{~R x y}) :
  {clos_refl R x y}+{~(clos_refl R) x y}.
Proof.
(* Goal: @clos_refl (term vv ff cc) (@PPO vv ff cc rk') x0 y0 *)
unfold clos_refl.
(* Goal: sumbool (or (R x y) (@eq A x y)) (not (or (R x y) (@eq A x y))) *)
destruct (A_dec x y) as [ Heq | Hneq ].

- left.
(* Goal: False *)
  tauto.

- destruct R_dec as [ Hr | Hnotr ].

  + left.
(* Goal: False *)
    tauto.

(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
  + right.
(* Goal: False *)
    tauto.
Defined.

Lemma product_dec (A : Type) (A_dec : forall x y:A, {x=y}+{x<>y})
  (R : A -> A -> Prop) (xs ys : list A)
  (R_dec : forall x y, In x xs -> In y ys -> {R x y}+{~R x y}) :
  {product R xs ys}+{~product R xs ys}.
Proof.
revert ys R_dec.
induction xs as [ | x xs IH ]; intros ys R_dec.

- right.
  intro Hproduct.
  inversion Hproduct.

- destruct ys as [ | y ys ].

(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
  + right.
    intro Hproduct.
    inversion Hproduct.

  + destruct (A_dec x y) as [ Heq | Hneq ].

    * {elim (IH ys).

      - intro Hprod.
(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
        left.
        apply product_conseq; assumption.

      - intro Hnotprod.
        elim (R_dec x y).

        + intro Hr.
          eelim (Forall2_dec_gen (clos_refl R) xs ys _).

Unshelve.

          * intro Hall.
(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
            left.
(* Goal: @product A R (@cons A t2 lt1) (@cons A t3 lt3) *)
            apply product_consst; trivial.

          * intro Hnotall.
(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
            right.
            intro Hprod.
(* Goal: False *)
            inversion Hprod; tauto.

          * intros x' y' Hx' Hy'.
            apply clos_refl_dec; [ exact A_dec | ].
(* Goal: @In A x' (@cons A x l) *)
            apply R_dec; simpl; tauto.

        + intro HnotR.
(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
          right.
          intro Hprod.
(* Goal: False *)
          inversion Hprod; tauto.

        + simpl; tauto.

        + simpl; tauto.

      - intros; apply R_dec; simpl; tauto.
      }

      * {elim (R_dec x y).

        - intro Hr.
          eelim (Forall2_dec_gen (clos_refl R) xs ys _).

Unshelve.

          + intro Hall.
(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
            left.
(* Goal: @product A R (@cons A t2 lt1) (@cons A t3 lt3) *)
            apply product_consst; trivial.

          + intro Hnotall.
(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
            right.
            intro Hprod.
(* Goal: False *)
            inversion Hprod; tauto.

          + intros x' y' Hx' Hy'.
            apply clos_refl_dec; [ exact A_dec | ].
(* Goal: @In A x' (@cons A x l) *)
            apply R_dec; simpl; tauto.

        - intro HnotR.
(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
          right.
          intro Hprod.
(* Goal: False *)
          inversion Hprod; tauto.

        - simpl; tauto.

        - simpl; tauto.
        }
Defined.

Lemma PPO_dec t1 t2: {PPO t1 t2}+{~PPO t1 t2}.
Proof.
clear rule_default.
remember (term_size t1 + term_size t2) as whole_size eqn: H_size.
(* Goal: forall _ : PPO t1 t2, not (PPO t2 t1) *)
revert t1 t2 H_size.
induction whole_size as [ whole_size IH ] using lt_wf_rect.
intros [ x | c lt | f lt ] [ x' | c' lt' | f' lt' ] H_size;
 try (right; intro Hppo; inversion Hppo; fail).

- destruct (@in_dec term term_dec (var x) lt') as [ Hin | Hnotin ].

  + left.
    apply ppo_constr_in; exact Hin.

  + eelim (Exists_dec_gen (fun t => PPO (var x) t) lt' _).

Unshelve.

(* Goal: not (@Exists A P (@cons A x l)) *)
    * intro Hex.
(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
      left.
      rewrite Exists_exists in Hex.
      destruct Hex as (t' & Hin & Hppo).
      apply ppo_constr_sub with t'; trivial.

    * intro Hnotex.
(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
      right.
      rewrite Exists_exists in Hnotex.
(* Goal: not (PPO t t) *)
      intro Hppo.
      inversion Hppo; [ tauto | ].
      apply Hnotex.
      eexists.
      split; eassumption.

    * simpl.
      intros t' Hin.
      eapply IH; [ | reflexivity ].
      subst whole_size.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
      simpl.
      apply le_lt_n_Sm, in_le_suml.
(* Goal: @In (Syntax.term variable function constructor) (@subst variable function constructor s (@term_from_pattern variable function constructor p)) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (fix term_from_value (v : Syntax.value constructor) : Syntax.term variable function constructor := match v with | c_capply c lc => @capply variable function constructor c (@map (Syntax.value constructor) (Syntax.term variable function constructor) term_from_value lc) end) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) ((fix psubst (s : forall _ : variable, Syntax.value constructor) (p : Syntax.pattern variable constructor) {struct p} : Syntax.value constructor := match p with | p_var x => s x | p_capply c lp => @c_capply constructor c (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (psubst s) lp) end) s) lp)) *)
      rewrite in_map_iff.
      exists t'.
(* Goal: False *)
      tauto.

- destruct (@in_dec term term_dec (var x) lt') as [ Hin | Hnotin ].

  + left.
    apply ppo_fun_in; exact Hin.

  + eelim (Exists_dec_gen (PPO (var x)) lt' _).

Unshelve.

(* Goal: not (@Exists A P (@cons A x l)) *)
    * intro Hex.
(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
      left.
      rewrite Exists_exists in Hex.
      destruct Hex as (t' & Hin & Hppo).
      apply ppo_fun_sub with t'; trivial.

    * intro Hnotex.
(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
      right.
      rewrite Exists_exists in Hnotex.
(* Goal: not (PPO t t) *)
      intro Hppo.
      inversion Hppo; [ tauto | ].
      apply Hnotex.
      eexists.
      split; eassumption.

    * intros t' Hin.
      eapply IH; [ | reflexivity ].
      subst whole_size.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
      simpl.
      apply le_lt_n_Sm, in_le_suml.
(* Goal: @In (Syntax.term variable function constructor) (@subst variable function constructor s (@term_from_pattern variable function constructor p)) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (fix term_from_value (v : Syntax.value constructor) : Syntax.term variable function constructor := match v with | c_capply c lc => @capply variable function constructor c (@map (Syntax.value constructor) (Syntax.term variable function constructor) term_from_value lc) end) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) ((fix psubst (s : forall _ : variable, Syntax.value constructor) (p : Syntax.pattern variable constructor) {struct p} : Syntax.value constructor := match p with | p_var x => s x | p_capply c lp => @c_capply constructor c (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (psubst s) lp) end) s) lp)) *)
      rewrite in_map_iff.
      exists t'.
(* Goal: False *)
      tauto.

- destruct (@in_dec term term_dec (capply c lt) lt') as [ Hin | Hnotin ].

  + left.
    apply ppo_constr_in; exact Hin.

  + eelim (Exists_dec_gen (PPO (capply c lt)) lt' _).

Unshelve.

(* Goal: not (@Exists A P (@cons A x l)) *)
    * intro Hex.
(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
      left.
      rewrite Exists_exists in Hex.
      destruct Hex as (t' & Hin & Hppo).
      apply ppo_constr_sub with t'; trivial.

    * intro Hnotex.
(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
      right.
      rewrite Exists_exists in Hnotex.
(* Goal: not (PPO t t) *)
      intro Hppo.
      inversion Hppo; [ tauto | ].
      apply Hnotex.
      eexists.
      split; eassumption.

    * intros t' Hin.
      eapply IH; [ | reflexivity ].
      subst whole_size.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
      simpl.
      apply le_lt_n_Sm, in_le_suml.
(* Goal: @In (Syntax.term variable function constructor) (@subst variable function constructor s (@term_from_pattern variable function constructor p)) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (fix term_from_value (v : Syntax.value constructor) : Syntax.term variable function constructor := match v with | c_capply c lc => @capply variable function constructor c (@map (Syntax.value constructor) (Syntax.term variable function constructor) term_from_value lc) end) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) ((fix psubst (s : forall _ : variable, Syntax.value constructor) (p : Syntax.pattern variable constructor) {struct p} : Syntax.value constructor := match p with | p_var x => s x | p_capply c lp => @c_capply constructor c (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (psubst s) lp) end) s) lp)) *)
      rewrite in_map_iff.
      exists t'.
(* Goal: False *)
      tauto.

- destruct (@in_dec term term_dec (capply c lt) lt') as [ Hin | Hnotin ].

  + left.
    apply ppo_fun_in; exact Hin.

  + eelim (Exists_dec_gen (PPO (capply c lt)) lt' _).

Unshelve.

(* Goal: not (@Exists A P (@cons A x l)) *)
    * intro Hex.
(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
      left.
      rewrite Exists_exists in Hex.
      destruct Hex as (t' & Hin & Hppo).
      apply ppo_fun_sub with t'; trivial.

    * intro Hnotex.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      {eelim (Forall_dec_gen (fun t => PPO t (fapply f' lt')) lt _).

Unshelve.

      - intro Hall.
(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
        left.
        rewrite Forall_forall in Hall.
        apply ppo_constr_split; assumption.

      - intro Hnotall.
(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
        right.
        rewrite Exists_exists in Hnotex.
        rewrite Forall_forall in Hnotall.
        intros Hppo.
        inversion Hppo; [ tauto | firstorder | tauto ].

      - intros t Hin.
        eapply IH; [ | reflexivity ].
        subst whole_size.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc s) (@term_size vv ff cc (@fapply vv ff cc f lt))) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
        apply plus_lt_compat_r.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
        simpl.
        apply le_lt_n_Sm, in_le_suml.
(* Goal: @In (Syntax.term variable function constructor) (@subst variable function constructor s (@term_from_pattern variable function constructor p)) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (fix term_from_value (v : Syntax.value constructor) : Syntax.term variable function constructor := match v with | c_capply c lc => @capply variable function constructor c (@map (Syntax.value constructor) (Syntax.term variable function constructor) term_from_value lc) end) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) ((fix psubst (s : forall _ : variable, Syntax.value constructor) (p : Syntax.pattern variable constructor) {struct p} : Syntax.value constructor := match p with | p_var x => s x | p_capply c lp => @c_capply constructor c (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (psubst s) lp) end) s) lp)) *)
        rewrite in_map_iff.
        exists t.
(* Goal: False *)
        tauto.
      }

    * intros t' Hin.
      eapply IH; [ | reflexivity ].
      subst whole_size.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
      simpl.
      apply le_lt_n_Sm, in_le_suml.
(* Goal: @In (Syntax.term variable function constructor) (@subst variable function constructor s (@term_from_pattern variable function constructor p)) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (fix term_from_value (v : Syntax.value constructor) : Syntax.term variable function constructor := match v with | c_capply c lc => @capply variable function constructor c (@map (Syntax.value constructor) (Syntax.term variable function constructor) term_from_value lc) end) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) ((fix psubst (s : forall _ : variable, Syntax.value constructor) (p : Syntax.pattern variable constructor) {struct p} : Syntax.value constructor := match p with | p_var x => s x | p_capply c lp => @c_capply constructor c (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (psubst s) lp) end) s) lp)) *)
      rewrite in_map_iff.
      exists t'.
(* Goal: False *)
      tauto.

- destruct (@in_dec term term_dec (fapply f lt) lt') as [ Hin | Hnotin ].

  + left.
    apply ppo_constr_in; exact Hin.

  + eelim (Exists_dec_gen (PPO (fapply f lt)) lt' _).

Unshelve.

(* Goal: not (@Exists A P (@cons A x l)) *)
    * intro Hex.
(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
      left.
      rewrite Exists_exists in Hex.
      destruct Hex as (t' & Hin & Hppo).
      apply ppo_constr_sub with t'; trivial.

    * intro Hnotex.
(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
      right.
      rewrite Exists_exists in Hnotex.
(* Goal: not (PPO t t) *)
      intro Hppo.
      inversion Hppo; [ tauto | ].
      apply Hnotex.
      eexists.
      split; eassumption.

    * intros t' Hin.
      eapply IH; [ | reflexivity ].
      subst whole_size.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
      simpl.
      apply le_lt_n_Sm, in_le_suml.
(* Goal: @In (Syntax.term variable function constructor) (@subst variable function constructor s (@term_from_pattern variable function constructor p)) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (fix term_from_value (v : Syntax.value constructor) : Syntax.term variable function constructor := match v with | c_capply c lc => @capply variable function constructor c (@map (Syntax.value constructor) (Syntax.term variable function constructor) term_from_value lc) end) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) ((fix psubst (s : forall _ : variable, Syntax.value constructor) (p : Syntax.pattern variable constructor) {struct p} : Syntax.value constructor := match p with | p_var x => s x | p_capply c lp => @c_capply constructor c (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (psubst s) lp) end) s) lp)) *)
      rewrite in_map_iff.
      exists t'.
(* Goal: False *)
      tauto.

- destruct (@in_dec term term_dec (fapply f lt) lt') as [ Hin | Hnotin ].

  + left.
    apply ppo_fun_in; exact Hin.

  + eelim (Exists_dec_gen (PPO (fapply f lt)) lt' _).

Unshelve.

(* Goal: not (@Exists A P (@cons A x l)) *)
    * intro Hex.
(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
      left.
      rewrite Exists_exists in Hex.
      destruct Hex as (t' & Hin & Hppo).
      apply ppo_fun_sub with t'; trivial.

    * intro Hnotex.
      rewrite Exists_exists in Hnotex.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      {destruct (lt_eq_lt_dec (rank f) (rank f')) as [ [ Hlt | Heq ] | Hgt ].

      - eelim (Forall_dec_gen (fun t => PPO t (fapply f' lt')) lt _).

Unshelve.

        * intro Hall.
(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
          left.
          rewrite Forall_forall in Hall.
          apply ppo_funlt_split; assumption.

        * intro Hnotall.
(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
          right.
          rewrite Forall_forall in Hnotall.
          intros Hppo.
          inversion Hppo; [ tauto | firstorder | tauto | omega ].

        * intros t Hin.
          eapply IH; [ | reflexivity ].
          subst whole_size.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc s) (@term_size vv ff cc (@fapply vv ff cc f lt))) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
          apply plus_lt_compat_r.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
          simpl.
          apply le_lt_n_Sm, in_le_suml.
(* Goal: @In (Syntax.term variable function constructor) (@subst variable function constructor s (@term_from_pattern variable function constructor p)) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (fix term_from_value (v : Syntax.value constructor) : Syntax.term variable function constructor := match v with | c_capply c lc => @capply variable function constructor c (@map (Syntax.value constructor) (Syntax.term variable function constructor) term_from_value lc) end) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) ((fix psubst (s : forall _ : variable, Syntax.value constructor) (p : Syntax.pattern variable constructor) {struct p} : Syntax.value constructor := match p with | p_var x => s x | p_capply c lp => @c_capply constructor c (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (psubst s) lp) end) s) lp)) *)
          rewrite in_map_iff.
          exists t.
(* Goal: False *)
          tauto.

      - destruct (product_dec term_dec PPO lt lt').

        + intros t t' Ht Ht'.
          eapply IH; [ | reflexivity ].
          subst whole_size.
          apply plus_lt_compat; simpl; apply le_lt_n_Sm, in_le_suml;
(* Goal: False *)
           rewrite in_map_iff; eexists; tauto.

        + left.
(* Goal: PPO (@subst variable function constructor s (@fapply variable function constructor g lt)) (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
          apply ppo_funeqv_split; trivial.

(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
        + right.
(* Goal: not (PPO t t) *)
          intro Hppo.
          inversion Hppo; [ tauto | firstorder | omega | tauto ].

      - right.
(* Goal: not (PPO t t) *)
        intro Hppo.
        inversion Hppo; [ tauto | firstorder | omega | omega ].
      }

    * intros t' Hin.
      eapply IH; [ | reflexivity ].
      subst whole_size.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
      simpl.
      apply le_lt_n_Sm, in_le_suml.
(* Goal: @In (Syntax.term variable function constructor) (@subst variable function constructor s (@term_from_pattern variable function constructor p)) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (fix term_from_value (v : Syntax.value constructor) : Syntax.term variable function constructor := match v with | c_capply c lc => @capply variable function constructor c (@map (Syntax.value constructor) (Syntax.term variable function constructor) term_from_value lc) end) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) ((fix psubst (s : forall _ : variable, Syntax.value constructor) (p : Syntax.pattern variable constructor) {struct p} : Syntax.value constructor := match p with | p_var x => s x | p_capply c lp => @c_capply constructor c (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (psubst s) lp) end) s) lp)) *)
      rewrite in_map_iff.
      exists t'.
(* Goal: False *)
      tauto.
Defined.

Lemma product_length A (R: A -> A -> Prop) xs ys :
  product R xs ys -> length xs = length ys.
Proof.
(* Goal: forall _ : @product A R xs ys, @eq nat (@length A xs) (@length A ys) *)
intro H.
(* Goal: @eq nat (@length A xs) (@length A ys) *)
induction H as [ x y xs ys H1 H2 IH | x y xs ys H1 H2 ].

- simpl; congruence.

- apply Forall2_length in H2.
(* Goal: @eq nat (@length A (@cons A x xs)) (@length A (@cons A y ys)) *)
  simpl; congruence.
Qed.

Lemma product_Forall2 A (R: A -> A -> Prop) ls lt : product R ls lt -> Forall2 (clos_refl R) ls lt.
Proof.
(* Goal: forall _ : @product A R ls lt, @Exists2 A A R ls lt *)
intro H_product.
(* Goal: @clos_refl (term vv ff cc) (@PPO vv ff cc rk') x0 y0 *)
unfold clos_refl.
(* Goal: @Exists2 A A R ls lt *)
induction H_product; auto.
Qed.

Lemma product_Exists2 A (R: A -> A -> Prop) ls lt : product R ls lt -> Exists2 R ls lt.
Proof.
(* Goal: forall _ : @product A R ls lt, @Exists2 A A R ls lt *)
intro H_product.
(* Goal: @Exists2 A A R ls lt *)
induction H_product; auto.
Qed.

Definition PPO_rule (r: rule) : Prop :=
  match r with
    | rule_intro f lp t => PPO t (fapply f (map (@term_from_pattern _ _ _) lp))
  end.

Definition PPO_prog : Prop :=
  forall r, In r prog -> PPO_rule r.

Lemma value_PPO_function (v: value) (f: function) (lt: list term) :
  PPO (@term_from_value _ _ _ v) (fapply f lt).
Proof.
  (* c’est juste un paquet de ppo_constr_split pour déconstruire la valeur *)
(* Goal: PPO (@term_from_value variable function constructor v) (@fapply variable function constructor f lt) *)
  induction v using value_ind2.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
  simpl.

(* Goal: @PPO vv ff cc rk' (@capply vv ff cc c ls) (@fapply vv ff cc f lt) *)
  apply ppo_constr_split.
(* Goal: forall (s : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) s (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) l)), PPO s (@fapply variable function constructor f lt) *)
  intros s H_s_in_map.
(* Goal: PPO s (@fapply variable function constructor f lt) *)
  rewrite in_map_iff in H_s_in_map.
(* Goal: PPO s (@fapply variable function constructor f lt) *)
  destruct H_s_in_map as (v & H1 & H2).
(* Goal: PPO s (@fapply variable function constructor f lt) *)
  subst s.
(* Goal: @eq nat (rk f0) (rk' f0) *)
  apply H.
(* Goal: @In (Syntax.value constructor) v l *)
  exact H2.
Qed.

Lemma product_trans (A: Type) (R : A -> A -> Prop) lt1 lt2 lt3 :
    (forall t1 t2 t3, In t1 lt1 -> In t2 lt2 -> In t3 lt3 -> R t1 t2 -> R t2 t3 -> R t1 t3) ->
    product R lt1 lt2 -> product R lt2 lt3 -> product R lt1 lt3.
Proof.
(* Goal: forall (_ : forall (t1 t2 t3 : A) (_ : @In A t1 lt1) (_ : @In A t2 lt2) (_ : @In A t3 lt3) (_ : R t1 t2) (_ : R t2 t3), R t1 t3) (_ : @product A R lt1 lt2) (_ : @product A R lt2 lt3), @product A R lt1 lt3 *)
intros H_R H12 H23.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
assert (length lt1 = length lt2) as Hlen12. { apply product_length in H12; trivial. }
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
assert (length lt2 = length lt3) as Hlen23. { apply product_length in H23; trivial. }
(* Goal: @product A R lt1 lt3 *)
revert lt1 H_R Hlen12 H12.
induction H23 as [ Ba t23 lt2 lt3 Be H_prod23 IH | t2 t3 lt2 lt3 HR23 HForall23 ];
intros lt1 H_R Hlen12 H12.

- subst.
  inversion H12 as [ Ba Bb lt1' Bd Be H_prod12 Bg Bh | t1 Bb lt1' Bd HR12 HForall12 Bg Bh ];
  subst; rename lt1' into lt1.

  + apply product_conseq; trivial.
    simpl in *.
(* Goal: @product A R lt1 lt3 *)
    apply IH; try congruence.
(* Goal: forall (t1 t2 t3 : A) (_ : @In A t1 lt1) (_ : @In A t2 lt2) (_ : @In A t3 lt3) (_ : R t1 t2) (_ : R t2 t3), R t1 t3 *)
    intros t1 t2 t3 H_In1 H_In2 H_In3.
(* Goal: False *)
    apply H_R; tauto.

  + apply product_consst; trivial.
(* Goal: @Forall2 A A (@clos_refl A R) lt1 lt3 *)
    apply Forall2_trans with (ys := lt2); trivial.

    * intros t1' t2; intros; apply clos_refl_trans with (t2:=t2); trivial.
(* Goal: @In A x' (@cons A x l) *)
      apply H_R; simpl; tauto.

    * apply product_Forall2.
(* Goal: @product A R lt2 lt3 *)
      exact H_prod23.

- inversion H12 as [ Ba Bb lt1' Bd Be Hprod12 Bg Bh | t1 Bb lt1' Bd HR12 HForall12 Bg Bh ];
  subst; rename lt1' into lt1.

  + apply product_consst; trivial.
(* Goal: @Forall2 A A (@clos_refl A R) lt1 lt3 *)
    apply Forall2_trans with (ys := lt2); trivial.

    * intros t1' t2' t3' Hin1' Hin2' Hin3' [ HR12' | Heq12'] [ HR23' | Heq23' ];
      subst;
      unfold clos_refl;
(* Goal: False *)
      try tauto.

(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
      left.
(* Goal: @In A x' (@cons A x l) *)
      apply (H_R t1' t2' t3'); trivial; simpl; tauto.

    * apply product_Forall2; trivial.

  + apply product_consst.

    * apply (H_R t1 t2 t3); simpl; tauto.

    * apply Forall2_trans with (ys := lt2); trivial.
      intros t1' t2' t3' Hin1' Hin2' Hin3' [ HR12' | Heq12'] [ HR23' | Heq23' ];
      subst;
      unfold clos_refl;
(* Goal: False *)
      try tauto.

(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
      left.
(* Goal: @In A x' (@cons A x l) *)
      apply (H_R t1' t2' t3'); trivial; simpl; tauto.
Qed.

Lemma PPO_trans t1 t2 t3 : PPO t1 t2 -> PPO t2 t3 -> PPO t1 t3.
Proof.
remember (term_size t1 + term_size t2 + term_size t3) as whole_size eqn: H_size.
(* Goal: forall (_ : PPO t1 t2) (_ : PPO t2 t3), PPO t1 t3 *)
revert t1 t2 t3 H_size.
(* Goal: forall (t s : term vv ff cc) (_ : @eq nat whole_size (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s))) (_ : forall (f : ff) (_ : @In ff f (@functions_of_term vv ff cc t)), @eq nat (rk f) (rk' f)) (_ : forall (f : ff) (_ : @In ff f (@functions_of_term vv ff cc s)), @eq nat (rk f) (rk' f)) (_ : @PPO vv ff cc rk t s), @PPO vv ff cc rk' t s *)
induction whole_size as [ whole_size IH ] using lt_wf_ind.
(* Goal: forall (t1 t2 t3 : Syntax.term variable function constructor) (_ : @eq nat whole_size (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3))) (_ : PPO t1 t2) (_ : PPO t2 t3), PPO t1 t3 *)
intros t1 t2 t3 H_size H12 H23.

inversion H23 as [ Ba c3 lt3 Hin3 Be Bf | Ba f3 lt3 Hin3 Be Bf | Ba t3' c3 lt3 Hin3 Hppo23 Bg Bh | Ba t3' f3 lt3 Hin3 Hppo23 Bg Bh | c2 lt2 f3 lt3 Hppo23 Bf Bg | f2 lt2 f3 lt3 Hrk23 Hppo23 Bg Bh | f2 lt2 f3 lt3 Hrk23 Hprodppo23 Bg Bh ];
(* Goal: @eq nat (rk f0) (rk' f0) *)
subst.

- (* ppo_constr_in *)
(* Goal: PPO t1 (@capply variable function constructor c3 lt3) *)
  apply ppo_constr_sub with (t:=t2); trivial.

- (* ppo_fun_in *)
(* Goal: PPO t1 (@fapply variable function constructor f3 lt3) *)
  apply ppo_fun_sub with (t:=t2); trivial.

- (* ppo_constr_sub *)
(* Goal: PPO t1 (@capply variable function constructor c3 lt3) *)
  apply ppo_constr_sub with (t:=t3'); trivial.
  apply IH with (m:= term_size t1 + term_size t2 + term_size t3') (t2 := t2); auto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
  apply plus_lt_compat_l.
(* Goal: lt (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3)) (Init.Nat.add (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
  apply (in_map (@term_size _ _ _)), in_le_suml in Hin3.
(* Goal: lt (@term_size variable function constructor t2) (@term_size variable function constructor (@fapply variable function constructor f2 lt2)) *)
  apply le_lt_n_Sm; trivial.

- (* ppo_fun_sub *)
(* Goal: PPO t1 (@fapply variable function constructor f3 lt3) *)
  apply ppo_fun_sub with (t:=t3'); trivial.
  apply IH with (m:= term_size t1 + term_size t2 + term_size t3') (t2 := t2); auto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
  apply plus_lt_compat_l.
(* Goal: lt (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3)) (Init.Nat.add (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
  apply (in_map (@term_size _ _ _)), in_le_suml in Hin3.
(* Goal: lt (@term_size variable function constructor t2) (@term_size variable function constructor (@fapply variable function constructor f2 lt2)) *)
  apply le_lt_n_Sm; trivial.

- (* ppo_constr_split *)
(* Goal: PPO t1 (@fapply variable function constructor f3 lt3) *)
  inversion H12 as [ | | Ba t2 Bc Bd Hin2 Hppo12 Bg Bh | | | | ]; subst; auto.
  apply IH with (m:= term_size t1 + term_size t2 + term_size (fapply f3 lt3)) (t2 := t2); auto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
  apply plus_lt_compat_r; apply plus_lt_compat_l.
(* Goal: lt (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3)) (Init.Nat.add (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
  apply (in_map (@term_size _ _ _)), in_le_suml in Hin2.
(* Goal: lt (@term_size variable function constructor t2) (@term_size variable function constructor (@fapply variable function constructor f2 lt2)) *)
  apply le_lt_n_Sm; trivial.

- (* ppo_funlt_split *)
(* Goal: @eq nat (rk f0) (rk' f0) *)
  inversion H12 as [ | Ba Bb Bc Hin1 Be Bf | | Ba t2 Bc Bd Hin2 Hppo12 Bg Bh | c1 lt1 Bc Bd Hppolt1f2 Bf Bg | f1 lt1 Bc Bd Hrk12 Hppolt1f2 Bg Bh | f1 lt1 Bc Bd Hrk12 Hprodppo12 Bg Bh ]; subst.

  + (* ppo_fun_in *)
(* Goal: PPO t1 (@fapply variable function constructor f3 lt3) *)
    apply Hppo23; trivial.

  + (* ppo_fun_sub *)
    apply IH with (m:= term_size t1 + term_size t2 + term_size (fapply f3 lt3)) (t2 := t2); auto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
    apply plus_lt_compat_r; apply plus_lt_compat_l.
(* Goal: lt (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3)) (Init.Nat.add (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
    apply (in_map (@term_size _ _ _)), in_le_suml in Hin2.
(* Goal: lt (@term_size variable function constructor t2) (@term_size variable function constructor (@fapply variable function constructor f2 lt2)) *)
    apply le_lt_n_Sm; trivial.

  + (* ppo_constr_split *)
(* Goal: @PPO vv ff cc rk' (@capply vv ff cc c ls) (@fapply vv ff cc f lt) *)
    apply ppo_constr_split.
(* Goal: forall (s : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) s lt1), PPO s (@fapply variable function constructor f3 lt3) *)
    intros t1 Hin1.
    apply IH with (m:= term_size t1 + term_size (fapply f2 lt2) + term_size (fapply f3 lt3)) (t2 := fapply f2 lt2);
(* Goal: @eq nat (rk f0) (rk' f0) *)
    auto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc s) (@term_size vv ff cc (@fapply vv ff cc f lt))) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
    do 2 apply plus_lt_compat_r.
(* Goal: lt (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3)) (Init.Nat.add (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
    apply (in_map (@term_size _ _ _)), in_le_suml in Hin1.
(* Goal: lt (@term_size variable function constructor t2) (@term_size variable function constructor (@fapply variable function constructor f2 lt2)) *)
    simpl; apply le_lt_n_Sm; trivial.

  + (* ppo_funlt_split *)
(* Goal: PPO (@fapply variable function constructor f1 lt1) (@fapply variable function constructor f3 lt3) *)
    apply ppo_funlt_split; try omega.
(* Goal: forall (s : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) s lt1), PPO s (@fapply variable function constructor f3 lt3) *)
    intros t1 Hin1.
    apply IH with (m:= term_size t1 + term_size (fapply f2 lt2) + term_size (fapply f3 lt3)) (t2:=fapply f2 lt2);
(* Goal: @eq nat (rk f0) (rk' f0) *)
    auto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc s) (@term_size vv ff cc (@fapply vv ff cc f lt))) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
    do 2 apply plus_lt_compat_r.
(* Goal: lt (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3)) (Init.Nat.add (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
    apply (in_map (@term_size _ _ _)), in_le_suml in Hin1.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
    simpl.
(* Goal: lt (@term_size variable function constructor t1) (S (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt1))) *)
    apply le_lt_n_Sm.
(* Goal: @eq nat (rk g) (rk f) *)
    trivial.

  + (* ppo_funeqv_split *)
(* Goal: PPO (@fapply variable function constructor f1 lt1) (@fapply variable function constructor f3 lt3) *)
    apply ppo_funlt_split; try omega.
(* Goal: forall (s : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) s lt1), PPO s (@fapply variable function constructor f3 lt3) *)
    intros t1 Hin1.
(* Goal: PPO t1 (@fapply variable function constructor f3 lt3) *)
    apply product_Forall2 in Hprodppo12.
(* Goal: @eq nat (rk g) (rk f) *)
    apply Forall2_In_l with (x := t1) in Hprodppo12; trivial.
(* Goal: PPO t1 (@fapply variable function constructor f3 lt3) *)
    destruct Hprodppo12 as ( t2 & Hin2 & [ Hppo12 | Heq12 ] ).

    * apply IH with (m:= term_size t1 + term_size t2 + term_size (fapply f3 lt3)) (t2 := t2); eauto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc s) (@term_size vv ff cc (@fapply vv ff cc f lt))) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_r.
(* Goal: lt (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3)) (Init.Nat.add (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
      apply (in_map (@term_size _ _ _)), in_le_suml in Hin1.
(* Goal: lt (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3)) (Init.Nat.add (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
      apply (in_map (@term_size _ _ _)), in_le_suml in Hin2.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
      simpl.
      auto with *.

    * subst.
(* Goal: PPO t2 (@fapply variable function constructor f3 lt3) *)
      apply Hppo23.
(* Goal: @eq nat (rk g) (rk f) *)
      trivial.

- (* ppo_funeqv_split *)
  inversion H12 as [ | Ba Bb Bc Hin1 Be Bf | | Ba t2 Bc Bd Hin2 Hppo12 Bg Bh | c1 lt1 Bc Bd Hppolt1f2 Bf Bg | f1 lt1 Bc Bd Hrk12 Hppolt1f2 Bg Bh | f1 lt1 Bc Bd Hrk12 Hprodppo12 Bg Bh ];
(* Goal: @eq nat (rk f0) (rk' f0) *)
  subst.

  + (* ppo_fun_in *)
(* Goal: PPO t1 (@fapply variable function constructor f3 lt3) *)
    apply product_Forall2 in Hprodppo23.
(* Goal: @eq nat (rk g) (rk f) *)
    apply Forall2_In_l with (x := t1) in Hprodppo23; trivial.
(* Goal: PPO t1 (@fapply variable function constructor f3 lt3) *)
    destruct Hprodppo23 as (t3 & Hin3 & [ Hppo13 | Heq13 ] ).

    * apply ppo_fun_sub with (t := t3); trivial.
    * apply ppo_fun_in; subst; trivial.

  + (* ppo_fun_sub *)
(* Goal: PPO t1 (@fapply variable function constructor f3 lt3) *)
    apply product_Forall2 in Hprodppo23.
(* Goal: @eq nat (rk g) (rk f) *)
    apply Forall2_In_l with (x := t2) in Hprodppo23; trivial.
(* Goal: PPO t1 (@fapply variable function constructor f3 lt3) *)
    destruct Hprodppo23 as (t3 & Hin3 & [ Hppo23 | Heq23 ] ).

    * apply ppo_fun_sub with (t := t3); trivial.
      apply IH with (m := term_size t1 + term_size t2 + term_size t3) (t2 := t2); trivial.
(* Goal: lt (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3)) (Init.Nat.add (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
      apply (in_map (@term_size _ _ _)), in_le_suml in Hin2.
(* Goal: lt (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3)) (Init.Nat.add (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
      apply (in_map (@term_size _ _ _)), in_le_suml in Hin3.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
      simpl.
      auto with *.

    * subst.
(* Goal: @eq nat (rk g) (rk f) *)
      apply ppo_fun_sub with (t := t3); trivial.

  + (* ppo_constr_split *)
(* Goal: @PPO vv ff cc rk' (@capply vv ff cc c ls) (@fapply vv ff cc f lt) *)
    apply ppo_constr_split.
(* Goal: forall (s : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) s lt1), PPO s (@fapply variable function constructor f3 lt3) *)
    intros t1 Hin1.
    apply IH with (m := term_size t1 + term_size (fapply f2 lt2) + term_size (fapply f3 lt3)) (t2 := fapply f2 lt2);
(* Goal: @eq nat (rk g) (rk f) *)
    trivial.

    * do 2 apply plus_lt_compat_r.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
      simpl.
(* Goal: lt (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3)) (Init.Nat.add (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
      apply (in_map (@term_size _ _ _)), in_le_suml in Hin1.
(* Goal: lt (@term_size variable function constructor t1) (S (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt1))) *)
      apply le_lt_n_Sm.
(* Goal: @eq nat (rk g) (rk f) *)
      trivial.

    * apply Hppolt1f2.
(* Goal: @eq nat (rk g) (rk f) *)
      trivial.

  + (* ppo_funlt_split *)
(* Goal: PPO (@fapply variable function constructor f1 lt1) (@fapply variable function constructor f3 lt3) *)
    apply ppo_funlt_split; try omega.
(* Goal: forall (s : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) s lt1), PPO s (@fapply variable function constructor f3 lt3) *)
    intros t1 Hin1.
    apply IH with (m := term_size t1 + term_size (fapply f2 lt2) + term_size (fapply f3 lt3)) (t2 := fapply f2 lt2);
(* Goal: @eq nat (rk g) (rk f) *)
    trivial.

    * do 2 apply plus_lt_compat_r.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
      simpl.
(* Goal: lt (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3)) (Init.Nat.add (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
      apply (in_map (@term_size _ _ _)), in_le_suml in Hin1.
(* Goal: lt (@term_size variable function constructor t1) (S (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt1))) *)
      apply le_lt_n_Sm.
(* Goal: @eq nat (rk g) (rk f) *)
      trivial.

    * apply Hppolt1f2.
(* Goal: @eq nat (rk g) (rk f) *)
      trivial.

  + (* ppo_funeqv_split *)
    (* Il s’agit de prouver ici que product PPO est transitif. *)
(* Goal: PPO (@fapply variable function constructor f1 lt1) (@fapply variable function constructor f3 lt3) *)
    apply ppo_funeqv_split; try congruence.
(* Goal: @eq nat (rk g) (rk f) *)
    apply product_trans with (lt2 := lt2); trivial.
(* Goal: forall (t1 t2 t3 : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) t1 lt1) (_ : @In (Syntax.term variable function constructor) t2 lt2) (_ : @In (Syntax.term variable function constructor) t3 lt3) (_ : PPO t1 t2) (_ : PPO t2 t3), PPO t1 t3 *)
    intros t1 t2 t3 Hin1 Hin2 Hin3 Hppo12 Hppo23.
    apply IH with (t2 := t2) (m := term_size t1 + term_size t2 + term_size t3); trivial.
(* Goal: lt (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3)) (Init.Nat.add (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
    apply (in_map (@term_size _ _ _)), in_le_suml in Hin1.
(* Goal: lt (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3)) (Init.Nat.add (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
    apply (in_map (@term_size _ _ _)), in_le_suml in Hin2.
(* Goal: lt (Init.Nat.add (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2)) (@term_size variable function constructor t3)) (Init.Nat.add (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
    apply (in_map (@term_size _ _ _)), in_le_suml in Hin3.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
    simpl.
    auto with *.
Qed.

Lemma PPO_trans_eq t1 t2 t3 : clos_refl PPO t1 t2 -> PPO t2 t3 -> PPO t1 t3.
Proof.
(* Goal: forall (_ : @clos_refl (Syntax.term variable function constructor) PPO t1 t2) (_ : PPO t2 t3), PPO t1 t3 *)
intros [H12 | H12] H23.

- apply PPO_trans with t2; trivial.

- congruence.
Qed.

Lemma PPO_trans_eq_r t1 t2 t3 : PPO t1 t2 -> clos_refl PPO t2 t3 -> PPO t1 t3.
Proof.
(* Goal: forall (_ : PPO t1 t2) (_ : @clos_refl (Syntax.term variable function constructor) PPO t2 t3), PPO t1 t3 *)
  intros H12 [H23 | H23].

  - apply PPO_trans with t2; trivial.
  - congruence.
Qed.

Lemma PPO_asym t1 t2 : PPO t1 t2 -> ~ PPO t2 t1.
Proof.
remember (term_size t1 + term_size t2) as whole_size eqn: H_size.
(* Goal: forall _ : PPO t1 t2, not (PPO t2 t1) *)
revert t1 t2 H_size.
(* Goal: forall (t s : term vv ff cc) (_ : @eq nat whole_size (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s))) (_ : forall (f : ff) (_ : @In ff f (@functions_of_term vv ff cc t)), @eq nat (rk f) (rk' f)) (_ : forall (f : ff) (_ : @In ff f (@functions_of_term vv ff cc s)), @eq nat (rk f) (rk' f)) (_ : @PPO vv ff cc rk t s), @PPO vv ff cc rk' t s *)
induction whole_size as [ whole_size IH ] using lt_wf_ind.
(* Goal: forall (t1 t2 : Syntax.term variable function constructor) (_ : @eq nat whole_size (Init.Nat.add (@term_size variable function constructor t1) (@term_size variable function constructor t2))) (_ : PPO t1 t2), not (PPO t2 t1) *)
intros t1 t2 H_size Hppo12 Hppo21.
(* Goal: False *)
destruct t1 as [ x | c lt | f lt ].

- inversion Hppo21.

- inversion Hppo21 as [ Ba Bb Bc Hin Be Bf | | aa t ac ad Hin Hppo ag ah | | | | ]; subst.

  + inversion Hppo12 as [ aa c2 lt2 Hin2 ae af | aa f2 lt2 Hin2 ae af | aa t3 c3 lt3 Hin3 Hppo3 ag ah | aa t3 f3 lt3 Hin3 Hppo3 ag ah | aa ab f3 lt3 Hall af ag | | ]
(* Goal: @eq nat (rk f0) (rk' f0) *)
    ; subst.

    * generalize (PPO_trans Hppo12 Hppo21).
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
      intro Hppo11.
(* Goal: False *)
      generalize Hppo11.
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
      intro Hppo11'.
      apply IH with (m := term_size (capply c lt) + term_size (capply c lt)) in Hppo11; try tauto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: @eq nat (rk g) (rk f) *)
      apply in_capply_term_size_lt; trivial.

    * generalize (PPO_trans Hppo12 Hppo21).
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
      intro Hppo11.
(* Goal: False *)
      generalize Hppo11.
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
      intro Hppo11'.
      apply IH with (m := term_size (capply c lt) + term_size (capply c lt)) in Hppo11; try tauto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: @eq nat (rk g) (rk f) *)
      apply in_fapply_term_size_lt; trivial.

    * assert (PPO t3 (capply c lt)) as Hppo. {
(* Goal: @eq nat (rk g) (rk f) *)
        apply PPO_trans with (t2 := capply c3 lt3); trivial.
(* Goal: PPO t3 (@capply variable function constructor c3 lt3) *)
        eapply ppo_constr_in.
(* Goal: @In (Syntax.term variable function constructor) t3 lt3 *)
        exact Hin3.
      }
      eapply IH with (m := term_size (capply c lt) + term_size t3) in Hppo; try tauto; try ring.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: @eq nat (rk g) (rk f) *)
      apply in_capply_term_size_lt; trivial.

    * assert (PPO t3 (capply c lt)) as Hppo. {
(* Goal: @eq nat (rk g) (rk f) *)
        apply PPO_trans with (t2 := fapply f3 lt3); trivial.
(* Goal: PPO t3 (@fapply variable function constructor f3 lt3) *)
        eapply ppo_fun_in.
(* Goal: @In (Syntax.term variable function constructor) t3 lt3 *)
        exact Hin3.
      }
      eapply IH with (m := term_size (capply c lt) + term_size t3) in Hppo; try tauto; try ring.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: @eq nat (rk g) (rk f) *)
      apply in_fapply_term_size_lt; trivial.

    * generalize Hin.
(* Goal: forall _ : @In (Syntax.term variable function constructor) t3 lt3, False *)
      intro Hin'.
(* Goal: False *)
      apply Hall in Hin.
      {apply IH with (m := term_size (fapply f3 lt3) + term_size (fapply f3 lt3)) in Hin; trivial.

      - assert (PPO (fapply f3 lt3) (fapply f3 lt3)) as H. {
(* Goal: @eq nat (rk g) (rk f) *)
        apply PPO_trans with (capply c lt); trivial.
        }
(* Goal: False *)
        tauto.

      - apply plus_lt_compat_r.
(* Goal: @eq nat (rk g) (rk f) *)
        apply in_capply_term_size_lt; trivial.
      }

  + inversion Hppo12 as [ aa c2 lt2 Hin2 ae af | aa f2 lt2 Hin2 ae af | aa t3 c3 lt3 Hin3 Hppo3 ag ah | aa t3 f3 lt3 Hin3 Hppo3 ag ah | aa ab f3 lt3 Hall af ag | | ]; subst.

    * generalize (PPO_trans Hppo12 Hppo21).
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
      intro Hppo11.
(* Goal: False *)
      generalize Hppo11.
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
      intro Hppo11'.
      apply IH with (m := term_size (capply c lt) + term_size (capply c lt)) in Hppo11; try tauto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: @eq nat (rk g) (rk f) *)
      apply in_capply_term_size_lt; trivial.

    * generalize (PPO_trans Hppo12 Hppo21).
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
      intro Hppo11.
(* Goal: False *)
      generalize Hppo11.
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
      intro Hppo11'.
      apply IH with (m := term_size (capply c lt) + term_size (capply c lt)) in Hppo11; try tauto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: @eq nat (rk g) (rk f) *)
      apply in_fapply_term_size_lt; trivial.

    * assert (PPO t3 (capply c lt)) as Hppo'. {
(* Goal: @eq nat (rk g) (rk f) *)
        apply PPO_trans with (t2 := capply c3 lt3); trivial.
(* Goal: PPO t3 (@capply variable function constructor c3 lt3) *)
        eapply ppo_constr_in.
(* Goal: @In (Syntax.term variable function constructor) t3 lt3 *)
        exact Hin3.
      }
      apply IH with (m := term_size (capply c lt) + term_size t3) in Hppo'; try tauto; try ring.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: @eq nat (rk g) (rk f) *)
      apply in_capply_term_size_lt; trivial.

    * assert (PPO t3 (capply c lt)) as Hppo'. {
(* Goal: @eq nat (rk g) (rk f) *)
        apply PPO_trans with (t2 := fapply f3 lt3); trivial.
(* Goal: PPO t3 (@fapply variable function constructor f3 lt3) *)
        eapply ppo_fun_in.
(* Goal: @In (Syntax.term variable function constructor) t3 lt3 *)
        exact Hin3.
      }
      apply IH with (m := term_size (capply c lt) + term_size t3) in Hppo'; try tauto; try ring.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: @eq nat (rk g) (rk f) *)
      apply in_fapply_term_size_lt; trivial.

    * generalize Hin.
(* Goal: forall _ : @In (Syntax.term variable function constructor) t3 lt3, False *)
      intro Hin'.
(* Goal: False *)
      apply Hall in Hin.
      apply IH with (m := term_size t + term_size (fapply f3 lt3)) in Hin; trivial; try tauto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc s) (@term_size vv ff cc (@fapply vv ff cc f lt))) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_r.
(* Goal: @eq nat (rk g) (rk f) *)
      apply in_capply_term_size_lt; trivial.

- inversion Hppo21 as [ | aa ab ac Hin ae af | | aa t3 ac ad Hin Hppo ag ah | c3 lt3 ac ad Hall af ag | f3 lt3 ac ad Hrank Hall ag ah | f3 lt3 ac ad Hrank Hprod ag ah ];
(* Goal: @eq nat (rk f0) (rk' f0) *)
  subst.

  + generalize (PPO_trans Hppo21 Hppo12).
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
    intro Hppo11.
(* Goal: False *)
    generalize Hppo11.
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
    intro Hppo11'.
    apply IH with (m := term_size t2 + term_size t2) in Hppo11; try tauto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc s) (@term_size vv ff cc (@fapply vv ff cc f lt))) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
    apply plus_lt_compat_r.
(* Goal: @eq nat (rk g) (rk f) *)
    apply in_fapply_term_size_lt; trivial.

  + generalize Hin.
(* Goal: forall _ : @In (Syntax.term variable function constructor) t3 lt3, False *)
    intro Hin'.
(* Goal: False *)
    apply ppo_fun_in with (f := f) in Hin.
(* Goal: False *)
    generalize (PPO_trans Hin Hppo12).
(* Goal: forall _ : PPO t3 t2, False *)
    intro Hppo32.
(* Goal: False *)
    eapply IH in Hppo32; try tauto; try reflexivity.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc s) (@term_size vv ff cc (@fapply vv ff cc f lt))) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
    apply plus_lt_compat_r.
(* Goal: @eq nat (rk g) (rk f) *)
    apply in_fapply_term_size_lt; trivial.

  + inversion Hppo12 as [ aa ab ac Hin ae af | | aa t3 ac ad Hin Hppo ag ah | | | | ]; subst; try omega.

    * generalize (PPO_trans Hppo12 Hppo21).
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
      intro Hppo11.
(* Goal: False *)
      generalize Hppo11.
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
      intro Hppo11'.
      apply IH with (m := term_size (fapply f lt) + term_size (fapply f lt)) in Hppo11; try tauto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: @eq nat (rk g) (rk f) *)
      apply in_capply_term_size_lt; trivial.

    * generalize Hin.
(* Goal: forall _ : @In (Syntax.term variable function constructor) t3 lt3, False *)
      intro Hin'.
(* Goal: False *)
      apply ppo_constr_in with (c := c3) in Hin.
(* Goal: False *)
      generalize (PPO_trans Hin Hppo21).
(* Goal: forall _ : PPO t3 (@fapply variable function constructor f lt), False *)
      intro Hppo31.
      apply IH with (m := term_size (fapply f lt) + term_size t3)in Hppo31;
       try tauto; try ring.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: @eq nat (rk g) (rk f) *)
      apply in_capply_term_size_lt; trivial.

  + inversion Hppo12 as [ | aa ab ac Hin ae af | | aa t3 ac ad Hin Hppo ag ah | | | ]; subst; try omega.

    * generalize (PPO_trans Hppo12 Hppo21).
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
      intro Hppo11.
(* Goal: False *)
      generalize Hppo11.
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
      intro Hppo11'.
      apply IH with (m := term_size (fapply f lt) + term_size (fapply f lt)) in Hppo11; try tauto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: @eq nat (rk g) (rk f) *)
      apply in_fapply_term_size_lt; trivial.

    * generalize Hin.
(* Goal: forall _ : @In (Syntax.term variable function constructor) t3 lt3, False *)
      intro Hin'.
(* Goal: False *)
      apply ppo_fun_in with (f := f3) in Hin.
(* Goal: False *)
      generalize (PPO_trans Hin Hppo21).
(* Goal: forall _ : PPO t3 (@fapply variable function constructor f lt), False *)
      intro Hppo31.
      apply IH with (m := term_size (fapply f lt) + term_size t3)in Hppo31;
       try tauto; try ring.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: @eq nat (rk g) (rk f) *)
      apply in_fapply_term_size_lt; trivial.

  + inversion Hppo12 as [ | aa ab ac Hin ae af | | aa t3 ac ad Hin Hppo ag ah | | | aa ab ac ad Hrank' Hprodrev ag ah ];
(* Goal: @eq nat (S (@length (term vv ff cc) l)) (S (@length (term vv ff cc) l')) *)
    subst; try omega.

    * generalize (PPO_trans Hppo12 Hppo21).
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
      intro Hppo11.
(* Goal: False *)
      generalize Hppo11.
(* Goal: forall _ : PPO (@fapply variable function constructor f lt) (@fapply variable function constructor f lt), False *)
      intro Hppo11'.
      apply IH with (m := term_size (fapply f lt) + term_size (fapply f lt)) in Hppo11; try tauto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: @eq nat (rk g) (rk f) *)
      apply in_fapply_term_size_lt; trivial.

    * generalize Hin.
(* Goal: forall _ : @In (Syntax.term variable function constructor) t3 lt3, False *)
      intro Hin'.
(* Goal: False *)
      apply ppo_fun_in with (f := f3) in Hin.
(* Goal: False *)
      generalize (PPO_trans Hin Hppo21).
(* Goal: forall _ : PPO t3 (@fapply variable function constructor f lt), False *)
      intro Hppo31.
      apply IH with (m := term_size (fapply f lt) + term_size t3)in Hppo31;
       try tauto; try ring.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc t0)) (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      apply plus_lt_compat_l.
(* Goal: @eq nat (rk g) (rk f) *)
      apply in_fapply_term_size_lt; trivial.

    * set (term_default := fapply f [] : term).
(* Goal: False *)
    apply product_Exists2, (Exists2_exists term_default) in Hprod.
(* Goal: False *)
      destruct Hprod as ( i & Hlen & Hppoi ).
(* Goal: False *)
      assert (Hlen' : i < length lt).
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      { apply product_length in Hprodrev.
(* Goal: Peano.lt i (@length (Syntax.term variable function constructor) lt) *)
        congruence.
      }
(* Goal: False *)
      apply product_Forall2 in Hprodrev.
(* Goal: @eq nat (rk g) (rk f) *)
      apply (Forall2_forall term_default) with (i := i) in Hprodrev; trivial.
(* Goal: False *)
      rename Hprodrev into Hppoeqi.

(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      { destruct Hppoeqi as [ Hpporevi | Hppoeqi ].

        - apply IH with (m := term_size (nth i lt3 term_default) + term_size (nth i lt term_default)) in Hppoi; trivial; try tauto.
(* Goal: Peano.lt (Init.Nat.add (@term_size variable function constructor (@nth (Syntax.term variable function constructor) i lt3 term_default)) (@term_size variable function constructor (@nth (Syntax.term variable function constructor) i lt term_default))) (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f lt)) (@term_size variable function constructor (@fapply variable function constructor f3 lt3))) *)
          rewrite plus_comm.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
          apply plus_lt_compat.

          + apply in_fapply_term_size_lt; trivial.
(* Goal: @eq nat (rk g) (rk f) *)
            apply nth_In; trivial.

          + apply in_fapply_term_size_lt; trivial.
(* Goal: @eq nat (rk g) (rk f) *)
            apply nth_In; trivial.

        - generalize Hppoi; intros Hppoibis.
          apply IH with (m := term_size (nth i lt3 term_default) + term_size (nth i lt term_default)) in Hppoi; trivial.

          + rewrite Hppoeqi in Hppoi, Hppoibis.
(* Goal: False *)
            tauto.

          + rewrite plus_comm.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
            apply plus_lt_compat.

            * apply in_fapply_term_size_lt; trivial.
(* Goal: @eq nat (rk g) (rk f) *)
              apply nth_In; trivial.

            * apply in_fapply_term_size_lt; trivial.
(* Goal: @eq nat (rk g) (rk f) *)
              apply nth_In; trivial.
      }
Qed.

Lemma PPO_irrefl t : ~PPO t t.
Proof.
(* Goal: not (PPO t t) *)
intro Hppo.
(* Goal: False *)
generalize Hppo.
(* Goal: forall _ : PPO t t, False *)
intro Hppo'.
(* Goal: False *)
apply PPO_asym in Hppo.
(* Goal: False *)
tauto.
Qed.

Lemma PPO_term_pattern_subst p t s :
  PPO t (@term_from_pattern _ _ _ p) ->
  PPO (subst s t) (@term_from_value _ _ _ (psubst s p)).
Proof.
(* Goal: forall _ : PPO t (@term_from_pattern variable function constructor p), PPO (@subst variable function constructor s t) (@term_from_value variable function constructor (@psubst variable constructor s p)) *)
  revert t s.
  induction p as [ v | c lp IH ] using pattern_ind2;
    intros t s Hppo;
    [ solve [inversion Hppo] | idtac ].
(* Goal: @eq nat (rk f0) (rk' f0) *)
  inversion Hppo as [ aa ab ac Hin ae af | | aa t' ac ad Hin Hppo' ag ah | | | | ]; subst.

  - (* ppo_constr_in *)
(* Goal: PPO t (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
    rewrite in_map_iff in Hin.
(* Goal: PPO (@subst variable function constructor s (@fapply variable function constructor g lt)) (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
    destruct Hin as (p & Heq & Hin).
(* Goal: PPO t (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
    subst t.
(* Goal: PPO (@subst variable function constructor s (@term_from_pattern variable function constructor p)) (@term_from_value variable function constructor (@psubst variable constructor s (@p_capply variable constructor c lp))) *)
    apply ppo_constr_in.
(* Goal: @In (Syntax.term variable function constructor) (@subst variable function constructor s (@term_from_pattern variable function constructor p)) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (fix term_from_value (v : Syntax.value constructor) : Syntax.term variable function constructor := match v with | c_capply c lc => @capply variable function constructor c (@map (Syntax.value constructor) (Syntax.term variable function constructor) term_from_value lc) end) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) ((fix psubst (s : forall _ : variable, Syntax.value constructor) (p : Syntax.pattern variable constructor) {struct p} : Syntax.value constructor := match p with | p_var x => s x | p_capply c lp => @c_capply constructor c (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (psubst s) lp) end) s) lp)) *)
    rewrite in_map_iff.
(* Goal: @ex (Syntax.value constructor) (fun v : Syntax.value constructor => @eq (Syntax.term variable function constructor) t (@term_from_value variable function constructor v)) *)
    exists (psubst s p).
(* Goal: and (@eq (Syntax.term variable function constructor) ((fix term_from_value (v : Syntax.value constructor) : Syntax.term variable function constructor := match v with | c_capply c lc => @capply variable function constructor c (@map (Syntax.value constructor) (Syntax.term variable function constructor) term_from_value lc) end) (@psubst variable constructor s p)) (@subst variable function constructor s (@term_from_pattern variable function constructor p))) (@In (Syntax.value constructor) (@psubst variable constructor s p) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) ((fix psubst (s : forall _ : variable, Syntax.value constructor) (p : Syntax.pattern variable constructor) {struct p} : Syntax.value constructor := match p with | p_var x => s x | p_capply c lp => @c_capply constructor c (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (psubst s) lp) end) s) lp)) *)
    split.

    + symmetry.
(* Goal: @eq nat (rk f0) (rk' f0) *)
      apply subst_psubst.

    + apply in_map.
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
      assumption.

  - (* ppo_constr_sub *)
(* Goal: PPO t (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
    rewrite in_map_iff in Hin.
(* Goal: PPO (@subst variable function constructor s (@fapply variable function constructor g lt)) (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
    destruct Hin as (p & Heq & Hin).
(* Goal: PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f lv) *)
    subst t'.
(* Goal: PPO (@subst variable function constructor s t) (@term_from_value variable function constructor (@psubst variable constructor s (@p_capply variable constructor c lp))) *)
    apply ppo_constr_sub with (t := @term_from_value _ _ _ (psubst s p)).

    + do 2 apply in_map; assumption.

    + apply IH; assumption.
Qed.

Lemma fapply_not_PPO_value f lt v :
  term_value v -> ~ PPO (fapply f lt) v.
Proof.
(* Goal: not (PPO (@fapply variable function constructor f lt) (@term_from_pattern variable function constructor p)) *)
  revert f lt.
(* Goal: False *)
  induction v as [ | c lv IH | f' lt' ] using term_ind2; intros f lt Hval Hppo; simpl in Hval; try tauto.
  rewrite <- forall_andl in Hval; rewrite Forall_forall in Hval.
(* Goal: @eq nat (rk f0) (rk' f0) *)
  inversion Hppo as [ Ba Bb Bc Hin Be Bf | | Ba v Bc Bd Hin Hpposub Bg Bh | | | | ]; subst.
  - apply Hval in Hin.
(* Goal: @clos_refl (Syntax.term variable function constructor) PPO t (@fapply variable function constructor f lt') *)
    simpl in Hin.
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
    assumption.
  - apply IH in Hpposub; trivial.
(* Goal: @term_value variable function constructor v *)
    apply Hval.
(* Goal: @eq nat (rk g) (rk f) *)
    trivial.
Qed.

Lemma fapply_not_PPO_pattern f lt p :
  ~ PPO (fapply f lt) (@term_from_pattern _ _ _ p).
Proof.
(* Goal: not (PPO (@fapply variable function constructor f lt) (@term_from_pattern variable function constructor p)) *)
  revert f lt.
  induction p as [ v | c lp IH ] using pattern_ind2;
    intros f lt Hppo;
    [ solve [ inversion Hppo ] | idtac ].
(* Goal: @eq nat (rk f0) (rk' f0) *)
  inversion Hppo as [ aa ab ac Hin ae af | | aa t ac ad Hin Hppo' ag ah | | | | ]; subst.

  - rewrite in_map_iff in Hin.
(* Goal: False *)
    destruct Hin as ( p & Heq & _ ).
(* Goal: False *)
    destruct p; discriminate Heq.

  - rewrite in_map_iff in Hin.
(* Goal: PPO (@subst variable function constructor s (@fapply variable function constructor g lt)) (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
    destruct Hin as ( p & Heq & Hin ).
(* Goal: PPO t (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
    subst t.
(* Goal: False *)
    revert Hppo'.
(* Goal: @Forall2 (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@clos_refl (Syntax.term variable function constructor) PPO) ((fix map (l : list (Syntax.term variable function constructor)) : list (Syntax.term variable function constructor) := match l with | nil => @nil (Syntax.term variable function constructor) | cons a t => @cons (Syntax.term variable function constructor) (@subst variable function constructor s a) (map t) end) lt) ((fix map (l : list (Syntax.value constructor)) : list (Syntax.term variable function constructor) := match l with | nil => @nil (Syntax.term variable function constructor) | cons a t => @cons (Syntax.term variable function constructor) (@term_from_value variable function constructor a) (map t) end) ((fix map (l : list (Syntax.pattern variable constructor)) : list (Syntax.value constructor) := match l with | nil => @nil (Syntax.value constructor) | cons a t => @cons (Syntax.value constructor) (@psubst variable constructor s a) (map t) end) lp)) *)
    apply IH.
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
    assumption.
Qed.

Lemma PPO_rule_PPO_instance s f lp t :
  PPO_rule (rule_intro f lp t) ->
  PPO (subst s t) (fapply f (map (@term_from_value _ _ _) (map (psubst s) lp))).
Proof.
(* Goal: not (PPO t t) *)
induction t as [ x | c lt IH | g lt IH ] using term_ind2; intro Hppo.

- apply value_PPO_function.

- apply ppo_constr_split.
(* Goal: forall (s0 : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) s0 (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) ((fix subst (s : forall _ : variable, Syntax.value constructor) (t : Syntax.term variable function constructor) {struct t} : Syntax.term variable function constructor := match t with | var x => @term_from_value variable function constructor (s x) | capply c lt => @capply variable function constructor c (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) | fapply f lt => @fapply variable function constructor f (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) end) s) lt)), PPO s0 (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
  intros t Hin.
(* Goal: PPO t (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
  rewrite in_map_iff in Hin.
(* Goal: PPO t (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
  destruct Hin as (t' & Hsubst & Hin).
(* Goal: @eq nat (rk f0) (rk' f0) *)
  fold (subst s t') in Hsubst.
(* Goal: PPO t (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
  subst t.
(* Goal: @eq nat (rk g) (rk f) *)
  apply IH; trivial.
  simpl in *.
(* Goal: @eq nat (rk g) (rk f) *)
  apply PPO_trans with (capply c lt); trivial.
(* Goal: @eq nat (rk g) (rk f) *)
  apply ppo_constr_in; trivial.

- inversion Hppo as [ | aa ab ac Hin ae af | | aa t ac ad Hin Hppo' ag ah | | aa ab ac ad Hrank Hppo' ag ah | aa ab ac ad Hrank Hproduct ag ah];
(* Goal: @eq nat (rk f0) (rk' f0) *)
   clear Hppo; subst.

  + rewrite in_map_iff in Hin.
(* Goal: PPO (@subst variable function constructor s (@fapply variable function constructor g lt)) (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
    destruct Hin as (p & Heq & Hin).
(* Goal: Peano.lt i (@length (Syntax.term variable function constructor) lt) *)
    destruct p; simpl in Heq; congruence.

  + rewrite in_map_iff in Hin.
(* Goal: PPO (@subst variable function constructor s (@fapply variable function constructor g lt)) (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
    destruct Hin as (p & Heq & Hin).
(* Goal: PPO t (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
    subst t.
(* Goal: False *)
    exfalso; revert Hppo'.
(* Goal: forall _ : PPO (@fapply variable function constructor g lt) (@term_from_pattern variable function constructor p), False *)
    apply fapply_not_PPO_pattern.

  + apply ppo_funlt_split; trivial.
(* Goal: forall (s0 : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) s0 (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) ((fix subst (s : forall _ : variable, Syntax.value constructor) (t : Syntax.term variable function constructor) {struct t} : Syntax.term variable function constructor := match t with | var x => @term_from_value variable function constructor (s x) | capply c lt => @capply variable function constructor c (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) | fapply f lt => @fapply variable function constructor f (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) end) s) lt)), PPO s0 (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
    intros t Hin.
(* Goal: PPO t (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
    rewrite in_map_iff in Hin.
(* Goal: PPO t (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
    destruct Hin as (t' & Heq & Hin).
(* Goal: PPO t (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
    fold (subst s t') in Heq.
(* Goal: PPO t (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
    subst t.
(* Goal: @eq nat (rk g) (rk f) *)
    apply IH; trivial.
(* Goal: @eq nat (rk g) (rk f) *)
    apply Hppo'; trivial.

  + apply ppo_funeqv_split; trivial.
(* Goal: @product (Syntax.term variable function constructor) PPO (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) ((fix subst (s : forall _ : variable, Syntax.value constructor) (t : Syntax.term variable function constructor) {struct t} : Syntax.term variable function constructor := match t with | var x => @term_from_value variable function constructor (s x) | capply c lt => @capply variable function constructor c (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) | fapply f lt => @fapply variable function constructor f (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) end) s) lt) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp)) *)
    clear Hrank IH.
(* Goal: @product (Syntax.term variable function constructor) PPO (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) ((fix subst (s : forall _ : variable, Syntax.value constructor) (t : Syntax.term variable function constructor) {struct t} : Syntax.term variable function constructor := match t with | var x => @term_from_value variable function constructor (s x) | capply c lt => @capply variable function constructor c (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) | fapply f lt => @fapply variable function constructor f (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) end) s) lt) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp)) *)
    revert lp Hproduct.
(* Goal: forall (lp : list (Syntax.pattern variable constructor)) (_ : @product (Syntax.term variable function constructor) PPO lt (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (@term_from_pattern variable function constructor) lp)), @product (Syntax.term variable function constructor) PPO (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) ((fix subst (s : forall _ : variable, Syntax.value constructor) (t : Syntax.term variable function constructor) {struct t} : Syntax.term variable function constructor := match t with | var x => @term_from_value variable function constructor (s x) | capply c lt => @capply variable function constructor c (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) | fapply f lt => @fapply variable function constructor f (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) end) s) lt) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp)) *)
    induction lt as [ | t lt IH ]; intros lp Hproduct; try solve[inversion Hproduct].
(* Goal: @product (Syntax.term variable function constructor) PPO (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) ((fix subst (s : forall _ : variable, Syntax.value constructor) (t : Syntax.term variable function constructor) {struct t} : Syntax.term variable function constructor := match t with | var x => @term_from_value variable function constructor (s x) | capply c lt => @capply variable function constructor c (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) | fapply f lt => @fapply variable function constructor f (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) end) s) (@cons (Syntax.term variable function constructor) t lt)) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp)) *)
    destruct lp as [ | p lp ]; try solve[inversion Hproduct].
    inversion Hproduct as [ aa ab ac ad ae Hproduct' ag ah | aa ab ac ad Hppo Hforall ag ah ];
(* Goal: @eq nat (rk f0) (rk' f0) *)
     clear Hproduct; subst.

    * apply IH in Hproduct'.
(* Goal: @product (Syntax.term variable function constructor) PPO (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) ((fix subst (s : forall _ : variable, Syntax.value constructor) (t : Syntax.term variable function constructor) {struct t} : Syntax.term variable function constructor := match t with | var x => @term_from_value variable function constructor (s x) | capply c lt => @capply variable function constructor c (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) | fapply f lt => @fapply variable function constructor f (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) end) s) (@cons (Syntax.term variable function constructor) t lt)) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) (@cons (Syntax.pattern variable constructor) p lp))) *)
      clear IH.
(* Goal: @product (Syntax.term variable function constructor) PPO (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) ((fix subst (s : forall _ : variable, Syntax.value constructor) (t : Syntax.term variable function constructor) {struct t} : Syntax.term variable function constructor := match t with | var x => @term_from_value variable function constructor (s x) | capply c lt => @capply variable function constructor c (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) | fapply f lt => @fapply variable function constructor f (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) end) s) (@cons (Syntax.term variable function constructor) (@term_from_pattern variable function constructor p) lt)) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) (@cons (Syntax.pattern variable constructor) p lp))) *)
      apply product_conseq; trivial.
(* Goal: @eq nat (rk f0) (rk' f0) *)
      apply subst_psubst.

    * clear IH.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      { apply product_consst.

      - apply PPO_term_pattern_subst; trivial.


      - change (
          Forall2 (clos_refl PPO) (map (subst s) lt)
            (map (@term_from_value _ _ _) (map (psubst s) lp))
        ).
(* Goal: @Forall2 (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@clos_refl (Syntax.term variable function constructor) PPO) (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@subst variable function constructor s) lt) (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp)) *)
        revert lp Hforall.
        induction lt as [ | t' lt IH ]; intros lp Hforall;
         destruct lp as [ | p' lp ]; trivial; try solve[inversion Hforall].
(* Goal: @Forall2 (term vv ff cc) (term vv ff cc) (@clos_refl (term vv ff cc) (@PPO vv ff cc rk')) (@cons (term vv ff cc) x0 l) (@cons (term vv ff cc) y0 l') *)
        apply Forall2_cons.

        + inversion Hforall as [ | aa ab ac ad Hclos Hforall' ag ah ]; subst.
(* Goal: @clos_refl (Syntax.term variable function constructor) PPO (@subst variable function constructor s t') (@term_from_value variable function constructor (@psubst variable constructor s p')) *)
          destruct Hclos as [ Hppo' | Heq' ].

(* Goal: or (@PPO vv ff cc rk' x0 y0) (@eq (term vv ff cc) x0 y0) *)
          * left.
(* Goal: @eq nat (rk f0) (rk' f0) *)
            apply PPO_term_pattern_subst.
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
            assumption.

(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
          * right.
(* Goal: PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f lv) *)
            subst t'.
(* Goal: @eq nat (rk f0) (rk' f0) *)
            apply subst_psubst.

        + apply IH.
(* Goal: @eq nat (rk g) (rk f) *)
          inversion Hforall; trivial.
      }
Qed.

Lemma PPO_rule_instance i s p c1 t c2 v :
  PPO_prog ->
  wf (cbv_update i s p c1 t c2 v) ->
  PPO (proj_left p) t.
Proof.
(* Goal: forall (_ : PPO_prog) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity (@cbv_update variable function constructor i s p c1 t c2 v)), PPO (@proj_left variable function constructor p) t *)
  simpl; intros Hppoprog Hwf.
(* Goal: False *)
  destruct t; try tauto.
(* Goal: PPO (@proj_left variable function constructor p) (@fapply variable function constructor f l) *)
  destruct Hwf as (_ & lp & t & Hi & Hrule & Heqlt & Heqp_l & _).
(* Goal: PPO (@proj_left variable function constructor p) (@fapply variable function constructor f l) *)
  rewrite Heqp_l; rewrite Heqlt.
(* Goal: PPO (@subst variable function constructor s t) (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
  apply PPO_rule_PPO_instance.
(* Goal: PPO_rule (@rule_intro variable function constructor f lp t) *)
  apply Hppoprog.
  rewrite <- Hrule.
(* Goal: @In (Syntax.rule variable function constructor) (@nth (Syntax.rule variable function constructor) i prog rule_default) prog *)
  apply nth_In.
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
  assumption.
Qed.

Definition activation_rank (p : cbv) : nat :=
  match p with
  | cbv_update _ _ _ _ (fapply f _) _ _ => rank f
  | _                                   => 0
  end.

Lemma fapplies_rec_PPO t t': In t (fapplies_in_term t') -> clos_refl PPO t t'.
Proof.
(* Goal: forall (_ : PPO t v) (_ : @term_value variable function constructor v), @term_value variable function constructor t *)
  revert t.
(* Goal: forall (s0 : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) s0 (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) ((fix subst (s : forall _ : variable, Syntax.value constructor) (t : Syntax.term variable function constructor) {struct t} : Syntax.term variable function constructor := match t with | var x => @term_from_value variable function constructor (s x) | capply c lt => @capply variable function constructor c (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) | fapply f lt => @fapply variable function constructor f (@map (Syntax.term variable function constructor) (Syntax.term variable function constructor) (subst s) lt) end) s) lt)), PPO s0 (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
  induction t' as [ | c lt' IH | f lt' IH ] using term_ind2; intros t Hin.
  - simpl in *.
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
    exfalso; assumption.
  - left.
    simpl in *.
(* Goal: PPO (@proj_left variable function constructor p') (@proj_left variable function constructor proof_tree) *)
    apply in_flat_map in Hin.
(* Goal: PPO t (@fapply variable function constructor f lt') *)
    destruct Hin as ( t' & Hint' & Hint ).
(* Goal: PPO t (@fapply variable function constructor f lt') *)
    destruct (IH t' Hint' t Hint) as [ Hppo | Heq ].
    + apply PPO_trans with (t2 := t'); trivial.
(* Goal: PPO t' (@fapply variable function constructor f lt') *)
      constructor.
(* Goal: @eq nat (rk g) (rk f) *)
      trivial.
    + subst; constructor; trivial.
  - simpl in Hin.
(* Goal: @clos_refl (Syntax.term variable function constructor) PPO t (@fapply variable function constructor f lt') *)
    destruct Hin as [ Heq | Hin ].
    + right; symmetry; trivial.
    + left.
(* Goal: PPO (@proj_left variable function constructor p') (@proj_left variable function constructor proof_tree) *)
      apply in_flat_map in Hin.

(* Goal: PPO t (@fapply variable function constructor f lt') *)
      destruct Hin as ( t' & Hint' & Hint ).
(* Goal: PPO t (@fapply variable function constructor f lt') *)
      destruct (IH t' Hint' t Hint) as [ Hppo | Heq ].
      * apply PPO_trans with (t2 := t'); trivial.
(* Goal: PPO t' (@fapply variable function constructor f lt') *)
        constructor.
(* Goal: @eq nat (rk g) (rk f) *)
        trivial.
      * subst; constructor; trivial.
Qed.

Lemma PPO_value_is_value t v : PPO t v -> term_value v -> term_value t.
Proof.
(* Goal: forall (_ : PPO t v) (_ : @term_value variable function constructor v), @term_value variable function constructor t *)
  revert t.
  induction v as [ | c lv IH | ] using term_ind2; intros t Hppo Hvalv;
  [ inversion Hppo | idtac | inversion Hvalv ].
(* Goal: @eq nat (rk f0) (rk' f0) *)
  inversion Hppo as [ Ba Bb Bc Hin Be Bf | | Ba s Bc Bd Hin Hppos Bg Bh | | | | ]; subst.

  - simpl in Hvalv.
(* Goal: @eq nat (rk g) (rk f) *)
    apply andl_in with (l := map (@term_value _ _ _) lv); trivial.
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
    apply in_map; assumption.

  - apply IH with (t := s); trivial.
(* Goal: @term_value variable function constructor s *)
    simpl in Hvalv.
(* Goal: @eq nat (rk g) (rk f) *)
    apply andl_in with (l := map (@term_value _ _ _) lv); trivial.
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
    apply in_map; assumption.
Qed.

Lemma PPO_activation_le_rank f1 lt1 f2 lv2 :
  PPO (fapply f1 lt1) (fapply f2 (map (@term_from_value _ _ _) lv2)) -> rank f1 <= rank f2.
Proof.
  remember (term_size (fapply f1 lt1) + term_size (fapply f2 (map (@term_from_value variable function constructor) lv2))) as whole_size eqn: Hsize.
  revert f1 lt1 f2 lv2 Hsize.
(* Goal: forall (t s : term vv ff cc) (_ : @eq nat whole_size (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s))) (_ : forall (f : ff) (_ : @In ff f (@functions_of_term vv ff cc t)), @eq nat (rk f) (rk' f)) (_ : forall (f : ff) (_ : @In ff f (@functions_of_term vv ff cc s)), @eq nat (rk f) (rk' f)) (_ : @PPO vv ff cc rk t s), @PPO vv ff cc rk' t s *)
  induction whole_size as [ whole_size IH ] using lt_wf_ind.
(* Goal: forall (f1 : function) (lt1 : list (Syntax.term variable function constructor)) (f2 : function) (lp2 : list (Syntax.pattern variable constructor)) (_ : @eq nat whole_size (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (@term_from_pattern variable function constructor) lp2))))) (_ : PPO (@fapply variable function constructor f1 lt1) (@fapply variable function constructor f2 (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (@term_from_pattern variable function constructor) lp2))), le (rank f1) (rank f2) *)
  intros f1 lt1 f2 lv2 Hsize Hppo.
(* Goal: @eq nat (rk f0) (rk' f0) *)
  inversion Hppo as [ | Ba Bb Bc Hin Be Bf | | Ba v Bc Bd Hin Hpposub Bh Bi | | | ]; subst.
  - (* Impossible car les lt2 sont des valeurs *)
(* Goal: le (rank f1) (rank f2) *)
    apply in_map_iff in Hin; destruct Hin as (v & Heqv & Hv).
    contradict Heqv; apply term_from_value_not_fapply.

  - apply in_map_iff in Hin; destruct Hin as (v' & Heqv' & Hv').
(* Goal: le (rank f1) (rank f2) *)
    subst v.
    contradict Hpposub; apply fapply_not_PPO_value.
    apply term_value_eqv; eauto.

  - apply lt_le_weak; assumption.
  
  - apply le_lt_or_eq_iff; right; assumption.
Qed.

Lemma PPO_pattern_le_rank f1 lt1 f2 lp2 :
  PPO (fapply f1 lt1) (fapply f2 (map (@term_from_pattern _ _ _) lp2)) -> rank f1 <= rank f2.
Proof.
  remember (term_size (fapply f1 lt1) + term_size (fapply f2 (map (@term_from_pattern variable function constructor) lp2))) as whole_size eqn: Hsize.
(* Goal: forall _ : PPO (@fapply variable function constructor f1 lt1) (@fapply variable function constructor f2 (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (@term_from_pattern variable function constructor) lp2)), le (rank f1) (rank f2) *)
  revert f1 lt1 f2 lp2 Hsize.
(* Goal: forall (t s : term vv ff cc) (_ : @eq nat whole_size (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s))) (_ : forall (f : ff) (_ : @In ff f (@functions_of_term vv ff cc t)), @eq nat (rk f) (rk' f)) (_ : forall (f : ff) (_ : @In ff f (@functions_of_term vv ff cc s)), @eq nat (rk f) (rk' f)) (_ : @PPO vv ff cc rk t s), @PPO vv ff cc rk' t s *)
  induction whole_size as [ whole_size IH ] using lt_wf_ind.
(* Goal: forall (f1 : function) (lt1 : list (Syntax.term variable function constructor)) (f2 : function) (lp2 : list (Syntax.pattern variable constructor)) (_ : @eq nat whole_size (Init.Nat.add (@term_size variable function constructor (@fapply variable function constructor f1 lt1)) (@term_size variable function constructor (@fapply variable function constructor f2 (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (@term_from_pattern variable function constructor) lp2))))) (_ : PPO (@fapply variable function constructor f1 lt1) (@fapply variable function constructor f2 (@map (Syntax.pattern variable constructor) (Syntax.term variable function constructor) (@term_from_pattern variable function constructor) lp2))), le (rank f1) (rank f2) *)
  intros f1 lt1 f2 lv2 Hsize Hppo.
(* Goal: @eq nat (rk f0) (rk' f0) *)
  inversion Hppo as [ | Ba Bb Bc Hin Be Bf | | Ba v Bc Bd Hin Hpposub Bh Bi | | | ]; subst.
  - (* Impossible car les lt2 sont des valeurs *)
(* Goal: le (rank f1) (rank f2) *)
    apply in_map_iff in Hin; destruct Hin as (v & Heqv & Hv).
(* Goal: le (rank f1) (rank f2) *)
    contradict Heqv. apply term_from_pattern_not_fapply.

  - apply in_map_iff in Hin; destruct Hin as (v' & Heqv' & Hv').
(* Goal: le (rank f1) (rank f2) *)
    subst v.
(* Goal: forall _ : PPO (@fapply variable function constructor g lt) (@term_from_pattern variable function constructor p), False *)
    contradict Hpposub; apply fapply_not_PPO_pattern.

  - apply lt_le_weak; assumption.
  
  - apply le_lt_or_eq_iff; right; assumption.
Qed.

Lemma subfapplies_activation_le_rank i s p c1 f lt c2 v f' lt' :
  let proof_tree := cbv_update i s p c1 (fapply f lt) c2 v in
  PPO_prog -> wf proof_tree ->
  In (fapply f' lt') (fapplies_in_term (proj_left p)) ->
  rank f' <= rank f.
Proof.
(* Goal: let proof_tree := @cbv_update variable function constructor i s p c1 (@fapply variable function constructor f lt) c2 v in forall (_ : PPO_prog) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity proof_tree) (_ : @In (Syntax.term variable function constructor) (@fapply variable function constructor f' lt') (@fapplies_in_term variable function constructor (@proj_left variable function constructor p))), le (rank f') (rank f) *)
  intros proof_tree Hppoprog Hwf Hin.
(* Goal: le (rank f') (rank f) *)
  assert (PPO (fapply f' lt') (fapply f lt)) as Hppo.
  - apply PPO_trans_eq with (t2 := proj_left p).
    + apply fapplies_rec_PPO.
(* Goal: @eq nat (rk g) (rk f) *)
      trivial.
    + apply (PPO_rule_instance i s p c1 (fapply f lt) c2 v); assumption.

  - assert (Hltval : Forall (@term_value _ _ _) lt).
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
    {
(* Goal: @Forall (Syntax.term variable function constructor) (@term_value variable function constructor) lt *)
      destruct Hwf as (_ & lp & _ & _ & _ & Heqlt & _ & _ & _ & _ & _ & _ & _).
(* Goal: @Forall (Syntax.term variable function constructor) (@term_value variable function constructor) lt *)
      clear i p c1 f c2 v f' lt' proof_tree Hppoprog Hin Hppo.
      revert lp Heqlt;
        induction lt as [ | t lt IH ]; intros lp Heqlt;
        constructor;
        rewrite map_map in Heqlt;
        destruct lp as [ | p lp ]; [ discriminate | idtac | discriminate | idtac ].

      - rewrite term_value_eqv.
(* Goal: @ex (Syntax.value constructor) (fun v : Syntax.value constructor => @eq (Syntax.term variable function constructor) t (@term_from_value variable function constructor v)) *)
        exists (psubst s p).
(* Goal: @eq (Syntax.term variable function constructor) t (@term_from_value variable function constructor (@psubst variable constructor s p)) *)
        injection Heqlt.
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
        intros; assumption.

      - apply IH with (lp := lp).
(* Goal: @eq (list (Syntax.term variable function constructor)) lt (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp)) *)
        rewrite map_map.
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
        injection Heqlt; intros; assumption.
    }

(* Goal: le (rank f') (rank f) *)
    clear i s p c1 c2 v proof_tree Hppoprog Hwf Hin.
(* Goal: @eq nat (rk f0) (rk' f0) *)
    inversion Hppo as [ | | | Ba t Bc Bd Hin Hppot Bg Bh | | | ]; subst.

    + (* ppo_fun_in : absurde *)
(* Goal: le (rank f') (rank f) *)
      assert (Himp : term_value (fapply f' lt')).
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      { apply Forall_In_l with (xs := lt); assumption. }
(* Goal: le (rank f') (rank f) *)
      inversion Himp.

    + (* ppo_fun_sub : absurde *)
(* Goal: @Forall (Syntax.term variable function constructor) (@term_value variable function constructor) lt *)
      exfalso.
(* Goal: False *)
      generalize Hppot.
(* Goal: forall _ : PPO (@fapply variable function constructor f' lt) v, False *)
      apply fapply_not_PPO_value.
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
      apply Forall_In_l with (xs := lt); assumption.

    + (* ppo_funlt_split *)
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
      apply lt_le_weak; assumption.

    + (* ppo_funeqv_split *)
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
      apply Nat.eq_le_incl; assumption.
Qed.

Lemma le_rank_first_activation i s p c1 t c2 v p' :
  let proof_tree := cbv_update i s p c1 t c2 v in
  PPO_prog -> wf proof_tree ->
  In p' (first_activations proof_tree) ->
  activation_rank p' <= activation_rank proof_tree.
Proof.
(* Goal: let proof_tree := @cbv_update variable function constructor i s p c1 t c2 v in forall (_ : PPO_prog) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity proof_tree) (_ : @In (CBV_cache.cbv variable function constructor) p' (@first_activations variable function constructor proof_tree)), le (activation_rank p') (activation_rank proof_tree) *)
  intros proof_tree Hppoprog Hwf Hinfst.
(* Goal: le (activation_rank p') (activation_rank proof_tree) *)
  apply incl_first_activations_semi in Hinfst.
(* Goal: le (activation_rank p') (activation_rank proof_tree) *)
  generalize Hwf; intros Hfor2.
(* Goal: @eq nat (rk g) (rk f) *)
  apply first_activations_residues_activation in Hfor2; trivial.
(* Goal: @eq nat (rk g) (rk f) *)
  apply Forall2_In_l with (x:= p') in Hfor2 as (t' & Hinfapp & Hfor2); trivial.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
  assert (exists f' lt', t' = fapply f' lt') as (f' & lt' & Heqt'). {
    apply fapplies_in_term_are_fapplies with (t2 := proj_left p);
(* Goal: False *)
    tauto.
  }
(* Goal: le (activation_rank p') (activation_rank proof_tree) *)
  transitivity (rank f').
  - subst.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
    assert (wf p') as Hwfp'. {
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
      apply wf_InCBV_wf with (proof_tree := proof_tree); try assumption.
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
        apply InCBV_In_sub_trees, first_activations_and_semi_incl_sub_trees; assumption.
    }
(* Goal: le (activation_rank p') (rank f') *)
    destruct p' as [ | | i' s' p'' c1' t'' c2' v'' | ] ; simpl; try apply le_0_n.
    simpl in *.
(* Goal: False *)
    destruct t''; try tauto.
(* Goal: le (rank f) (rank f') *)
    destruct Hfor2 as [ Heqf _ ].
(* Goal: le (rank f) (rank f') *)
    subst; auto.
  - subst t'.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
    simpl.
(* Goal: le (rank f') match t with | var v => O | capply c l => O | fapply f l => rank f end *)
    generalize Hwf; intros Hwf'; simpl in Hwf'.
(* Goal: False *)
    destruct t as [ | | f lt ]; try tauto.
(* Goal: False *)
    apply (@subfapplies_activation_le_rank i s p c1 f lt c2 v f' lt'); tauto.
Qed.

Lemma PPO_first_activations i s p c1 t c2 v p' :
  let proof_tree := cbv_update i s p c1 t c2 v in
  PPO_prog -> wf proof_tree ->
  In p' (first_activations proof_tree) ->
  PPO (proj_left p') (proj_left proof_tree).
Proof.
(* Goal: let proof_tree := @cbv_update variable function constructor i s p c1 t c2 v in forall (_ : PPO_prog) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity proof_tree) (_ : @In (CBV_cache.cbv variable function constructor) p' (@first_activations variable function constructor proof_tree)), PPO (@proj_left variable function constructor p') (@proj_left variable function constructor proof_tree) *)
  intros proof_tree.
(* Goal: forall (_ : PPO_prog) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity proof_tree) (_ : @In (CBV_cache.cbv variable function constructor) p' (@first_activations variable function constructor proof_tree)), PPO (@proj_left variable function constructor p') (@proj_left variable function constructor proof_tree) *)
  unfold proof_tree.
(* Goal: forall (_ : PPO_prog) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity (@cbv_update variable function constructor i s p c1 t c2 v)) (_ : @In (CBV_cache.cbv variable function constructor) p' (@first_activations variable function constructor (@cbv_update variable function constructor i s p c1 t c2 v))), PPO (@proj_left variable function constructor p') (@proj_left variable function constructor (@cbv_update variable function constructor i s p c1 t c2 v)) *)
  intros H_ppo H_wf H_p'.
(* Goal: PPO (@proj_left variable function constructor p') (@proj_left variable function constructor (@cbv_update variable function constructor i s p c1 t c2 v)) *)
  destruct t as [ | | f lv ]; try (simpl in H_wf; tauto).
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
  simpl.
(* Goal: PPO (@proj_left variable function constructor p') (@fapply variable function constructor f lv) *)
  generalize H_p'.
(* Goal: @eq nat (rk g) (rk f) *)
  intros H_rank; apply le_rank_first_activation in H_rank; trivial.
(* Goal: PPO (@proj_left variable function constructor p') (@fapply variable function constructor f lv) *)
  apply le_lt_or_eq in H_rank.
(* Goal: PPO (@proj_left variable function constructor p') (@fapply variable function constructor f lv) *)
  assert ( exists f' lv', proj_left p' = fapply f' lv' ) as H_p'_fapply.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
  { apply first_activations_incl_activations in H_p'.
(* Goal: PPO v'' (@fapply variable function constructor f lv) *)
    generalize H_p'; intros Hwfp'.
(* Goal: PPO v'' (@fapply variable function constructor f lv) *)
    apply (activations_wf H_wf) in Hwfp'.
(* Goal: @ex function (fun f' : function => @ex (list (Syntax.term variable function constructor)) (fun lv' : list (Syntax.term variable function constructor) => @eq (Syntax.term variable function constructor) (@proj_left variable function constructor p') (@fapply variable function constructor f' lv'))) *)
    apply activation_is_function in H_p'.
(* Goal: @ex function (fun f' : function => @ex (list (Syntax.term variable function constructor)) (fun lv' : list (Syntax.term variable function constructor) => @eq (Syntax.term variable function constructor) (@proj_left variable function constructor p') (@fapply variable function constructor f' lv'))) *)
    destruct H_p' as (i' & s' & p'' & c1' & t' & c2' & v' & Heqp').
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
    subst p'; simpl.
(* Goal: @ex function (fun f' : function => @ex (list (Syntax.term variable function constructor)) (fun lv' : list (Syntax.term variable function constructor) => @eq (Syntax.term variable function constructor) t' (@fapply variable function constructor f' lv'))) *)
    simpl in Hwfp'.
(* Goal: False *)
    destruct t' as [ | | f'' lt'' ] ; try tauto.
(* Goal: @eq nat (rk g) (rk f) *)
    exists f''; exists lt''; trivial.
  }

(* Goal: PPO (@proj_left variable function constructor p') (@fapply variable function constructor f lv) *)
  destruct H_p'_fapply as (f' & lv' & H_p'_fapply).
(* Goal: PPO (@proj_left variable function constructor p') (@fapply variable function constructor f lv) *)
  rewrite H_p'_fapply.

(* Goal: PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f lv) *)
  destruct H_rank as [ H_rank | H_rank ].

  - apply first_activations_incl_activations in H_p'.
    destruct p' as [ | | i' s' p'' c1' t' c2' v'| ];
      try (apply activation_is_function in H_p';
           repeat match goal with
                    | H : exists _, _ |- _ => destruct H
                  end;
           discriminate).
(* Goal: PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f lv) *)
    simpl in H_p'_fapply.
(* Goal: PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f lv) *)
    subst t'.
(* Goal: @eq nat (rk g) (rk f) *)
    apply ppo_funlt_split; trivial.
(* Goal: forall (s : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) s lv'), PPO s (@fapply variable function constructor f lv) *)
    intros v'' Hin.
(* Goal: PPO v'' (@fapply variable function constructor f lv) *)
    generalize H_p'; intros Hwfp'.
(* Goal: PPO v'' (@fapply variable function constructor f lv) *)
    apply (activations_wf H_wf) in Hwfp'.
(* Goal: PPO v'' (@fapply variable function constructor f lv) *)
    destruct Hwfp' as (_ & lp & _ & _ & _ & Heqlv' & _).
(* Goal: PPO v'' (@fapply variable function constructor f lv) *)
    subst lv'.
(* Goal: PPO v'' (@fapply variable function constructor f lv) *)
    apply in_map_iff in Hin; destruct Hin as (v''' & Heqv'' & Hin).
    rewrite <- Heqv''.
(* Goal: PPO (@term_from_value variable function constructor v''') (@fapply variable function constructor f lv) *)
    apply value_PPO_function.

  - generalize H_wf; intros Hresidues;
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
    apply first_activations_residues_activation in Hresidues; try assumption.
    generalize H_p'; intros Hin;
    apply incl_first_activations_semi in Hin.
(* Goal: PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f lv) *)
    apply Forall2_In_l with (x := p') in Hresidues; [ clear Hin | assumption ].
(* Goal: PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f lv) *)
    destruct Hresidues as (t & Hin & Hresidues).
(* Goal: PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f lv) *)
    rewrite H_p'_fapply in Hresidues.
(* Goal: False *)
    destruct t as [ | | f'' lt ]; try tauto.
(* Goal: PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f lv) *)
    destruct Hresidues as [ Heqf Hlooklt ]; subst f''.
    generalize H_p'; intros Hactp';
    apply first_activations_incl_activations in Hactp'.
    generalize Hactp'; intros Hwfp';
    apply (@activations_wf _ _ _ _ _ _ _ _ _ _ _ H_wf) in Hwfp'.
(* Goal: PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f lv) *)
    apply activation_is_function in Hactp'.
(* Goal: PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f lv) *)
    destruct Hactp' as ( i' & s' & p'' & c1' & t' & c2' & v' & Heqp' ).
(* Goal: PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f lv) *)
    subst p'.
(* Goal: PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f lv) *)
    simpl in H_p'_fapply; subst t'.
(* Goal: PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f lv) *)
    simpl in H_rank; simpl in Hlooklt.

(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
    assert (Hppofapp: PPO (fapply f' lt) (fapply f lv)). {
(* Goal: PPO (@fapply variable function constructor f' lt) (@fapply variable function constructor f lv) *)
      apply PPO_trans_eq with (t2 := proj_left p).
      - apply fapplies_rec_PPO; assumption.
      - apply (PPO_rule_instance i s p c1 (fapply f lv) c2 v); assumption.
    }

(* Goal: PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f lv) *)
    apply PPO_trans_eq with (t2 := fapply f' lt); [ idtac | assumption ].
(* Goal: @clos_refl (Syntax.term variable function constructor) PPO (@fapply variable function constructor f' lv') (@fapply variable function constructor f' lt) *)
    right; f_equal.

(* Goal: @eq (list (Syntax.term variable function constructor)) lv' lt *)
    assert (Hltval: Forall (@term_value _ _ _) lt).
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
    {
(* Goal: @Forall (Syntax.term variable function constructor) (@term_value variable function constructor) lt *)
      simpl in H_wf.
(* Goal: @Forall (Syntax.term variable function constructor) (@term_value variable function constructor) lt *)
      destruct H_wf as (_ & lp & _ & _ & _ & Hlvval & _).
(* Goal: @Forall (Syntax.term variable function constructor) (@term_value variable function constructor) lt *)
      clear i p c1 c2 v proof_tree H_ppo lv' Hin i' s' p'' c1' c2' v' H_p' Hlooklt Hwfp'.
      inversion Hppofapp as [ | Ba Bb Bc Hinval | | Ba v Bc Bd Hin Hppoval Bg Bh | | Ba Bb Bc Bd Hranklt Bf Bg Bh | Ba Bb Bc Bd Be Hprodppo Bg Bh];
(* Goal: @eq nat (rk f0) (rk' f0) *)
        subst.

      - exfalso.
(* Goal: False *)
        rewrite in_map_iff in Hinval.
(* Goal: False *)
        destruct Hinval as (v & Heq & _).
(* Goal: False *)
        destruct v; discriminate.

      - exfalso.
(* Goal: False *)
        revert Hppoval.
(* Goal: forall _ : PPO (@fapply variable function constructor f' lt) v, False *)
        apply fapply_not_PPO_value.
(* Goal: @term_value variable function constructor v *)
        apply term_value_eqv.
(* Goal: @ex (Syntax.value constructor) (fun v0 : Syntax.value constructor => @eq (Syntax.term variable function constructor) v (@term_from_value variable function constructor v0)) *)
        apply in_map_iff in Hin.
(* Goal: @ex (Syntax.value constructor) (fun v0 : Syntax.value constructor => @eq (Syntax.term variable function constructor) v (@term_from_value variable function constructor v0)) *)
        destruct Hin as (v' & Heq & _).
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
        exists v'; symmetry; assumption.

      - exfalso.
(* Goal: False *)
        rewrite H_rank in Hranklt; revert Hranklt.
(* Goal: forall _ : Peano.lt (rank f) (rank f), False *)
        apply lt_irrefl.

      - apply product_Forall2 in Hprodppo.
(* Goal: @Forall (Syntax.term variable function constructor) (@term_value variable function constructor) lt *)
        revert Hprodppo; clear; revert lp.
(* Goal: PPO t' (@fapply variable function constructor f lt') *)
        induction lt as [ | t lt IH ]; intros lp Hfor2; constructor.
        + inversion Hfor2 as [ | Ba v Bc lv Hppot Hppolt Bg Heq ]; subst.
          destruct Hppot as [ Hppot | Heqt ];
            [ (apply PPO_value_is_value with (v := v); trivial) | subst t ];
            ( destruct lp as [ | p lp ]; simpl in Heq; [ discriminate | idtac ];
              injection Heq; intros _ Heqv;
              apply term_value_eqv;
              exists (psubst s p); assumption ).

        + destruct lp as [ | p lp ].
          * simpl in Hfor2.
(* Goal: @Forall (Syntax.term variable function constructor) (@term_value variable function constructor) lt *)
            inversion Hfor2.
          * apply IH with (lp := lp).
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
            inversion Hfor2; assumption.
    }

(* Goal: @eq (list (Syntax.term variable function constructor)) lv' lt *)
    revert Hltval Hlooklt; clear; revert lv'.
    induction lt as [ | t lt IH ];
      intros lv Hltval Hlooklt;
      inversion Hlooklt as [ | Ba Bb Bc lv' Be Hlooklt_tl Bg Bh];
      trivial;
(* Goal: @eq nat (rk f0) (rk' f0) *)
      subst.
(* Goal: @eq (list (Syntax.term variable function constructor)) (@cons (Syntax.term variable function constructor) (@cache_lookup variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec c1' t) lv') (@cons (Syntax.term variable function constructor) t lt) *)
    f_equal.

    + inversion Hltval as [ | Ba Bb Htval ]; subst.
(* Goal: PPO t (@fapply variable function constructor f (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (Syntax.pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) lp))) *)
      apply term_value_eqv in Htval; destruct Htval; subst t.
(* Goal: @eq (Syntax.term variable function constructor) (@cache_lookup variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec c1' (@term_from_value variable function constructor x)) (@term_from_value variable function constructor x) *)
      apply cache_lookup_value.
    + apply IH; [ inversion Hltval | idtac ]; assumption.
Qed.

Lemma PPO_activations i s p c1 t c2 v p' :
  let proof_tree := cbv_update i s p c1 t c2 v in
  PPO_prog -> wf proof_tree ->
  In p' (activations proof_tree) ->
  p' = proof_tree \/ PPO (proj_left p') (proj_left proof_tree).
Proof.
(* Goal: let proof_tree := @cbv_update variable function constructor i s p c1 t c2 v in forall (_ : PPO_prog) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity proof_tree) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor proof_tree)), or (@eq (CBV_cache.cbv variable function constructor) p' proof_tree) (PPO (@proj_left variable function constructor p') (@proj_left variable function constructor proof_tree)) *)
  revert p'.
(* Goal: False *)
  apply cbv_big_induction; try tauto.
(* Goal: forall (i : nat) (s : forall _ : variable, Syntax.value constructor) (p : CBV_cache.cbv variable function constructor) (c1 : CBV_cache.cache variable function constructor) (t : Syntax.term variable function constructor) (c2 : CBV_cache.cache variable function constructor) (v : Syntax.value constructor) (_ : forall (p' : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p' (@first_activations variable function constructor (@cbv_update variable function constructor i s p c1 t c2 v))) (p'0 : CBV_cache.cbv variable function constructor), let proof_tree := p' in forall (_ : PPO_prog) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity proof_tree) (_ : @In (CBV_cache.cbv variable function constructor) p'0 (@activations variable function constructor proof_tree)), or (@eq (CBV_cache.cbv variable function constructor) p'0 proof_tree) (PPO (@proj_left variable function constructor p'0) (@proj_left variable function constructor proof_tree))) (p' : CBV_cache.cbv variable function constructor), let proof_tree := @cbv_update variable function constructor i s p c1 t c2 v in forall (_ : PPO_prog) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity proof_tree) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor proof_tree)), or (@eq (CBV_cache.cbv variable function constructor) p' proof_tree) (PPO (@proj_left variable function constructor p') (@proj_left variable function constructor proof_tree)) *)
  clear i s p c1 t c2 v.
(* Goal: forall (i : nat) (s : forall _ : variable, Syntax.value constructor) (p : CBV_cache.cbv variable function constructor) (c1 : CBV_cache.cache variable function constructor) (t : Syntax.term variable function constructor) (c2 : CBV_cache.cache variable function constructor) (v : Syntax.value constructor) (_ : forall (p' : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p' (@first_activations variable function constructor (@cbv_update variable function constructor i s p c1 t c2 v))) (p'0 : CBV_cache.cbv variable function constructor), let proof_tree := p' in forall (_ : PPO_prog) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity proof_tree) (_ : @In (CBV_cache.cbv variable function constructor) p'0 (@activations variable function constructor proof_tree)), or (@eq (CBV_cache.cbv variable function constructor) p'0 proof_tree) (PPO (@proj_left variable function constructor p'0) (@proj_left variable function constructor proof_tree))) (p' : CBV_cache.cbv variable function constructor), let proof_tree := @cbv_update variable function constructor i s p c1 t c2 v in forall (_ : PPO_prog) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity proof_tree) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor proof_tree)), or (@eq (CBV_cache.cbv variable function constructor) p' proof_tree) (PPO (@proj_left variable function constructor p') (@proj_left variable function constructor proof_tree)) *)
  intros i s p c1 t c2 v Hbig p' proof_tree Hppoprg Hwf Hin.
  unfold proof_tree in Hin;
    rewrite -> activations_first_activations in Hin.
(* Goal: or (@eq (CBV_cache.cbv variable function constructor) p' proof_tree) (PPO (@proj_left variable function constructor p') (@proj_left variable function constructor proof_tree)) *)
  apply in_inv in Hin.
(* Goal: or (@eq (CBV_cache.cbv variable function constructor) p' proof_tree) (PPO (@proj_left variable function constructor p') (@proj_left variable function constructor proof_tree)) *)
  destruct Hin as [ Heq | Hin ]; [ left; symmetry; assumption | right ].
(* Goal: PPO (@proj_left variable function constructor p') (@proj_left variable function constructor proof_tree) *)
  apply in_flat_map in Hin.
(* Goal: PPO (@proj_left variable function constructor p') (@proj_left variable function constructor proof_tree) *)
  destruct Hin as (p'' & Hinfst & Hin).
  apply PPO_trans_eq with (t2 := proj_left p'');
    [ idtac | apply PPO_first_activations; assumption ].
  assert (Hgen : p' = p'' \/ PPO (proj_left p') (proj_left p'') -> clos_refl PPO (proj_left p') (proj_left p'')).
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
  { intros H.
    destruct H as [ Heq | Hppo ];
      [ subst; right; trivial | left; assumption ].
  }
(* Goal: @clos_refl (Syntax.term variable function constructor) PPO (@proj_left variable function constructor p') (@proj_left variable function constructor p'') *)
  apply Hgen; clear Hgen.
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
  apply Hbig; try assumption.
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
  apply activations_wf with (proof_tree := proof_tree); try assumption.
(* Goal: lt i (@length (Syntax.rule variable function constructor) prog) *)
  apply first_activations_incl_activations; assumption.
Qed.

End Ordering.

Lemma same_rank_same_prod vv ff cc lt ls rk rk':
  (forall t s, In t lt -> In s ls ->
      (forall f, In f (functions_of_term t) -> rk f = rk' f) ->
      (forall f, In f (functions_of_term s) -> rk f = rk' f) ->
      PPO rk t s -> PPO rk' t s) ->
  (forall f, In f (flat_map (@functions_of_term vv ff cc) lt) -> rk f = rk' f) ->
  (forall f, In f (flat_map (@functions_of_term _ _ _) ls) -> rk f = rk' f) ->
  product (PPO rk) lt ls -> product (PPO rk') lt ls.
Proof.
(* Goal: forall (_ : @eq nat (rk f) (rk' f)) (_ : forall (g : ff) (_ : @In ff g (@functions_of_term vv ff cc t)), @eq nat (rk g) (rk' g)) (_ : @PPO vv ff cc rk t (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @PPO vv ff cc rk' t (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp)) *)
intros. assert (length lt = length ls).
- apply product_length in H2; trivial.
- revert H0 H1. induction H2; intros.
  + apply product_conseq; auto.
(* Goal: forall (_ : @eq nat (rk f) (rk' f)) (_ : forall (g : ff) (_ : @In ff g (@functions_of_term vv ff cc t)), @eq nat (rk g) (rk' g)) (_ : @PPO vv ff cc rk t (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @PPO vv ff cc rk' t (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp)) *)
    apply IHproduct; auto; intros.
    * apply H; simpl; auto.
    * apply H1. simpl. rewrite in_app_iff. auto.
    * apply H4. simpl. rewrite in_app_iff. auto.
  + apply product_consst; auto.
    * {
(* Goal: forall (_ : @eq nat (rk f) (rk' f)) (_ : forall (g : ff) (_ : @In ff g (@functions_of_term vv ff cc t)), @eq nat (rk g) (rk' g)) (_ : @PPO vv ff cc rk t (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @PPO vv ff cc rk' t (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp)) *)
        apply H; simpl; auto; intros.
        - apply H2. simpl. rewrite in_app_iff. auto.
        - apply H4. simpl. rewrite in_app_iff. auto.
      }
    * {
(* Goal: @Forall2 (term vv ff cc) (term vv ff cc) (@clos_refl (term vv ff cc) (@PPO vv ff cc rk')) (@cons (term vv ff cc) x0 l) (@cons (term vv ff cc) y0 l') *)
        induction H1; auto. apply Forall2_cons.
        - unfold clos_refl. unfold clos_refl in H1. destruct H1.
          + left. apply H; simpl; auto; intros.
            * apply H2. simpl. repeat (rewrite in_app_iff). auto.
            * apply H4. simpl. repeat (rewrite in_app_iff). auto.
(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
          + right. auto.
        - apply IHForall2; simpl; intros.
          + apply H; simpl; auto.
            * destruct H6; auto.
            * destruct H7; auto.
          + simpl in H3. omega.
          + apply H2. simpl. repeat (rewrite in_app_iff).
(* Goal: @eq nat (rk f0) (rk' f0) *)
            rewrite in_app_iff in H6. destruct H6; auto.
          + apply H4. simpl. repeat (rewrite in_app_iff).
(* Goal: @eq nat (rk f0) (rk' f0) *)
            rewrite in_app_iff in H6. destruct H6; auto.
      }
Qed.

Hint Constructors PPO.

Lemma same_rank_same_ppo vv ff cc (t : term vv ff cc) s rk rk':
  (forall f, In f (functions_of_term t) -> rk f = rk' f) ->
  (forall f, In f (functions_of_term s) -> rk f = rk' f) ->
  PPO rk t s -> PPO rk' t s.
Proof.
remember (term_size t + term_size s) as whole_size eqn: H_size.
(* Goal: forall (_ : forall (f : ff) (_ : @In ff f (@functions_of_term vv ff cc t)), @eq nat (rk f) (rk' f)) (_ : forall (f : ff) (_ : @In ff f (@functions_of_term vv ff cc s)), @eq nat (rk f) (rk' f)) (_ : @PPO vv ff cc rk t s), @PPO vv ff cc rk' t s *)
revert t s H_size.
(* Goal: forall (t s : term vv ff cc) (_ : @eq nat whole_size (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s))) (_ : forall (f : ff) (_ : @In ff f (@functions_of_term vv ff cc t)), @eq nat (rk f) (rk' f)) (_ : forall (f : ff) (_ : @In ff f (@functions_of_term vv ff cc s)), @eq nat (rk f) (rk' f)) (_ : @PPO vv ff cc rk t s), @PPO vv ff cc rk' t s *)
induction whole_size as [whole_size IH] using lt_wf_ind.
(* Goal: forall (t s : term vv ff cc) (_ : @eq nat whole_size (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s))) (_ : forall (f : ff) (_ : @In ff f (@functions_of_term vv ff cc t)), @eq nat (rk f) (rk' f)) (_ : forall (f : ff) (_ : @In ff f (@functions_of_term vv ff cc s)), @eq nat (rk f) (rk' f)) (_ : @PPO vv ff cc rk t s), @PPO vv ff cc rk' t s *)
intros t s H_size H H0 Hppo.
(* Goal: @eq nat (rk f0) (rk' f0) *)
inversion Hppo; subst.
- auto.
- auto.
- apply ppo_constr_sub with (t:=t0); auto.
  apply IH with (m:=term_size t + term_size t0); auto.
  + apply plus_lt_compat_l.
(* Goal: Peano.lt (@term_size vv ff cc t0) (@term_size vv ff cc (@fapply vv ff cc f lt)) *)
    apply (in_map (@term_size _ _ _)), in_le_suml in H1.
(* Goal: @eq nat (rk f0) (rk' f0) *)
    apply le_lt_n_Sm; auto.
  + intros. apply H0. simpl. rewrite in_flat_map.
(* Goal: @eq nat (rk f0) (rk' f0) *)
    exists t0. auto.
- apply ppo_fun_sub with (t:=t0); auto.
  apply IH with (m:=term_size t + term_size t0); auto.
  + apply plus_lt_compat_l.
(* Goal: Peano.lt (@term_size vv ff cc t0) (@term_size vv ff cc (@fapply vv ff cc f lt)) *)
    apply (in_map (@term_size _ _ _)), in_le_suml in H1.
(* Goal: @eq nat (rk f0) (rk' f0) *)
    apply le_lt_n_Sm; auto.
(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
  + intros. apply H0. simpl. right. rewrite in_flat_map.
(* Goal: @eq nat (rk f0) (rk' f0) *)
    exists t0. auto.
- apply ppo_constr_split. intros.
  apply IH with (m:=term_size s + term_size (fapply f lt)); auto.
  + apply plus_lt_compat_r.
(* Goal: Peano.lt (@term_size vv ff cc s) (@term_size vv ff cc (@capply vv ff cc c ls)) *)
    apply (in_map (@term_size _ _ _)), in_le_suml in H2.
(* Goal: @eq nat (rk f0) (rk' f0) *)
    apply le_lt_n_Sm; auto.
  + intros. apply H. simpl. rewrite in_flat_map.
(* Goal: @eq nat (rk f0) (rk' f0) *)
    exists s. auto.
- apply ppo_funlt_split.
  + replace (rk' g) with (rk g). replace (rk' f) with (rk f).
    * trivial.
    * apply H0. simpl. auto.
    * apply H. simpl. auto.
  + intros. apply IH with (m:=term_size s + term_size (fapply f lt)); auto.
    * apply plus_lt_compat_r.
(* Goal: Peano.lt (@term_size vv ff cc t) (@term_size vv ff cc (@fapply vv ff cc g ls)) *)
      apply (in_map (@term_size _ _ _)), in_le_suml in H3.
(* Goal: @eq nat (rk f0) (rk' f0) *)
      apply le_lt_n_Sm; auto.
(* Goal: or (@eq ff g f0) (@In ff f0 (@flat_map (term vv ff cc) ff (@functions_of_term vv ff cc) ls)) *)
    * intros. apply H. simpl. right. rewrite in_flat_map.
(* Goal: @eq nat (rk f0) (rk' f0) *)
      exists s. auto.
- apply ppo_funeqv_split.
  + replace (rk' g) with (rk g). replace (rk' f) with (rk f).
    * trivial.
    * apply H0. simpl. auto.
    * apply H. simpl. auto.
  + apply same_rank_same_prod with (rk:=rk); auto; intros.
    * apply IH with (m:=term_size t + term_size s); auto.
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
      {
(* Goal: Peano.lt (Init.Nat.add (@term_size vv ff cc t) (@term_size vv ff cc s)) (Init.Nat.add (@term_size vv ff cc (@fapply vv ff cc g ls)) (@term_size vv ff cc (@fapply vv ff cc f lt))) *)
        apply plus_lt_compat.
        - apply (in_map (@term_size _ _ _)), in_le_suml in H3.
(* Goal: @eq nat (rk f0) (rk' f0) *)
          apply le_lt_n_Sm; auto.
        - apply (in_map (@term_size _ _ _)), in_le_suml in H4.
(* Goal: @eq nat (rk f0) (rk' f0) *)
          apply le_lt_n_Sm; auto.
      }
    * apply H. simpl. auto.
    * apply H0. simpl. auto.
Qed.

Lemma same_rank_same_ppo_rule vv ff cc f lp (t : term vv ff cc) rk rk':
  rk f = rk' f ->
  (forall g, g ∈ (functions_of_term t) -> rk g = rk' g) ->
  PPO rk t (fapply f (map (@term_from_pattern _ _ _) lp)) ->
  PPO rk' t (fapply f (map (@term_from_pattern _ _ _) lp)).
Proof.
(* Goal: forall (_ : @eq nat (rk f) (rk' f)) (_ : forall (g : ff) (_ : @In ff g (@functions_of_term vv ff cc t)), @eq nat (rk g) (rk' g)) (_ : @PPO vv ff cc rk t (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @PPO vv ff cc rk' t (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp)) *)
intros. apply same_rank_same_ppo with (rk:=rk); auto.
(* Goal: forall _ : @In ff f0 (@functions_of_term vv ff cc (@fapply vv ff cc f (@map (pattern vv cc) (term vv ff cc) (@term_from_pattern vv ff cc) lp))), @eq nat (rk f0) (rk' f0) *)
intro. simpl. intro. destruct H2.
- subst. auto.
- rewrite no_funcs_in_patterns in H2. simpl in H2. now exfalso.
Qed.

Ltac ppo variable_eq_dec function_eq_dec constructor_eq_dec :=
match goal with
| |- PPO ?rk ?t1 ?t2 =>
    let t := eval compute in (@PPO_dec _ _ _ variable_eq_dec function_eq_dec constructor_eq_dec rk t1 t2) in
    match t with
    | left ?H => try exact H
    | _ => let t := constr:(pair t1 t2) in idtac t
    end
end.
