]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/static/fsle.ma
update in ground and delayed updating
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / fsle.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "ground/xoa/ex_4_4.ma".
16 include "ground/relocation/rtmap_id.ma".
17 include "static_2/notation/relations/subseteq_4.ma".
18 include "static_2/syntax/lveq.ma".
19 include "static_2/static/frees.ma".
20
21 (* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************)
22
23 definition fsle: bi_relation lenv term ≝ λL1,T1,L2,T2.
24                  ∃∃n1,n2,f1,f2. L1 ⊢ 𝐅+❨T1❩ ≘ f1 & L2 ⊢ 𝐅+❨T2❩ ≘ f2 &
25                                 L1 ≋ⓧ*[n1,n2] L2 & ⫰*[n1]f1 ⊆ ⫰*[n2]f2.
26
27 interpretation "free variables inclusion (restricted closure)"
28    'SubSetEq L1 T1 L2 T2 = (fsle L1 T1 L2 T2).
29
30 interpretation "free variables inclusion (term)"
31    'subseteq T1 T2 = (fsle LAtom T1 LAtom T2).
32
33 (* Basic properties *********************************************************)
34
35 lemma fsle_sort: ∀L,s1,s2. ❨L,⋆s1❩ ⊆ ❨L,⋆s2❩.
36 /3 width=8 by frees_sort, pr_sle_refl, ex4_4_intro/ qed.
37
38 lemma fsle_gref: ∀L,l1,l2. ❨L,§l1❩ ⊆ ❨L,§l2❩.
39 /3 width=8 by frees_gref, pr_sle_refl, ex4_4_intro/ qed.