(* File: NWeight.v  (last edited on 27/10/2000) (c) Klaus Weich  *)

Require Export Lt.
Require Export Le.
Require Export Regular_Avl.
Require Export Le_Ks.


(*********************************************************************)


Fixpoint nweight (a : form) : nat :=
  match a with
  | Atom _ => 0
  | Falsum => 0
  | AndF a0 a1 => S (nweight a0 + nweight a1)
  | OrF a0 a1 => S (nweight a0 + nweight a1)
  | Imp a0 a1 => S (nweight a0 + nweight a1)
  end.


(******************************************************************)




Definition nweight_work :=
  fold_right (fun (a : normal_form) (n : nat) => nweight (nf2form a) + n) 0.


Remark nweight_work_app :
 forall bs work : nf_list,
 nweight_work (bs ++ work) = nweight_work bs + nweight_work work.
(* Goal: forall bs work : nf_list, @eq nat (nweight_work (@app normal_form bs work)) (Nat.add (nweight_work bs) (nweight_work work)) *)
intros bs work; elim bs; clear bs.
(* Goal: le (S (Nat.add W (Nat.add ds n))) (Nat.add (S W) (Nat.add ds n)) *)
simpl in |- *; trivial.
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : @eq nat (nweight_work (@app normal_form l work)) (Nat.add (nweight_work l) (nweight_work work))), @eq nat (nweight_work (@app normal_form (@cons normal_form a l) work)) (Nat.add (nweight_work (@cons normal_form a l)) (nweight_work work)) *)
intros b bs ih.
(* Goal: le (S (nweight_work (@cons normal_form b bs))) (nweight_bs (@cons normal_form b bs)) *)
unfold nweight_work in |- *.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: @eq nat (S (Nat.add (nweight_work work) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (S (Nat.add (nweight_ds ds) n))) *)
fold nweight_work in |- *.
(* Goal: @eq nat (Nat.add (nweight (nf2form b)) (nweight_work (@app normal_form bs work))) (Nat.add (Nat.add (nweight (nf2form b)) (nweight_work bs)) (nweight_work work)) *)
 rewrite ih.
(* Goal: @eq nat (Nat.add x (Nat.add ni ai)) (Nat.add (Nat.add x ni) ai) *)
apply plus_assoc.
Qed.



Definition nweight_disj (d : disj) := nweight (disj2form d).
Definition nweight_ds :=
  fold_right (fun (d : disj) (n : nat) => nweight_disj d + n) 0.


Definition nweight_nestedimp (x : nested_imp) := nweight (nested_imp2form x).
Definition nweight_ni :=
  fold_right (fun (x : nested_imp) (n : nat) => nweight_nestedimp x + n) 0.


Definition nweight_decoratednestedimp (x : decorated_nested_imp) :=
  match x with
  | (x0, _) => nweight (nimp2form x0)
  end.

Definition nweight_dni :=
  fold_right
    (fun (x : decorated_nested_imp) (n : nat) =>
     nweight_decoratednestedimp x + n) 0.


Definition nweight_atomicimp (a : normal_form) := S (nweight (nf2form a)).
Definition nweight_bs :=
  fold_right (fun (b : normal_form) (n : nat) => nweight_atomicimp b + n) 0.
Definition nweight_ibs (x : Int * nf_list) :=
  match x with
  | (_, bs) => nweight_bs bs
  end.

Definition nweight_ai (ai : atomic_imps) :=
  fold_right (fun (x : Int * nf_list) (n : nat) => nweight_ibs x + n) 0
    (LIN_AVL nf_list ai).


(***************************************************************************)


Remark nweight_ai_perm :
 forall (l0 l1 : list (Int * nf_list)) (x : Int * nf_list),
 fold_right (fun (x : Int * nf_list) (n : nat) => nweight_ibs x + n) 0
   (l0 ++ x :: l1) =
 fold_right (fun (x : Int * nf_list) (n : nat) => nweight_ibs x + n) 0
   (x :: l0 ++ l1).
(* Goal: forall (l0 l1 : list (prod Int nf_list)) (x : prod Int nf_list), @eq nat (@fold_right nat (prod Int nf_list) (fun (x0 : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x0) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) x l1))) (@fold_right nat (prod Int nf_list) (fun (x0 : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x0) n) O (@cons (prod Int nf_list) x (@app (prod Int nf_list) l0 l1))) *)
intros l0 l1 x.
(* Goal: @eq nat (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) x l1))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@cons (prod Int nf_list) x (@app (prod Int nf_list) l0 l1))) *)
apply fold_right_perm.
(* Goal: forall (i : Int) (b : normal_form) (work : nf_list) (ds : disjs) (ni : nested_imps) (ai ai' : atomic_imps) (_ : LIN_INS nf_list i (@cons normal_form b) nf_nil ai ai'), @eq nat (nweight_Sequent (@cons normal_form (AImp i b) work) ds ni ai) (nweight_Sequent work ds ni ai') *)
intros.
(* Goal: @eq nat (Nat.add (nweight_ibs a) (Nat.add (nweight_ibs b) c)) (Nat.add (nweight_ibs b) (Nat.add (nweight_ibs a) c)) *)
apply plus_permute.
Qed.


Remark nweight_ai_ins :
 forall (i : Int) (b : normal_form) (ai ai' : atomic_imps),
 LIN_INS nf_list i (cons b) nf_nil ai ai' ->
 nweight (nf2form (AImp i b)) + nweight_ai ai = nweight_ai ai'.
(* Goal: forall (i : Int) (b : normal_form) (ai ai' : atomic_imps) (_ : LIN_INS nf_list i (@cons normal_form b) nf_nil ai ai'), @eq nat (Nat.add (nweight (nf2form (AImp i b))) (nweight_ai ai)) (nweight_ai ai') *)
intros i b ai ai'.
(* Goal: forall _ : LIN_INS nf_list i (@cons normal_form b) nf_nil ai ai', @eq nat (Nat.add (nweight (nf2form (AImp i b))) (nweight_ai ai)) (nweight_ai ai') *)
elim ai; clear ai.
(* Goal: forall (t : avl_tree nf_list) (i0 : is_avl nf_list t) (_ : LIN_INS nf_list i (@cons normal_form b) nf_nil (AVL_intro nf_list t i0) ai'), @eq nat (Nat.add (nweight (nf2form (AImp i b))) (nweight_ai (AVL_intro nf_list t i0))) (nweight_ai ai') *)
elim ai'; clear ai'.
(* Goal: forall (t : avl_tree nf_list) (i0 : is_avl nf_list t) (t0 : avl_tree nf_list) (i1 : is_avl nf_list t0) (_ : LIN_INS nf_list i (@cons normal_form b) nf_nil (AVL_intro nf_list t0 i1) (AVL_intro nf_list t i0)), @eq nat (Nat.add (nweight (nf2form (AImp i b))) (nweight_ai (AVL_intro nf_list t0 i1))) (nweight_ai (AVL_intro nf_list t i0)) *)
intros t' avl_t' t avl_t.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: forall _ : lin_ins_spec nf_list i (@cons normal_form b) nf_nil t t', @eq nat (S (Nat.add (nweight (nf2form b)) (nweight_ai (AVL_intro nf_list t avl_t)))) (nweight_ai (AVL_intro nf_list t' avl_t')) *)
intro lin_ins.
(* Goal: lt (Nat.add (nweight_work bs) (nweight_ai (AVL_intro nf_list t' avl_t'))) (nweight_ai (AVL_intro nf_list t avl_t)) *)
unfold nweight_ai in |- *.
(* Goal: @eq nat (S (Nat.add (nweight (nf2form b)) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (LIN_AVL nf_list (AVL_intro nf_list t avl_t))))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (LIN_AVL nf_list (AVL_intro nf_list t' avl_t'))) *)
unfold LIN_AVL in |- *.
(* Goal: @eq nat (S (Nat.add (nweight (nf2form b)) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (lin_avl nf_list t)))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (lin_avl nf_list t')) *)
clear avl_t' avl_t.
(* Goal: @eq nat (S (Nat.add (nweight (nf2form b)) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (lin_avl nf_list t)))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (lin_avl nf_list t')) *)
inversion_clear lin_ins.
(* Goal: @eq nat (S (Nat.add (nweight (nf2form b)) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (lin_avl nf_list t)))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (lin_avl nf_list t')) *)
 rewrite H.
(* Goal: @eq nat (S (Nat.add (nweight (nf2form b)) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) (@pair Int nf_list i d) l1))))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (lin_avl nf_list t')) *)
 rewrite H0.
(* Goal: @eq nat (S (Nat.add (nweight (nf2form b)) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) (@pair Int nf_list i d) l1))))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) (@pair Int nf_list i (@cons normal_form b d)) l1))) *)
clear H H0.
transitivity
 (fold_right (fun (x : Int * nf_list) (n : nat) => nweight_ibs x + n) 0
    ((i, b :: nf_nil) :: l0 ++ l1)).
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: @eq nat (S (Nat.add (nweight (nf2form b)) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 l1)))) (S (Nat.add (Nat.add (nweight (nf2form b)) O) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 l1)))) *)
(* Goal: @eq nat (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@cons (prod Int (list normal_form)) (@pair Int (list normal_form) i (@cons normal_form b nf_nil)) (@app (prod Int nf_list) l0 l1))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) (@pair Int nf_list i (@cons normal_form b nf_nil)) l1))) *)
(* Goal: @eq nat (S (Nat.add (nweight (nf2form b)) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (lin_avl nf_list t)))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (lin_avl nf_list t')) *)
 rewrite (plus_O (nweight (nf2form b))).
(* Goal: @eq nat (Nat.add (nweight_ni ni2) n) (Nat.add (nweight_ni ni2) n) *)
trivial.
symmetry  in |- *.
(* Goal: @eq nat (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) (@pair Int nf_list i (@cons normal_form b d)) l1))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@cons (prod Int (list normal_form)) (@pair Int (list normal_form) i (@cons normal_form b d)) (@app (prod Int nf_list) l0 l1))) *)
apply nweight_ai_perm. 
(* Goal: @eq nat (S (Nat.add (nweight (nf2form b)) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (lin_avl nf_list t)))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (lin_avl nf_list t')) *)
 rewrite H.
(* Goal: @eq nat (S (Nat.add (nweight (nf2form b)) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) (@pair Int nf_list i d) l1))))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (lin_avl nf_list t')) *)
 rewrite H0.
(* Goal: @eq nat (S (Nat.add (nweight (nf2form b)) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) (@pair Int nf_list i d) l1))))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) (@pair Int nf_list i (@cons normal_form b d)) l1))) *)
clear H H0.
transitivity
 (fold_right (fun (x : Int * nf_list) (n : nat) => nweight_ibs x + n) 0
    ((i, b :: d) :: l0 ++ l1)).
change
  (S
     (nweight (nf2form b) +
      fold_right (fun (x : Int * nf_list) (n : nat) => nweight_ibs x + n) 0
        (l0 ++ (i, d) :: l1)) =
   S
     (nweight (nf2form b) + nweight_bs d +
      fold_right (fun (x : Int * nf_list) (n : nat) => nweight_ibs x + n) 0
        (l0 ++ l1))) in |- *.
(* Goal: @eq nat (S (Nat.add (Nat.add b W) (Nat.add ds n))) (S (Nat.add W (Nat.add ds (Nat.add b n)))) *)
apply S_reg.
(* Goal: @eq nat (Nat.add (nweight (nf2form b)) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) (@pair Int nf_list i d) l1)))) (Nat.add (Nat.add (nweight (nf2form b)) (nweight_bs d)) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 l1))) *)
(* Goal: @eq nat (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@cons (prod Int (list normal_form)) (@pair Int (list normal_form) i (@cons normal_form b d)) (@app (prod Int nf_list) l0 l1))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) (@pair Int nf_list i (@cons normal_form b d)) l1))) *)
generalize (nweight (nf2form b)); clear b; intro b.
 rewrite
 (plus_assoc_reverse b (nweight_bs d)
    (fold_right (fun (x : Int * nf_list) (n : nat) => nweight_ibs x + n) 0
       (l0 ++ l1))).
(* Goal: @eq nat (Nat.add W (Nat.add b (Nat.add ds n))) (Nat.add W (Nat.add ds (Nat.add b n))) *)
apply plus_reg.
change
  (fold_right (fun (x : Int * nf_list) (n : nat) => nweight_ibs x + n) 0
     (l0 ++ (i, d) :: l1) =
   fold_right (fun (x : Int * nf_list) (n : nat) => nweight_ibs x + n) 0
     ((i, d) :: l0 ++ l1)) in |- *.
(* Goal: @eq nat (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) (@pair Int nf_list i (@cons normal_form b d)) l1))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@cons (prod Int (list normal_form)) (@pair Int (list normal_form) i (@cons normal_form b d)) (@app (prod Int nf_list) l0 l1))) *)
apply nweight_ai_perm.
symmetry  in |- *.
(* Goal: @eq nat (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) (@pair Int nf_list i (@cons normal_form b d)) l1))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@cons (prod Int (list normal_form)) (@pair Int (list normal_form) i (@cons normal_form b d)) (@app (prod Int nf_list) l0 l1))) *)
apply nweight_ai_perm.
Qed.



Remark nweight_ai_del :
 forall (i : Int) (bs : nf_list) (ai ai' : atomic_imps),
 REGULAR normal_form ai ->
 LOOKUP nf_list i ai bs ->
 LIN_DEL nf_list i bs ai ai' ->
 nweight_work bs + nweight_ai ai' < nweight_ai ai.
(* Goal: forall (i : Int) (bs : nf_list) (ai ai' : atomic_imps) (_ : REGULAR normal_form ai) (_ : LOOKUP nf_list i ai bs) (_ : LIN_DEL nf_list i bs ai ai'), lt (Nat.add (nweight_work bs) (nweight_ai ai')) (nweight_ai ai) *)
intros i bs ai ai'. 
(* Goal: forall (_ : REGULAR normal_form ai) (_ : LOOKUP nf_list i ai bs) (_ : LIN_DEL nf_list i bs ai ai'), lt (Nat.add (nweight_work bs) (nweight_ai ai')) (nweight_ai ai) *)
elim ai; clear ai; intros t avl_t.
(* Goal: forall (_ : REGULAR normal_form (AVL_intro nf_list t avl_t)) (_ : LOOKUP nf_list i (AVL_intro nf_list t avl_t) bs) (_ : LIN_DEL nf_list i bs (AVL_intro nf_list t avl_t) ai'), lt (Nat.add (nweight_work bs) (nweight_ai ai')) (nweight_ai (AVL_intro nf_list t avl_t)) *)
elim ai'; clear ai'; intros t' avl_t'.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: forall (_ : Regular normal_form t) (_ : lookup nf_list i t bs) (_ : lin_del_spec nf_list i bs t t'), lt (Nat.add (nweight_work bs) (nweight_ai (AVL_intro nf_list t' avl_t'))) (nweight_ai (AVL_intro nf_list t avl_t)) *)
intros reg_t lookup lin_del.
(* Goal: lt (Nat.add (nweight_work bs) (nweight_ai (AVL_intro nf_list t' avl_t'))) (nweight_ai (AVL_intro nf_list t avl_t)) *)
unfold nweight_ai in |- *.
(* Goal: lt (Nat.add (nweight_work bs) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (LIN_AVL nf_list (AVL_intro nf_list t' avl_t')))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (LIN_AVL nf_list (AVL_intro nf_list t avl_t))) *)
inversion_clear lin_del.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: lt (Nat.add (nweight_work bs) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (lin_avl nf_list t'))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (lin_avl nf_list t)) *)
 rewrite H; clear H.
(* Goal: lt (Nat.add (nweight_work bs) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (lin_avl nf_list t'))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) (@pair Int nf_list i bs) l1))) *)
 rewrite H0; clear H0.
(* Goal: lt (Nat.add (nweight_work bs) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 l1))) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 (@cons (prod Int nf_list) (@pair Int nf_list i bs) l1))) *)
 rewrite (nweight_ai_perm l0 l1 (i, bs)).
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: lt (Nat.add (nweight_work bs) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 l1))) (Nat.add (nweight_bs bs) (@fold_right nat (prod Int nf_list) (fun (x : prod Int nf_list) (n : nat) => Nat.add (nweight_ibs x) n) O (@app (prod Int nf_list) l0 l1))) *)
apply plus_lt_compat_r.
(* Goal: lt (nweight_work bs) (nweight_bs bs) *)
generalize (reg_t i bs lookup); clear reg_t lookup.
(* Goal: forall _ : forall _ : @eq (list normal_form) bs (@nil normal_form), False, lt (nweight_work bs) (nweight_bs bs) *)
case bs; clear bs.
(* Goal: forall _ : forall _ : @eq (list normal_form) (@nil normal_form) (@nil normal_form), False, lt (nweight_work (@nil normal_form)) (nweight_bs (@nil normal_form)) *)
(* Goal: forall (n : normal_form) (l : list normal_form) (_ : forall _ : @eq (list normal_form) (@cons normal_form n l) (@nil normal_form), False), lt (nweight_work (@cons normal_form n l)) (nweight_bs (@cons normal_form n l)) *)
intros H; elimtype False.
(* Goal: @eq nat (Nat.add (nweight_ni ni2) n) (Nat.add (nweight_ni ni2) n) *)
apply H; trivial.
(* Goal: forall (n : normal_form) (l : list normal_form) (_ : forall _ : @eq (list normal_form) (@cons normal_form n l) (@nil normal_form), False), lt (nweight_work (@cons normal_form n l)) (nweight_bs (@cons normal_form n l)) *)
intros b bs H.
(* Goal: lt (nweight_work (@cons normal_form b bs)) (nweight_bs (@cons normal_form b bs)) *)
unfold lt in |- *.
(* Goal: le (S (nweight_work (@cons normal_form b bs))) (nweight_bs (@cons normal_form b bs)) *)
unfold nweight_work in |- *.
(* Goal: le (S (@fold_right nat normal_form (fun (a : normal_form) (n : nat) => Nat.add (nweight (nf2form a)) n) O (@cons normal_form b bs))) (nweight_bs (@cons normal_form b bs)) *)
unfold nweight_bs in |- *.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: le (S (Nat.add (nweight (nf2form b)) (@fold_right nat normal_form (fun (a : normal_form) (n : nat) => Nat.add (nweight (nf2form a)) n) O bs))) (S (Nat.add (nweight (nf2form b)) (@fold_right nat normal_form (fun (b : normal_form) (n : nat) => S (Nat.add (nweight (nf2form b)) n)) O bs))) *)
apply le_n_S.
(* Goal: le (Nat.add (nweight (nf2form b)) (@fold_right nat normal_form (fun (a : normal_form) (n : nat) => Nat.add (nweight (nf2form a)) n) O bs)) (Nat.add (nweight (nf2form b)) (@fold_right nat normal_form (fun (b : normal_form) (n : nat) => S (Nat.add (nweight (nf2form b)) n)) O bs)) *)
apply plus_le_compat_l.
(* Goal: le (@fold_right nat normal_form (fun (a : normal_form) (n : nat) => Nat.add (nweight (nf2form a)) n) O bs) (@fold_right nat normal_form (fun (b : normal_form) (n : nat) => S (Nat.add (nweight (nf2form b)) n)) O bs) *)
elim bs; clear H bs.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: le O O *)
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : le (@fold_right nat normal_form (fun (a0 : normal_form) (n : nat) => Nat.add (nweight (nf2form a0)) n) O l) (@fold_right nat normal_form (fun (b : normal_form) (n : nat) => S (Nat.add (nweight (nf2form b)) n)) O l)), le (@fold_right nat normal_form (fun (a0 : normal_form) (n : nat) => Nat.add (nweight (nf2form a0)) n) O (@cons normal_form a l)) (@fold_right nat normal_form (fun (b : normal_form) (n : nat) => S (Nat.add (nweight (nf2form b)) n)) O (@cons normal_form a l)) *)
apply le_O_n.
(* Goal: forall (a : normal_form) (l : list normal_form) (_ : le (@fold_right nat normal_form (fun (a0 : normal_form) (n : nat) => Nat.add (nweight (nf2form a0)) n) O l) (@fold_right nat normal_form (fun (b : normal_form) (n : nat) => S (Nat.add (nweight (nf2form b)) n)) O l)), le (@fold_right nat normal_form (fun (a0 : normal_form) (n : nat) => Nat.add (nweight (nf2form a0)) n) O (@cons normal_form a l)) (@fold_right nat normal_form (fun (b : normal_form) (n : nat) => S (Nat.add (nweight (nf2form b)) n)) O (@cons normal_form a l)) *)
intros b0 bs ih.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
change
  (nweight (nf2form b0) +
   fold_right (fun (a : normal_form) (n : nat) => nweight (nf2form a) + n) 0
     bs <=
   S (nweight (nf2form b0)) +
   fold_right
     (fun (b : normal_form) (n : nat) => S (nweight (nf2form b) + n)) 0 bs)
 in |- *.
(* Goal: le (Nat.add (nweight (nf2form b0)) (@fold_right nat normal_form (fun (a : normal_form) (n : nat) => Nat.add (nweight (nf2form a)) n) O bs)) (Nat.add (S (nweight (nf2form b0))) (@fold_right nat normal_form (fun (b : normal_form) (n : nat) => S (Nat.add (nweight (nf2form b)) n)) O bs)) *)
apply plus_le_compat.
(* Goal: le (nweight (nf2form b0)) (S (nweight (nf2form b0))) *)
(* Goal: le (@fold_right nat normal_form (fun (a : normal_form) (n : nat) => Nat.add (nweight (nf2form a)) n) O bs) (@fold_right nat normal_form (fun (b : normal_form) (n : nat) => S (Nat.add (nweight (nf2form b)) n)) O bs) *)
apply le_n_Sn.
(* Goal: LIN_INS nf_list i (@cons normal_form b) nf_nil ai ai' *)
assumption.
Qed.

(*********************************************************************)

Remark nweight_eqv_ni :
 forall ni1 ni2 : nested_imps,
 eqv_ni ni1 ni2 -> nweight_ni ni1 = nweight_ni ni2.
(* Goal: forall (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2), @eq nat (nweight_ni ni1) (nweight_ni ni2) *)
intros ni1 ni2 eqv12.
(* Goal: @eq nat (nweight_ni ni1) (nweight_ni ni2) *)
elim eqv12; clear eqv12 ni1 ni2.
(* Goal: @eq nat (Nat.add (nweight_ni ni2) n) (Nat.add (nweight_ni ni2) n) *)
trivial.
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : @eq nat (nweight_ni ni1) (nweight_ni ni2)), @eq nat (nweight_ni (@cons nested_imp (Undecorated x) ni1)) (nweight_ni (@cons nested_imp (Undecorated x) ni2)) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : @eq nat (nweight_ni ni1) (nweight_ni ni2)), @eq nat (nweight_ni (@cons nested_imp (Decorated x k) ni1)) (nweight_ni (@cons nested_imp (Undecorated x) ni2)) *)
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : @eq nat (nweight_ni ni1) (nweight_ni ni2)), @eq nat (nweight_ni (@cons nested_imp (Decorated x k) ni1)) (nweight_ni (@cons nested_imp (Decorated x k') ni2)) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : @eq nat (nweight_ni ni1) (nweight_ni ni2)), @eq nat (nweight_ni (@cons nested_imp (Undecorated x) ni1)) (nweight_ni (@cons nested_imp (Decorated x k) ni2)) *)
intros x ni1 ni2 eqv12 ih.
(* Goal: @eq nat (nweight_ni (@cons nested_imp (Undecorated x) ni1)) (nweight_ni (@cons nested_imp (Decorated x k) ni2)) *)
unfold nweight_ni in |- *.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: @eq nat (Nat.add (nweight_nestedimp (Undecorated x)) (@fold_right nat nested_imp (fun (x : nested_imp) (n : nat) => Nat.add (nweight_nestedimp x) n) O ni1)) (Nat.add (nweight_nestedimp (Decorated x k)) (@fold_right nat nested_imp (fun (x : nested_imp) (n : nat) => Nat.add (nweight_nestedimp x) n) O ni2)) *)
fold nweight_ni in |- *.
(* Goal: @eq nat (Nat.add (nweight_ni ni2) n) (Nat.add (nweight_ni ni2) n) *)
 rewrite ih; trivial.
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : @eq nat (nweight_ni ni1) (nweight_ni ni2)), @eq nat (nweight_ni (@cons nested_imp (Undecorated x) ni1)) (nweight_ni (@cons nested_imp (Decorated x k) ni2)) *)
intros x k ni1 ni2 eqv12 ih.
(* Goal: @eq nat (nweight_ni (@cons nested_imp (Undecorated x) ni1)) (nweight_ni (@cons nested_imp (Decorated x k) ni2)) *)
unfold nweight_ni in |- *.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: @eq nat (Nat.add (nweight_nestedimp (Undecorated x)) (@fold_right nat nested_imp (fun (x : nested_imp) (n : nat) => Nat.add (nweight_nestedimp x) n) O ni1)) (Nat.add (nweight_nestedimp (Decorated x k)) (@fold_right nat nested_imp (fun (x : nested_imp) (n : nat) => Nat.add (nweight_nestedimp x) n) O ni2)) *)
fold nweight_ni in |- *.
(* Goal: @eq nat (Nat.add (nweight_ni ni2) n) (Nat.add (nweight_ni ni2) n) *)
 rewrite ih; trivial.
(* Goal: forall (x : nimp) (k k' : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : @eq nat (nweight_ni ni1) (nweight_ni ni2)), @eq nat (nweight_ni (@cons nested_imp (Decorated x k) ni1)) (nweight_ni (@cons nested_imp (Decorated x k') ni2)) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : @eq nat (nweight_ni ni1) (nweight_ni ni2)), @eq nat (nweight_ni (@cons nested_imp (Undecorated x) ni1)) (nweight_ni (@cons nested_imp (Decorated x k) ni2)) *)
intros x k k' ni1 ni2 eqv12 ih.
(* Goal: @eq nat (nweight_ni (@cons nested_imp (Undecorated x) ni1)) (nweight_ni (@cons nested_imp (Decorated x k) ni2)) *)
unfold nweight_ni in |- *.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: @eq nat (Nat.add (nweight_nestedimp (Undecorated x)) (@fold_right nat nested_imp (fun (x : nested_imp) (n : nat) => Nat.add (nweight_nestedimp x) n) O ni1)) (Nat.add (nweight_nestedimp (Decorated x k)) (@fold_right nat nested_imp (fun (x : nested_imp) (n : nat) => Nat.add (nweight_nestedimp x) n) O ni2)) *)
fold nweight_ni in |- *.
(* Goal: @eq nat (Nat.add (nweight_ni ni2) n) (Nat.add (nweight_ni ni2) n) *)
 rewrite ih; trivial.
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : eqv_ni ni1 ni2) (_ : @eq nat (nweight_ni ni1) (nweight_ni ni2)), @eq nat (nweight_ni (@cons nested_imp (Undecorated x) ni1)) (nweight_ni (@cons nested_imp (Decorated x k) ni2)) *)
intros x k ni1 ni2 eqv12 ih.
(* Goal: @eq nat (nweight_ni (@cons nested_imp (Undecorated x) ni1)) (nweight_ni (@cons nested_imp (Decorated x k) ni2)) *)
unfold nweight_ni in |- *.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: @eq nat (Nat.add (nweight_nestedimp (Undecorated x)) (@fold_right nat nested_imp (fun (x : nested_imp) (n : nat) => Nat.add (nweight_nestedimp x) n) O ni1)) (Nat.add (nweight_nestedimp (Decorated x k)) (@fold_right nat nested_imp (fun (x : nested_imp) (n : nat) => Nat.add (nweight_nestedimp x) n) O ni2)) *)
fold nweight_ni in |- *.
(* Goal: @eq nat (Nat.add (nweight_ni ni2) n) (Nat.add (nweight_ni ni2) n) *)
 rewrite ih; trivial.
Qed.





Remark nweight_rev_app :
 forall (dni : decorated_nested_imps) (ni : nested_imps),
 nweight_ni ni + nweight_dni dni = nweight_ni (rev_app dni ni).
(* Goal: forall (dni : decorated_nested_imps) (ni : nested_imps), @eq nat (Nat.add (nweight_ni ni) (nweight_dni dni)) (nweight_ni (rev_app dni ni)) *)
intros dni; elim dni; clear dni.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
intros ni; unfold nweight_dni in |- *; simpl in |- *.
(* Goal: @eq nat (Nat.add (nweight_ni ni) O) (nweight_ni ni) *)
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall ni : nested_imps, @eq nat (Nat.add (nweight_ni ni) (nweight_dni l)) (nweight_ni (rev_app l ni))) (ni : nested_imps), @eq nat (Nat.add (nweight_ni ni) (nweight_dni (@cons decorated_nested_imp a l))) (nweight_ni (rev_app (@cons decorated_nested_imp a l) ni)) *)
apply plus_O.
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall ni : nested_imps, @eq nat (Nat.add (nweight_ni ni) (nweight_dni l)) (nweight_ni (rev_app l ni))) (ni : nested_imps), @eq nat (Nat.add (nweight_ni ni) (nweight_dni (@cons decorated_nested_imp a l))) (nweight_ni (rev_app (@cons decorated_nested_imp a l) ni)) *)
intros x dni ih ni.
(* Goal: @eq nat (Nat.add (nweight_ni ni) (nweight_dni (@cons decorated_nested_imp x dni))) (nweight_ni (rev_app (@cons decorated_nested_imp x dni) ni)) *)
case x; clear x.
(* Goal: forall (n : nimp) (k : kripke_tree), @eq nat (Nat.add (nweight_ni ni) (nweight_dni (@cons decorated_nested_imp (@pair nimp kripke_tree n k) dni))) (nweight_ni (rev_app (@cons decorated_nested_imp (@pair nimp kripke_tree n k) dni) ni)) *)
intros n k.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: @eq nat (Nat.add (nweight_ni ni) (Nat.add (nweight (nimp2form n)) (nweight_dni dni))) (nweight_ni (rev_app dni (@cons nested_imp (Decorated n k) ni))) *)
 rewrite <- (ih (Decorated n k :: ni)); clear ih.
(* Goal: @eq nat (Nat.add (nweight_nestedimp (Undecorated x)) (@fold_right nat nested_imp (fun (x : nested_imp) (n : nat) => Nat.add (nweight_nestedimp x) n) O ni1)) (Nat.add (nweight_nestedimp (Decorated x k)) (@fold_right nat nested_imp (fun (x : nested_imp) (n : nat) => Nat.add (nweight_nestedimp x) n) O ni2)) *)
unfold nweight_ni in |- *; simpl in |- *; fold nweight_ni in |- *.
(* Goal: @eq nat (Nat.add (nweight_ni ni) (Nat.add (nweight (nimp2form n)) (nweight_dni dni))) (Nat.add (Nat.add (nweight_nestedimp (Decorated n k)) (nweight_ni ni)) (nweight_dni dni)) *)
unfold nweight_nestedimp in |- *.
(* Goal: @eq nat (Nat.add (nweight_ni ni) (Nat.add (nweight (nimp2form n)) (nweight_dni dni))) (Nat.add (Nat.add (nweight (nested_imp2form (Decorated n k))) (nweight_ni ni)) (nweight_dni dni)) *)
unfold nested_imp2form in |- *.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: @eq nat (Nat.add (nweight_ni ni) (Nat.add (nweight (nimp2form n)) (nweight_dni dni))) (Nat.add (Nat.add (nweight (nimp2form n)) (nweight_ni ni)) (nweight_dni dni)) *)
generalize (nweight (nimp2form n)); clear n; intros n.
(* Goal: @eq nat (Nat.add (Nat.add (nweight (nimp2form x)) W) (Nat.add ds (Nat.add (nweight_ni ni) ai))) (Nat.add W (Nat.add ds (Nat.add (Nat.add (nweight_nestedimp (Undecorated x)) (nweight_ni ni)) ai))) *)
generalize (nweight_ni ni); clear ni; intros ni.
(* Goal: @eq nat (Nat.add ni (Nat.add n (nweight_dni dni))) (Nat.add (Nat.add n ni) (nweight_dni dni)) *)
generalize (nweight_dni dni); clear dni; intros dni.
(* Goal: @eq nat (Nat.add ni (Nat.add n dni)) (Nat.add (Nat.add n ni) dni) *)
 rewrite (plus_assoc ni n dni).
(* Goal: @eq nat (PeanoNat.Nat.add (PeanoNat.Nat.add ni n) dni) (Nat.add (Nat.add n ni) dni) *)
 rewrite (plus_comm ni n).
(* Goal: @eq nat (Nat.add (nweight_ni ni2) n) (Nat.add (nweight_ni ni2) n) *)
trivial.
Qed.


(**********************************************************************)


Definition nweight_Sequent (work : nf_list) (ds : disjs) 
  (ni : nested_imps) (ai : atomic_imps) :=
  nweight_work work + (nweight_ds ds + (nweight_ni ni + nweight_ai ai)).



Lemma nweight_shift_work_ni0 :
 forall (x : nimp) (work : nf_list) (ds : disjs) (ni : nested_imps)
   (ai : atomic_imps),
 nweight_Sequent (NImp_NF x :: work) ds ni ai =
 nweight_Sequent work ds (Undecorated x :: ni) ai.
(* Goal: forall (x : nimp) (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps), @eq nat (nweight_Sequent (@cons normal_form (NImp_NF x) work) ds ni ai) (nweight_Sequent work ds (@cons nested_imp (Undecorated x) ni) ai) *)
intros x work ds ni ai.
(* Goal: le (S (nweight_Sequent (@cons normal_form (NAtom j) work) ds ni2 ai)) (nweight_Sequent work (@cons (prod Int Int) (@pair Int Int i j) ds) ni1 ai) *)
unfold nweight_Sequent in |- *.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: @eq nat (Nat.add (Nat.add (nweight (nimp2form x)) (nweight_work work)) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni) (nweight_ai ai)))) (Nat.add (nweight_work work) (Nat.add (nweight_ds ds) (Nat.add (Nat.add (nweight_nestedimp (Undecorated x)) (nweight_ni ni)) (nweight_ai ai)))) *)
fold nimp2form in |- *.
(* Goal: @eq nat (Nat.add (Nat.add (nweight (nimp2form x)) (nweight_work work)) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni) (nweight_ai ai)))) (Nat.add (nweight_work work) (Nat.add (nweight_ds ds) (Nat.add (Nat.add (nweight_nestedimp (Undecorated x)) (nweight_ni ni)) (nweight_ai ai)))) *)
generalize (nweight_ai ai); clear ai; intro ai.
(* Goal: lt (Nat.add (nweight_work (@app normal_form bs work)) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni) (nweight_ai ai')))) (Nat.add (nweight_work work) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni) (nweight_ai ai)))) *)
generalize (nweight_ds ds); clear ds; intro ds.
(* Goal: lt (Nat.add (Nat.add (nweight_work bs) (nweight_work work)) (Nat.add ds (Nat.add ni (nweight_ai ai')))) (Nat.add (nweight_work work) (Nat.add ds (Nat.add ni (nweight_ai ai)))) *)
generalize (nweight_work work); clear work; intro W.
(* Goal: @eq nat (Nat.add (Nat.add (nweight (nimp2form x)) W) (Nat.add ds (Nat.add (nweight_ni ni) ai))) (Nat.add W (Nat.add ds (Nat.add (Nat.add (nweight_nestedimp (Undecorated x)) (nweight_ni ni)) ai))) *)
generalize (nweight_ni ni); clear ni; intros ni.
change
  (nweight (nimp2form x) + W + (ds + (ni + ai)) =
   W + (ds + (nweight (nimp2form x) + ni + ai))) in |- *.
(* Goal: @eq nat (Nat.add (Nat.add (nweight (nimp2form x)) W) (Nat.add ds (Nat.add ni ai))) (Nat.add W (Nat.add ds (Nat.add (Nat.add (nweight (nimp2form x)) ni) ai))) *)
generalize (nweight (nimp2form x)); clear x; intro x.
(* Goal: @eq nat (Nat.add (Nat.add x W) (Nat.add ds (Nat.add ni ai))) (Nat.add W (Nat.add ds (Nat.add (Nat.add x ni) ai))) *)
 rewrite (plus_comm x W).
(* Goal: @eq nat (Nat.add (PeanoNat.Nat.add W x) (Nat.add ds (Nat.add ni ai))) (Nat.add W (Nat.add ds (Nat.add (Nat.add x ni) ai))) *)
 rewrite (plus_assoc_reverse W x (ds + (ni + ai))).
(* Goal: @eq nat (Nat.add W (Nat.add b (Nat.add ds n))) (Nat.add W (Nat.add ds (Nat.add b n))) *)
apply plus_reg.
(* Goal: @eq nat (Nat.add x (Nat.add ds (Nat.add ni ai))) (Nat.add ds (Nat.add (Nat.add x ni) ai)) *)
 rewrite (plus_assoc x ds (ni + ai)).
(* Goal: @eq nat (PeanoNat.Nat.add (PeanoNat.Nat.add x ds) (Nat.add ni ai)) (Nat.add ds (Nat.add (Nat.add x ni) ai)) *)
 rewrite (plus_comm x ds).
(* Goal: @eq nat (PeanoNat.Nat.add (PeanoNat.Nat.add ds x) (Nat.add ni ai)) (Nat.add ds (Nat.add (Nat.add x ni) ai)) *)
 rewrite (plus_assoc_reverse ds x (ni + ai)).
(* Goal: @eq nat (Nat.add W (Nat.add b (Nat.add ds n))) (Nat.add W (Nat.add ds (Nat.add b n))) *)
apply plus_reg.
(* Goal: @eq nat (Nat.add x (Nat.add ni ai)) (Nat.add (Nat.add x ni) ai) *)
apply plus_assoc.
Qed.


Lemma nweight_shift_work_ds :
 forall (i j : Int) (work : nf_list) (ds : disjs) (ni : nested_imps)
   (ai : atomic_imps),
 nweight_Sequent (NDisj i j :: work) ds ni ai =
 nweight_Sequent work ((i, j) :: ds) ni ai.
(* Goal: forall (i j : Int) (work : nf_list) (ds : disjs) (ni : nested_imps) (ai : atomic_imps), @eq nat (nweight_Sequent (@cons normal_form (NDisj i j) work) ds ni ai) (nweight_Sequent work (@cons (prod Int Int) (@pair Int Int i j) ds) ni ai) *)
intros i j work ds ni ai.
(* Goal: le (S (nweight_Sequent (@cons normal_form (NAtom j) work) ds ni2 ai)) (nweight_Sequent work (@cons (prod Int Int) (@pair Int Int i j) ds) ni1 ai) *)
unfold nweight_Sequent in |- *.
(* Goal: @eq nat (Nat.add (nweight_work (@cons normal_form (NDisj i j) work)) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni) (nweight_ai ai)))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) (Nat.add (nweight_ni ni) (nweight_ai ai)))) *)
generalize (nweight_ni ni + nweight_ai ai).
(* Goal: forall n : nat, @eq nat (Nat.add (nweight_work (@cons normal_form (NDisj i j) work)) (Nat.add (nweight_ds ds) n)) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
clear ni ai; intros n.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: @eq nat (S (Nat.add (nweight_work work) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (S (Nat.add (nweight_ds ds) n))) *)
fold nweight_work in |- *.
(* Goal: @eq nat (S (Nat.add (nweight_work work) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (S (Nat.add (nweight_ds ds) n))) *)
fold nweight_ds in |- *.
(* Goal: @eq nat (S (Nat.add (nweight_work work) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (S (Nat.add (nweight_ds ds) n))) *)
 rewrite <- (plus_Snm_nSm (nweight_work work) (nweight_ds ds + n)).
(* Goal: @eq nat (Nat.add (nweight_ni ni2) n) (Nat.add (nweight_ni ni2) n) *)
trivial.
Qed.



Lemma nweight_shift_work_ai :
 forall (i : Int) (b : normal_form) (work : nf_list) 
   (ds : disjs) (ni : nested_imps) (ai ai' : atomic_imps),
 LIN_INS nf_list i (cons b) nf_nil ai ai' ->
 nweight_Sequent (AImp i b :: work) ds ni ai = nweight_Sequent work ds ni ai'.
(* Goal: forall (i : Int) (b : normal_form) (work : nf_list) (ds : disjs) (ni : nested_imps) (ai ai' : atomic_imps) (_ : LIN_INS nf_list i (@cons normal_form b) nf_nil ai ai'), @eq nat (nweight_Sequent (@cons normal_form (AImp i b) work) ds ni ai) (nweight_Sequent work ds ni ai') *)
intros.
(* Goal: le (S (nweight_Sequent (@cons normal_form (NAtom j) work) ds ni2 ai)) (nweight_Sequent work (@cons (prod Int Int) (@pair Int Int i j) ds) ni1 ai) *)
unfold nweight_Sequent in |- *.
(* Goal: @eq nat (Nat.add (nweight_work (@cons normal_form (AImp i b) work)) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni) (nweight_ai ai)))) (Nat.add (nweight_work work) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni) (nweight_ai ai')))) *)
 rewrite <- (nweight_ai_ins i b ai ai').
(* Goal: @eq nat (Nat.add (nweight_work (@cons normal_form (AImp i b) work)) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni) (nweight_ai ai)))) (Nat.add (nweight_work work) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni) (Nat.add (nweight (nf2form (AImp i b))) (nweight_ai ai))))) *)
(* Goal: LIN_INS nf_list i (@cons normal_form b) nf_nil ai ai' *)
generalize (nweight_ai ai); clear H ai ai'; intro ai.
(* Goal: lt (Nat.add (nweight_work (@app normal_form bs work)) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni) (nweight_ai ai')))) (Nat.add (nweight_work work) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni) (nweight_ai ai)))) *)
generalize (nweight_ds ds); clear ds; intro ds.
(* Goal: lt (Nat.add (nweight_work (@app normal_form bs work)) (Nat.add ds (Nat.add (nweight_ni ni) (nweight_ai ai')))) (Nat.add (nweight_work work) (Nat.add ds (Nat.add (nweight_ni ni) (nweight_ai ai)))) *)
generalize (nweight_ni ni); clear ni; intro ni.
change
  (nweight (nf2form (AImp i b)) + nweight_work work + (ds + (ni + ai)) =
   nweight_work work + (ds + (ni + (nweight (nf2form (AImp i b)) + ai))))
 in |- *.
(* Goal: @eq nat (Nat.add (Nat.add (nweight (nf2form (AImp i b))) (nweight_work work)) (Nat.add ds (Nat.add ni ai))) (Nat.add (nweight_work work) (Nat.add ds (Nat.add ni (Nat.add (nweight (nf2form (AImp i b))) ai)))) *)
(* Goal: LIN_INS nf_list i (@cons normal_form b) nf_nil ai ai' *)
generalize (nweight_work work); clear work; intro work.
(* Goal: @eq nat (Nat.add (Nat.add (nweight (nf2form (AImp i b))) work) (Nat.add ds (Nat.add ni ai))) (Nat.add work (Nat.add ds (Nat.add ni (Nat.add (nweight (nf2form (AImp i b))) ai)))) *)
(* Goal: LIN_INS nf_list i (@cons normal_form b) nf_nil ai ai' *)
generalize (nweight (nf2form (AImp i b))); clear i b; intro a.
(* Goal: @eq nat (Nat.add (Nat.add a work) (Nat.add ds (Nat.add ni ai))) (Nat.add work (Nat.add ds (Nat.add ni (Nat.add a ai)))) *)
(* Goal: LIN_INS nf_list i (@cons normal_form b) nf_nil ai ai' *)
 rewrite (plus_comm a work).
(* Goal: @eq nat (Nat.add (PeanoNat.Nat.add work a) (Nat.add ds (Nat.add ni ai))) (Nat.add work (Nat.add ds (Nat.add ni (Nat.add a ai)))) *)
(* Goal: LIN_INS nf_list i (@cons normal_form b) nf_nil ai ai' *)
 rewrite (plus_assoc_reverse work a (ds + (ni + ai))).
(* Goal: @eq nat (Nat.add W (Nat.add b (Nat.add ds n))) (Nat.add W (Nat.add ds (Nat.add b n))) *)
apply plus_reg.
(* Goal: @eq nat (Nat.add a (Nat.add ds (Nat.add ni ai))) (Nat.add ds (Nat.add ni (Nat.add a ai))) *)
(* Goal: LIN_INS nf_list i (@cons normal_form b) nf_nil ai ai' *)
 rewrite (plus_permute a ds (ni + ai)).
(* Goal: @eq nat (Nat.add W (Nat.add b (Nat.add ds n))) (Nat.add W (Nat.add ds (Nat.add b n))) *)
apply plus_reg.
(* Goal: @eq nat (PeanoNat.Nat.add a (Nat.add ni ai)) (Nat.add ni (Nat.add a ai)) *)
(* Goal: LIN_INS nf_list i (@cons normal_form b) nf_nil ai ai' *)
 rewrite (plus_permute a ni ai).
(* Goal: @eq nat (Nat.add W (Nat.add b (Nat.add ds n))) (Nat.add W (Nat.add ds (Nat.add b n))) *)
apply plus_reg.
(* Goal: @eq nat (Nat.add (nweight_ni ni2) n) (Nat.add (nweight_ni ni2) n) *)
trivial.
(* Goal: LIN_INS nf_list i (@cons normal_form b) nf_nil ai ai' *)
assumption.
Qed.


(*******************************************************************)


Lemma nweight_shift_ai_work :
 forall (i : Int) (bs work : nf_list) (ds : disjs) 
   (ni : nested_imps) (ai ai' : atomic_imps),
 LOOKUP nf_list i ai bs ->
 REGULAR normal_form ai ->
 LIN_DEL nf_list i bs ai ai' ->
 nweight_Sequent (bs ++ work) ds ni ai' < nweight_Sequent work ds ni ai.
(* Goal: forall (i : Int) (bs work : nf_list) (ds : disjs) (ni : nested_imps) (ai ai' : atomic_imps) (_ : LOOKUP nf_list i ai bs) (_ : REGULAR normal_form ai) (_ : LIN_DEL nf_list i bs ai ai'), lt (nweight_Sequent (@app normal_form bs work) ds ni ai') (nweight_Sequent work ds ni ai) *)
intros i bs work ds ni ai ai' lookup reg_ai lin_del.
(* Goal: le (S (nweight_Sequent (@cons normal_form (NAtom j) work) ds ni2 ai)) (nweight_Sequent work (@cons (prod Int Int) (@pair Int Int i j) ds) ni1 ai) *)
unfold nweight_Sequent in |- *.
(* Goal: lt (Nat.add (nweight_work (@app normal_form bs work)) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni) (nweight_ai ai')))) (Nat.add (nweight_work work) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni) (nweight_ai ai)))) *)
generalize (nweight_ds ds); clear ds; intro ds.
(* Goal: lt (Nat.add (nweight_work (@app normal_form bs work)) (Nat.add ds (Nat.add (nweight_ni ni) (nweight_ai ai')))) (Nat.add (nweight_work work) (Nat.add ds (Nat.add (nweight_ni ni) (nweight_ai ai)))) *)
generalize (nweight_ni ni); clear ni; intro ni.
(* Goal: lt (Nat.add (nweight_work (@app normal_form bs work)) (Nat.add ds (Nat.add ni (nweight_ai ai')))) (Nat.add (nweight_work work) (Nat.add ds (Nat.add ni (nweight_ai ai)))) *)
 rewrite (nweight_work_app bs work).
(* Goal: lt (Nat.add (Nat.add (nweight_work bs) (nweight_work work)) (Nat.add ds (Nat.add ni (nweight_ai ai')))) (Nat.add (nweight_work work) (Nat.add ds (Nat.add ni (nweight_ai ai)))) *)
generalize (nweight_work work); clear work; intro W.
(* Goal: lt (Nat.add (Nat.add (nweight_work bs) W) (Nat.add ds (Nat.add ni (nweight_ai ai')))) (Nat.add W (Nat.add ds (Nat.add ni (nweight_ai ai)))) *)
 rewrite (plus_comm (nweight_work bs) W).
 rewrite
 (plus_assoc_reverse W (nweight_work bs) (ds + (ni + nweight_ai ai')))
 .
(* Goal: lt (PeanoNat.Nat.add ni (PeanoNat.Nat.add (nweight_work bs) (nweight_ai ai'))) (Nat.add ni (nweight_ai ai)) *)
apply plus_lt_compat_l.
(* Goal: lt (Nat.add (nweight_work bs) (Nat.add ds (Nat.add ni (nweight_ai ai')))) (Nat.add ds (Nat.add ni (nweight_ai ai))) *)
 rewrite (plus_permute (nweight_work bs) ds (ni + nweight_ai ai')).
(* Goal: lt (PeanoNat.Nat.add ni (PeanoNat.Nat.add (nweight_work bs) (nweight_ai ai'))) (Nat.add ni (nweight_ai ai)) *)
apply plus_lt_compat_l.
(* Goal: lt (PeanoNat.Nat.add (nweight_work bs) (Nat.add ni (nweight_ai ai'))) (Nat.add ni (nweight_ai ai)) *)
 rewrite (plus_permute (nweight_work bs) ni (nweight_ai ai')).
(* Goal: lt (PeanoNat.Nat.add ni (PeanoNat.Nat.add (nweight_work bs) (nweight_ai ai'))) (Nat.add ni (nweight_ai ai)) *)
apply plus_lt_compat_l.
(* Goal: LIN_INS nf_list i (@cons normal_form b) nf_nil ai ai' *)
apply nweight_ai_del with i; assumption.
Qed.


(*************************************************************************)

Lemma nweight_sequent_eqv :
 forall (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps)
   (ai : atomic_imps),
 eqv_ni ni1 ni2 ->
 nweight_Sequent work ds ni1 ai = nweight_Sequent work ds ni2 ai.
(* Goal: forall (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps) (ai : atomic_imps) (_ : eqv_ni ni1 ni2), @eq nat (nweight_Sequent work ds ni1 ai) (nweight_Sequent work ds ni2 ai) *)
intros work ds ni1 ni2 ai eqv12.
(* Goal: le (S (nweight_Sequent (@cons normal_form (NAtom j) work) ds ni2 ai)) (nweight_Sequent work (@cons (prod Int Int) (@pair Int Int i j) ds) ni1 ai) *)
unfold nweight_Sequent in |- *.
(* Goal: @eq nat (Nat.add W (Nat.add b (Nat.add ds n))) (Nat.add W (Nat.add ds (Nat.add b n))) *)
apply plus_reg.
(* Goal: @eq nat (Nat.add W (Nat.add b (Nat.add ds n))) (Nat.add W (Nat.add ds (Nat.add b n))) *)
apply plus_reg.
(* Goal: @eq nat (Nat.add (nweight_ni ni1) (nweight_ai ai)) (Nat.add (nweight_ni ni2) (nweight_ai ai)) *)
generalize (nweight_ai ai); clear work ds ai.
(* Goal: forall n : nat, @eq nat (Nat.add (nweight_ni ni1) n) (Nat.add (nweight_ni ni2) n) *)
intros n.
(* Goal: @eq nat (Nat.add (nweight_ni ni1) n) (Nat.add (nweight_ni ni2) n) *)
 rewrite (nweight_eqv_ni ni1 ni2 eqv12).
(* Goal: @eq nat (Nat.add (nweight_ni ni2) n) (Nat.add (nweight_ni ni2) n) *)
trivial.
Qed.

(*******************************************************************)

Lemma nweight_sequent_nimp_left :
 forall (a0 a1 : Int) (b : normal_form) (work : nf_list) 
   (ds : disjs) (ni1 ni2 : nested_imps) (dni1 : decorated_nested_imps)
   (ai : atomic_imps) (n : nat),
 eqv_ni (rev_app dni1 ni1) ni2 ->
 nweight_Sequent work ds (rev_app dni1 (Undecorated (NImp a0 a1 b) :: ni1))
   ai < S n -> nweight_Sequent (AImp a1 b :: NAtom a0 :: work) ds ni2 ai < n.
(* Goal: forall (a0 a1 : Int) (b : normal_form) (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps) (dni1 : decorated_nested_imps) (ai : atomic_imps) (n : nat) (_ : eqv_ni (rev_app dni1 ni1) ni2) (_ : lt (nweight_Sequent work ds (rev_app dni1 (@cons nested_imp (Undecorated (NImp a0 a1 b)) ni1)) ai) (S n)), lt (nweight_Sequent (@cons normal_form b work) ds ni2 ai) n *)
intros a0 a1 b work ds ni1 ni2 dni1 ai n eqv12 lt1.
(* Goal: lt (nweight_Sequent (@cons normal_form (NAtom j) work) ds ni2 ai) n *)
apply lt_S_n.
apply
 eq_lt_trans
  with
    (nweight_Sequent work ds
       (rev_app dni1 (Undecorated (NImp a0 a1 b) :: ni1)) ai); 
 try assumption; clear lt1.
(* Goal: le (S (nweight_Sequent (@cons normal_form (NAtom j) work) ds ni2 ai)) (nweight_Sequent work (@cons (prod Int Int) (@pair Int Int i j) ds) ni1 ai) *)
unfold nweight_Sequent in |- *.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni2) (nweight_ai ai))))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) (Nat.add (nweight_ni ni1) (nweight_ai ai)))) *)
generalize (nweight_ai ai); clear ai; intros ai.
(* Goal: le (S (Nat.add W (Nat.add (nweight_ds ds) n))) (Nat.add W (S (Nat.add (nweight_ds ds) n))) *)
generalize (nweight_ds ds); clear ds; intros ds.
(* Goal: lt (S (Nat.add (nweight_work (@cons normal_form b work)) (Nat.add ds (Nat.add (nweight_ni ni2) ai)))) (Nat.add (nweight_work work) (Nat.add ds (Nat.add (nweight_ni (rev_app dni1 (@cons nested_imp (Undecorated (NImp a0 a1 b)) ni1))) ai))) *)
 rewrite <- (nweight_rev_app dni1 (Undecorated (NImp a0 a1 b) :: ni1)).
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: lt (S (Nat.add (Nat.add (nweight (nf2form b)) (nweight_work work)) (Nat.add ds (Nat.add (nweight_ni ni2) ai)))) (Nat.add (nweight_work work) (Nat.add ds (S (S (Nat.add (Nat.add (Nat.add (nweight (nf2form b)) (nweight_ni ni1)) (nweight_dni dni1)) ai))))) *)
fold nf2form in |- *.
(* Goal: lt (S (Nat.add (Nat.add (nweight (nf2form b)) (nweight_work work)) (Nat.add ds (Nat.add (nweight_ni ni2) ai)))) (Nat.add (nweight_work work) (Nat.add ds (S (S (Nat.add (Nat.add (Nat.add (nweight (nf2form b)) (nweight_ni ni1)) (nweight_dni dni1)) ai))))) *)
generalize (nweight (nf2form b)); clear b; intros b.
(* Goal: lt (S (Nat.add (Nat.add b W) (Nat.add ds (Nat.add (nweight_ni ni2) ai)))) (Nat.add W (Nat.add ds (S (S (Nat.add (Nat.add (Nat.add b (nweight_ni ni1)) (nweight_dni dni1)) ai))))) *)
 rewrite (plus_assoc_reverse b (nweight_ni ni1) (nweight_dni dni1)).
(* Goal: @eq nat (S (S (Nat.add (Nat.add b (nweight_work work)) (Nat.add ds (Nat.add (nweight_ni ni2) ai))))) (Nat.add (nweight_work work) (Nat.add ds (S (S (Nat.add (Nat.add b (Nat.add (nweight_ni ni1) (nweight_dni dni1))) ai))))) *)
 rewrite <- (nweight_eqv_ni (rev_app dni1 ni1) ni2 eqv12).
(* Goal: @eq nat (S (S (Nat.add (Nat.add b (nweight_work work)) (Nat.add ds (Nat.add (nweight_ni (rev_app dni1 ni1)) ai))))) (Nat.add (nweight_work work) (Nat.add ds (S (S (Nat.add (Nat.add b (Nat.add (nweight_ni ni1) (nweight_dni dni1))) ai))))) *)
 rewrite <- (nweight_rev_app dni1 ni1).
generalize (nweight_ni ni1 + nweight_dni dni1); clear eqv12 ni1 dni1 ni2 n;
(* Goal: forall n : nat, @eq nat (Nat.add (nweight_ni ni1) n) (Nat.add (nweight_ni ni2) n) *)
 intros n.
(* Goal: le (S (Nat.add (nweight_work work) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (S (Nat.add (nweight_ds ds) n))) *)
generalize (nweight_work work); clear work; intros W.
(* Goal: @eq nat (S (S (Nat.add (Nat.add b W) (Nat.add ds (Nat.add n ai))))) (Nat.add W (Nat.add ds (S (S (Nat.add (Nat.add b n) ai))))) *)
 rewrite (plus_assoc_reverse b n ai).
(* Goal: forall n : nat, @eq nat (Nat.add (nweight_ni ni1) n) (Nat.add (nweight_ni ni2) n) *)
generalize (n + ai); clear n ai; intros n.
(* Goal: lt (S (Nat.add W (Nat.add ds (Nat.add b n)))) (Nat.add W (Nat.add ds (S (S (Nat.add b n))))) *)
 rewrite <- (plus_Snm_nSm ds (S (b + n))).
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: lt (S (Nat.add W (Nat.add ds (Nat.add b n)))) (Nat.add W (S (Nat.add ds (S (Nat.add b n))))) *)
 rewrite <- (plus_Snm_nSm ds (b + n)).
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: lt (S (Nat.add W (Nat.add ds (Nat.add b n)))) (Nat.add W (S (S (Nat.add ds (Nat.add b n))))) *)
 rewrite <- (plus_Snm_nSm W (S (ds + (b + n)))).
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: lt (S (Nat.add W (Nat.add ds (Nat.add b n)))) (S (Nat.add W (S (Nat.add ds (Nat.add b n))))) *)
 rewrite <- (plus_Snm_nSm W (ds + (b + n))).
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: @eq nat (S (Nat.add (Nat.add b W) (Nat.add ds n))) (S (Nat.add W (Nat.add ds (Nat.add b n)))) *)
apply S_reg.
(* Goal: @eq nat (S (Nat.add (Nat.add b W) (Nat.add ds n))) (S (Nat.add W (Nat.add ds (Nat.add b n)))) *)
apply S_reg.
(* Goal: lt (S (Nat.add (Nat.add b W) (Nat.add ds n))) (Nat.add W (Nat.add ds (S (S (Nat.add b n))))) *)
 rewrite (plus_comm b W).
(* Goal: lt (S (Nat.add (PeanoNat.Nat.add W b) (Nat.add ds n))) (Nat.add W (Nat.add ds (S (S (Nat.add b n))))) *)
 rewrite (plus_assoc_reverse W b (ds + n)).
(* Goal: @eq nat (Nat.add W (Nat.add b (Nat.add ds n))) (Nat.add W (Nat.add ds (Nat.add b n))) *)
apply plus_reg.
(* Goal: lt (S (Nat.add W (Nat.add b (Nat.add ds n)))) (Nat.add W (Nat.add ds (S (S (Nat.add b n))))) *)
 rewrite (plus_assoc b ds n).
(* Goal: lt (S (Nat.add W (PeanoNat.Nat.add (PeanoNat.Nat.add b ds) n))) (Nat.add W (Nat.add ds (S (S (Nat.add b n))))) *)
 rewrite (plus_comm b ds).
(* Goal: @eq nat (PeanoNat.Nat.add (PeanoNat.Nat.add ds b) n) (Nat.add ds (Nat.add b n)) *)
apply plus_assoc_reverse.
Qed.



Lemma nweight_sequent_nimp_right :
 forall (a0 a1 : Int) (b : normal_form) (work : nf_list) 
   (ds : disjs) (ni1 ni2 : nested_imps) (dni1 : decorated_nested_imps)
   (ai : atomic_imps) (n : nat),
 eqv_ni (rev_app dni1 ni1) ni2 ->
 nweight_Sequent work ds (rev_app dni1 (Undecorated (NImp a0 a1 b) :: ni1))
   ai < S n -> nweight_Sequent (b :: work) ds ni2 ai < n.
(* Goal: forall (a0 a1 : Int) (b : normal_form) (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps) (dni1 : decorated_nested_imps) (ai : atomic_imps) (n : nat) (_ : eqv_ni (rev_app dni1 ni1) ni2) (_ : lt (nweight_Sequent work ds (rev_app dni1 (@cons nested_imp (Undecorated (NImp a0 a1 b)) ni1)) ai) (S n)), lt (nweight_Sequent (@cons normal_form b work) ds ni2 ai) n *)
intros a0 a1 b work ds ni1 ni2 dni1 ai n eqv12 lt1.
(* Goal: lt (nweight_Sequent (@cons normal_form (NAtom j) work) ds ni2 ai) n *)
apply lt_S_n.
apply
 lt_trans
  with
    (nweight_Sequent work ds
       (rev_app dni1 (Undecorated (NImp a0 a1 b) :: ni1)) ai); 
 try assumption; clear lt1.
(* Goal: le (S (nweight_Sequent (@cons normal_form (NAtom j) work) ds ni2 ai)) (nweight_Sequent work (@cons (prod Int Int) (@pair Int Int i j) ds) ni1 ai) *)
unfold nweight_Sequent in |- *.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni2) (nweight_ai ai))))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) (Nat.add (nweight_ni ni1) (nweight_ai ai)))) *)
generalize (nweight_ai ai); clear ai; intros ai.
(* Goal: le (S (Nat.add W (Nat.add (nweight_ds ds) n))) (Nat.add W (S (Nat.add (nweight_ds ds) n))) *)
generalize (nweight_ds ds); clear ds; intros ds.
(* Goal: lt (S (Nat.add (nweight_work (@cons normal_form b work)) (Nat.add ds (Nat.add (nweight_ni ni2) ai)))) (Nat.add (nweight_work work) (Nat.add ds (Nat.add (nweight_ni (rev_app dni1 (@cons nested_imp (Undecorated (NImp a0 a1 b)) ni1))) ai))) *)
 rewrite <- (nweight_rev_app dni1 (Undecorated (NImp a0 a1 b) :: ni1)).
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: lt (S (Nat.add (Nat.add (nweight (nf2form b)) (nweight_work work)) (Nat.add ds (Nat.add (nweight_ni ni2) ai)))) (Nat.add (nweight_work work) (Nat.add ds (S (S (Nat.add (Nat.add (Nat.add (nweight (nf2form b)) (nweight_ni ni1)) (nweight_dni dni1)) ai))))) *)
fold nf2form in |- *.
(* Goal: lt (S (Nat.add (Nat.add (nweight (nf2form b)) (nweight_work work)) (Nat.add ds (Nat.add (nweight_ni ni2) ai)))) (Nat.add (nweight_work work) (Nat.add ds (S (S (Nat.add (Nat.add (Nat.add (nweight (nf2form b)) (nweight_ni ni1)) (nweight_dni dni1)) ai))))) *)
generalize (nweight (nf2form b)); clear b; intros b.
(* Goal: le (S (Nat.add (nweight_work work) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (S (Nat.add (nweight_ds ds) n))) *)
generalize (nweight_work work); clear work; intros W.
(* Goal: lt (S (Nat.add (Nat.add b W) (Nat.add ds (Nat.add (nweight_ni ni2) ai)))) (Nat.add W (Nat.add ds (S (S (Nat.add (Nat.add (Nat.add b (nweight_ni ni1)) (nweight_dni dni1)) ai))))) *)
 rewrite (plus_assoc_reverse b (nweight_ni ni1) (nweight_dni dni1)).
(* Goal: lt (S (Nat.add (Nat.add b W) (Nat.add ds (Nat.add (nweight_ni ni2) ai)))) (Nat.add W (Nat.add ds (S (S (Nat.add (Nat.add b (Nat.add (nweight_ni ni1) (nweight_dni dni1))) ai))))) *)
 rewrite (nweight_rev_app dni1 ni1).
(* Goal: lt (S (Nat.add (Nat.add b W) (Nat.add ds (Nat.add (nweight_ni ni2) ai)))) (Nat.add W (Nat.add ds (S (S (Nat.add (Nat.add b (nweight_ni (rev_app dni1 ni1))) ai))))) *)
 rewrite (nweight_eqv_ni (rev_app dni1 ni1) ni2 eqv12).
(* Goal: lt (S (Nat.add (Nat.add b W) (Nat.add ds (Nat.add (nweight_ni ni2) ai)))) (Nat.add W (Nat.add ds (S (S (Nat.add (Nat.add b (nweight_ni ni2)) ai))))) *)
generalize (nweight_ni ni2); clear eqv12 ni2; intros ni2.
(* Goal: lt (S (Nat.add (Nat.add b W) (Nat.add ds (Nat.add ni2 ai)))) (Nat.add W (Nat.add ds (S (S (Nat.add (Nat.add b ni2) ai))))) *)
 rewrite (plus_assoc_reverse b ni2 ai).
(* Goal: forall n : nat, @eq nat (Nat.add (nweight_ni ni1) n) (Nat.add (nweight_ni ni2) n) *)
generalize (ni2 + ai); clear ni1 dni1 ni2 ai n; intros n.
(* Goal: lt (S (Nat.add (Nat.add b W) (Nat.add ds n))) (Nat.add W (Nat.add ds (S (S (Nat.add b n))))) *)
 rewrite (plus_comm b W).
(* Goal: lt (S (Nat.add (PeanoNat.Nat.add W b) (Nat.add ds n))) (Nat.add W (Nat.add ds (S (S (Nat.add b n))))) *)
 rewrite (plus_assoc_reverse W b (ds + n)).
(* Goal: lt (S (Nat.add W (Nat.add b (Nat.add ds n)))) (Nat.add W (Nat.add ds (S (S (Nat.add b n))))) *)
 rewrite (plus_assoc b ds n).
(* Goal: lt (S (Nat.add W (PeanoNat.Nat.add (PeanoNat.Nat.add b ds) n))) (Nat.add W (Nat.add ds (S (S (Nat.add b n))))) *)
 rewrite (plus_comm b ds).
(* Goal: lt (S (Nat.add W (PeanoNat.Nat.add (PeanoNat.Nat.add ds b) n))) (Nat.add W (Nat.add ds (S (S (Nat.add b n))))) *)
 rewrite (plus_assoc_reverse ds b n).
(* Goal: lt (S (Nat.add W (Nat.add ds (Nat.add b n)))) (Nat.add W (Nat.add ds (S (S (Nat.add b n))))) *)
 rewrite <- (plus_Snm_nSm ds (S (b + n))).
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: lt (S (Nat.add W (Nat.add ds (Nat.add b n)))) (Nat.add W (S (Nat.add ds (S (Nat.add b n))))) *)
 rewrite <- (plus_Snm_nSm ds (b + n)).
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: lt (S (Nat.add W (Nat.add ds (Nat.add b n)))) (Nat.add W (S (S (Nat.add ds (Nat.add b n))))) *)
 rewrite <- (plus_Snm_nSm W (S (ds + (b + n)))).
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: lt (S (Nat.add W (Nat.add ds (Nat.add b n)))) (S (Nat.add W (S (Nat.add ds (Nat.add b n))))) *)
 rewrite <- (plus_Snm_nSm W (ds + (b + n))).
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: lt (S (Nat.add W (Nat.add ds (Nat.add b n)))) (S (S (Nat.add W (Nat.add ds (Nat.add b n))))) *)
apply lt_n_Sn.
Qed.



Lemma nweight_sequent_left_disj_left :
 forall (i j : Int) (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps)
   (ai : atomic_imps) (n : nat),
 eqv_ni ni1 ni2 ->
 nweight_Sequent work ((i, j) :: ds) ni1 ai < S n ->
 nweight_Sequent (NAtom i :: work) ds ni2 ai < n.
(* Goal: forall (i j : Int) (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps) (ai : atomic_imps) (n : nat) (_ : eqv_ni ni1 ni2) (_ : lt (nweight_Sequent work (@cons (prod Int Int) (@pair Int Int i j) ds) ni1 ai) (S n)), lt (nweight_Sequent (@cons normal_form (NAtom j) work) ds ni2 ai) n *)
intros i j work ds ni1 ni2 ai n eqv12 lt1.
(* Goal: lt (nweight_Sequent (@cons normal_form (NAtom j) work) ds ni2 ai) n *)
apply lt_S_n.
apply le_lt_trans with (nweight_Sequent work ((i, j) :: ds) ni1 ai);
 try assumption; clear lt1.
(* Goal: le (S (nweight_Sequent (@cons normal_form (NAtom j) work) ds ni2 ai)) (nweight_Sequent work (@cons (prod Int Int) (@pair Int Int i j) ds) ni1 ai) *)
unfold nweight_Sequent in |- *.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni2) (nweight_ai ai))))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) (Nat.add (nweight_ni ni1) (nweight_ai ai)))) *)
generalize (nweight_ai ai); clear ai; intros ai.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni2) ai)))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) (Nat.add (nweight_ni ni1) ai))) *)
 rewrite (nweight_eqv_ni ni1 ni2 eqv12); clear eqv12.
(* Goal: forall n : nat, @eq nat (Nat.add (nweight_ni ni1) n) (Nat.add (nweight_ni ni2) n) *)
generalize (nweight_ni ni2 + ai); clear ni2 ai n; intros n.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: le (S (Nat.add (nweight_work work) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (S (Nat.add (nweight_ds ds) n))) *)
generalize (nweight_work work); clear work; intros W.
(* Goal: le (S (Nat.add W (Nat.add (nweight_ds ds) n))) (Nat.add W (S (Nat.add (nweight_ds ds) n))) *)
generalize (nweight_ds ds); clear ds; intros ds.
(* Goal: le (S (Nat.add W (Nat.add ds n))) (Nat.add W (S (Nat.add ds n))) *)
 rewrite <- (plus_Snm_nSm W (ds + n)).
(* Goal: le (S (Nat.add W (Nat.add ds n))) (Nat.add (S W) (Nat.add ds n)) *)
simpl in |- *; trivial.
Qed.


Lemma nweight_sequent_left_disj_right :
 forall (i j : Int) (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps)
   (ai : atomic_imps) (n : nat),
 eqv_ni ni1 ni2 ->
 nweight_Sequent work ((i, j) :: ds) ni1 ai < S n ->
 nweight_Sequent (NAtom j :: work) ds ni2 ai < n.
(* Goal: forall (i j : Int) (work : nf_list) (ds : disjs) (ni1 ni2 : nested_imps) (ai : atomic_imps) (n : nat) (_ : eqv_ni ni1 ni2) (_ : lt (nweight_Sequent work (@cons (prod Int Int) (@pair Int Int i j) ds) ni1 ai) (S n)), lt (nweight_Sequent (@cons normal_form (NAtom j) work) ds ni2 ai) n *)
intros i j work ds ni1 ni2 ai n eqv12 lt1.
(* Goal: lt (nweight_Sequent (@cons normal_form (NAtom j) work) ds ni2 ai) n *)
apply lt_S_n.
apply le_lt_trans with (nweight_Sequent work ((i, j) :: ds) ni1 ai);
 try assumption; clear lt1.
(* Goal: le (S (nweight_Sequent (@cons normal_form (NAtom j) work) ds ni2 ai)) (nweight_Sequent work (@cons (prod Int Int) (@pair Int Int i j) ds) ni1 ai) *)
unfold nweight_Sequent in |- *.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni2) (nweight_ai ai))))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) (Nat.add (nweight_ni ni1) (nweight_ai ai)))) *)
generalize (nweight_ai ai); clear ai; intros ai.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) (Nat.add (nweight_ni ni2) ai)))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) (Nat.add (nweight_ni ni1) ai))) *)
 rewrite (nweight_eqv_ni ni1 ni2 eqv12); clear eqv12.
(* Goal: forall n : nat, @eq nat (Nat.add (nweight_ni ni1) n) (Nat.add (nweight_ni ni2) n) *)
generalize (nweight_ni ni2 + ai); clear ni2 ai n; intros n.
(* Goal: le (S (Nat.add (nweight_work (@cons normal_form (NAtom j) work)) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (Nat.add (nweight_ds (@cons (prod Int Int) (@pair Int Int i j) ds)) n)) *)
simpl in |- *.
(* Goal: le (S (Nat.add (nweight_work work) (Nat.add (nweight_ds ds) n))) (Nat.add (nweight_work work) (S (Nat.add (nweight_ds ds) n))) *)
generalize (nweight_work work); clear work; intros W.
(* Goal: le (S (Nat.add W (Nat.add (nweight_ds ds) n))) (Nat.add W (S (Nat.add (nweight_ds ds) n))) *)
generalize (nweight_ds ds); clear ds; intros ds.
(* Goal: le (S (Nat.add W (Nat.add ds n))) (Nat.add W (S (Nat.add ds n))) *)
 rewrite <- (plus_Snm_nSm W (ds + n)).
(* Goal: le (S (Nat.add W (Nat.add ds n))) (Nat.add (S W) (Nat.add ds n)) *)
simpl in |- *; trivial.
Qed.
