(* *)
(**************************************************************************)
-include "Basic-2/grammar/term.ma".
+include "Basic_2/grammar/term.ma".
(* WEIGHT OF A TERM *********************************************************)
(* Basic properties *********************************************************)
+(* Basic_1: was: tweight_lt *)
lemma tw_pos: ∀T. 1 ≤ #[T].
-#T elim T -T /2/
+#T elim T -T //
qed.
(* Basic eliminators ********************************************************)
-axiom tw_wf_ind: ∀R:term→Prop.
+axiom tw_wf_ind: ∀R:predicate term.
(∀T2. (∀T1. #[T1] < #[T2] → R T1) → R T2) →
∀T. R T.
-(* Basic-1: removed theorems 11:
+(* Basic_1: removed theorems 11:
wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O
- weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind
+ weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind
removed local theorems 1: q_ind
*)