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/predtysn_3.ma".
16 include "static_2/relocation/lex.ma".
17 include "basic_2/rt_transition/cpx_ext.ma".
19 (* EXTENDED PARALLEL RT-TRANSITION FOR FULL LOCAL ENVIRONMENTS **************)
21 definition lpx (G): relation lenv ≝ lex (cpx G).
24 "extended parallel rt-transition on all entries (local environment)"
25 'PRedTySn G L1 L2 = (lpx G L1 L2).
27 (* Basic properties *********************************************************)
30 ∀K1,K2. ❨G,K1❩ ⊢ ⬈ K2 → ∀I1,I2. ❨G,K1❩ ⊢ I1 ⬈ I2 →
31 ❨G,K1.ⓘ[I1]❩ ⊢ ⬈ K2.ⓘ[I2].
32 /2 width=1 by lex_bind/ qed.
34 lemma lpx_refl (G): reflexive … (lpx G).
35 /2 width=1 by lex_refl/ qed.
37 (* Advanced properties ******************************************************)
39 lemma lpx_bind_refl_dx (G):
40 ∀K1,K2. ❨G,K1❩ ⊢ ⬈ K2 →
41 ∀I. ❨G,K1.ⓘ[I]❩ ⊢ ⬈ K2.ⓘ[I].
42 /2 width=1 by lex_bind_refl_dx/ qed.
45 ∀K1,K2. ❨G,K1❩ ⊢ ⬈ K2 → ∀V1,V2. ❨G,K1❩ ⊢ V1 ⬈ V2 →
46 ∀I.❨G,K1.ⓑ[I]V1❩ ⊢ ⬈ K2.ⓑ[I]V2.
47 /2 width=1 by lex_pair/ qed.
49 (* Basic inversion lemmas ***************************************************)
51 (* Basic_2A1: was: lpx_inv_atom1 *)
52 lemma lpx_inv_atom_sn (G):
53 ∀L2. ❨G,⋆❩ ⊢ ⬈ L2 → L2 = ⋆.
54 /2 width=2 by lex_inv_atom_sn/ qed-.
56 lemma lpx_inv_bind_sn (G):
57 ∀I1,L2,K1. ❨G,K1.ⓘ[I1]❩ ⊢ ⬈ L2 →
58 ∃∃I2,K2. ❨G,K1❩ ⊢ ⬈ K2 & ❨G,K1❩ ⊢ I1 ⬈ I2 & L2 = K2.ⓘ[I2].
59 /2 width=1 by lex_inv_bind_sn/ qed-.
61 (* Basic_2A1: was: lpx_inv_atom2 *)
62 lemma lpx_inv_atom_dx (G):
63 ∀L1. ❨G,L1❩ ⊢ ⬈ ⋆ → L1 = ⋆.
64 /2 width=2 by lex_inv_atom_dx/ qed-.
66 lemma lpx_inv_bind_dx (G):
67 ∀I2,L1,K2. ❨G,L1❩ ⊢ ⬈ K2.ⓘ[I2] →
68 ∃∃I1,K1. ❨G,K1❩ ⊢ ⬈ K2 & ❨G,K1❩ ⊢ I1 ⬈ I2 & L1 = K1.ⓘ[I1].
69 /2 width=1 by lex_inv_bind_dx/ qed-.
71 (* Advanced inversion lemmas ************************************************)
73 lemma lpx_inv_unit_sn (G):
74 ∀I,L2,K1. ❨G,K1.ⓤ[I]❩ ⊢ ⬈ L2 →
75 ∃∃K2. ❨G,K1❩ ⊢ ⬈ K2 & L2 = K2.ⓤ[I].
76 /2 width=1 by lex_inv_unit_sn/ qed-.
78 (* Basic_2A1: was: lpx_inv_pair1 *)
79 lemma lpx_inv_pair_sn (G):
80 ∀I,L2,K1,V1. ❨G,K1.ⓑ[I]V1❩ ⊢ ⬈ L2 →
81 ∃∃K2,V2. ❨G,K1❩ ⊢ ⬈ K2 & ❨G,K1❩ ⊢ V1 ⬈ V2 & L2 = K2.ⓑ[I]V2.
82 /2 width=1 by lex_inv_pair_sn/ qed-.
84 lemma lpx_inv_unit_dx (G):
85 ∀I,L1,K2. ❨G,L1❩ ⊢ ⬈ K2.ⓤ[I] →
86 ∃∃K1. ❨G,K1❩ ⊢ ⬈ K2 & L1 = K1.ⓤ[I].
87 /2 width=1 by lex_inv_unit_dx/ qed-.
89 (* Basic_2A1: was: lpx_inv_pair2 *)
90 lemma lpx_inv_pair_dx (G):
91 ∀I,L1,K2,V2. ❨G,L1❩ ⊢ ⬈ K2.ⓑ[I]V2 →
92 ∃∃K1,V1. ❨G,K1❩ ⊢ ⬈ K2 & ❨G,K1❩ ⊢ V1 ⬈ V2 & L1 = K1.ⓑ[I]V1.
93 /2 width=1 by lex_inv_pair_dx/ qed-.
95 lemma lpx_inv_pair (G):
96 ∀I1,I2,L1,L2,V1,V2. ❨G,L1.ⓑ[I1]V1❩ ⊢ ⬈ L2.ⓑ[I2]V2 →
97 ∧∧ ❨G,L1❩ ⊢ ⬈ L2 & ❨G,L1❩ ⊢ V1 ⬈ V2 & I1 = I2.
98 /2 width=1 by lex_inv_pair/ qed-.