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 "ground_2/lib/lstar.ma".
16 include "basic_2/relocation/drops.ma".
18 (* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
20 (* Properties on reflexive and transitive closure ***************************)
22 (* Basic_2A1: was: d_liftable_LTC *)
23 lemma d2_liftable_LTC: ∀R. d_liftable2 R → d_liftable2 (LTC … R).
24 #R #HR #K #T1 #T2 #H elim H -T2
25 [ #T2 #HT12 #L #c #f #HLK #U1 #HTU1
26 elim (HR … HT12 … HLK … HTU1) /3 width=3 by inj, ex2_intro/
27 | #T #T2 #_ #HT2 #IHT1 #L #c #f #HLK #U1 #HTU1
28 elim (IHT1 … HLK … HTU1) -T1 #U #HTU #HU1
29 elim (HR … HT2 … HLK … HTU) -HR -K -T /3 width=5 by step, ex2_intro/
33 (* Basic_2A1: was: d_deliftable_sn_LTC *)
34 lemma d2_deliftable_sn_LTC: ∀R. d_deliftable2_sn R → d_deliftable2_sn (LTC … R).
35 #R #HR #L #U1 #U2 #H elim H -U2
36 [ #U2 #HU12 #K #c #f #HLK #T1 #HTU1
37 elim (HR … HU12 … HLK … HTU1) -HR -L -U1 /3 width=3 by inj, ex2_intro/
38 | #U #U2 #_ #HU2 #IHU1 #K #c #f #HLK #T1 #HTU1
39 elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
40 elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by step, ex2_intro/
44 lemma dropable_sn_TC: ∀R. dropable_sn R → dropable_sn (LTC … R).
45 #R #HR #L1 #K1 #c #f #HLK1 #L2 #u2 #H elim H -L2
46 [ #L2 #HL12 #u1 #H elim (HR … HLK1 … HL12 … H) -HR -L1 -u2
47 /3 width=3 by inj, ex2_intro/
48 | #L #L2 #_ #HL2 #IH #u1 #H elim (IH … H) -IH
49 #K #HK1 #HLK elim (HR … HLK … HL2 … H) -HR -L -u2
50 /3 width=3 by step, ex2_intro/
54 (* Basic_2A1: was: d_liftable_llstar *)
55 lemma d2_liftable_llstar: ∀R. d_liftable2 R → ∀d. d_liftable2 (llstar … R d).
56 #R #HR #d #K #T1 #T2 #H @(lstar_ind_r … d T2 H) -d -T2
57 [ #L #c #f #_ #U1 #HTU1 -HR -K -c /2 width=3 by ex2_intro/
58 | #d #T #T2 #_ #HT2 #IHT1 #L #c #f #HLK #U1 #HTU1
59 elim (IHT1 … HLK … HTU1) -T1 #U #HTU #HU1
60 elim (HR … HT2 … HLK … HTU) -T /3 width=5 by lstar_dx, ex2_intro/
64 (* Basic_2A1: was: d_deliftable_sn_llstar *)
65 lemma d2_deliftable_sn_llstar: ∀R. d_deliftable2_sn R →
66 ∀d. d_deliftable2_sn (llstar … R d).
67 #R #HR #d #L #U1 #U2 #H @(lstar_ind_r … d U2 H) -d -U2
68 [ /2 width=3 by lstar_O, ex2_intro/
69 | #d #U #U2 #_ #HU2 #IHU1 #K #c #f #HLK #T1 #HTU1
70 elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
71 elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/