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 "basic_2/notation/relations/lazyeq_4.ma".
16 include "basic_2/grammar/term.ma".
17 include "basic_2/static/sd.ma".
19 (* STRATIFIED EQUIVALENCE FOR TERMS *****************************************)
21 inductive steq (h) (g): relation term ≝
22 | steq_refl: ∀T. steq h g T T
23 | steq_zero: ∀k1,k2. deg h g k1 0 → deg h g k2 0 → steq h g (⋆k1) (⋆k2)
27 "stratified equivalence (term)"
28 'LazyEq h g T1 T2 = (steq h g T1 T2).
30 (* Basic inversion lemmas ****************************************************)
32 lemma steq_inv: ∀h,g,T1,T2. T1 ≡[h, g] T2 → T1 = T2 ∨
33 ∃∃k1,k2. deg h g k1 0 & deg h g k2 0 & T1 = ⋆k1 & T2 = ⋆k2.
34 #h #g #T1 #T2 * /3 width=6 by or_introl, or_intror, ex4_2_intro/
37 (* Basic properties *********************************************************)
39 lemma steq_sym: ∀h,g. symmetric … (steq h g).
40 #h #g #T1 #T2 * /2 width=1 by steq_zero/