Require Import FunctionalExtensionality.
Require Import Arith Bool Omega Psatz Cecoa.Lib Cecoa.Syntax List Cecoa.CBV_cache Cecoa.Ordering.
Import List.ListNotations.

Section Bounds.

Variables variable function constructor : Type.

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 max_arity : nat.

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

Variable prog : list rule.
Variable rule_default : rule.
Variable subst_default : variable -> value.

Notation assoc_cache := (assoc (term_beq variable_eq_dec function_eq_dec constructor_eq_dec)).

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

Variable rank: function -> nat.

Variable max_rank : nat.

Hypothesis pos_max_rank : 0 < max_rank.

Hypothesis max_rank_is_max_rank : forall f, rank f <= max_rank.

Notation PPO_prog := (Ordering.PPO_prog prog rank).

(* Lemme pas de doublons dans les activations *)
Lemma NoDup_left_activations_cache_order i s p c1 t c2 v:
  PPO_prog ->
  wf (cbv_update i s p c1 t c2 v) ->
  NoDup (map (@proj_left _ _ _) (activations_cache_order (cbv_update i s p c1 t c2 v))).
Proof.
  intros Hppoprg Hwf;
  assert (Hgeneralized:
            forall (p: cbv),
              let act_lefts := map (@proj_left _ _ _) (activations_cache_order p) in
              wf p ->
              NoDup act_lefts /\
              (forall t, In t act_lefts -> ~ In t (map (@fst term value) (cache_left p))));
  [ idtac | apply Hgeneralized; assumption ].

  clear i s p c1 t c2 v Hwf.
(* Goal: let p := @cbv_update variable function constructor i s p0 c1 (@fapply variable function constructor f l) c2 v in @eq (list (CBV_cache.cbv variable function constructor)) (first_activations_at_given_rank rk p) (if Nat.eq_dec rk (@activation_rank variable function constructor rank p) then @cons (CBV_cache.cbv variable function constructor) p (@nil (CBV_cache.cbv variable function constructor)) else @flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) (@first_activations_rec variable function constructor p0)) *)
  intros p.

  induction p as [ lp c1 t c2 v IHlp | lp p' c1 t c2 v IHlp IHp | i s p' c1 t c2 v IHp | c t v ]
                   using cbv_ind2;
    intros act_lefts Hwf.

  - (* cbv_constr *)
    simpl; simpl in act_lefts.
    assert (Hwf' : andl (map wf lp)
                   /\ @cache_path _ _ _ variable_eq_dec function_eq_dec constructor_eq_dec c1 c2 lp = true).
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
    { simpl in Hwf.
      repeat match goal with
               | _ : match ?x with _ => _ end |- _ => destruct x; try tauto
             end.
    }
    clear t v Hwf.
    destruct Hwf' as [ Hwflp Hcachepath ].
    revert c1 c2 Hcachepath;
      induction lp as [ | p' lp' IH ];
      intros c1 c2 Hcachepath.

    + simpl in act_lefts.
      unfold act_lefts.
      split; [ solve[apply NoDup_nil] | idtac ].
      intros t' Hin_nil;
        exfalso;
        revert Hin_nil.
      apply in_nil.

    + split.

      * simpl in act_lefts;
        unfold act_lefts.

        rewrite map_app.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
        { apply NoDup_app.

          - intros t Hin.
            eapply cache_path_proj_left_in_tail_not_in_head; eauto.

          - apply cache_path_cons in Hcachepath;
            try assumption;
            destruct Hcachepath as ( Hcache1 & Hcachepath ).
            destruct Hwflp.
            eapply IH; [ idtac | assumption | exact Hcachepath ].
            intros;
              apply IHlp;
              [ apply in_cons | idtac ];
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
              assumption.

          - destruct Hwflp.
            apply IHlp; [ apply in_eq | assumption ].
        }

      * intros t.
        eapply cache_path_proj_left_not_in_init with (c2 := c2); eauto.

  - (* cbv_split *)
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
    simpl.
    simpl in Hwf, act_lefts.
    assert (Hwf' : wf p' /\ andl (map wf lp)
            /\ @cache_path _ _ _ variable_eq_dec function_eq_dec constructor_eq_dec c1 (cache_left p') lp = true).
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
    {
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
      simpl in Hwf.
      repeat match goal with
      | _ : match ?x with _ => _ end |- _ => destruct x; try tauto
      end.
    }
     clear t v Hwf.
     destruct Hwf' as ( Hwfp' & Hwflp & Hcachepath ).
     revert c1 c2 Hcachepath;
     induction lp as [ | p'' lp'' IH ];
     intros c1 c2 Hcachepath.
     + simpl in act_lefts.
        unfold act_lefts.
        repeat rewrite app_nil_r.
(* Goal: and (@In function f0 (@functions_of_prog variable function constructor prog)) (@In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor f0 sa) (all_possible_subarguments lt))) *)
       split.
       * apply IHp; assumption.

       * intros t' Hin_nil.
          replace c1 with (cache_left p') by
            (simpl in Hcachepath; apply cache_beq_eq in Hcachepath;
              symmetry; try assumption).
          apply IHp; assumption.

      + destruct Hwflp.
(* Goal: and (@In function f0 (@functions_of_prog variable function constructor prog)) (@In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor f0 sa) (all_possible_subarguments lt))) *)
         split.
        * simpl in act_lefts;
           unfold act_lefts.
           do 2 rewrite map_app.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
          { apply NoDup_app.
            - intros t Hin.
                apply cache_path_cons in Hcachepath; try assumption.
                destruct Hcachepath as ( Hcacheeq & Hcachepath ).
                rewrite in_app_iff.
                intro Hf; destruct Hf as [Hflp'' | Hfp''].
              + assert (HND : NoDup  (map (proj_left (constructor:=constructor)) (activations_cache_order p' ++ revflatten (map (activations_cache_order (constructor:=constructor)) lp'')))).
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
                {
                    eapply IH with (c1 := cache_right p''); try trivial.
                    intros; apply IHlp; auto with *.
                }
                  rewrite map_app in HND.
                  apply NoDup_app_in_l with (x := t) in HND; tauto.

              + simpl in Hcacheeq.
                  apply IH with (t := t) ( c1 := cache_right p''); try tauto.
                * intros.
                    apply IHlp; auto with *.

                * rewrite map_app, in_app_iff; tauto.

                * erewrite cache_content; eauto.
                    rewrite map_app, in_app_iff, map_map.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
                    simpl.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
                    tauto.

            - apply IHp; assumption.

            - apply NoDup_app.
              + intros x Hx.
                  eapply cache_path_proj_left_in_tail_not_in_head; eauto.
                  split; eassumption.

              + simpl in Hcachepath.
                  rewrite andb_true_iff in Hcachepath.
                  destruct Hcachepath as [Hcacheeq Hcachepath].
                  apply IH in Hcachepath; try assumption.
                * destruct Hcachepath as [HH _].
                    rewrite map_app in HH.
                    apply NoDup_split_right in HH.
                    exact HH.

                * intros.
                    apply IHlp; [right |]; assumption.

              + apply IHlp; [ left | ]; trivial.
          }

        * replace c1 with (cache_left p'') by
            (simpl in Hcachepath; rewrite andb_true_iff in Hcachepath;
            rewrite cache_beq_eq in Hcachepath; symmetry; tauto).
(* Goal: @incl (Syntax.term variable function constructor) (@filter (Syntax.term variable function constructor) (fun t : Syntax.term variable function constructor => Nat.eqb (rank f) match t with | var y => O | capply y l => O | fapply g l => rank g end) (@map (CBV_cache.cbv variable function constructor) (Syntax.term variable function constructor) (fun p : CBV_cache.cbv variable function constructor => @proj_left variable function constructor p) (@activations variable function constructor proof_tree))) (all_possible_sub_activation_same_rank f lt) *)
           intros t Ht.
           unfold act_lefts in Ht.
           rewrite map_app in Ht.
           apply in_app_iff in Ht.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
          {
             simpl in Hcachepath.
             rewrite andb_true_iff in Hcachepath;
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
             rewrite cache_beq_eq in Hcachepath; try tauto.
             destruct Hcachepath as [Heq Hcachepath]. (* utile ? *)
             destruct Ht as [Ht | Ht].
            - assert (Hnin : ~ t ∈ map (@fst _ _) (cache_left p')).
              + apply IHp; assumption.

              + intro HH; apply Hnin.
                  eapply cache_path_incl in Hcachepath; eauto.
                  assert (HC2 : cache_path variable_eq_dec function_eq_dec constructor_eq_dec (cache_left p'') (cache_right p'') [p''] = true) by
                    (simpl; rewrite andb_true_iff;
                    repeat rewrite cache_beq_eq; tauto).
                  eapply cache_path_incl in HC2; simpl; eauto.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
                  apply map_incl with (l1 :=  (cache_left p'')); try assumption.
                  eapply incl_tran; eauto.

            - simpl in Ht.
                rewrite map_app, in_app_iff in Ht.
                destruct Ht as [Ht | Ht].
              + assert (~ t ∈ map (@fst _ _) (cache_right p'')).
                * apply IH; try tauto.
                    intros; apply IHlp; [auto with * | assumption].
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
                    rewrite map_app, in_app_iff. tauto.

                * intro Hf; apply H1.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
                    apply map_incl with (l1 :=  (cache_left p'')); try assumption.
                    eapply cache_path_incl with (c1 := cache_left p'') (lp := [p'']); simpl;
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
                    try rewrite andb_true_iff, cache_beq_eq, cache_beq_eq; eauto.

              + apply IHlp; [ left | | ]; trivial.
          }

  - (* cbv_update *)
    unfold act_lefts.
(* Goal: and (@In function f0 (@functions_of_prog variable function constructor prog)) (@In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor f0 sa) (all_possible_subarguments lt))) *)
    split.
    + simpl.
       apply NoDup_cons.
      * intro Hfalse.
         apply in_map_iff in Hfalse.
         destruct Hfalse as (p0 & Hp0eq & Hp0act).
         eapply Permutation.Permutation_in in Hp0act;
           [| symmetry; apply activations_cache_order_are_activations].
         pose (proof_tree := cbv_update i s p' c1 t c2 v).
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
         apply PPO_activations with (rank := rank) (p' := p0) in Hwf; simpl; try tauto.
         destruct Hwf.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (@first_activations variable function constructor p0)) (@max_nb_rhs_functions variable function constructor prog) *)
            subst p0.
            clear Hp0eq.
            apply activations_inCBV,
                  InCBV_In_sub_trees,
                  sub_trees_size_rec_le,
                  le_not_lt in Hp0act.

            apply Hp0act.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
            simpl.
            assert (0 < value_size v) by
             (destruct v; simpl; omega).
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
            omega.

            rewrite Hp0eq in *.
(* Goal: lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
            simpl in H.
(* Goal: le (rank g) (rank f) *)
            subst.
            apply PPO_irrefl in H.
            exact H.

(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
      * simpl in Hwf.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
         destruct t; try tauto.
         destruct Hwf as (Hassoc & lp & t & _ & _ & Hl & Hpl & Hpr & Hcl & _ & Hc2 & Hwf & _).
         apply IHp; assumption.

    + simpl in *.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
      destruct t; try tauto.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
      decompose record Hwf.
      clear Hwf.
(* Goal: @incl (Syntax.term variable function constructor) (@filter (Syntax.term variable function constructor) (fun t : Syntax.term variable function constructor => Nat.eqb (rank f) match t with | var y => O | capply y l => O | fapply g l => rank g end) (@map (CBV_cache.cbv variable function constructor) (Syntax.term variable function constructor) (fun p : CBV_cache.cbv variable function constructor => @proj_left variable function constructor p) (@activations variable function constructor proof_tree))) (all_possible_sub_activation_same_rank f lt) *)
      intros t Ht.
      destruct Ht as [Ht | Ht].
      * subst t.
        apply assoc_None_not_in in H; [ | apply term_beq_eq]; assumption.

      * replace c1 with (cache_left p').
        apply IHp; assumption.

  - (* cbv_read *)
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
    unfold act_lefts; simpl.
(* Goal: and (@In function f0 (@functions_of_prog variable function constructor prog)) (@In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor f0 sa) (all_possible_subarguments lt))) *)
    split.
    + apply NoDup_nil.

    + tauto.
Qed.

Lemma NoDup_left_activations i s p c1 t c2 v:
  PPO_prog ->
  wf (cbv_update i s p c1 t c2 v) ->
  NoDup (map (@proj_left _ _ _) (activations (cbv_update i s p c1 t c2 v))).
Proof.
(* Goal: forall (_ : @Ordering.PPO_prog variable function constructor prog rank) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p), not (@In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor p)) *)
  intros HPPO Hwf.
  eapply NoDup_Permutation_NoDup. (* 8.5 : Permutation.Permutation_NoDup *)
  - apply NoDup_left_activations_cache_order.
    +  exact HPPO.

    + exact Hwf.

  - apply Permutation.Permutation_map.
    apply Permutation.Permutation_sym.
    apply activations_cache_order_are_activations.
Qed.

(* Proposition 7 *)

Definition activations_at_rank (rk: nat) (p : cbv) : list cbv :=
  filter (fun p => beq_nat rk (activation_rank rank p)) (activations p).

Lemma activations_at_rank_incl_activations (rk: nat) (p: cbv) :
  incl (activations_at_rank rk p) (activations p).
Proof.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (activations_at_rank (rank f) proof_tree)) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor proof_tree))) *)
unfold activations_at_rank.
(* Goal: @incl (CBV_cache.cbv variable function constructor) (@filter (CBV_cache.cbv variable function constructor) (fun p : CBV_cache.cbv variable function constructor => Nat.eqb rk (@activation_rank variable function constructor rank p)) (@activations variable function constructor p)) (@activations variable function constructor p) *)
apply incl_filter.
Qed.

Lemma activations_at_rank_wf (rk: nat) (p p': cbv) :
  wf p ->
  In p' (activations_at_rank rk p) ->
  wf p'.
Proof.
(* Goal: forall _ : @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 p0 c1 t c2 v), not (@In (CBV_cache.cbv variable function constructor) (@cbv_update variable function constructor i s p0 c1 t c2 v) (@activations variable function constructor p0)) *)
intros Hwf Hin.
apply activations_at_rank_incl_activations in Hin.
eapply activations_wf.
- eexact Hwf.
- assumption.
Qed.

(* Computes A_T, with a given maximal *)
Definition A_T (proof_tree: cbv) : nat :=
  maxl (map (fun p => length (activations_at_rank (activation_rank rank p) p)) (activations proof_tree)).

(* B_i, with i = rank *)
Definition activations_at_rank_bound (A_T: nat) (rank: nat) :=
  Nat.pow max_rank (max_rank - rank) *
  Nat.pow (max 1 (max_nb_rhs_functions prog)) (max_rank - rank) *
  Nat.pow A_T (S (max_rank - rank)).

Definition gary_seven_poly (A_T:nat) :=
  suml (map (activations_at_rank_bound A_T) (seq 0 (S max_rank))).

Lemma PPO_activation_rank_decreasing i s p c1 f lt c2 v:
  let proof_tree := cbv_update i s p c1 (fapply f lt) c2 v in
  PPO_prog ->
  wf proof_tree ->
  forall p, In p (activations proof_tree) ->
  activation_rank rank p <= 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 (_ : @Ordering.PPO_prog variable function constructor prog rank) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity proof_tree) (p : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p (@activations variable function constructor proof_tree)), le (@activation_rank variable function constructor rank p) (rank f) *)
  intros proof_tree HPPO Hwf p' Hp'.
  assert (p' = proof_tree \/ PPO rank (proj_left p') (proj_left proof_tree)) as H by 
         (eapply PPO_activations; eauto).
(* Goal: le (@activation_rank variable function constructor rank p') (rank f) *)
  destruct H as [H | H].
  - rewrite H; trivial.

  - simpl in H.
(* Goal: le (@activation_rank variable function constructor rank p') (rank f) *)
    apply activation_is_function in Hp'.
(* Goal: le (@activation_rank variable function constructor rank p') (rank f) *)
    destruct Hp' as (x1 & x2 & x3 & x4 & t & x6 & v0 & Hp').
(* Goal: le (@activation_rank variable function constructor rank p') (rank f) *)
    rewrite Hp'.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
    simpl.
(* Goal: le match t with | var v => O | capply c l => O | fapply f l => rank f end (rank f) *)
    destruct t; try apply le_0_n.
(* Goal: le (rank f0) (rank f) *)
    rewrite Hp' in H.
(* Goal: lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
    simpl in H.
(* Goal: @eq nat (@activation_rank variable function constructor rank p') (rank f) *)
    subst p'.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
    simpl in Hwf. 
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
    decompose record Hwf.
(* Goal: le (rank f0) (rank f) *)
    rewrite H3 in H.
(* Goal: le (rank f0) (rank f) *)
    now apply PPO_activation_le_rank in H.
Qed.

Hint Resolve lt_0_pow.

Hint Rewrite mult_1_l.

Fixpoint first_activations_at_given_rank (rk: nat) (proof_tree : cbv) : list cbv :=
  match proof_tree with
  | cbv_constr lp _ _ _ _ => flat_map (first_activations_at_given_rank rk) lp
  | cbv_split lp p _ _ _ _ => first_activations_at_given_rank rk p ++ flat_map (first_activations_at_given_rank rk) lp
  | cbv_update _ _ p _ (fapply f _) _ _ as p' => if eq_nat_dec rk (rank f)
                                                then [ p' ]
                                                else first_activations_at_given_rank rk p
  | _ => [] (* cbv_read and ill-formed cbv_update *)
  end.

Definition activation_function (function_default : function) (p: cbv) :=
  match p with
    | cbv_update _ _ _ _ (fapply f _) _ _ => f
    | _                                   => function_default
  end.

Lemma first_activations_at_given_rank_rank rk p p' :
  In p' (first_activations_at_given_rank rk p) ->
  rk = activation_rank rank p'.
Proof.
  induction p using cbv_ind2; intro Hp'; simpl in *.
  - apply in_flat_map in Hp'.
(* Goal: @eq nat rk (@activation_rank variable function constructor rank p') *)
    destruct Hp' as (p0 & Hp0in & Hp'in).
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
    apply H with p0; assumption.
  - apply in_app_iff in Hp'.
(* Goal: @eq nat rk (@activation_rank variable function constructor rank p') *)
    rewrite in_flat_map in Hp'.
(* Goal: @eq nat rk (@activation_rank variable function constructor rank p') *)
    destruct Hp' as [ Hin | (p0 & Hinp0 & Hfirst)].
    + tauto.
    + apply H with p0; assumption.
  - destruct t; try (inversion Hp').
(* Goal: or (@eq (CBV_cache.cbv variable function constructor) (@cbv_update variable function constructor n s p c1 (@fapply variable function constructor f l) c2 v) p') (@In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p)) *)
    destruct (eq_nat_dec rk (rank f)).
    + destruct Hp'.
      * subst p'.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
        assumption.
      * inversion H.
    + tauto.
  - tauto.
Qed.

Lemma first_activations_at_given_rank_sublist_activations rk p :
  sublist (first_activations_at_given_rank rk p) (activations p).
Proof.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
induction p using cbv_ind2; simpl.
- apply sublist_flatmap_in_ext; assumption.
- apply sublist_app_compat.
  + assumption.
  + apply sublist_flatmap_in_ext; assumption.
- destruct t; try tauto; try (apply sublist_nil).
(* Goal: @sublist (CBV_cache.cbv variable function constructor) (if Nat.eq_dec rk (rank f) then @cons (CBV_cache.cbv variable function constructor) (@cbv_update variable function constructor n s p c1 (@fapply variable function constructor f l) c2 v) (@nil (CBV_cache.cbv variable function constructor)) else first_activations_at_given_rank rk p) (@cons (CBV_cache.cbv variable function constructor) (@cbv_update variable function constructor n s p c1 (@fapply variable function constructor f l) c2 v) (@activations variable function constructor p)) *)
  case eq_nat_dec; intro Heq.
  + apply sublist_cons, sublist_nil.
  + apply sublist_skip. assumption.
- apply sublist_refl.
Qed.

Lemma NoDup_activations i s p c1 t c2 v : 
  PPO_prog ->
  wf (cbv_update i s p c1 t c2 v) ->
  NoDup (activations (cbv_update i s p c1 t c2 v)).
Proof.
(* Goal: forall (_ : @Ordering.PPO_prog variable function constructor prog rank) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p), not (@In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor p)) *)
intros HPPO Hwf.
eapply NoDup_map_inv.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
  apply NoDup_left_activations; assumption.
Qed.

Lemma NoDup_first_activations_at_given_rank rk i s p c1 t c2 v : 
  PPO_prog ->
  wf (cbv_update i s p c1 t c2 v) ->
  NoDup (first_activations_at_given_rank rk (cbv_update i s p c1 t c2 v)).
Proof.
(* Goal: forall (x : nat) (_ : @In nat x (@map (CBV_cache.cbv variable function constructor) nat (fun pi : CBV_cache.cbv variable function constructor => bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor pi))) (@activations variable function constructor proof_tree))), le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
intros.
eapply NoDup_sublist.
- apply first_activations_at_given_rank_sublist_activations.

- apply NoDup_activations; assumption.
Qed.

Lemma first_activations_at_given_rank_activations rk p: 
  incl (first_activations_at_given_rank rk p) (activations p).
Proof.
  induction p using cbv_ind2; intros p' Hin; simpl in *.
  - apply in_flat_map in Hin.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@activations variable function constructor) lp) *)
    destruct Hin as (p0 & Hinp0 & Hfirst).
(* Goal: @In (Syntax.term variable function constructor) t (@flat_map (Syntax.term variable function constructor) (Syntax.term variable function constructor) sub_terms lt) *)
    apply in_flat_map.
(* Goal: @ex (CBV_cache.cbv variable function constructor) (fun x : CBV_cache.cbv variable function constructor => and (@In (CBV_cache.cbv variable function constructor) x lp) (@In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor x))) *)
    exists p0.
(* Goal: and (@In function f0 (@functions_of_prog variable function constructor prog)) (@In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor f0 sa) (all_possible_subarguments lt))) *)
    split.
    + assumption.

    + apply H; assumption.

  - apply in_app_iff in Hin.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@app (CBV_cache.cbv variable function constructor) (@activations variable function constructor p) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@activations variable function constructor) lp)) *)
    rewrite in_flat_map in Hin.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@app (CBV_cache.cbv variable function constructor) (@activations variable function constructor p) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@activations variable function constructor) lp)) *)
    destruct Hin as [ Hin | (p0 & Hinp0 & Hfirst)].
    + auto with *.

    + apply in_app_iff.
(* Goal: or (@eq (Syntax.term variable function constructor) (@fapply variable function constructor f2 lt2) t1) (lt (@term_size variable function constructor t1) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) *)
      right.
(* Goal: @In (Syntax.term variable function constructor) t (@flat_map (Syntax.term variable function constructor) (Syntax.term variable function constructor) sub_terms lt) *)
      apply in_flat_map.
(* Goal: @ex (CBV_cache.cbv variable function constructor) (fun x : CBV_cache.cbv variable function constructor => and (@In (CBV_cache.cbv variable function constructor) x lp) (@In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor x))) *)
      exists p0.
(* Goal: and (@In function f0 (@functions_of_prog variable function constructor prog)) (@In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor f0 sa) (all_possible_subarguments lt))) *)
      split.
      * assumption.

      * apply H; assumption.

  - destruct t; try inversion Hin.
(* Goal: or (@eq (CBV_cache.cbv variable function constructor) (@cbv_update variable function constructor n s p c1 (@fapply variable function constructor f l) c2 v) p') (@In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p)) *)
    destruct (eq_nat_dec rk (rank f)).
    + subst.
(* Goal: or (@eq (CBV_cache.cbv variable function constructor) (@cbv_update variable function constructor n s p c1 (@fapply variable function constructor f l) c2 v) p') (@In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p)) *)
      destruct Hin.
      * tauto.

      * inversion H.

    + right.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
      auto.

  - assumption.
Qed.

Lemma A_T_activation_rank (p p' : cbv) :
  In p' (first_activations_at_given_rank (activation_rank rank p') p) ->
    length (activations_at_rank (activation_rank rank p') p') <= A_T p.
Proof.
(* Goal: not (@In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor p)) *)
  intro Hin.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (activations_at_rank (rank f) proof_tree)) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor proof_tree))) *)
  unfold activations_at_rank.
(* Goal: le (A_T proof_tree) (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
  unfold A_T.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (activations_at_rank (rank f) proof_tree)) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor proof_tree))) *)
  unfold activations_at_rank.
(* Goal: le (@nb_rhs_functions variable function constructor (@rule_intro variable function constructor f lp t)) (maxl (@map (Syntax.rule variable function constructor) nat (@nb_rhs_functions variable function constructor) prog)) *)
  apply maxl_is_max.
(* Goal: @In nat (@nb_rhs_functions variable function constructor (@rule_intro variable function constructor f lp t)) (@map (Syntax.rule variable function constructor) nat (@nb_rhs_functions variable function constructor) prog) *)
  apply in_map_iff.
(* Goal: @ex (CBV_cache.cbv variable function constructor) (fun x : CBV_cache.cbv variable function constructor => and (@eq nat (@length (CBV_cache.cbv variable function constructor) (@filter (CBV_cache.cbv variable function constructor) (fun p : CBV_cache.cbv variable function constructor => Nat.eqb (@activation_rank variable function constructor rank x) (@activation_rank variable function constructor rank p)) (@activations variable function constructor x))) (@length (CBV_cache.cbv variable function constructor) (@filter (CBV_cache.cbv variable function constructor) (fun p : CBV_cache.cbv variable function constructor => Nat.eqb (@activation_rank variable function constructor rank p') (@activation_rank variable function constructor rank p)) (@activations variable function constructor p')))) (@In (CBV_cache.cbv variable function constructor) x (@activations variable function constructor p))) *)
  exists p'.
(* Goal: and (@In function f0 (@functions_of_prog variable function constructor prog)) (@In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor f0 sa) (all_possible_subarguments lt))) *)
  split.
  - trivial.
  - apply first_activations_at_given_rank_activations in Hin.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
    assumption.
Qed.

Lemma activation_eq_dec p i s p0 c1 t c2 v:
  let proof_tree := cbv_update i s p0 c1 t c2 v in
  PPO_prog ->
  wf proof_tree ->
  In p (activations proof_tree) -> p = proof_tree \/ p <> proof_tree.
Proof.
(* Goal: let proof_tree := @cbv_update variable function constructor i s p0 c1 t c2 v in forall (_ : @Ordering.PPO_prog variable function constructor prog rank) (_ : @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) (not (@eq (CBV_cache.cbv variable function constructor) p proof_tree)) *)
intros proof_tree HPPO H1 H2.
(* Goal: or (@eq (CBV_cache.cbv variable function constructor) p proof_tree) (not (@eq (CBV_cache.cbv variable function constructor) p proof_tree)) *)
unfold proof_tree in H2.
(* Goal: or (@eq (CBV_cache.cbv variable function constructor) p proof_tree) (not (@eq (CBV_cache.cbv variable function constructor) p proof_tree)) *)
rewrite activations_first_activations in H2.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (activations_at_rank match t0 with | var v => O | capply c l => O | fapply f l => rank f end (@cbv_update variable function constructor n v1 x c t0 c4 v2))) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor (@cbv_update variable function constructor n v1 x c t0 c4 v2)))) *)
simpl in H2.
(* Goal: or (@eq (CBV_cache.cbv variable function constructor) p proof_tree) (not (@eq (CBV_cache.cbv variable function constructor) p proof_tree)) *)
destruct H2 as [ | H2]; [ subst; tauto | ].
(* Goal: or (@eq (Syntax.term variable function constructor) (@fapply variable function constructor f2 lt2) t1) (lt (@term_size variable function constructor t1) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) *)
right.
(* Goal: not (@eq (CBV_cache.cbv variable function constructor) p proof_tree) *)
intro Heq.
(* Goal: False *)
apply NoDup_app_in_l with (l := [cbv_update i s p0 c1 t c2 v]) (l' := flat_map (activations (constructor:=constructor)) (first_activations_rec p0)) (x := cbv_update i s p0 c1 t c2 v).
- simpl.
  erewrite <- activations_first_activations.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
  apply NoDup_activations; assumption.

- auto with *.

- subst; assumption.
Qed.

Lemma activations_trans p p' p'' : wf p'' ->
  In p (activations p') -> In p' (activations p'') -> In p (activations p'').
Proof.
(* Goal: forall (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p'') (_ : @In (CBV_cache.cbv variable function constructor) p (@activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p'')), @In (CBV_cache.cbv variable function constructor) p (@activations variable function constructor p'') *)
intros Hwf Hin1 Hin2.
(* Goal: @In (CBV_cache.cbv variable function constructor) p (@activations variable function constructor p'') *)
generalize Hin1.
(* Goal: forall _ : @In (CBV_cache.cbv variable function constructor) p (@activations variable function constructor p'), @In (CBV_cache.cbv variable function constructor) p (@activations variable function constructor p'') *)
intro Hin1'.
(* Goal: @In (CBV_cache.cbv variable function constructor) p (@activations variable function constructor p'') *)
apply activation_is_function in Hin1.
(* Goal: @In (CBV_cache.cbv variable function constructor) p (@activations variable function constructor p'') *)
destruct Hin1 as (i & s & p0 & c1 & t & c2 & v & Heq).
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
apply cbv_update_in_activations_InCBV with i s p0 c1 t c2 v; try tauto.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
eapply InCBV_trans; apply activations_inCBV; eauto.
Qed.

Lemma first_activation_down p i s p0 c1 t c2 v:
  let proof_tree := cbv_update i s p0 c1 t c2 v in
  PPO_prog ->
  wf proof_tree -> p <> proof_tree ->
  In p (activations proof_tree) ->
  exists p', In p' (activations proof_tree) /\ In p (first_activations p').
Proof.
intros proof_tree PPO_prog.
(* Goal: forall (p p' : CBV_cache.cbv variable function constructor) (_ : @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 p0 c1 t c2 v)) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor (@cbv_update variable function constructor i s p0 c1 t c2 v))) (_ : @In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p (first_activations_at_given_rank (@activation_rank variable function constructor rank p) (@cbv_update variable function constructor i s p0 c1 t c2 v))), lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
apply cbv_big_induction.
clear proof_tree i s c1 t c2 v.
(* Goal: forall (x : nat) (_ : @In nat x (@map (CBV_cache.cbv variable function constructor) nat (fun pi : CBV_cache.cbv variable function constructor => bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor pi))) (@activations variable function constructor proof_tree))), le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
intros.
(* Goal: or (@eq (CBV_cache.cbv variable function constructor) p proof_tree) (not (@eq (CBV_cache.cbv variable function constructor) p proof_tree)) *)
rewrite activations_first_activations in H2.
(* Goal: or (@eq (CBV_cache.cbv variable function constructor) p proof_tree) (not (@eq (CBV_cache.cbv variable function constructor) p proof_tree)) *)
destruct H2 as [ | H2]; [ subst; tauto | ].
apply in_flat_map in H2.
destruct H2 as (p' & Hin1 & Hin2).
generalize Hin2.
intro Hin2'.
edestruct activation_is_function with (p:= p'); 
  [(apply first_activations_incl_activations; exact Hin1) |] .
destruct H2 as (s' & p'0 & c1' & t' & c2' & v' & Heq).
(* Goal: @eq nat (@activation_rank variable function constructor rank p') (rank f) *)
subst p'.
assert (Hwf' : wf (cbv_update x s' p'0 c1' t' c2' v')) by
  (eapply wf_InCBV_wf; try eauto;
  apply activations_inCBV;
  apply first_activations_incl_activations;
  exact Hin1).
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
edestruct activation_eq_dec with (p:=p); eauto.
- exists (cbv_update i s p1 c1 t c2 v); simpl activations.
  split; [auto with * | subst; assumption].

- generalize Hin1.
(* Goal: forall _ : @In (CBV_cache.cbv variable function constructor) p (@activations variable function constructor p'), @In (CBV_cache.cbv variable function constructor) p (@activations variable function constructor p'') *)
  intro Hin1'.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
  apply H in Hin1'; try tauto.
  destruct Hin1' as (p'' & Hp'').
(* Goal: @ex (CBV_cache.cbv variable function constructor) (fun p'' : CBV_cache.cbv variable function constructor => and (@In (CBV_cache.cbv variable function constructor) p'' (@activations variable function constructor proof_tree)) (and (@In (CBV_cache.cbv variable function constructor) p' (@first_activations variable function constructor p'')) (lt (@activation_rank variable function constructor rank p') (@activation_rank variable function constructor rank p'')))) *)
  exists p''.
(* Goal: and (@In function f0 (@functions_of_prog variable function constructor prog)) (@In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor f0 sa) (all_possible_subarguments lt))) *)
  split.
  + eapply activations_trans.
    * assumption.

    * destruct Hp''; eauto.

    * apply first_activations_incl_activations; assumption.

  + tauto.
Qed.

Fixpoint FA_path p p' (lp : list cbv) := match lp with
 | [] => p = p'
 | h :: t => In p (first_activations h) /\ FA_path h p' t
end.

Lemma FA_path_app p p' p'' lp1 lp2 : 
  FA_path p p' lp1 /\ FA_path p' p'' lp2 -> FA_path p p'' (lp1 ++ lp2).
Proof.
(* Goal: forall _ : FA_path p p' lp, iff (@In (CBV_cache.cbv variable function constructor) p' (@first_activations variable function constructor p'')) (FA_path p p'' (@app (CBV_cache.cbv variable function constructor) lp (@cons (CBV_cache.cbv variable function constructor) p'' (@nil (CBV_cache.cbv variable function constructor))))) *)
revert p p' p''.
(* Goal: forall (p p' p'' : CBV_cache.cbv variable function constructor) (_ : and (FA_path p p' lp1) (FA_path p' p'' lp2)), FA_path p p'' (@app (CBV_cache.cbv variable function constructor) lp1 lp2) *)
induction lp1; simpl; intros p p' p'' (Heq & Hpath).
- subst; assumption.

- split; try tauto.
(* Goal: FA_path a p'' (@app (CBV_cache.cbv variable function constructor) lp1 lp2) *)
  eapply IHlp1 with p'.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
  tauto.
Qed.

Lemma FA_path_right p p' p'' lp : 
  FA_path p p' lp ->
  (In p' (first_activations p'') <->
   FA_path p p'' (lp ++ [p''])).
Proof.
(* Goal: forall _ : FA_path p p' lp, iff (@In (CBV_cache.cbv variable function constructor) p' (@first_activations variable function constructor p'')) (FA_path p p'' (@app (CBV_cache.cbv variable function constructor) lp (@cons (CBV_cache.cbv variable function constructor) p'' (@nil (CBV_cache.cbv variable function constructor))))) *)
revert p p' p''.
(* Goal: forall (p p' p'' : CBV_cache.cbv variable function constructor) (_ : FA_path p p' lp), iff (@In (CBV_cache.cbv variable function constructor) p' (@first_activations variable function constructor p'')) (FA_path p p'' (@app (CBV_cache.cbv variable function constructor) lp (@cons (CBV_cache.cbv variable function constructor) p'' (@nil (CBV_cache.cbv variable function constructor))))) *)
induction lp; intros p p' p'' Hpath; (split; [intro Hin | intro Hpath2]).
- simpl in *.
(* Goal: @eq nat (@activation_rank variable function constructor rank p') (rank f) *)
  subst p'.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
  tauto.

- simpl in *.
(* Goal: le (rank g) (rank f) *)
  subst.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
  tauto.

- simpl in *.
(* Goal: and (@In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor a)) (FA_path a p'' (@app (CBV_cache.cbv variable function constructor) lp (@cons (CBV_cache.cbv variable function constructor) p'' (@nil (CBV_cache.cbv variable function constructor))))) *)
  split; intuition.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
  apply IHlp with p'; assumption.

- simpl in *.
  rewrite <- IHlp with (p' := p') in Hpath2; tauto.
Qed.

Lemma FA_path_end p p' x lp : FA_path p p' (lp++[x]) -> x = p'.
Proof.
(* Goal: forall _ : FA_path p p' (@app (CBV_cache.cbv variable function constructor) lp (@cons (CBV_cache.cbv variable function constructor) x (@nil (CBV_cache.cbv variable function constructor)))), @eq (CBV_cache.cbv variable function constructor) x p' *)
revert p p' x.
(* Goal: forall (p p' x : CBV_cache.cbv variable function constructor) (_ : FA_path p p' (@app (CBV_cache.cbv variable function constructor) lp (@cons (CBV_cache.cbv variable function constructor) x (@nil (CBV_cache.cbv variable function constructor))))), @eq (CBV_cache.cbv variable function constructor) x p' *)
induction lp; intros p p' x Hpath.
- simpl in Hpath; tauto. 

- simpl in Hpath.
(* Goal: @eq (CBV_cache.cbv variable function constructor) x p' *)
  destruct Hpath as (Hin & Hpath).
(* Goal: @eq (CBV_cache.cbv variable function constructor) x p' *)
  apply IHlp in Hpath.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
  trivial.
Qed.

Lemma first_activations_at_given_rank_caract rk i s p0 c1 f l c2 v :
  let p := cbv_update i s p0 c1 (fapply f l) c2 v in
  first_activations_at_given_rank rk p =
  if eq_nat_dec rk (activation_rank rank p) then [p] else
    flat_map (first_activations_at_given_rank rk) (first_activations_rec p0).
Proof.
(* Goal: let p := @cbv_update variable function constructor i s p0 c1 (@fapply variable function constructor f l) c2 v in @eq (list (CBV_cache.cbv variable function constructor)) (first_activations_at_given_rank rk p) (if Nat.eq_dec rk (@activation_rank variable function constructor rank p) then @cons (CBV_cache.cbv variable function constructor) p (@nil (CBV_cache.cbv variable function constructor)) else @flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) (@first_activations_rec variable function constructor p0)) *)
intros p.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
unfold p; simpl.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
induction p0 using cbv_ind2; simpl; case eq_nat_dec; intro Heq; try omega; trivial.
- apply comp_flat_map.
(* Goal: forall (a : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) a lp), @eq (list (CBV_cache.cbv variable function constructor)) (first_activations_at_given_rank rk a) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) (@first_activations_rec variable function constructor a)) *)
  intros p' Hp'.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (first_activations_at_given_rank rk p') (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) (@first_activations_rec variable function constructor p')) *)
  apply H in Hp'.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
  case eq_nat_dec in Hp'; tauto.

- case eq_nat_dec in IHp0; try tauto.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@app (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk p0) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) lp)) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) (@app (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor p0) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor) lp))) *)
  rewrite flat_map_app, IHp0.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@app (CBV_cache.cbv variable function constructor) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) (@first_activations_rec variable function constructor p0)) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) lp)) (@app (CBV_cache.cbv variable function constructor) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) (@first_activations_rec variable function constructor p0)) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor) lp))) *)
  apply app_eq_compat_l.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) lp) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor) lp)) *)
  apply comp_flat_map.
  intros p' Hp';
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (first_activations_at_given_rank rk p') (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) (@first_activations_rec variable function constructor p')) *)
  apply H in Hp'.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
  case eq_nat_dec in Hp'; tauto.

- destruct t; try tauto.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
  case eq_nat_dec; try tauto.
(* Goal: forall _ : not (@eq nat rk (rank f0)), @eq (list (CBV_cache.cbv variable function constructor)) (first_activations_at_given_rank rk p0) (@app (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk p0) (@nil (CBV_cache.cbv variable function constructor))) *)
  intro HH; clear HH.
  auto with *.
Qed.

Lemma first_activations_at_given_rank_path p p' i s p0 c1 t c2 v :
  let proof_tree := cbv_update i s p0 c1 t c2 v in
  In p' (activations proof_tree) ->
  In p (activations p') ->
  exists lp, FA_path p p' lp.
Proof.
(* Goal: let proof_tree := @cbv_update variable function constructor i s p0 c1 t c2 v in forall (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor proof_tree)) (_ : @In (CBV_cache.cbv variable function constructor) p (@activations variable function constructor p')), @ex (list (CBV_cache.cbv variable function constructor)) (fun lp : list (CBV_cache.cbv variable function constructor) => FA_path p p' lp) *)
intro proof_tree.
(* Goal: forall (_ : @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 p0 c1 t c2 v)) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor (@cbv_update variable function constructor i s p0 c1 t c2 v))) (_ : @In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p (first_activations_at_given_rank (@activation_rank variable function constructor rank p) (@cbv_update variable function constructor i s p0 c1 t c2 v))), lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
revert p p'.
(* Goal: forall (p p' : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor proof_tree)) (_ : @In (CBV_cache.cbv variable function constructor) p (@activations variable function constructor p')), @ex (list (CBV_cache.cbv variable function constructor)) (fun lp : list (CBV_cache.cbv variable function constructor) => FA_path p p' lp) *)
unfold proof_tree.
(* Goal: forall (p p' : CBV_cache.cbv variable function constructor) (_ : @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 p0 c1 t c2 v)) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor (@cbv_update variable function constructor i s p0 c1 t c2 v))) (_ : @In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p (first_activations_at_given_rank (@activation_rank variable function constructor rank p) (@cbv_update variable function constructor i s p0 c1 t c2 v))), lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
apply cbv_big_induction.
(* Goal: forall (i : nat) (s : forall _ : variable, Syntax.value constructor) (p : CBV_cache.cbv variable function constructor) (c1 : cache variable function constructor) (t : Syntax.term variable function constructor) (c2 : 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))) (p0 p'0 : CBV_cache.cbv variable function constructor) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p') (_ : @In (CBV_cache.cbv variable function constructor) p'0 (@activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p0 (@first_activations variable function constructor p'0)) (_ : @In (CBV_cache.cbv variable function constructor) p0 (first_activations_at_given_rank (@activation_rank variable function constructor rank p0) p')), lt (@activation_rank variable function constructor rank p0) (@activation_rank variable function constructor rank p'0)) (p0 p' : CBV_cache.cbv variable function constructor) (_ : @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' (@activations variable function constructor (@cbv_update variable function constructor i s p c1 t c2 v))) (_ : @In (CBV_cache.cbv variable function constructor) p0 (@first_activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p0 (first_activations_at_given_rank (@activation_rank variable function constructor rank p0) (@cbv_update variable function constructor i s p c1 t c2 v))), lt (@activation_rank variable function constructor rank p0) (@activation_rank variable function constructor rank p') *)
clear i s p0 c1 t c2 v proof_tree.
(* Goal: forall (i : nat) (s : forall _ : variable, Syntax.value constructor) (p : CBV_cache.cbv variable function constructor) (c1 : cache variable function constructor) (t : Syntax.term variable function constructor) (c2 : 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))) (p0 p'0 : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p'0 (@activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p0 (@activations variable function constructor p'0)), @ex (list (CBV_cache.cbv variable function constructor)) (fun lp : list (CBV_cache.cbv variable function constructor) => FA_path p0 p'0 lp)) (p0 p' : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor (@cbv_update variable function constructor i s p c1 t c2 v))) (_ : @In (CBV_cache.cbv variable function constructor) p0 (@activations variable function constructor p')), @ex (list (CBV_cache.cbv variable function constructor)) (fun lp : list (CBV_cache.cbv variable function constructor) => FA_path p0 p' lp) *)
intros i s p0 c1 t c2 v Hind p' p'' Hp'' Hp'.
(* Goal: @ex (list (CBV_cache.cbv variable function constructor)) (fun lp : list (CBV_cache.cbv variable function constructor) => FA_path p' p'' lp) *)
rewrite activations_first_activations in Hp''.
(* Goal: @ex (list (CBV_cache.cbv variable function constructor)) (fun lp : list (CBV_cache.cbv variable function constructor) => FA_path p' p'' lp) *)
destruct Hp'' as [Heq | Hin].
- subst.
(* Goal: @ex (list (CBV_cache.cbv variable function constructor)) (fun lp : list (CBV_cache.cbv variable function constructor) => FA_path p' (@cbv_update variable function constructor i s p0 c1 t c2 v) lp) *)
  rewrite activations_first_activations in Hp'.
(* Goal: @ex (list (CBV_cache.cbv variable function constructor)) (fun lp : list (CBV_cache.cbv variable function constructor) => FA_path p' (@cbv_update variable function constructor i s p0 c1 t c2 v) lp) *)
  destruct Hp' as [Heq | Hin].
  + subst.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
    exists []; simpl; trivial.

  + apply in_flat_map in Hin; destruct Hin as (p'' & Hp''1 & Hp''2).
(* Goal: @ex (list (CBV_cache.cbv variable function constructor)) (fun lp : list (CBV_cache.cbv variable function constructor) => FA_path p' (@cbv_update variable function constructor i s p0 c1 t c2 v) lp) *)
     assert (Hlp : exists lp : list cbv, FA_path p' p'' lp).
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
     {
(* Goal: @ex (list (CBV_cache.cbv variable function constructor)) (fun lp : list (CBV_cache.cbv variable function constructor) => FA_path p' p'' lp) *)
       eapply (Hind p'' Hp''1).
(* Goal: @In (CBV_cache.cbv variable function constructor) p'' (@activations variable function constructor p'') *)
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p'') *)
       apply first_activations_incl_activations, activation_is_function in Hp''1.
(* Goal: @In (CBV_cache.cbv variable function constructor) p'' (@activations variable function constructor p'') *)
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p'') *)
       destruct Hp''1 as (a1 & a2 & a3 & a4 & a5 & a6 & a7 & H).
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
       subst; simpl;tauto.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
       assumption.
     }
(* Goal: @ex (list (CBV_cache.cbv variable function constructor)) (fun lp : list (CBV_cache.cbv variable function constructor) => FA_path p' (@cbv_update variable function constructor i s p0 c1 t c2 v) lp) *)
    destruct Hlp as (lp & Hlp).
    exists (lp ++ [cbv_update i s p0 c1 t c2 v]).
(* Goal: FA_path p' (@cbv_update variable function constructor i s p0 c1 t c2 v) (@app (CBV_cache.cbv variable function constructor) lp (@cons (CBV_cache.cbv variable function constructor) (@cbv_update variable function constructor i s p0 c1 t c2 v) (@nil (CBV_cache.cbv variable function constructor)))) *)
    apply FA_path_app with p''.
(* Goal: and (FA_path p' p'' lp) (FA_path p'' (@cbv_update variable function constructor i s p0 c1 t c2 v) (@cons (CBV_cache.cbv variable function constructor) (@cbv_update variable function constructor i s p0 c1 t c2 v) (@nil (CBV_cache.cbv variable function constructor)))) *)
    split; [assumption | simpl; tauto].

- apply in_flat_map in Hin.
(* Goal: @ex (list (CBV_cache.cbv variable function constructor)) (fun lp : list (CBV_cache.cbv variable function constructor) => FA_path p' p'' lp) *)
  destruct Hin as (p''' & Hp''1 & Hp''2).
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
  eapply Hind; eauto.
Qed.

Lemma FA_path_activation p p' i s p0 c1 t c2 v lp :
  let proof_tree := cbv_update i s p0 c1 t c2 v in
  wf proof_tree ->
  In p' (activations proof_tree) ->
  FA_path p p' lp -> In p (activations p').
Proof.
(* Goal: forall (_ : @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 p0 c1 t c2 v)) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor (@cbv_update variable function constructor i s p0 c1 t c2 v))) (_ : @In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p (first_activations_at_given_rank (@activation_rank variable function constructor rank p) (@cbv_update variable function constructor i s p0 c1 t c2 v))), lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
revert p p'.
(* Goal: forall p p' : CBV_cache.cbv variable function constructor, let proof_tree := @cbv_update variable function constructor i s p0 c1 t c2 v in forall (_ : @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)) (_ : FA_path p p' lp), @In (CBV_cache.cbv variable function constructor) p (@activations variable function constructor p') *)
induction lp; intros p p' proof_tree Hwf Ha Hpath.
- simpl in Hpath.
(* Goal: le (rank g) (rank f) *)
  subst.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p') *)
  apply activation_is_function in Ha.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p') *)
  destruct Ha as (ii & ss & pp & cc & tt & ccc & vv & Ha).
(* Goal: @eq (list A) (@nil A) (@nil A) *)
  subst; left; trivial.

- simpl in Hpath.
(* Goal: @In (CBV_cache.cbv variable function constructor) p (@activations variable function constructor p') *)
  apply activations_trans with a.
  + eapply activations_wf; eauto.

  + apply first_activations_incl_activations; tauto.

  + apply IHlp; tauto.
Qed.

Lemma first_activations_strict p :
  PPO_prog ->
  wf p ->
 ~ p ∈ first_activations p.
Proof.
(* Goal: forall (_ : @Ordering.PPO_prog variable function constructor prog rank) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p), not (@In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor p)) *)
intros HPPO Hwf.
(* Goal: not (@In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor p)) *)
intro Hin.
(* Goal: False *)
generalize Hin; intro Hfa.
(* Goal: False *)
apply first_activations_incl_activations, activation_is_function in Hfa.
(* Goal: False *)
destruct Hfa as (i & s & p0 & c1 & t & c2 & v & Heq); subst p.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
apply NoDup_activations in Hwf; try assumption.
(* Goal: False *)
rewrite activations_first_activations in Hwf.
(* Goal: False *)
apply In_prefix_suffix in Hin.
(* Goal: False *)
destruct Hin as (l1 & l2 & H12).
(* Goal: False *)
rewrite H12 in Hwf; clear H12.
(* Goal: False *)
rewrite flat_map_app, app_comm_cons in Hwf.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
simpl in Hwf.
(* Goal: False *)
rewrite app_comm_cons in Hwf.
(* Goal: False *)
apply NoDup_remove_2 in Hwf.
auto with *.
Qed.

Lemma first_activations_irrefl i s p0 c1 t c2 v p:
  PPO_prog ->
  wf (cbv_update i s p0 c1 t c2 v) ->
   (cbv_update i s p0 c1 t c2 v) ∈ activations p ->
   ~ In p (first_activations  (cbv_update i s p0 c1 t c2 v)).
Proof.
intros PPO_prog.
revert p.
(* Goal: forall (p p' : CBV_cache.cbv variable function constructor) (_ : @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 p0 c1 t c2 v)) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor (@cbv_update variable function constructor i s p0 c1 t c2 v))) (_ : @In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p (first_activations_at_given_rank (@activation_rank variable function constructor rank p) (@cbv_update variable function constructor i s p0 c1 t c2 v))), lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
apply cbv_big_induction.
clear i s p0 c1 t c2 v.
intros i s p0 c1 t c2 v H p Hwf Ha Hfa.
assert (Hact : In p (activations (cbv_update i s p0 c1 t c2 v)))
  by (apply first_activations_incl_activations; assumption).
apply activation_is_function in Hact.
destruct Hact as (ii & ss & pp & cc1 & tt & cc2 & vv & Heq).
(* Goal: le (rank g) (rank f) *)
subst.
(* Goal: lt (@activation_rank variable function constructor rank (@cbv_update variable function constructor i s p0 c1 (@fapply variable function constructor f l) c2 v)) (@activation_rank variable function constructor rank p') *)
rewrite activations_first_activations in Ha.
destruct Ha as [Heq | Hflat].
- rewrite Heq in Hfa; apply first_activations_strict in Hfa; assumption.

- apply in_flat_map in Hflat.
  destruct Hflat as (p' & Hin' & Ha').
(* Goal: lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
  simpl in H.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
  eapply H; try eauto.
  + apply activations_wf with (cbv_update i s p0 c1 t c2 v).
     * assumption.

     * apply first_activations_incl_activations; assumption.

  + eapply activations_trans.
    * eapply activations_wf; [apply Hwf|].
       apply activations_trans with (cbv_update ii ss pp cc1 tt cc2 vv).
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
        assumption.

(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
        apply first_activations_incl_activations; assumption.

(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
        apply first_activations_incl_activations; assumption.

    * apply first_activations_incl_activations.
      exact Hfa. 

    * assumption.
Qed.

Lemma FA_path_refl p p' lp : PPO_prog -> wf p' -> FA_path p p' lp -> In p' (activations p) -> lp = [].
Proof.
(* Goal: forall (_ : @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 p0 c1 t c2 v)) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor (@cbv_update variable function constructor i s p0 c1 t c2 v))) (_ : @In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p (first_activations_at_given_rank (@activation_rank variable function constructor rank p) (@cbv_update variable function constructor i s p0 c1 t c2 v))), lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
revert p p'.
(* Goal: forall (p p' : CBV_cache.cbv variable function constructor) (_ : @Ordering.PPO_prog variable function constructor prog rank) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p') (_ : FA_path p p' lp) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p)), @eq (list (CBV_cache.cbv variable function constructor)) lp (@nil (CBV_cache.cbv variable function constructor)) *)
induction lp; intros p p' PPO_prog Hwf Hpath Hin.
- trivial.

- simpl in Hpath.
(* Goal: @ex (CBV_cache.cbv variable function constructor) (fun p'' : CBV_cache.cbv variable function constructor => and (FA_path p p'' (@cons (CBV_cache.cbv variable function constructor) a lp1)) (FA_path p'' p' lp2)) *)
  destruct Hpath as (Hfa & Hpath).
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@cons (CBV_cache.cbv variable function constructor) a lp) (@nil (CBV_cache.cbv variable function constructor)) *)
  assert (Hnil : lp = []).
  + eapply IHlp; eauto.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor a) *)
    eapply activations_trans; [| exact Hin| apply first_activations_incl_activations; assumption].
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
    apply activations_wf with p'; try assumption.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) (Nat.eqb (rank f) (@activation_rank variable function constructor rank p')) *)
    apply activation_is_function in Hin.
(* Goal: @In (CBV_cache.cbv variable function constructor) a (@activations variable function constructor p') *)
    destruct Hin as (i & s & p0 & c1 & t & c2 & v & Heq).
(* Goal: @eq nat (@activation_rank variable function constructor rank p') (rank f) *)
    subst p'.
(* Goal: @In (CBV_cache.cbv variable function constructor) a (@activations variable function constructor (@cbv_update variable function constructor i s p0 c1 t c2 v)) *)
    eapply FA_path_activation; [ exact Hwf| left; trivial| exact Hpath].

  + subst lp.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@cons (CBV_cache.cbv variable function constructor) a (@nil (CBV_cache.cbv variable function constructor))) (@nil (CBV_cache.cbv variable function constructor)) *)
     simpl in Hpath.
(* Goal: @eq nat (@activation_rank variable function constructor rank p') (rank f) *)
     subst p'.
(* Goal: lt (@activation_rank variable function constructor rank (@cbv_update variable function constructor i s p0 c1 (@fapply variable function constructor f l) c2 v)) (@activation_rank variable function constructor rank (@cbv_update variable function constructor i s p0 c1 (@fapply variable function constructor f l) c2 v)) *)
     contradict Hfa.
(* Goal: not (@eq (CBV_cache.cbv variable function constructor) p proof_tree) *)
     generalize Hin; intro Heq.
(* Goal: not (@In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor a)) *)
     apply activation_is_function in Heq.
(* Goal: not (@In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor a)) *)
     destruct Heq as (i & s & p0 & c1 & t & c2 & v & Heq).
(* Goal: not (@In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor a)) *)
     subst a.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
     apply first_activations_irrefl; assumption.
Qed.

Lemma FA_path_app_destruct p p' lp1 lp2 : FA_path p p' (lp1 ++ lp2) ->
  exists p'', FA_path p p'' lp1 /\ FA_path p'' p' lp2.
Proof.
(* Goal: forall _ : FA_path p p' (@app (CBV_cache.cbv variable function constructor) lp1 lp2), @ex (CBV_cache.cbv variable function constructor) (fun p'' : CBV_cache.cbv variable function constructor => and (FA_path p p'' lp1) (FA_path p'' p' lp2)) *)
revert p lp2.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (lp2 : list (CBV_cache.cbv variable function constructor)) (_ : FA_path p p' (@app (CBV_cache.cbv variable function constructor) lp1 lp2)), @ex (CBV_cache.cbv variable function constructor) (fun p'' : CBV_cache.cbv variable function constructor => and (FA_path p p'' lp1) (FA_path p'' p' lp2)) *)
induction lp1; intros p lp2 Hpath.
- exists p; simpl in *; auto.

- destruct Hpath as (Hfa & Hpath).
(* Goal: @ex (CBV_cache.cbv variable function constructor) (fun p'' : CBV_cache.cbv variable function constructor => and (FA_path p p'' (@cons (CBV_cache.cbv variable function constructor) a lp1)) (FA_path p'' p' lp2)) *)
  apply IHlp1 in Hpath.
(* Goal: @ex (CBV_cache.cbv variable function constructor) (fun p'' : CBV_cache.cbv variable function constructor => and (FA_path p p'' (@cons (CBV_cache.cbv variable function constructor) a lp1)) (FA_path p'' p' lp2)) *)
  destruct Hpath as (p'' & Hp''1 & Hp''2).
(* Goal: @ex (CBV_cache.cbv variable function constructor) (fun p'' : CBV_cache.cbv variable function constructor => and (@In (CBV_cache.cbv variable function constructor) p'' (@activations variable function constructor proof_tree)) (and (@In (CBV_cache.cbv variable function constructor) p' (@first_activations variable function constructor p'')) (lt (@activation_rank variable function constructor rank p') (@activation_rank variable function constructor rank p'')))) *)
  exists p''.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
  split; simpl; auto.
Qed.

Lemma FA_path_uniqueness p i s p0 c1 t c2 v lp1 lp2 : PPO_prog -> 
  let p' := (cbv_update i s p0 c1 t c2 v) in
  wf p' ->
  FA_path p p' lp1 -> FA_path p p' lp2 -> lp1 = lp2.
Proof.
(* Goal: forall _ : @Ordering.PPO_prog variable function constructor prog rank, let p' := @cbv_update variable function constructor i s p0 c1 t c2 v in forall (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p') (_ : FA_path p p' lp1) (_ : FA_path p p' lp2), @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
revert p i s p0 c1 t c2 v lp2.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (i : nat) (s : forall _ : variable, Syntax.value constructor) (p0 : CBV_cache.cbv variable function constructor) (c1 : cache variable function constructor) (t : Syntax.term variable function constructor) (c2 : cache variable function constructor) (v : Syntax.value constructor) (lp2 : list (CBV_cache.cbv variable function constructor)) (_ : @Ordering.PPO_prog variable function constructor prog rank), let p' := @cbv_update variable function constructor i s p0 c1 t c2 v in forall (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p') (_ : FA_path p p' lp1) (_ : FA_path p p' lp2), @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
induction lp1 using rev_ind; intros p i s p0 c1 t c2 v lp2 HPPO p' Hwf Hpath1 Hpath2.
- simpl in Hpath1; subst.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@nil (CBV_cache.cbv variable function constructor)) lp2 *)
  destruct lp2.
  + trivial.

  + destruct Hpath2 as (Hin & Hpath2).
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@nil (CBV_cache.cbv variable function constructor)) (@cons (CBV_cache.cbv variable function constructor) c lp2) *)
    destruct lp2 using rev_ind.
    * intros; simpl in Hpath2; subst c.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@nil (CBV_cache.cbv variable function constructor)) (@cons (CBV_cache.cbv variable function constructor) p' (@nil (CBV_cache.cbv variable function constructor))) *)
       contradict Hin.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
       apply first_activations_strict; assumption.

(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
    * assert( Hwfc : wf c). {
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity c *)
         eapply activations_wf; [eauto|].
(* Goal: @eq (list A) (@nil A) (@nil A) *)
         eapply FA_path_activation; eauto; left; trivial.
      }
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
       assert (In c (activations c)). {
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
        eapply FA_path_activation, activation_is_function in Hpath2; try left; eauto.
(* Goal: @In (CBV_cache.cbv variable function constructor) c (@activations variable function constructor c) *)
        destruct Hpath2 as (i' & s' & p0' & c1' & t' & c2' & v' & Heq'); subst c.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
        left; trivial.
      }
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
       eapply FA_path_right with (p'' := c) in Hin; eauto.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
       apply FA_path_refl in Hin; try assumption.
       assert (H0 : length((lp2 ++ [x]) ++ [c]) = 0) by (rewrite Hin; trivial).
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@nil (CBV_cache.cbv variable function constructor)) (@cons (CBV_cache.cbv variable function constructor) c (@app (CBV_cache.cbv variable function constructor) lp2 (@cons (CBV_cache.cbv variable function constructor) x (@nil (CBV_cache.cbv variable function constructor))))) *)
       do 2 rewrite app_length in H0.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@nil (CBV_cache.cbv variable function constructor)) (@cons (CBV_cache.cbv variable function constructor) c (@app (CBV_cache.cbv variable function constructor) lp2 (@cons (CBV_cache.cbv variable function constructor) x (@nil (CBV_cache.cbv variable function constructor))))) *)
       simpl in H0.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
       omega.

- assert (Heqx : x = p') by (eapply FA_path_end; eauto).
(* Goal: le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
  subst x.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@app (CBV_cache.cbv variable function constructor) lp1 (@cons (CBV_cache.cbv variable function constructor) p' (@nil (CBV_cache.cbv variable function constructor)))) lp2 *)
  revert p Hwf Hpath2 Hpath1.
(* Goal: forall (p : CBV_cache.cbv variable function constructor) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p') (_ : FA_path p p' lp2) (_ : FA_path p p' (@app (CBV_cache.cbv variable function constructor) lp1 (@cons (CBV_cache.cbv variable function constructor) p' (@nil (CBV_cache.cbv variable function constructor))))), @eq (list (CBV_cache.cbv variable function constructor)) (@app (CBV_cache.cbv variable function constructor) lp1 (@cons (CBV_cache.cbv variable function constructor) p' (@nil (CBV_cache.cbv variable function constructor)))) lp2 *)
  destruct lp2 using rev_ind; intros p Hwf Hpath2 Hpath.
  + simpl in Hpath2; subst.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
    eapply FA_path_refl; eauto.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
    subst p'; left; trivial.

  + assert (Heqx : x = p') by (eapply FA_path_end; eauto).
(* Goal: le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
    subst x.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@app (CBV_cache.cbv variable function constructor) lp1 (@cons (CBV_cache.cbv variable function constructor) p' (@nil (CBV_cache.cbv variable function constructor)))) (@app (CBV_cache.cbv variable function constructor) lp2 (@cons (CBV_cache.cbv variable function constructor) p' (@nil (CBV_cache.cbv variable function constructor)))) *)
    apply FA_path_app_destruct in Hpath.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@app (CBV_cache.cbv variable function constructor) lp1 (@cons (CBV_cache.cbv variable function constructor) p' (@nil (CBV_cache.cbv variable function constructor)))) (@app (CBV_cache.cbv variable function constructor) lp2 (@cons (CBV_cache.cbv variable function constructor) p' (@nil (CBV_cache.cbv variable function constructor)))) *)
    apply FA_path_app_destruct in Hpath2.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@app (CBV_cache.cbv variable function constructor) lp1 (@cons (CBV_cache.cbv variable function constructor) p' (@nil (CBV_cache.cbv variable function constructor)))) (@app (CBV_cache.cbv variable function constructor) lp2 (@cons (CBV_cache.cbv variable function constructor) p' (@nil (CBV_cache.cbv variable function constructor)))) *)
    destruct Hpath as (p1 & Hp1 & Hp1').
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@app (CBV_cache.cbv variable function constructor) lp1 (@cons (CBV_cache.cbv variable function constructor) p' (@nil (CBV_cache.cbv variable function constructor)))) (@app (CBV_cache.cbv variable function constructor) lp2 (@cons (CBV_cache.cbv variable function constructor) p' (@nil (CBV_cache.cbv variable function constructor)))) *)
    destruct Hpath2 as (p2 & Hp2 & Hp2').
(* Goal: @eq (list A) (@nil A) (@nil A) *)
    replace lp1 with lp2; trivial.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp2 lp1 *)
    symmetry.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
    destruct Hp1' as (Hp1' & _).
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
    destruct Hp2' as (Hp2' & _).
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
    pose (H := In_In_list_decompose p1 p2 _ Hp1' Hp2').
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
    destruct H as [Heq | (l1 & l2 & l3 & [Hl | Hl])].
    * subst p1.
(* Goal: not (@eq (CBV_cache.cbv variable function constructor) p proof_tree) *)
      generalize Hp1'; intro Heq.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
      apply first_activations_incl_activations, activation_is_function in Heq.
      destruct Heq as  (i' & s' & p0' & c1' & t' & c2' & v' & Heq'); subst p2.
       eapply (IHlp1 p _); [trivial |
                            apply activations_wf with p', first_activations_incl_activations; trivial|
                            eauto |
(* Goal: @eq (list A) (@nil A) (@nil A) *)
                            eauto ]; trivial.
    * assert (H : NoDup (activations p')) by (apply NoDup_activations; subst p'; trivial).
(* Goal: @eq nat (@activation_rank variable function constructor rank p') (rank f) *)
       subst p'.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       rewrite activations_first_activations in H.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       rewrite Hl in H.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       repeat (rewrite flat_map_app in H; simpl in H).
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       eapply FA_path_activation in Hp1; [ | exact Hwf | apply first_activations_incl_activations; trivial].
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       eapply FA_path_activation in Hp2; [ | exact Hwf | apply first_activations_incl_activations; trivial].
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       apply in_split in Hp1; apply in_split in Hp2.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       destruct Hp1 as (ll1 & ll1' & Hll1).
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       destruct Hp2 as (ll2 & ll2' & Hll2).
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       rewrite Hll1, Hll2 in H.
       replace ((cbv_update i s p0 c1 t c2 v :: flat_map (activations (constructor:=constructor)) l1 ++
          (ll1 ++ p :: ll1') ++ flat_map (activations (constructor:=constructor)) l2 ++
          (ll2 ++ p :: ll2') ++ flat_map (activations (constructor:=constructor)) l3)) with
          ((cbv_update i s p0 c1 t c2 v :: flat_map (activations (constructor:=constructor)) l1 ++
          (ll1 ++ p :: ll1')) ++
          (flat_map (activations (constructor:=constructor)) l2 ++
          (ll2 ++ p :: ll2') ++ flat_map (activations (constructor:=constructor)) l3)) in H by
          (repeat rewrite app_assoc; trivial).
       eapply NoDup_app_in_l with (x := p) in H; [contradict H | right];
              repeat rewrite in_app_iff; auto with *.

    * assert (H : NoDup (activations p')) by (apply NoDup_activations; subst p'; trivial).
(* Goal: @eq nat (@activation_rank variable function constructor rank p') (rank f) *)
       subst p'.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       rewrite activations_first_activations in H.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       rewrite Hl in H.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       repeat (rewrite flat_map_app in H; simpl in H).
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       eapply FA_path_activation in Hp1; [ | exact Hwf | apply first_activations_incl_activations; trivial].
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       eapply FA_path_activation in Hp2; [ | exact Hwf | apply first_activations_incl_activations; trivial].
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       apply in_split in Hp1; apply in_split in Hp2.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       destruct Hp1 as (ll1 & ll1' & Hll1).
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       destruct Hp2 as (ll2 & ll2' & Hll2).
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) lp1 lp2 *)
       rewrite Hll1, Hll2 in H.
       replace ((cbv_update i s p0 c1 t c2 v :: flat_map (activations (constructor:=constructor)) l1 ++
          (ll2 ++ p :: ll2') ++ flat_map (activations (constructor:=constructor)) l2 ++
          (ll1 ++ p :: ll1') ++ flat_map (activations (constructor:=constructor)) l3)) with
          ((cbv_update i s p0 c1 t c2 v :: flat_map (activations (constructor:=constructor)) l1 ++
          (ll2 ++ p :: ll2')) ++
          (flat_map (activations (constructor:=constructor)) l2 ++
          (ll1 ++ p :: ll1') ++ flat_map (activations (constructor:=constructor)) l3)) in H by
          (repeat rewrite app_assoc; trivial).
       eapply NoDup_app_in_l with (x := p) in H; [contradict H | right];
              repeat rewrite in_app_iff; auto with *. 
Qed.

Lemma activations_strict i s p0 c1 t c2 v :
  wf (cbv_update i s p0 c1 t c2 v) ->
  ~ cbv_update i s p0 c1 t c2 v ∈ activations p0.
Proof.
(* Goal: forall _ : @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 p0 c1 t c2 v), not (@In (CBV_cache.cbv variable function constructor) (@cbv_update variable function constructor i s p0 c1 t c2 v) (@activations variable function constructor p0)) *)
intros Hwf Hin.
(* Goal: False *)
assert (size_rec (cbv_update i s p0 c1 t c2 v) <= size_rec p0).
(* Goal: le (@size_rec variable function constructor (@cbv_update variable function constructor i s p0 c1 t c2 v)) (@size_rec variable function constructor p0) *)
(* Goal: False *)
  apply sub_trees_size_rec_le.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
  apply activations_are_subtrees; assumption.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
destruct t; simpl in H; omega.
Qed.

Lemma first_activation_down_rank_lt p p' i s p0 c1 t c2 v:
  let proof_tree := cbv_update i s p0 c1 t c2 v in
  PPO_prog ->
  wf proof_tree ->
  In p' (activations proof_tree) -> In p (first_activations p') ->
  In p (first_activations_at_given_rank (activation_rank rank p) proof_tree) ->
  activation_rank rank p < activation_rank rank p'.
Proof.
(* Goal: let proof_tree := @cbv_update variable function constructor i s p0 c1 t c2 v in forall (_ : @Ordering.PPO_prog variable function constructor prog rank) (_ : @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)) (_ : @In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p (first_activations_at_given_rank (@activation_rank variable function constructor rank p) proof_tree)), lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
intros proof_tree HPPO.
unfold proof_tree in *.
(* Goal: forall (_ : @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 p0 c1 t c2 v)) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor (@cbv_update variable function constructor i s p0 c1 t c2 v))) (_ : @In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p (first_activations_at_given_rank (@activation_rank variable function constructor rank p) (@cbv_update variable function constructor i s p0 c1 t c2 v))), lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
revert p p'.
(* Goal: forall (p p' : CBV_cache.cbv variable function constructor) (_ : @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 p0 c1 t c2 v)) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor (@cbv_update variable function constructor i s p0 c1 t c2 v))) (_ : @In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p (first_activations_at_given_rank (@activation_rank variable function constructor rank p) (@cbv_update variable function constructor i s p0 c1 t c2 v))), lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
apply cbv_big_induction.
(* Goal: forall (i : nat) (s : forall _ : variable, Syntax.value constructor) (p : CBV_cache.cbv variable function constructor) (c1 : cache variable function constructor) (t : Syntax.term variable function constructor) (c2 : 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))) (p0 p'0 : CBV_cache.cbv variable function constructor) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p') (_ : @In (CBV_cache.cbv variable function constructor) p'0 (@activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p0 (@first_activations variable function constructor p'0)) (_ : @In (CBV_cache.cbv variable function constructor) p0 (first_activations_at_given_rank (@activation_rank variable function constructor rank p0) p')), lt (@activation_rank variable function constructor rank p0) (@activation_rank variable function constructor rank p'0)) (p0 p' : CBV_cache.cbv variable function constructor) (_ : @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' (@activations variable function constructor (@cbv_update variable function constructor i s p c1 t c2 v))) (_ : @In (CBV_cache.cbv variable function constructor) p0 (@first_activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p0 (first_activations_at_given_rank (@activation_rank variable function constructor rank p0) (@cbv_update variable function constructor i s p c1 t c2 v))), lt (@activation_rank variable function constructor rank p0) (@activation_rank variable function constructor rank p') *)
clear i s p0 c1 t c2 v proof_tree.
(* Goal: forall (i : nat) (s : forall _ : variable, Syntax.value constructor) (p : CBV_cache.cbv variable function constructor) (c1 : cache variable function constructor) (t : Syntax.term variable function constructor) (c2 : 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))) (p0 p'0 : CBV_cache.cbv variable function constructor) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p') (_ : @In (CBV_cache.cbv variable function constructor) p'0 (@activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p0 (@first_activations variable function constructor p'0)) (_ : @In (CBV_cache.cbv variable function constructor) p0 (first_activations_at_given_rank (@activation_rank variable function constructor rank p0) p')), lt (@activation_rank variable function constructor rank p0) (@activation_rank variable function constructor rank p'0)) (p0 p' : CBV_cache.cbv variable function constructor) (_ : @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' (@activations variable function constructor (@cbv_update variable function constructor i s p c1 t c2 v))) (_ : @In (CBV_cache.cbv variable function constructor) p0 (@first_activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p0 (first_activations_at_given_rank (@activation_rank variable function constructor rank p0) (@cbv_update variable function constructor i s p c1 t c2 v))), lt (@activation_rank variable function constructor rank p0) (@activation_rank variable function constructor rank p') *)
intros i s p0 c1 t c2 v H p p'.
(* Goal: forall (_ : @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 p0 c1 t c2 v)) (_ : @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor (@cbv_update variable function constructor i s p0 c1 t c2 v))) (_ : @In (CBV_cache.cbv variable function constructor) p (@first_activations variable function constructor p')) (_ : @In (CBV_cache.cbv variable function constructor) p (first_activations_at_given_rank (@activation_rank variable function constructor rank p) (@cbv_update variable function constructor i s p0 c1 t c2 v))), lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
intros Hwf Ha Hfa Hfagr.
(* Goal: lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
destruct t; try tauto; try inversion Hfagr.
(* Goal: lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
rewrite first_activations_at_given_rank_caract in Hfagr.
(* Goal: lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
destruct eq_nat_dec as [Heq | Hneq] in Hfagr.
- simpl in Hfagr; destruct Hfagr ; try tauto.
(* Goal: lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
  subst p.
(* Goal: lt (@activation_rank variable function constructor rank (@cbv_update variable function constructor i s p0 c1 (@fapply variable function constructor f l) c2 v)) (@activation_rank variable function constructor rank p') *)
  clear Heq.
(* Goal: lt (@activation_rank variable function constructor rank (@cbv_update variable function constructor i s p0 c1 (@fapply variable function constructor f l) c2 v)) (@activation_rank variable function constructor rank p') *)
  rewrite activations_first_activations in Ha.
(* Goal: lt (@activation_rank variable function constructor rank (@cbv_update variable function constructor i s p0 c1 (@fapply variable function constructor f l) c2 v)) (@activation_rank variable function constructor rank p') *)
  destruct Ha as [Hroot | Htail].
  +  subst p'.
(* Goal: lt (@activation_rank variable function constructor rank (@cbv_update variable function constructor i s p0 c1 (@fapply variable function constructor f l) c2 v)) (@activation_rank variable function constructor rank (@cbv_update variable function constructor i s p0 c1 (@fapply variable function constructor f l) c2 v)) *)
     contradict Hfa.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
     apply first_activations_strict; assumption.

  +  apply in_flat_map in Htail.
(* Goal: lt (@activation_rank variable function constructor rank (@cbv_update variable function constructor i s p0 c1 (@fapply variable function constructor f l) c2 v)) (@activation_rank variable function constructor rank p') *)
     destruct Htail as (p'' & Hin'' & Hp'').
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
     apply first_activations_irrefl in Hin''; try tauto.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
     apply activations_trans with p'; try assumption.
     * eapply activations_wf; [exact Hwf|].
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
        apply first_activations_incl_activations; assumption.

     * apply first_activations_incl_activations; assumption.

- destruct Ha as [Heqp' | Hneqp'].
  + subst p'.
(* Goal: lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank (@cbv_update variable function constructor i s p0 c1 (@fapply variable function constructor f l) c2 v)) *)
    simpl in Hfa.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
    simpl.
(* Goal: lt (@activation_rank variable function constructor rank p) (rank f) *)
    assert (activation_rank rank p <= rank f).
    * eapply PPO_activation_rank_decreasing; eauto.
(* Goal: @In (CBV_cache.cbv variable function constructor) p'' (@activations variable function constructor (@cbv_update variable function constructor i s p0 c1 (@fapply variable function constructor f l) c2 v)) *)
       apply first_activations_incl_activations.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
       assumption.

    * simpl in Hneq.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
       omega.

  + apply in_flat_map in Hfagr.
(* Goal: lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
     destruct Hfagr as (p'' & Hin'' & Hp'').
(* Goal: lt (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') *)
     simpl in H.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
     apply H with p''; try tauto.
     * eapply activations_wf; [exact Hwf |].
(* Goal: @In (CBV_cache.cbv variable function constructor) p'' (@activations variable function constructor (@cbv_update variable function constructor i s p0 c1 (@fapply variable function constructor f l) c2 v)) *)
        apply first_activations_incl_activations.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
        assumption.

     * apply first_activations_at_given_rank_activations in Hp''.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p'') *)
        generalize Hp''; intro Hpp''. 
        eapply (first_activations_at_given_rank_path _ _ i s p0 c1 (fapply f l) c2 v)  in Hp'';
          [| apply first_activations_incl_activations; simpl; assumption].
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p'') *)
        destruct Hp'' as (lp1 & Hpath1).
        assert( Hpath2 :FA_path p (cbv_update i s p0 c1 (fapply f l) c2 v) (lp1 ++ [(cbv_update i s p0 c1 (fapply f l) c2 v)] )) by (apply FA_path_right with p''; assumption).

(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p'') *)
        assert (Hpath3 : In p' (activations (cbv_update i s p0 c1 (fapply f l) c2 v))) by (right; assumption).
        eapply first_activations_at_given_rank_path in  Hpath3;  [| left; trivial].
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p'') *)
        destruct Hpath3 as (lp2 & Hlp2).
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p'') *)
        assert(Hpath4 : FA_path p (cbv_update i s p0 c1 (fapply f l) c2 v) (p' :: lp2)) by (simpl; tauto).

        assert (Heq : lp1 ++ [cbv_update i s p0 c1 (fapply f l) c2 v]= p' :: lp2) by
          (eapply FA_path_uniqueness; eauto).
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
        {
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
          destruct lp1; destruct lp2; simpl in Heq; try tauto.
          - inversion Heq; subst.
(* Goal: @In (CBV_cache.cbv variable function constructor) (@cbv_update variable function constructor i s p0 c1 (@fapply variable function constructor f l) c2 v) (@activations variable function constructor p'') *)
              contradict Hneqp'.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
              apply activations_strict; assumption.

          - inversion Heq.

          - destruct lp1; inversion Heq.

          - inversion Heq; subst.
              eapply FA_path_activation with (lp := lp1) ; [exact Hwf | | simpl in *; tauto].
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
              apply first_activations_incl_activations; assumption.
        }
Qed.

Lemma first_activations_at_given_rank_lt_previous 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_at_given_rank (activation_rank rank p') proof_tree) ->
  activation_rank rank p' < activation_rank rank proof_tree ->
  exists p'', In p'' (activations proof_tree) /\
         In p' (first_activations p'') /\
         activation_rank rank p' < activation_rank rank p''.
Proof.
(* Goal: let proof_tree := @cbv_update variable function constructor i s p c1 t c2 v in forall (_ : @Ordering.PPO_prog variable function constructor prog rank) (_ : @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_at_given_rank (@activation_rank variable function constructor rank p') proof_tree)) (_ : lt (@activation_rank variable function constructor rank p') (@activation_rank variable function constructor rank proof_tree)), @ex (CBV_cache.cbv variable function constructor) (fun p'' : CBV_cache.cbv variable function constructor => and (@In (CBV_cache.cbv variable function constructor) p'' (@activations variable function constructor proof_tree)) (and (@In (CBV_cache.cbv variable function constructor) p' (@first_activations variable function constructor p'')) (lt (@activation_rank variable function constructor rank p') (@activation_rank variable function constructor rank p'')))) *)
intros proof_tree HPPO Hwf Hp' Hlt.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
destruct (first_activation_down p' i s p c1 t c2 v) as (p'' & H); trivial.

- contradict Hlt.
(* Goal: le (rank g) (rank f) *)
  subst.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
  simpl; omega.

- apply first_activations_at_given_rank_activations in Hp'.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
  assumption.

- exists p''.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
  repeat split; try tauto.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
  unfold proof_tree in Hwf.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
  eapply first_activation_down_rank_lt with i s p c1 t c2 v; try tauto.
Qed.

Lemma length_fapplies_le_functions s t : length (fapplies_in_term (@subst variable function constructor s t)) <= length (functions_of_term t).
Proof.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
induction t using term_ind2; simpl.
 - rewrite fapplies_in_value_nil.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
   trivial.

  - do 2 rewrite length_flat_map.
(* Goal: le (suml (@map (list (CBV_cache.cbv variable function constructor)) nat (@length (CBV_cache.cbv variable function constructor)) (@map (CBV_cache.cbv variable function constructor) (list (CBV_cache.cbv variable function constructor)) (@first_activations_rec variable function constructor) lp))) (suml (@map (list (CBV_cache.cbv variable function constructor)) nat (@length (CBV_cache.cbv variable function constructor)) (@map (CBV_cache.cbv variable function constructor) (list (CBV_cache.cbv variable function constructor)) (@first_activations_and_semi_rec variable function constructor) lp))) *)
    repeat rewrite map_map. 
(* Goal: le (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => @length (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor x)) lp)) (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => @length (CBV_cache.cbv variable function constructor) (@first_activations_and_semi_rec variable function constructor x)) lp)) *)
    apply suml_map_le.
(* Goal: forall (x : nat) (_ : @In nat x (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt)), le x (@term_size variable function constructor (@proj_left variable function constructor proof_tree)) *)
    intros x Hx.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
    apply H; assumption.

  - apply le_n_S.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor) lp)) (@length (CBV_cache.cbv variable function constructor) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@first_activations_and_semi_rec variable function constructor) lp)) *)
    do 2 rewrite length_flat_map.
(* Goal: le (suml (@map (list (CBV_cache.cbv variable function constructor)) nat (@length (CBV_cache.cbv variable function constructor)) (@map (CBV_cache.cbv variable function constructor) (list (CBV_cache.cbv variable function constructor)) (@first_activations_rec variable function constructor) lp))) (suml (@map (list (CBV_cache.cbv variable function constructor)) nat (@length (CBV_cache.cbv variable function constructor)) (@map (CBV_cache.cbv variable function constructor) (list (CBV_cache.cbv variable function constructor)) (@first_activations_and_semi_rec variable function constructor) lp))) *)
    repeat rewrite map_map. 
(* Goal: le (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => @length (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor x)) lp)) (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => @length (CBV_cache.cbv variable function constructor) (@first_activations_and_semi_rec variable function constructor x)) lp)) *)
    apply suml_map_le.
(* Goal: forall (x : nat) (_ : @In nat x (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt)), le x (@term_size variable function constructor (@proj_left variable function constructor proof_tree)) *)
    intros x Hx.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
    apply H; assumption.
Qed.

Lemma first_activations_length_le_first_and_semi_activations n s p c1 f l c2 v : length (first_activations (cbv_update n s p c1 (@fapply variable function constructor f l) c2 v)) <=
length (first_activations_and_semi (cbv_update n s p c1 (fapply f l) c2 v)).
Proof.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
simpl.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
induction p using cbv_ind2; simpl.
- do 2 rewrite length_flat_map. 
(* Goal: le (suml (@map (list (CBV_cache.cbv variable function constructor)) nat (@length (CBV_cache.cbv variable function constructor)) (@map (CBV_cache.cbv variable function constructor) (list (CBV_cache.cbv variable function constructor)) (@first_activations_rec variable function constructor) lp))) (suml (@map (list (CBV_cache.cbv variable function constructor)) nat (@length (CBV_cache.cbv variable function constructor)) (@map (CBV_cache.cbv variable function constructor) (list (CBV_cache.cbv variable function constructor)) (@first_activations_and_semi_rec variable function constructor) lp))) *)
  repeat rewrite map_map.
(* Goal: le (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => @length (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor x)) lp)) (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => @length (CBV_cache.cbv variable function constructor) (@first_activations_and_semi_rec variable function constructor x)) lp)) *)
  apply suml_map_le.
(* Goal: forall (x : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) x lp), le (@length (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor x)) (@length (CBV_cache.cbv variable function constructor) (@first_activations_and_semi_rec variable function constructor x)) *)
  apply H.

- do 2 rewrite app_length.
(* Goal: le (Init.Nat.add (@length (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor p)) (@length (CBV_cache.cbv variable function constructor) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor) lp))) (Init.Nat.add (@length (CBV_cache.cbv variable function constructor) (@first_activations_and_semi_rec variable function constructor p)) (@length (CBV_cache.cbv variable function constructor) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@first_activations_and_semi_rec variable function constructor) lp))) *)
  apply plus_le_compat.
  + assumption.

  + do 2 rewrite length_flat_map. 
(* Goal: le (suml (@map (list (CBV_cache.cbv variable function constructor)) nat (@length (CBV_cache.cbv variable function constructor)) (@map (CBV_cache.cbv variable function constructor) (list (CBV_cache.cbv variable function constructor)) (@first_activations_rec variable function constructor) lp))) (suml (@map (list (CBV_cache.cbv variable function constructor)) nat (@length (CBV_cache.cbv variable function constructor)) (@map (CBV_cache.cbv variable function constructor) (list (CBV_cache.cbv variable function constructor)) (@first_activations_and_semi_rec variable function constructor) lp))) *)
    repeat rewrite map_map.
(* Goal: le (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => @length (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor x)) lp)) (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => @length (CBV_cache.cbv variable function constructor) (@first_activations_and_semi_rec variable function constructor x)) lp)) *)
    apply suml_map_le.
(* Goal: forall (x : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) x lp), le (@length (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor x)) (@length (CBV_cache.cbv variable function constructor) (@first_activations_and_semi_rec variable function constructor x)) *)
    apply H.

- trivial.

- apply le_S, le_n.
Qed.

Lemma degree_bounded p :
  wf p -> length (first_activations p) <= max_nb_rhs_functions prog.
Proof.
(* Goal: forall _ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p, le (@length (CBV_cache.cbv variable function constructor) (@first_activations variable function constructor p)) (@max_nb_rhs_functions variable function constructor prog) *)
  intro Wfp.
  assert( H : forall p0 : cbv,
  InCBV p0 p -> length (first_activations p0) <= max_nb_rhs_functions prog); 
  [| apply H; apply InCBV_refl].
(* Goal: forall (p0 : CBV_cache.cbv variable function constructor) (_ : @InCBV variable function constructor p0 p), le (@length (CBV_cache.cbv variable function constructor) (@first_activations variable function constructor p0)) (@max_nb_rhs_functions variable function constructor prog) *)
  induction p using cbv_ind2; intros p0 Hin; simpl in Hin.
  - destruct Hin as [Heq | Hneq].
    + subst p0; apply le_0_n.

    + apply orl_map in Hneq.
      destruct Hneq as (p' & Hp'  & Hin').
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
      apply H in Hin'; try assumption.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p *)
      simpl in Wfp.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
      destruct t; try tauto; destruct v; try tauto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p' *)
      destruct Wfp as (_ & _ & _ & _ & Hwf & _).
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
      apply andl_in_map with lp; assumption.

  - destruct Hin as [Heq | [Hin | Hor]].
    + subst p0; apply le_0_n.

    + apply IHp.
      * simpl in Wfp.
            repeat match goal with
        | _ : match ?x with _ => _ end |- _ => destruct x; try tauto
      end.

      * assumption.

    + apply orl_map in Hor.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (@first_activations variable function constructor p0)) (@max_nb_rhs_functions variable function constructor prog) *)
      destruct Hor as (p' & Hp'1 & Hp'2).
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
      apply H with p'; try assumption.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p *)
      simpl in Wfp.
            repeat match goal with
        | _ : match ?x with _ => _ end |- _ => destruct x; try tauto
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
      end; destruct Wfp as (_ & _ & _ & _ & Hwf & _); apply andl_in_map with lp; assumption.

  - destruct Hin as [Heq | Hneq].
    + subst p0.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (@first_activations variable function constructor (@cbv_update variable function constructor n s p c1 t c2 v))) (@max_nb_rhs_functions variable function constructor prog) *)
      assert (Hres := Wfp).
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
      eapply first_activations_residues_activation in Hres; eauto.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p *)
      simpl in Wfp.
      repeat match goal with
        | _ : match ?x with _ => _ end |- _ => destruct x; try tauto
      end.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (@first_activations variable function constructor (@cbv_update variable function constructor n s p c1 (@fapply variable function constructor f l) c2 v))) (@max_nb_rhs_functions variable function constructor prog) *)
      destruct Wfp as (_ & lp & t & Hn & Hrule & Hl & Ht & Hrem).
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (@first_activations variable function constructor (@cbv_update variable function constructor n s p c1 (@fapply variable function constructor f l) c2 v))) (@max_nb_rhs_functions variable function constructor prog) *)
      transitivity (nb_rhs_functions (rule_intro f lp t)).
      * apply Forall2_length in Hres.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (@first_activations variable function constructor (@cbv_update variable function constructor n s p c1 (@fapply variable function constructor f l) c2 v))) (@nb_rhs_functions variable function constructor (@rule_intro variable function constructor f lp t)) *)
        rewrite Ht in Hres.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (@first_activations variable function constructor (@cbv_update variable function constructor n s p c1 (@fapply variable function constructor f l) c2 v))) (@nb_rhs_functions variable function constructor (@rule_intro variable function constructor f lp t)) *)
        simpl in Hres.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
        { transitivity (length (fapplies_in_term (subst s t))).
          - rewrite <- Hres.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
            replace (first_activations_and_semi_rec p) with (first_activations_and_semi (cbv_update n s p c1 (fapply f l) c2 v)) by trivial.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (@first_activations variable function constructor (@cbv_update variable function constructor n s p c1 (@fapply variable function constructor f l) c2 v))) (@length (CBV_cache.cbv variable function constructor) (@first_activations_and_semi variable function constructor (@cbv_update variable function constructor n s p c1 (@fapply variable function constructor f l) c2 v))) *)
            apply first_activations_length_le_first_and_semi_activations.

          - apply length_fapplies_le_functions.
        }

      * unfold max_nb_rhs_functions.
(* Goal: le (@nb_rhs_functions variable function constructor (@rule_intro variable function constructor f lp t)) (maxl (@map (Syntax.rule variable function constructor) nat (@nb_rhs_functions variable function constructor) prog)) *)
        apply maxl_is_max.
(* Goal: @In nat (@nb_rhs_functions variable function constructor (@rule_intro variable function constructor f lp t)) (@map (Syntax.rule variable function constructor) nat (@nb_rhs_functions variable function constructor) prog) *)
        apply in_map_iff.
(* Goal: @ex (Syntax.rule variable function constructor) (fun x : Syntax.rule variable function constructor => and (@eq nat (@nb_rhs_functions variable function constructor x) (@nb_rhs_functions variable function constructor (@rule_intro variable function constructor f lp t))) (@In (Syntax.rule variable function constructor) x prog)) *)
        exists (rule_intro f lp t).
(* Goal: @eq (list A) (@nil A) (@nil A) *)
        split; try trivial.
        rewrite <- Hrule.
(* Goal: @In (Syntax.rule variable function constructor) (@nth (Syntax.rule variable function constructor) n prog rule_default) prog *)
        apply nth_In.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
        assumption.

    + apply IHp.
      * simpl in Wfp.
        repeat match goal with
         | _ : match ?x with _ => _ end |- _ => destruct x; try tauto
        end.
(* Goal: @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity p *)
        decompose record Wfp.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
        assumption.

      * assumption.

  - destruct Hin as [Heq | Hneq].
    + subst p0; apply le_0_n.

    + tauto.
Qed.

Lemma split_activations_by_first_activations_at_rank rk p :
  wf p ->
  activations_at_rank rk p = flat_map (activations_at_rank rk) (first_activations_at_given_rank rk p).
Proof.
intro Hwf.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (activations_at_rank (rank f) proof_tree)) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor proof_tree))) *)
unfold activations_at_rank.
induction p as [ lp c1 t c2 v IHlp | lp p' c1 t c2 v IHlp IHp | i s p' c1 t c2 v IHp | c t v ]
(* Goal: @eq (list A) (@nil A) (@nil A) *)
 using cbv_ind2; simpl; trivial.

- etransitivity.

  + rewrite filter_flat_map.
    apply flat_map_in_ext.
    intros p Hp.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
    apply IHlp; trivial.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
    apply wf_InCBV_wf with (proof_tree := cbv_constr lp c1 t c2 v); trivial.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
    simpl.
(* Goal: or (@eq (Syntax.term variable function constructor) (@fapply variable function constructor f2 lt2) t1) (lt (@term_size variable function constructor t1) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) *)
    right.
    apply orl_map.
    exists p.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
    split; trivial.
    apply InCBV_refl.

  + clear IHlp Hwf.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
    induction lp as [ | p lp IH ]; trivial.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
    simpl.
    rewrite IH.
    symmetry; apply flat_map_app.

- etransitivity.

  + rewrite filter_app, filter_flat_map.
(* Goal: @eq (list (CBV_cache.cbv variable function constructor)) (@app (CBV_cache.cbv variable function constructor) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) (@first_activations_rec variable function constructor p0)) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) lp)) (@app (CBV_cache.cbv variable function constructor) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) (@first_activations_rec variable function constructor p0)) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (first_activations_at_given_rank rk) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor) lp))) *)
    apply app_eq_compat_l.
    apply flat_map_in_ext.
    intros p Hp.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
    apply IHlp; trivial.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
    apply wf_InCBV_wf with (proof_tree := cbv_split lp p' c1 t c2 v); trivial.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
    simpl.
(* Goal: or (@eq (Syntax.term variable function constructor) (@fapply variable function constructor f2 lt2) t1) (lt (@term_size variable function constructor t1) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) *)
    right.
(* Goal: or (@eq (Syntax.term variable function constructor) (@fapply variable function constructor f2 lt2) t1) (lt (@term_size variable function constructor t1) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) *)
    right.
    apply orl_map.
    exists p.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
    split; trivial.
    apply InCBV_refl.

  + rewrite IHp.

    * clear IHlp IHp Hwf.
      rewrite flat_map_app.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
      induction lp as [ | p lp IH ]; trivial.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
      simpl.
      rewrite flat_map_app.
      apply app_insert_r; [ exact IH | ].
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor) lp)) (@length (CBV_cache.cbv variable function constructor) (@flat_map (CBV_cache.cbv variable function constructor) (CBV_cache.cbv variable function constructor) (@first_activations_and_semi_rec variable function constructor) lp)) *)
      do 2 rewrite length_flat_map.
(* Goal: forall _ : @PPO variable function constructor rank (@term_from_value variable function constructor v) (@term_from_value variable function constructor v'), lt (@value_size constructor v) (@value_size constructor v') *)
      clear.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
      induction lp as [ | p lp IH]; trivial.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
      simpl.
      rewrite IH.
      do 2 rewrite map_app.
      rewrite length_flat_map, suml_app.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
      trivial.

    * apply wf_InCBV_wf with (proof_tree := cbv_split lp p' c1 t c2 v); trivial.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
      simpl.
(* Goal: or (@eq (Syntax.term variable function constructor) (@fapply variable function constructor f2 lt2) t1) (lt (@term_size variable function constructor t1) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) *)
      right.
      left.
      apply InCBV_refl.

- destruct t as [ | | f lv ]; try (simpl in Hwf; tauto).
  destruct (eq_nat_dec rk (rank f)) as [ Heq | Hneq ].

  + simpl.
    apply app_nil_end.

  + case_eq (beq_nat rk (rank f)).

    * intro Heq.
      contradict Hneq.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
      apply beq_nat_true; assumption.

    * intros _.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (@first_activations variable function constructor p0)) (@max_nb_rhs_functions variable function constructor prog) *)
      apply IHp.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
      apply wf_InCBV_wf with (proof_tree := cbv_update i s p' c1 (fapply f lv) c2 v); trivial.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
      simpl.
(* Goal: or (@eq (Syntax.term variable function constructor) (@fapply variable function constructor f2 lt2) t1) (lt (@term_size variable function constructor t1) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) *)
      right.
      apply InCBV_refl.
Qed.

Lemma notin_nil (A: Type) (xs: list A):
  (forall x, ~ In x xs) -> [] = xs.
Proof.
(* Goal: forall _ : forall x : A, not (@In A x xs), @eq (list A) (@nil A) xs *)
 intro Hnin.
(* Goal: @eq (list A) (@nil A) xs *)
 destruct xs.
 - trivial.
 
 - elim (Hnin a).
(* Goal: @In A a (@cons A a xs) *)
   apply in_eq.
Qed.

Lemma activations_at_rank_activation_rank proof_tree p:
  In p (activations proof_tree) ->
  In p (activations_at_rank (activation_rank rank p) proof_tree).
Proof.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (activations_at_rank (rank f) proof_tree)) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor proof_tree))) *)
unfold activations_at_rank.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
induction (activations proof_tree) as [ | p' lp IH]; trivial.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
simpl.
(* Goal: forall _ : or (@eq (CBV_cache.cbv variable function constructor) p' p) (@In (CBV_cache.cbv variable function constructor) p lp), @In (CBV_cache.cbv variable function constructor) p (if Nat.eqb (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p') then @cons (CBV_cache.cbv variable function constructor) p' (@filter (CBV_cache.cbv variable function constructor) (fun p0 : CBV_cache.cbv variable function constructor => Nat.eqb (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p0)) lp) else @filter (CBV_cache.cbv variable function constructor) (fun p0 : CBV_cache.cbv variable function constructor => Nat.eqb (@activation_rank variable function constructor rank p) (@activation_rank variable function constructor rank p0)) lp) *)
intros [ H | H ].

- subst p'.
  rewrite <- beq_nat_refl.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
  simpl.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
  tauto.

- case_eq (beq_nat (activation_rank rank p) (activation_rank rank p')); simpl; tauto.
Qed.

Lemma first_activations_at_given_rank_incl i s p c1 t c2 v r :
  let proof_tree := cbv_update i s p c1 t c2 v in
  PPO_prog ->
  wf proof_tree ->
  r < activation_rank rank proof_tree ->
  incl (first_activations_at_given_rank r proof_tree)
       (flat_map (@first_activations _ _ _)
                 (flat_map (fun r' => activations_at_rank r' proof_tree)
                           (seq (1 + r) (max_rank - r)))).
Proof.
  (* utilise first_activations_at_given_rank_lt_previous *)
intros proof_tree PPO_prog Hwf Hlt p' Hp'.
assert (Hr: r = activation_rank rank p').
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
{
  eapply first_activations_at_given_rank_rank.
  eexact Hp'.
}
subst r.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
apply first_activations_at_given_rank_lt_previous in Hp'; trivial.
destruct Hp' as (p'' & Hp'' & Hp' & Hlt').
(* Goal: @In (Syntax.term variable function constructor) t (@flat_map (Syntax.term variable function constructor) (Syntax.term variable function constructor) sub_terms lt) *)
apply in_flat_map.
(* Goal: @ex (CBV_cache.cbv variable function constructor) (fun p'' : CBV_cache.cbv variable function constructor => and (@In (CBV_cache.cbv variable function constructor) p'' (@activations variable function constructor proof_tree)) (and (@In (CBV_cache.cbv variable function constructor) p' (@first_activations variable function constructor p'')) (lt (@activation_rank variable function constructor rank p') (@activation_rank variable function constructor rank p'')))) *)
exists p''.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
split; trivial.
(* Goal: @In (Syntax.term variable function constructor) t (@flat_map (Syntax.term variable function constructor) (Syntax.term variable function constructor) sub_terms lt) *)
apply in_flat_map.
exists (activation_rank rank p'').
(* Goal: and (@In function f0 (@functions_of_prog variable function constructor prog)) (@In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor f0 sa) (all_possible_subarguments lt))) *)
split.

- apply in_seq.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
  split; trivial.
  assert (Hrank: activation_rank rank p'' < S max_rank).
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
  {
    apply activation_is_function in Hp''.
    destruct Hp'' as (i' & s' & p''' & c1' & t' & c2' & v' & Hp'').
    subst p''.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
    simpl.
    destruct t'; auto with *.
  }
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
  omega.

- apply activations_at_rank_activation_rank; trivial.
Qed.

Definition compatible_rule (r:rule) : Prop :=
  match r with
    | rule_intro f _ t => forall f', In f' (functions_of_term t) -> rank f' <= rank f
  end.

Definition compatible_prog : Prop :=
  forall r, In r prog -> compatible_rule r.

Lemma PPO_is_compatible_rule:
  forall r, PPO_rule rank r -> compatible_rule r.
Proof.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
intros [f l t]; simpl.
(* Goal: forall (_ : @PPO variable function constructor rank t (@fapply variable function constructor f (@map (pattern variable constructor) (Syntax.term variable function constructor) (@term_from_pattern variable function constructor) l))) (f' : function) (_ : @In function f' (@functions_of_term variable function constructor t)), le (rank f') (rank f) *)
induction t using term_ind2; intros HPPO g Hg; simpl in Hg.
- inversion HPPO; subst; inversion Hg.

- apply in_flat_map in Hg; destruct Hg as (t0 & Hin0 & Hg).
(* Goal: @eq (list A) (@nil A) (@nil A) *)
  apply H with t0; trivial.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
  apply PPO_trans with (capply c l0); trivial.
(* Goal: @PPO variable function constructor rank t0 (@capply variable function constructor c l0) *)
  now apply ppo_constr_in.

- destruct Hg as [Heq| Hin].
  + subst.
(* Goal: le (rank g) (rank f) *)
    now apply PPO_pattern_le_rank in HPPO.

  + apply in_flat_map in Hin; destruct Hin as (t0 & Hin0 & Hg).
(* Goal: @eq (list A) (@nil A) (@nil A) *)
    apply H with t0; trivial.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
    apply PPO_trans with (fapply f0 l0); trivial.
(* Goal: @PPO variable function constructor rank t0 (@fapply variable function constructor f0 l0) *)
    now apply ppo_fun_in.
Qed.

Lemma PPO_is_compatible_prog:
  PPO_prog -> compatible_prog.
Proof.
(* Goal: forall _ : @Ordering.PPO_prog variable function constructor prog rank, compatible_prog *)
unfold PPO_prog;unfold compatible_prog.
(* Goal: forall (x : nat) (_ : @In nat x (@map (CBV_cache.cbv variable function constructor) nat (fun pi : CBV_cache.cbv variable function constructor => bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor pi))) (@activations variable function constructor proof_tree))), le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
intros.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
apply PPO_is_compatible_rule;auto.
Qed.

Lemma gary_seven i s p c1 f lt c2 v:
  let proof_tree := cbv_update i s p c1 (fapply f lt) c2 v in
  compatible_prog ->
  wf proof_tree ->
  PPO_prog ->
  length (activations proof_tree) <= gary_seven_poly (A_T proof_tree).
Proof.
intros proof_tree Hcompat Hwf Hppoprog.
assert (H :
  forall r, r <= max_rank ->
  length(activations_at_rank r proof_tree) <=
  activations_at_rank_bound (A_T proof_tree) r
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
). {
  intro r.
  remember (max_rank - r) as n.
  revert i s p c1 f lt c2 v proof_tree Hwf r Heqn.
  induction n as [ n IH ] using lt_wf_ind; intros i s p c1 f lt c2 v proof_tree Hwf r Heqn Hr.
  case(eq_nat_dec r (activation_rank rank proof_tree)) as [Heq | Hneq].
  - transitivity (A_T proof_tree).
    + subst r.
      apply A_T_activation_rank.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
      simpl.
      destruct (eq_nat_dec (rank f) (rank f)) as [Heq | Hneq];
      [ apply in_eq | tauto].

    + unfold activations_at_rank_bound.
      transitivity (A_T proof_tree ^ S (max_rank - r)).
      * simpl.
        case (eq_nat_dec 0 (A_T proof_tree)).
          intro He; rewrite <- He.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
          trivial.

          intro Hneq.
          rewrite <- (mult_1_r (A_T proof_tree)) at 1.
(* Goal: le (Init.Nat.mul (@length function (@functions_of_prog variable function constructor prog)) (prodl (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt))) (Init.Nat.mul (@length function (@functions_of_prog variable function constructor prog)) (Nat.pow (@term_size variable function constructor (@proj_left variable function constructor proof_tree)) max_arity)) *)
          apply mult_le_compat_l.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
          destruct (A_T proof_tree); try tauto.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
          simpl.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
          apply lt_0_pow; omega.

      * rewrite <- mult_1_l at 1.
        apply mult_le_compat_r.
        rewrite <- mult_1_l at 1.
        apply mult_le_compat; auto using (pos_max_rank) with * .

  - destruct (lt_eq_lt_dec r (activation_rank rank proof_tree)) as [ [ Hlt | Heq ] | Hgt ].

    + clear Hneq.
      fold (activations_at_rank r proof_tree).
      rewrite split_activations_by_first_activations_at_rank; [ | trivial ].
      rewrite length_flat_map.
      rewrite map_map.
      transitivity (length (map (fun x => length (activations_at_rank r x)) (first_activations_at_given_rank r proof_tree)) * A_T proof_tree).

      * apply suml_le_len_times_bound.
        intros x Hin.
        apply in_map_iff in Hin.
        destruct Hin as ( p' & Heq & Hin ).
(* Goal: le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
        subst x.
        assert( Hreq : r = activation_rank rank p') by
        (apply first_activations_at_given_rank_rank with proof_tree; assumption).
        subst r.  
        apply A_T_activation_rank.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
        assumption.

      * unfold activations_at_rank_bound.
        simpl Nat.pow at 3.
        ring_simplify.
        rewrite mult_comm.
        repeat rewrite <- mult_assoc.
(* Goal: le (Init.Nat.mul (@length function (@functions_of_prog variable function constructor prog)) (prodl (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt))) (Init.Nat.mul (@length function (@functions_of_prog variable function constructor prog)) (Nat.pow (@term_size variable function constructor (@proj_left variable function constructor proof_tree)) max_arity)) *)
        apply mult_le_compat_l.
(* Goal: le (@length nat (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt)) max_arity *)
        rewrite map_length.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
        { etransitivity; [
            eapply NoDup_incl_le_length; [
              apply NoDup_first_activations_at_given_rank; assumption | ] |].

          - apply first_activations_at_given_rank_incl; assumption.

          - rewrite length_flat_map, map_map.
            etransitivity.

            + apply suml_le_len_times_bound.
               intros len Hin.
               apply in_map_iff in Hin.
               destruct Hin as ( p' & Heq & Hin ).
               subst len.
               apply degree_bounded.
(* Goal: @PPO variable function constructor rank t (@capply variable function constructor c lt) *)
               apply in_flat_map in Hin.
               destruct Hin as ( r' & _ & Hin ).
               apply activations_at_rank_wf with (rk := r') (p := proof_tree);
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
               assumption.

            + rewrite map_length, length_flat_map, map_map.
              fold proof_tree.
              transitivity (suml
                              (map (fun x : nat => activations_at_rank_bound (A_T proof_tree) x)
                                   (seq (1 + r) (max_rank - r))) * max_nb_rhs_functions prog).

              * apply mult_le_compat_r.
(* Goal: le (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => @length (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor x)) lp)) (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => @length (CBV_cache.cbv variable function constructor) (@first_activations_and_semi_rec variable function constructor x)) lp)) *)
                apply suml_map_le.
                intros r' Hin.
                apply in_seq in Hin; destruct Hin as ( Hltr & Hler ).
                assert ( Hle_max: r < max_rank ).
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
                { apply lt_le_trans with (m := activation_rank rank proof_tree); simpl; trivial. }
                apply IH with (m := max_rank - r'); trivial; omega.

              * unfold activations_at_rank_bound.
                assert (H_A_T: A_T proof_tree <> 0).
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
                {
(* Goal: le (A_T proof_tree) (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
                  unfold A_T.
                  apply all_maxl; [simpl; congruence | ].
                  intros r0 Hr0.
                  apply in_map_iff in Hr0.
                  destruct Hr0 as (p' & Hp'1 & Hp'2).
                  subst r0.
                  apply activation_is_function in Hp'2.
                  destruct Hp'2 as (i' & s' & p'' & c1' & t & c2' & v' & Hp'2).
(* Goal: @eq nat (@activation_rank variable function constructor rank p') (rank f) *)
                  subst p'.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
                  simpl.
                  destruct t as [ | | f' lv]; simpl; try congruence.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (activations_at_rank (rank f) proof_tree)) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor proof_tree))) *)
                  unfold activations_at_rank.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
                  simpl.
                  rewrite <- beq_nat_refl.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
                  simpl.
                  congruence.
                }
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
                { transitivity (suml
                                  (map
                                     (fun x : nat =>
                                        Nat.pow max_rank (max_rank - (1+r)) *
                                        Nat.pow (max 1 (max_nb_rhs_functions prog)) (max_rank - (1+r)) *
                                        Nat.pow (A_T proof_tree) (max_rank - r))
                                     (seq (1 + r) (max_rank - r))) * max_nb_rhs_functions prog).
                  - apply mult_le_compat_r.
(* Goal: le (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => @length (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor x)) lp)) (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => @length (CBV_cache.cbv variable function constructor) (@first_activations_and_semi_rec variable function constructor x)) lp)) *)
                    apply suml_map_le.
                    intros r' Hin.
                    apply in_seq in Hin as ( Hler & Hltr ).
                    apply mult_le_compat; [ apply mult_le_compat | ].

                    + apply Nat.pow_le_mono_r; omega.
                    + apply Nat.pow_le_mono_r; [ lia | omega].
                    + apply Nat.pow_le_mono_r; [trivial | omega].

                  - rewrite suml_map_const, seq_length.
                    replace (Nat.pow max_rank (max_rank - (1 + r)) *
                             Nat.pow (max 1 (max_nb_rhs_functions prog)) (max_rank - (1 + r)) *
                             Nat.pow (A_T proof_tree) (max_rank - r) *
                             (max_rank - r) * max_nb_rhs_functions prog)
                            with
                            ((Nat.pow max_rank (max_rank - (1 + r)) * (max_rank - r))
                             * ((Nat.pow (max 1 (max_nb_rhs_functions prog)) (max_rank - (1 + r)) * max_nb_rhs_functions prog)
                                * Nat.pow (A_T proof_tree) (max_rank - r)));
                      [ | ring ].
(* Goal: @eq (list A) (@nil A) (@nil A) *)
                    apply mult_le_compat; [ | apply mult_le_compat ]; trivial.

                    + apply Nat.le_lteq in Hr.
                      destruct Hr as [ Hr | Hr ]; [ | nia].
                      apply Nat.le_lteq in Hr.
                      destruct Hr as [ Hr | Hr ].

                      * transitivity (Nat.pow max_rank (S (max_rank - (1 + r)))); [ simpl; nia | ].
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
                        apply Nat.pow_le_mono_r; omega.

                      * simpl.
                        rewrite <- Hr, minus_diag.
                        replace (S r - r) with 1 by omega.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
                        simpl; omega.

                    + destruct (O_or_S (max_nb_rhs_functions prog)) as [ H | H ]; [ | nia ].
                      destruct H as [m Hm].
                      rewrite <- Hm.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
                      simpl.
                      apply Nat.le_lteq in Hr.
                      destruct Hr as [ Hr | Hr ].
                      * apply Nat.le_lteq in Hr.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
                        {destruct Hr as [ Hr | Hr ].
                        - rewrite mult_comm, <- Nat.pow_succ_r; [ | omega].
                          apply Nat.pow_le_mono_r; [congruence | omega].

                        - subst max_rank.
                          rewrite minus_diag.
                          replace (S r - r) with 1 by omega.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
                          simpl; omega.
                        }

                      * subst r.
                        change (activation_rank rank proof_tree) with (rank f) in Hlt.
(* Goal: not (@eq (CBV_cache.cbv variable function constructor) p' (@cbv_update variable function constructor i s p c1 t c2 v)) *)
                        contradict Hlt.
                        apply le_not_lt.
                        apply max_rank_is_max_rank.
            }
        }

    + contradiction.

    + replace (activations_at_rank r proof_tree) with ([]: list cbv);
      [ apply le_0_n | ].
      apply notin_nil.
      intros r' Hin.
      unfold activations_at_rank in Hin.
      apply filter_In in Hin.
      destruct Hin as [ Hin Heq ].
      apply beq_nat_true_iff in Heq; subst r.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
      apply PPO_activation_rank_decreasing in Hin; try trivial.
      change (rank f) with (activation_rank rank proof_tree) in Hin.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
      omega.
}
replace (length(activations proof_tree)) with
  (suml (map (fun r => length(activations_at_rank r proof_tree)) (seq 0 (S max_rank)))).
- unfold gary_seven_poly.
(* Goal: le (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => @length (CBV_cache.cbv variable function constructor) (@first_activations_rec variable function constructor x)) lp)) (suml (@map (CBV_cache.cbv variable function constructor) nat (fun x : CBV_cache.cbv variable function constructor => @length (CBV_cache.cbv variable function constructor) (@first_activations_and_semi_rec variable function constructor x)) lp)) *)
  apply suml_map_le.
  intros r Hr.
  rewrite In_seq in Hr.
  auto with *.

- unfold activations_at_rank.
  transitivity (
    suml (map
     (fun r : nat => length (filter (beq_nat r) (map (activation_rank rank) (activations proof_tree))))
     (seq 0 (S max_rank)))
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
  ). {
    do 2 f_equal.
    extensionality r.
    apply length_filter.
  }
  rewrite <- map_length with (f := activation_rank rank).
  apply length_suml_filter.
  intros x Hinx.
  split; [ apply le_0_n | ].
  apply in_map_iff in Hinx.
  destruct Hinx as (p0 & Hrank & Hin).
(* Goal: le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
  subst x.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) (Nat.eqb (rank f) (@activation_rank variable function constructor rank p')) *)
  apply activation_is_function in Hin.
  destruct Hin as (ii & ss & pp & cc & tt & ccc & vv & Heq).
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (@first_activations variable function constructor p0)) (@max_nb_rhs_functions variable function constructor prog) *)
  subst p0.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
  simpl.
  destruct tt; auto with *.
Qed.

(* Proposition 8 *)

Lemma all_functions_in_prog (function_default : function) (proof_tree: cbv) :
  wf proof_tree ->
  forall p, In p (activations proof_tree) ->
       In (activation_function function_default p) (functions_of_prog prog).
Proof.
  induction proof_tree using cbv_ind2; intros Hwf p Hp.
    - simpl in Hp. apply in_flat_map in Hp.
      destruct Hp as [y [Hy Hp]].
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
      apply H with y; try auto.
      eapply wf_InCBV_wf.
      + eauto.
      + right; apply orl_map; eauto.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
         exists y; split; trivial.
         apply InCBV_refl.

    - assert (wf proof_tree);[eapply wf_InCBV_wf; [eauto |  right; left; apply InCBV_refl]|].
       apply in_app_or in Hp; destruct Hp.
        + auto.

        + simpl in H1. apply in_flat_map in H1.
          destruct H1 as [y [Hy Hp]].
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
          apply H with y; try auto.
          eapply wf_InCBV_wf.
          * apply Hwf.
          * right; right; apply orl_map; eauto using InCBV_refl.

    - assert (wf proof_tree);[eapply wf_InCBV_wf; [ apply Hwf | right; auto using InCBV_refl]|].
      destruct Hp.
      + rewrite <- H0 in *.
(* Goal: forall (x : nat) (_ : @In nat x (@map (CBV_cache.cbv variable function constructor) nat (fun pi : CBV_cache.cbv variable function constructor => bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor pi))) (@activations variable function constructor proof_tree))), le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
        destruct t; intros.
        * inversion Hwf.

        * inversion Hwf.

        * (* functions_of_prog intervient ici *)
          destruct Hwf as [_ [ll [t [Hlen [Hin _]]]]].
(* Goal: @In nat (@nb_rhs_functions variable function constructor (@rule_intro variable function constructor f lp t)) (@map (Syntax.rule variable function constructor) nat (@nb_rhs_functions variable function constructor) prog) *)
          apply in_map_iff.
          exists (rule_intro f ll t).
(* Goal: and (@In function f0 (@functions_of_prog variable function constructor prog)) (@In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor f0 sa) (all_possible_subarguments lt))) *)
          split.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
            auto.

            rewrite <- Hin.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
            apply nth_In; trivial.

      + auto.

    - inversion Hp.
Qed.

(* liens entre PPO et sous-terme *)

Fixpoint sub_terms (t: term) : list term :=
  t :: match t with
         | var _ => []
         | capply _ lt => flat_map sub_terms lt
         | fapply _ lt => flat_map sub_terms lt
       end.

Definition sub_terms_strict (t: term) : list term :=
  match t with
    | var _ => []
    | capply _ lt => flat_map sub_terms lt
    | fapply _ lt => flat_map sub_terms lt
  end.

Lemma sub_term_strict_incl (t: term) :
  incl (sub_terms_strict t) (sub_terms t).
Proof.
  destruct t;
    simpl;
    intros t' Hin;
    apply in_cons;
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
    assumption.
Qed.

Lemma sub_term_eq_or_strict (t1 t2: term) :
  In t1 (sub_terms t2) <-> t1 = t2 \/ In t1 (sub_terms_strict t2).
Proof.
(* Goal: and (@In function f0 (@functions_of_prog variable function constructor prog)) (@In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor f0 sa) (all_possible_subarguments lt))) *)
  split.

  - (* sous-terme → égal ou strict *)
(* Goal: forall _ : @In (Syntax.term variable function constructor) t1 (sub_terms_strict t2), lt (@term_size variable function constructor t1) (@term_size variable function constructor t2) *)
    intros Hin.
    destruct t2 as [ v | c lt | f lt ];
      simpl in *;
      ( destruct Hin;
        [left; symmetry | right ];
        assumption ).

  - (* égal ou strict → sous-terme *)
(* Goal: forall _ : or (@eq (Syntax.term variable function constructor) t1 t2) (@In (Syntax.term variable function constructor) t1 (sub_terms_strict t2)), @In (Syntax.term variable function constructor) t1 (sub_terms t2) *)
    intros H; destruct H as [ Heq | Hin ].

    + subst t2; destruct t1; simpl; left; trivial.

    + apply sub_term_strict_incl; assumption.
Qed.

Lemma sub_term_le_size (t1 t2: term) :
  In t1 (sub_terms t2) -> t2 = t1 \/ term_size t1 < term_size t2.
Proof.
(* Goal: forall _ : @PPO variable function constructor rank (@term_from_value variable function constructor v) (@term_from_value variable function constructor v'), lt (@value_size constructor v) (@value_size constructor v') *)
  clear.
  revert t1;
  induction t2 as [ v2 | c2 lt2 IH | f2 lt2 IH ]  using term_ind2;
  intros t1 Hin;
(* Goal: @PPO variable function constructor rank t (@capply variable function constructor c lt) *)
  simpl in Hin.

  - destruct Hin as [ Heq | Hin ]; tauto.

  - destruct Hin as [ Heq | Hin ]; [ tauto | idtac ].
(* Goal: or (@eq (Syntax.term variable function constructor) (@fapply variable function constructor f2 lt2) t1) (lt (@term_size variable function constructor t1) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) *)
    right.
(* Goal: @PPO variable function constructor rank t (@capply variable function constructor c lt) *)
    apply in_flat_map in Hin.
(* Goal: lt (@term_size variable function constructor t1) (@term_size variable function constructor (@fapply variable function constructor f2 lt2)) *)
    destruct Hin as ( t & Hinlt2 & Hint1 ).
(* Goal: lt (@term_size variable function constructor t1) (@term_size variable function constructor (@fapply variable function constructor f2 lt2)) *)
    apply le_lt_trans with (m := term_size t).
    + destruct (IH t Hinlt2 t1 Hint1) as [ Heq | Hlt ].
      * subst t; apply le_refl.
      * apply lt_le_weak; assumption.
    + simpl.
(* Goal: lt (@term_size variable function constructor t) (S (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt2))) *)
      apply le_lt_n_Sm.
(* Goal: le (@term_size variable function constructor t) (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt2)) *)
      apply in_le_suml.
(* Goal: @In (list (Syntax.term variable function constructor)) (@cons (Syntax.term variable function constructor) x l) (@map (list (Syntax.term variable function constructor)) (list (Syntax.term variable function constructor)) (fun sa : list (Syntax.term variable function constructor) => @cons (Syntax.term variable function constructor) x sa) (all_possible_subarguments l')) *)
      apply in_map.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
      assumption.

  - destruct Hin as [ Heq | Hin ]; [ tauto | idtac ].
(* Goal: or (@eq (Syntax.term variable function constructor) (@fapply variable function constructor f2 lt2) t1) (lt (@term_size variable function constructor t1) (@term_size variable function constructor (@fapply variable function constructor f2 lt2))) *)
    right.
(* Goal: @PPO variable function constructor rank t (@capply variable function constructor c lt) *)
    apply in_flat_map in Hin.
(* Goal: lt (@term_size variable function constructor t1) (@term_size variable function constructor (@fapply variable function constructor f2 lt2)) *)
    destruct Hin as ( t & Hinlt2 & Hint1 ).
(* Goal: lt (@term_size variable function constructor t1) (@term_size variable function constructor (@fapply variable function constructor f2 lt2)) *)
    apply le_lt_trans with (m := term_size t).
    + destruct (IH t Hinlt2 t1 Hint1) as [ Heq | Hlt ].
      * subst t; apply le_refl.
      * apply lt_le_weak; assumption.
    + simpl.
(* Goal: lt (@term_size variable function constructor t) (S (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt2))) *)
      apply le_lt_n_Sm.
(* Goal: le (@term_size variable function constructor t) (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt2)) *)
      apply in_le_suml.
(* Goal: @In (list (Syntax.term variable function constructor)) (@cons (Syntax.term variable function constructor) x l) (@map (list (Syntax.term variable function constructor)) (list (Syntax.term variable function constructor)) (fun sa : list (Syntax.term variable function constructor) => @cons (Syntax.term variable function constructor) x sa) (all_possible_subarguments l')) *)
      apply in_map.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
      assumption.
Qed.

Lemma sub_terms_strict_strict (t: term) :
  ~ In t (sub_terms_strict t).
Proof.
(* Goal: forall _ : @PPO variable function constructor rank (@term_from_value variable function constructor v) (@term_from_value variable function constructor v'), lt (@value_size constructor v) (@value_size constructor v') *)
  clear.
  destruct t as [ | c lt | f lt ];
  try (simpl; tauto).

  - assert (Hobv: Forall (fun t => term_size t < term_size (capply c lt)) lt).
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
    {
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
      simpl.
      induction lt as [ | t lt IH ];
        [ intros; constructor | idtac ].
(* Goal: @Forall (Syntax.term variable function constructor) (fun t0 : Syntax.term variable function constructor => Peano.lt (@term_size variable function constructor t0) (S (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) (@cons (Syntax.term variable function constructor) t lt))))) (@cons (Syntax.term variable function constructor) t lt) *)
      constructor.
      - simpl; omega.
      - rewrite Forall_forall in IH.
(* Goal: @Forall (Syntax.term variable function constructor) (fun t0 : Syntax.term variable function constructor => Peano.lt (@term_size variable function constructor t0) (S (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) (@cons (Syntax.term variable function constructor) t lt))))) lt *)
        rewrite Forall_forall.
(* Goal: forall (x : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) x lt), Peano.lt (@term_size variable function constructor x) (S (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) (@cons (Syntax.term variable function constructor) t lt)))) *)
        intros t' Hin.
(* Goal: Peano.lt (@term_size variable function constructor t') (S (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) (@cons (Syntax.term variable function constructor) t lt)))) *)
        apply lt_le_trans with (m := S (suml (map (@term_size _ _ _) lt))).
        + apply IH; assumption.
        + simpl; omega.
    }
(* Goal: forall _ : @In (Syntax.term variable function constructor) t1 (sub_terms_strict t2), lt (@term_size variable function constructor t1) (@term_size variable function constructor t2) *)
    intros Hin.
(* Goal: False *)
    generalize Hin; simpl; intros Hsub.
(* Goal: False *)
    apply in_flat_map in Hsub.
(* Goal: False *)
    destruct Hsub as ( t & Hinlt & Hint ).
(* Goal: False *)
    apply (Forall_In_l _ Hobv) in Hinlt.
(* Goal: False *)
    apply sub_term_le_size in Hint.
(* Goal: False *)
    destruct Hint as [ Heq | Hlt ].
    + subst t.
(* Goal: False *)
      revert Hinlt.
(* Goal: forall _ : Peano.lt (@term_size variable function constructor t) (@term_size variable function constructor t), False *)
      apply lt_irrefl.
    + generalize (lt_trans _ _ _ Hinlt Hlt).
(* Goal: forall _ : Peano.lt (@term_size variable function constructor t) (@term_size variable function constructor t), False *)
      apply lt_irrefl.

  - assert (Hobv: Forall (fun t => term_size t < term_size (fapply f lt)) lt).
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
    {
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
      simpl.
      induction lt as [ | t lt IH ];
        [ intros; constructor | idtac ].
(* Goal: @Forall (Syntax.term variable function constructor) (fun t0 : Syntax.term variable function constructor => Peano.lt (@term_size variable function constructor t0) (S (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) (@cons (Syntax.term variable function constructor) t lt))))) (@cons (Syntax.term variable function constructor) t lt) *)
      constructor.
      - simpl; omega.
      - rewrite Forall_forall in IH.
(* Goal: @Forall (Syntax.term variable function constructor) (fun t0 : Syntax.term variable function constructor => Peano.lt (@term_size variable function constructor t0) (S (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) (@cons (Syntax.term variable function constructor) t lt))))) lt *)
        rewrite Forall_forall.
(* Goal: forall (x : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) x lt), Peano.lt (@term_size variable function constructor x) (S (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) (@cons (Syntax.term variable function constructor) t lt)))) *)
        intros t' Hin.
(* Goal: Peano.lt (@term_size variable function constructor t') (S (suml (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) (@cons (Syntax.term variable function constructor) t lt)))) *)
        apply lt_le_trans with (m := S (suml (map (@term_size _ _ _) lt))).
        + apply IH; assumption.
        + simpl; omega.
    }
(* Goal: forall _ : @In (Syntax.term variable function constructor) t1 (sub_terms_strict t2), lt (@term_size variable function constructor t1) (@term_size variable function constructor t2) *)
    intros Hin.
(* Goal: False *)
    generalize Hin; simpl; intros Hsub.
(* Goal: False *)
    apply in_flat_map in Hsub.
(* Goal: False *)
    destruct Hsub as ( t & Hinlt & Hint ).
(* Goal: False *)
    apply (Forall_In_l _ Hobv) in Hinlt.
(* Goal: False *)
    apply sub_term_le_size in Hint.
(* Goal: False *)
    destruct Hint as [ Heq | Hlt ].
    + subst t.
(* Goal: False *)
      revert Hinlt.
(* Goal: forall _ : Peano.lt (@term_size variable function constructor t) (@term_size variable function constructor t), False *)
      apply lt_irrefl.
    + generalize (lt_trans _ _ _ Hinlt Hlt).
(* Goal: forall _ : Peano.lt (@term_size variable function constructor t) (@term_size variable function constructor t), False *)
      apply lt_irrefl.
Qed.

Lemma sub_term_strict_lt_size (t1 t2: term) :
   In t1 (sub_terms_strict t2) -> term_size t1 < term_size t2.
Proof.
(* Goal: forall _ : @PPO variable function constructor rank (@term_from_value variable function constructor v) (@term_from_value variable function constructor v'), lt (@value_size constructor v) (@value_size constructor v') *)
  clear.
(* Goal: forall _ : @In (Syntax.term variable function constructor) t1 (sub_terms_strict t2), lt (@term_size variable function constructor t1) (@term_size variable function constructor t2) *)
  intros Hin.
(* Goal: lt (@term_size variable function constructor t1) (@term_size variable function constructor t2) *)
  generalize Hin; intros Hsize.
(* Goal: lt (@term_size variable function constructor t1) (@term_size variable function constructor t2) *)
  apply sub_term_strict_incl, sub_term_le_size in Hsize.
(* Goal: lt (@term_size variable function constructor t1) (@term_size variable function constructor t2) *)
  destruct Hsize as [ Heq | Hlt ]; [ idtac | assumption ].

(* Goal: lt (@term_size variable function constructor t1) (@term_size variable function constructor t2) *)
  exfalso.
(* Goal: False *)
  subst t2.
(* Goal: False *)
  revert Hin.
(* Goal: forall _ : @In (Syntax.term variable function constructor) t1 (sub_terms_strict t1), False *)
  apply sub_terms_strict_strict.
Qed.

Lemma PPO_value_is_sub_term (t v: term) :
  @term_value _ _ _ v ->
  (PPO rank t v <-> In t (sub_terms_strict v)).
Proof.
(* Goal: forall _ : @PPO variable function constructor rank (@term_from_value variable function constructor v) (@term_from_value variable function constructor v'), lt (@value_size constructor v) (@value_size constructor v') *)
  clear.
(* Goal: forall _ : @term_value variable function constructor v, iff (@PPO variable function constructor rank t v) (@In (Syntax.term variable function constructor) t (sub_terms_strict v)) *)
  intros Hval.
(* Goal: and (@In function f0 (@functions_of_prog variable function constructor prog)) (@In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor f0 sa) (all_possible_subarguments lt))) *)
  split.

  - (* PPO → sous-terme *)
(* Goal: forall _ : @In (Syntax.term variable function constructor) t (sub_terms_strict v), @PPO variable function constructor rank t v *)
    revert t Hval.
    induction v as [ | c lt IH | ] using term_ind2;
      try (simpl; intros; exfalso; assumption).
(* Goal: forall (t : Syntax.term variable function constructor) (_ : @term_value variable function constructor (@capply variable function constructor c lt)) (_ : @PPO variable function constructor rank t (@capply variable function constructor c lt)), @In (Syntax.term variable function constructor) t (sub_terms_strict (@capply variable function constructor c lt)) *)
    intros t Hval Hppo.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
    inversion Hppo as [ aa ab ac Hin ae af | | aa t' ac ad Hin Hppo2 ag ah | | | | ]; subst; simpl.

    + apply in_flat_map.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
      exists t; split; try assumption.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
      destruct t; simpl; tauto.

    + apply in_flat_map.
(* Goal: @ex (Syntax.term variable function constructor) (fun x : Syntax.term variable function constructor => and (@In (Syntax.term variable function constructor) x lt) (@In (Syntax.term variable function constructor) t (sub_terms x))) *)
      exists t'.
(* Goal: and (@In (Syntax.term variable function constructor) t' lt) (@In (Syntax.term variable function constructor) t (sub_terms t')) *)
      split; [ assumption | idtac ].
(* Goal: @In (Syntax.term variable function constructor) t (sub_terms t') *)
      apply sub_term_strict_incl.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
      apply IH; try assumption.
(* Goal: @term_value variable function constructor t' *)
      apply andl_in with (l := map (@term_value _ _ _) lt); [ assumption | idtac ].
(* Goal: @In (list (Syntax.term variable function constructor)) (@cons (Syntax.term variable function constructor) x l) (@map (list (Syntax.term variable function constructor)) (list (Syntax.term variable function constructor)) (fun sa : list (Syntax.term variable function constructor) => @cons (Syntax.term variable function constructor) x sa) (all_possible_subarguments l')) *)
      apply in_map.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
      assumption.

  - (* sous-terme → PPO *)
(* Goal: forall _ : @In (Syntax.term variable function constructor) t (sub_terms_strict v), @PPO variable function constructor rank t v *)
    revert t Hval.
    induction v as [ | c lt IH | ] using term_ind2;
      intros t Hval Hin; try (simpl in Hval; exfalso; assumption).
(* Goal: @PPO variable function constructor rank t (@capply variable function constructor c lt) *)
    simpl in Hin.
(* Goal: @PPO variable function constructor rank t (@capply variable function constructor c lt) *)
    apply in_flat_map in Hin.
(* Goal: @PPO variable function constructor rank t (@capply variable function constructor c lt) *)
    destruct Hin as ( t' & Hint' & Hin ).
(* Goal: @PPO variable function constructor rank t (@capply variable function constructor c lt) *)
    apply sub_term_eq_or_strict in Hin.
    destruct Hin as [ Heq | Hin ];
      [ subst; constructor; assumption | idtac ].
(* Goal: @PPO variable function constructor rank t (@capply variable function constructor c lt) *)
    apply ppo_constr_sub with (t := t'); [ assumption | idtac ].
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
    apply IH; try assumption.
(* Goal: @term_value variable function constructor t' *)
    apply andl_in with (l := map (@term_value _ _ _) lt); [ assumption | idtac ].
(* Goal: @In (list (Syntax.term variable function constructor)) (@cons (Syntax.term variable function constructor) x l) (@map (list (Syntax.term variable function constructor)) (list (Syntax.term variable function constructor)) (fun sa : list (Syntax.term variable function constructor) => @cons (Syntax.term variable function constructor) x sa) (all_possible_subarguments l')) *)
    apply in_map.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
    assumption.
Qed.

Lemma PPO_value_lt_size (v v': value) :
  PPO rank (@term_from_value variable function constructor v) (@term_from_value _ _ _ v') ->
  value_size v < value_size v'.
Proof.
(* Goal: forall _ : @PPO variable function constructor rank (@term_from_value variable function constructor v) (@term_from_value variable function constructor v'), lt (@value_size constructor v) (@value_size constructor v') *)
  clear.
  do 2 rewrite <- (compatible_sizes variable function).
(* Goal: forall _ : @PPO variable function constructor rank (@term_from_value variable function constructor v) (@term_from_value variable function constructor v'), lt (@term_size variable function constructor (@term_from_value variable function constructor v)) (@term_size variable function constructor (@term_from_value variable function constructor v')) *)
  set (t := @term_from_value _ _ _ v).
(* Goal: forall _ : @PPO variable function constructor rank t (@term_from_value variable function constructor v'), lt (@term_size variable function constructor t) (@term_size variable function constructor (@term_from_value variable function constructor v')) *)
  set (t' := @term_from_value _ _ _ v').
(* Goal: forall _ : @PPO variable function constructor rank t t', lt (@term_size variable function constructor t) (@term_size variable function constructor t') *)
  intros Hppo.
(* Goal: lt (@term_size variable function constructor t) (@term_size variable function constructor t') *)
  apply sub_term_strict_lt_size.
(* Goal: @In (Syntax.term variable function constructor) t (sub_terms_strict t') *)
  apply PPO_value_is_sub_term; [ | assumption ].
(* Goal: @term_value variable function constructor (@term_from_value variable function constructor xx) *)
  apply term_value_eqv.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
  exists v'; trivial.
Qed.

Fixpoint all_possible_subarguments (args: list term) : list (list term) :=
  match args with
    | [] => [[]]
    | (x::xs) => let psa := all_possible_subarguments xs in
                let pst := sub_terms x in
                flat_map (fun st => map (fun sa => st::sa) psa) pst
  end.

Lemma length_sub_terms a : length (sub_terms a) = term_size a.
Proof.
  induction a using term_ind2;
    try(simpl;
      rewrite length_flat_map;
      replace (map (length (A:=term)) (map sub_terms l)) with (map (term_size (constructor:=constructor)) l);
        [trivial |

        rewrite map_map;
        apply map_in_ext;
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
        intros; rewrite H ]) ; auto.
Qed.

Lemma all_possible_subarguments_length (args: list term) :
  length (all_possible_subarguments args) = prodl (map (@term_size _ _ _) args).
Proof.
  induction args.
  - trivial.

  - simpl prodl.
    rewrite <- IHargs.
    simpl all_possible_subarguments.
    rewrite length_flat_map.
    rewrite map_map.
    erewrite map_ext.
    + rewrite <- length_sub_terms.
      rewrite suml_map_const; apply mult_comm.

    + intro. apply map_length.
Qed.

Definition all_possible_sub_activation_same_rank (f: function) (lv: list term) : list term :=
  let psa := all_possible_subarguments lv in
  flat_map (fun g => map (fun sa => fapply g sa) psa) (functions_of_prog prog).

Lemma all_possible_sub_activation_same_rank_bound (f: function) (lv: list term) :
  length (all_possible_sub_activation_same_rank f lv)
  <= length (functions_of_prog prog) * prodl (map (@term_size _ _ _) lv).
Proof.
(* Goal: @In (Syntax.term variable function constructor) (@proj_left variable function constructor p') (all_possible_sub_activation_same_rank f lt) *)
  unfold all_possible_sub_activation_same_rank.
  rewrite length_flat_map.
  erewrite <- map_length.
  rewrite map_map.
  apply suml_le_len_times_bound.
  intros n Hn.
  apply in_map_iff in Hn.
  destruct Hn as (g & Hgn & Hg).
  rewrite <- Hgn.
(* Goal: le (@length nat (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt)) max_arity *)
  rewrite map_length.
  rewrite all_possible_subarguments_length.
  apply le_n.
Qed.

Lemma all_possible_subarguments_self lt : lt ∈ all_possible_subarguments lt.
Proof.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
induction lt; simpl.
- tauto.

- apply in_flat_map; exists a.
(* Goal: and (@In function f0 (@functions_of_prog variable function constructor prog)) (@In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor f0 sa) (all_possible_subarguments lt))) *)
  split.
  + case a; simpl; tauto.

  + apply in_map_iff; exists lt; tauto.
Qed.

Lemma sub_terms_self a : In a (sub_terms a).
Proof.
(* Goal: @In (Syntax.term variable function constructor) a (sub_terms a) *)
clear subst_default.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
destruct a; simpl; tauto.
Qed.

Lemma PPO_value_all_possible_subarguments l lv:
  (forall x, In x lv -> term_value x) ->
  Forall2 (clos_refl (PPO rank)) l lv ->  l ∈ all_possible_subarguments lv.
Proof.
(* Goal: forall (_ : forall (x : Syntax.term variable function constructor) (_ : @In (Syntax.term variable function constructor) x lv), @term_value variable function constructor x) (_ : @Forall2 (Syntax.term variable function constructor) (Syntax.term variable function constructor) (@clos_refl (Syntax.term variable function constructor) (@PPO variable function constructor rank)) l lv), @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments lv) *)
intros Hvalue HPPO.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments lv) *)
induction HPPO.
- simpl; tauto.

- simpl.
(* Goal: @In (list (Syntax.term variable function constructor)) (@cons (Syntax.term variable function constructor) x l) (@flat_map (Syntax.term variable function constructor) (list (Syntax.term variable function constructor)) (fun st : Syntax.term variable function constructor => @map (list (Syntax.term variable function constructor)) (list (Syntax.term variable function constructor)) (fun sa : list (Syntax.term variable function constructor) => @cons (Syntax.term variable function constructor) st sa) (all_possible_subarguments l')) (sub_terms y)) *)
  apply in_flat_map; exists x.
(* Goal: and (@In function f0 (@functions_of_prog variable function constructor prog)) (@In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor f0 sa) (all_possible_subarguments lt))) *)
  split.
  + destruct H.
    * apply sub_term_strict_incl, PPO_value_is_sub_term; [apply Hvalue|]; simpl; tauto.

    * subst x; apply sub_terms_self; trivial.

  + apply in_map.
     auto with *.
Qed.

  (* Toute activation de même rang doit être un « sous-terme » *)
Lemma  all_possible_sub_activation_same_rank_spec p' i s p c1 f lt c2 v:
  PPO_prog -> 
  let proof_tree := cbv_update i s p c1 (fapply f lt) c2 v in
  wf proof_tree ->
  In p' (activations proof_tree) ->
  activation_rank rank p' = rank f ->
  In (proj_left p') (all_possible_sub_activation_same_rank f lt).
Proof.
(* Goal: forall _ : @Ordering.PPO_prog variable function constructor prog rank, let proof_tree := @cbv_update variable function constructor i s p c1 (@fapply variable function constructor f lt) c2 v in forall (_ : @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)) (_ : @eq nat (@activation_rank variable function constructor rank p') (rank f)), @In (Syntax.term variable function constructor) (@proj_left variable function constructor p') (all_possible_sub_activation_same_rank f lt) *)
intros HPPO proof_tree Hwf Hin Hrank.
(* Goal: @In (Syntax.term variable function constructor) (@proj_left variable function constructor p') (all_possible_sub_activation_same_rank f lt) *)
unfold all_possible_sub_activation_same_rank.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) (Nat.eqb (rank f) (@activation_rank variable function constructor rank p')) *)
assert (Hwf' : wf p') by (apply (activations_wf Hwf) ; trivial).
(* Goal: @In (Syntax.term variable function constructor) (@proj_left variable function constructor p') (@flat_map function (Syntax.term variable function constructor) (fun g : function => @map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor g sa) (all_possible_subarguments lt)) (@functions_of_prog variable function constructor prog)) *)
generalize Hin; intro Hpact.
assert (Hppo : p' = proof_tree \/ PPO rank (proj_left p') (proj_left proof_tree)) by
  (unfold proof_tree; eapply PPO_activations; eauto).
(* Goal: @eq nat (@activation_rank variable function constructor rank p') (rank f) *)
apply activation_is_function in Hpact.
(* Goal: @eq nat (@activation_rank variable function constructor rank p') (rank f) *)
destruct Hpact as (i' & s' & p'' & c1' & t'' & c2' & v'' & Heq).
(* Goal: @eq nat (@activation_rank variable function constructor rank p') (rank f) *)
subst p'.
simpl in *.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
destruct t''; try tauto.
(* Goal: @In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@flat_map function (Syntax.term variable function constructor) (fun g : function => @map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor g sa) (all_possible_subarguments lt)) (@functions_of_prog variable function constructor prog)) *)
apply in_flat_map; exists f0.
(* Goal: and (@In function f0 (@functions_of_prog variable function constructor prog)) (@In (Syntax.term variable function constructor) (@fapply variable function constructor f0 l) (@map (list (Syntax.term variable function constructor)) (Syntax.term variable function constructor) (fun sa : list (Syntax.term variable function constructor) => @fapply variable function constructor f0 sa) (all_possible_subarguments lt))) *)
split.
- replace f0 with (activation_function f0 (cbv_update i' s' p'' c1' (fapply f0 l) c2' v'')) by trivial.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
  apply all_functions_in_prog with proof_tree; assumption.

- apply in_map_iff; exists l.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
  split; trivial.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments lt) *)
  destruct Hppo as [Heq | Hppo].
  + inversion Heq; subst.
(* Goal: @In (list (Syntax.term variable function constructor)) lt (all_possible_subarguments lt) *)
    apply all_possible_subarguments_self.

  + destruct Hwf as (_ & l' & tt & _ & _ & Hl' & _); subst lt.
(* Goal: le (rank g) (rank f) *)
    inversion Hppo; subst.
    * apply in_map_iff in H1.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
       destruct H1 as (v' & Heqv' & Hinv').
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
       destruct v'.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
       inversion Heqv'.

    *  apply in_map_iff in H2.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
       destruct H2 as (v' & Heqv' & Hinv').
(* Goal: @In (Syntax.term variable function constructor) t (all_possible_sub_activation_same_rank f lt) *)
       subst t.
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
       contradict H3.
(* Goal: not (@PPO variable function constructor rank (@fapply variable function constructor f0 l) (@term_from_value variable function constructor v')) *)
       apply fapply_not_PPO_value.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
       apply term_value_eqv; eauto.

    * omega.

(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
    * { (* cas principal *)
(* Goal: @In (list (Syntax.term variable function constructor)) l (all_possible_subarguments (@map (Syntax.value constructor) (Syntax.term variable function constructor) (@term_from_value variable function constructor) (@map (pattern variable constructor) (Syntax.value constructor) (@psubst variable constructor s) l'))) *)
        apply PPO_value_all_possible_subarguments.
        - intros x Hx.
(* Goal: @term_value variable function constructor x *)
           apply in_map_iff in Hx.
(* Goal: @term_value variable function constructor x *)
           destruct Hx as (xx & Heq & Hxx).
(* Goal: le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
           subst x.
(* Goal: @term_value variable function constructor (@term_from_value variable function constructor xx) *)
           apply term_value_eqv.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
           eauto.

        - apply product_Forall2; trivial.
      }
Qed.

Definition bobby_eight_poly x := length (functions_of_prog prog) * Nat.pow x max_arity.

(* lemma 64 *)
Lemma bobby_eight i s p c1 f lt c2 v:
  let proof_tree := cbv_update i s p c1 (fapply f lt) c2 v in
  PPO_prog -> wf proof_tree ->
  length (activations_at_rank (rank f) proof_tree) <=
  bobby_eight_poly (term_size (proj_left proof_tree)).
Proof.
(* Goal: let proof_tree := @cbv_update variable function constructor i s p c1 (@fapply variable function constructor f lt) c2 v in forall (_ : @Ordering.PPO_prog variable function constructor prog rank) (_ : @CBV_cache.wf variable function constructor variable_eq_dec function_eq_dec constructor_eq_dec rule_default prog max_arity proof_tree), le (@length (CBV_cache.cbv variable function constructor) (activations_at_rank (rank f) proof_tree)) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor proof_tree))) *)
intros proof_tree HPPO Hwf.

(* Goal: le (@length (CBV_cache.cbv variable function constructor) (activations_at_rank (rank f) proof_tree)) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor proof_tree))) *)
unfold activations_at_rank.

(* Goal: le (@length (CBV_cache.cbv variable function constructor) (@filter (CBV_cache.cbv variable function constructor) (fun p : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank p)) (@activations variable function constructor proof_tree))) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor proof_tree))) *)
transitivity (length (all_possible_sub_activation_same_rank f lt)).
- replace (length (filter (fun g : cbv => rank f =? activation_rank rank g) (activations proof_tree))) with
  (length (filter (fun t => rank f =? match t with 
    | fapply g _ => rank g
    | _ => 0 end) (map (fun p => proj_left p) (activations proof_tree)))).
  + apply NoDup_incl_le_length.
(* Goal: @NoDup (Syntax.term variable function constructor) (@filter (Syntax.term variable function constructor) (fun t : Syntax.term variable function constructor => Nat.eqb (rank f) match t with | var y => O | capply y l => O | fapply g l => rank g end) (@map (CBV_cache.cbv variable function constructor) (Syntax.term variable function constructor) (fun p : CBV_cache.cbv variable function constructor => @proj_left variable function constructor p) (@activations variable function constructor proof_tree))) *)
(* Goal: @incl (Syntax.term variable function constructor) (@filter (Syntax.term variable function constructor) (fun t : Syntax.term variable function constructor => Nat.eqb (rank f) match t with | var y => O | capply y l => O | fapply g l => rank g end) (@map (CBV_cache.cbv variable function constructor) (Syntax.term variable function constructor) (fun p : CBV_cache.cbv variable function constructor => @proj_left variable function constructor p) (@activations variable function constructor proof_tree))) (all_possible_sub_activation_same_rank f lt) *)
    apply NoDup_filter.
    * apply NoDup_left_activations; trivial.

    * intros t Ht.
(* Goal: @In (Syntax.term variable function constructor) t (all_possible_sub_activation_same_rank f lt) *)
       apply filter_In in Ht; destruct Ht as (Hin & Hrank).
(* Goal: @In (Syntax.term variable function constructor) t (all_possible_sub_activation_same_rank f lt) *)
       apply in_map_iff in Hin; destruct Hin as (p' & Hp' & Hpact).
(* Goal: @In (Syntax.term variable function constructor) t (all_possible_sub_activation_same_rank f lt) *)
       subst t.
(* Goal: @In (CBV_cache.cbv variable function constructor) p' (@activations variable function constructor p) *)
       eapply all_possible_sub_activation_same_rank_spec; eauto.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) (Nat.eqb (rank f) (@activation_rank variable function constructor rank p')) *)
       assert (Hwf' : wf p') by (apply (activations_wf Hwf) ; trivial).
(* Goal: @eq nat (@activation_rank variable function constructor rank p') (rank f) *)
       apply activation_is_function in Hpact.
(* Goal: @eq nat (@activation_rank variable function constructor rank p') (rank f) *)
       destruct Hpact as (i' & s' & p'' & c1' & t'' & c2' & v'' & Heq).
(* Goal: @eq nat (@activation_rank variable function constructor rank p') (rank f) *)
       subst p'.
       simpl in *.
(* Goal: or (@eq (list (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor)) (@nil (Syntax.term variable function constructor))) False *)
       destruct t''; try tauto.
(* Goal: @eq nat (rank f0) (rank f) *)
       clear Hwf'.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
       apply beq_nat_true in Hrank; symmetry; assumption.

  + rewrite <- length_filter.
(* Goal: @eq nat (@length (CBV_cache.cbv variable function constructor) (@filter (CBV_cache.cbv variable function constructor) (fun x : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) match @proj_left variable function constructor x with | var y => O | capply y l => O | fapply g l => rank g end) (@activations variable function constructor proof_tree))) (@length (CBV_cache.cbv variable function constructor) (@filter (CBV_cache.cbv variable function constructor) (fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) (@activations variable function constructor proof_tree))) *)
    erewrite filter_ext_In; [reflexivity|].
(* Goal: forall (a : CBV_cache.cbv variable function constructor) (_ : @In (CBV_cache.cbv variable function constructor) a (@activations variable function constructor proof_tree)), @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor a with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) a) *)
    intros p' Hin.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
    simpl.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) (Nat.eqb (rank f) (@activation_rank variable function constructor rank p')) *)
    assert (Hwf' : wf p') by (apply (activations_wf Hwf) ; trivial). 
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) (Nat.eqb (rank f) (@activation_rank variable function constructor rank p')) *)
    apply activation_is_function in Hin.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) (Nat.eqb (rank f) (@activation_rank variable function constructor rank p')) *)
   destruct Hin as (i' & s' & p'' & c1' & t'' & c2' & v'' & Heq).
(* Goal: @eq (list A) (@nil A) (@nil A) *)
   subst; simpl; trivial.

- transitivity (length (functions_of_prog prog) * prodl (map (@term_size _ _ _) lt));
    [(apply all_possible_sub_activation_same_rank_bound)|].
(* Goal: le (bobby_eight_poly x) (bobby_eight_poly y) *)
  unfold bobby_eight_poly.
(* Goal: le (Init.Nat.mul (@length function (@functions_of_prog variable function constructor prog)) (prodl (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt))) (Init.Nat.mul (@length function (@functions_of_prog variable function constructor prog)) (Nat.pow (@term_size variable function constructor (@proj_left variable function constructor proof_tree)) max_arity)) *)
  apply mult_le_compat_l.
(* Goal: le (prodl (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt)) (Nat.pow (@term_size variable function constructor (@proj_left variable function constructor proof_tree)) max_arity) *)
  transitivity (term_size (proj_left proof_tree) ^ (length (map (term_size (constructor:=constructor)) lt))).
  + apply prodl_bound.
(* Goal: forall (x : nat) (_ : @In nat x (@map (Syntax.term variable function constructor) nat (@term_size variable function constructor) lt)), le x (@term_size variable function constructor (@proj_left variable function constructor proof_tree)) *)
    intros x Hx.
(* Goal: @eq bool (Nat.eqb (rank f) match @proj_left variable function constructor p' with | var y => O | capply y l => O | fapply g l => rank g end) ((fun g : CBV_cache.cbv variable function constructor => Nat.eqb (rank f) (@activation_rank variable function constructor rank g)) p') *)
    unfold proof_tree; simpl.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
    apply le_S, in_le_suml; trivial.

  + apply Nat.pow_le_mono_r.
    * pose (gt_term_size_O (proj_left proof_tree)); omega.

    * rewrite map_length.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
       unfold proof_tree in Hwf.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
       simpl in Hwf.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
       decompose record Hwf.
(* Goal: le (@length (Syntax.term variable function constructor) lt) max_arity *)
       assumption.
Qed.

Lemma bobby_increase:
  forall x y, x <= y -> (bobby_eight_poly x) <= (bobby_eight_poly y).
Proof.
(* Goal: forall (x : nat) (_ : @In nat x (@map (CBV_cache.cbv variable function constructor) nat (fun pi : CBV_cache.cbv variable function constructor => bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor pi))) (@activations variable function constructor proof_tree))), le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
intros.
(* Goal: le (bobby_eight_poly x) (bobby_eight_poly y) *)
unfold bobby_eight_poly.
(* Goal: le (Init.Nat.mul (@length function (@functions_of_prog variable function constructor prog)) (Nat.pow x max_arity)) (Init.Nat.mul (@length function (@functions_of_prog variable function constructor prog)) (Nat.pow y max_arity)) *)
apply Mult.mult_le_compat_l.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
apply pow_le_compat;trivial.
Qed.

(* Theorem 65 *)
Theorem A_T_bound i s p c1 f lt c2 v: 
  let proof_tree := cbv_update i s p c1 (fapply f lt) c2 v in
  PPO_prog -> wf proof_tree ->
  A_T proof_tree <= bobby_eight_poly (max_active_size proof_tree).
Proof.
(* Goal: forall (x : nat) (_ : @In nat x (@map (CBV_cache.cbv variable function constructor) nat (fun pi : CBV_cache.cbv variable function constructor => bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor pi))) (@activations variable function constructor proof_tree))), le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
intros.
(* Goal: le (A_T proof_tree) (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
unfold A_T.
(* Goal: le (maxl (@map (CBV_cache.cbv variable function constructor) nat (fun p : CBV_cache.cbv variable function constructor => @length (CBV_cache.cbv variable function constructor) (activations_at_rank (@activation_rank variable function constructor rank p) p)) (@activations variable function constructor proof_tree))) (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
apply le_trans with (m:=maxl (map (fun pi => bobby_eight_poly (term_size (proj_left pi))) (activations proof_tree))).
- apply maxl_le_maxl.
(* Goal: forall (x : nat) (_ : @In nat x (@map (CBV_cache.cbv variable function constructor) nat (fun pi : CBV_cache.cbv variable function constructor => bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor pi))) (@activations variable function constructor proof_tree))), le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
  intros.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (activations_at_rank (@activation_rank variable function constructor rank x) x)) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor x))) *)
  assert (wf x).
  + apply activations_wf with (proof_tree := proof_tree);trivial.
  + apply activation_is_function in H1.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (activations_at_rank (@activation_rank variable function constructor rank x) x)) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor x))) *)
    destruct H1 as (i0 & s0 & p' & c0 & t & c3 & v0 & x_is_upd).
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (activations_at_rank (@activation_rank variable function constructor rank x) x)) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor x))) *)
    unfold activation_rank.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (activations_at_rank match x with | cbv_constr l c t c0 v => O | cbv_split l c c0 t c1 v => O | cbv_update n v c c0 (var v1 as t) c1 v0 => O | cbv_update n v c c0 (capply c2 l as t) c1 v0 => O | cbv_update n v c c0 (fapply f l as t) c1 v0 => rank f | cbv_read c t v => O end x)) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor x))) *)
    destruct x;try discriminate.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (activations_at_rank match t0 with | var v => O | capply c l => O | fapply f l => rank f end (@cbv_update variable function constructor n v1 x c t0 c4 v2))) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor (@cbv_update variable function constructor n v1 x c t0 c4 v2)))) *)
    simpl in H2.
(* Goal: le (@length (CBV_cache.cbv variable function constructor) (activations_at_rank match t0 with | var v => O | capply c l => O | fapply f l => rank f end (@cbv_update variable function constructor n v1 x c t0 c4 v2))) (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor (@cbv_update variable function constructor n v1 x c t0 c4 v2)))) *)
    destruct t0.
    * exfalso;trivial.
    * exfalso;trivial.
    * apply bobby_eight;trivial.
- apply all_max_le.
(* Goal: forall (x : nat) (_ : @In nat x (@map (CBV_cache.cbv variable function constructor) nat (fun pi : CBV_cache.cbv variable function constructor => bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor pi))) (@activations variable function constructor proof_tree))), le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
  intros.
(* Goal: le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
  apply in_map_iff in H1.
(* Goal: le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
  destruct H1 as (x0 & bob & act).
(* Goal: le x (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
  subst x.
(* Goal: le (bobby_eight_poly (@term_size variable function constructor (@proj_left variable function constructor x0))) (bobby_eight_poly (@max_active_size variable function constructor proof_tree)) *)
  apply bobby_increase.
  apply le_trans with (m:= (term_size (proj_left x0)) + (value_size (proj_right x0))).
  + apply Plus.le_plus_l.
  + apply le_max_active_size;trivial.
Qed.

End Bounds.
