1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "delifting_substitution.ma".
17 (* MULTIPLICITY *************************************************************)
19 (* Note: this gives the number of variable references in M *)
20 let rec mult M on M ≝ match M with
23 | Appl B A ⇒ (mult B) + (mult A)
26 interpretation "term multiplicity"
27 'Multiplicity M = (mult M).
29 notation "hvbox( #{ term 46 M } )"
30 non associative with precedence 90
31 for @{ 'Multiplicity $M }.
33 lemma mult_positive: ∀M. 0 < #{M}.
34 #M elim M -M // /2 width=1/
37 lemma mult_lift: ∀h,M,d. #{↑[d, h] M} = #{M}.
38 #h #M elim M -M normalize //
41 theorem mult_dsubst: ∀D,M,d. #{[d ⬐ D] M} ≤ #{M} * #{D}.
43 [ #i #d elim (lt_or_eq_or_gt i d) #Hid
44 [ >(dsubst_vref_lt … Hid) normalize //
45 | destruct >dsubst_vref_eq normalize //
46 | >(dsubst_vref_gt … Hid) normalize //
49 | normalize #B #A #IHB #IHA #d
50 >distributive_times_plus_r /2 width=1/