From Undecidability Require Import TM.Prelim TM.Relations.
From Undecidability.L Require Import LM_heap_def.

Require Import FunInd.

Fixpoint sum (A:list nat) :=
  match A with
    [] => 0
  | a::A => a + sum A
  end.

Lemma sum_app A B : sum (A++B) = sum A + sum B.
Proof.
  induction A;cbn;omega.
Qed.

Hint Rewrite sum_app : list.

Definition sizeT t :=
    match t with
      varT n => 1 + n
    | _ => 1
    end.

Definition sizeP (P:Pro) := 1 + sum (map sizeT P).
Hint Unfold sizeP.

Section Analysis.

  Variable T V : list HClos.
  Variable H: list HEntr.

  Lemma jumpTarget_eq c c0 c1 c2: jumpTarget 0 c0 c = Some (c1,c2) -> c1++[retT]++c2=c0++c.
  Proof.
    generalize 0 as k.
    induction c as [ |[]] in c1,c2,c0|-*;cbn. congruence.
    all:intros ? H'.
    4:destruct k;[inv H';congruence| ].
    all:apply IHc in H'.
    all:autorewrite with list in *.
    all:now cbn in *.
  Qed.


  Variable i : nat.

  Variable P0 : Pro.
  Hypothesis R: pow step i ([(0,P0)],[],[None]) (T,V,H).

  Lemma size_clos P a : ((a,P) el (T++V) -> sizeP P <= sizeP P0 /\ a <= length H)
                        /\ (forall beta, Some ((a,P),beta) el H -> sizeP P <= sizeP P0 /\ a <= length H /\ beta <= length H).
  Proof.
    unfold sizeP.
    induction i in T,V,H,R,P,a|-*.
    -inv R. split.
     +intros [[= <- <-]|[]].
      eauto using Nat.le_0_l.
     +intros ? [H|[]]. inv H.
    -
  Admitted.

  Lemma length_H : length H <= 1+i.
  Proof.
    induction i in T,V,H,R|-*.
    -inv R. cbn;omega.
    -replace (S n) with (n + 1) in R by omega.
  Admitted.

  Lemma length_TV : length T + length V <= 1+i.
  Proof.
    induction i in T,V,H,R|-*.
    -inv R. cbn;omega.
    -replace (S n) with (n + 1) in R by omega.
  Admitted.


End Analysis.