(**************************************************************************)
include "Basic-2/grammar/lenv_weight.ma".
+include "Basic-2/grammar/cl_shift.ma".
(* WEIGHT OF A CLOSURE ******************************************************)
(* Basic properties *********************************************************)
-lemma cw_shift: βK,I,V,T. #[K. π{I} V, T] < #[K, π{I} V. T].
-normalize //
-qed.
+(* Basic-1: was: flt_wf__q_ind *)
+(* Basic-1: was: flt_wf_ind *)
axiom cw_wf_ind: βR:lenvβtermβProp.
(βL2,T2. (βL1,T1. #[L1,T1] < #[L2,T2] β R L1 T1) β R L2 T2) β
βL,T. R L T.
+
+(* Basic-1: was: flt_shift *)
+lemma cw_shift: βK,I,V,T. #[K. π{I} V, T] < #[K, π{I} V. T].
+normalize //
+qed.
+
+lemma tw_shift: βL,T. #[L, T] β€ #[L @ T].
+#L elim L //
+#K #I #V #IHL #T
+@transitive_le [3: @IHL |2: /2/ | skip ]
+qed.
+
+(* Basic-1: removed theorems 6:
+ flt_thead_sx flt_thead_dx flt_arith0 flt_arith1 flt_arith2 flt_trans
+*)