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/predtywhead_5.ma".
16 include "static_2/syntax/item_sd.ma".
17 include "static_2/syntax/lenv.ma".
18 include "static_2/syntax/genv.ma".
20 (* WHD NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ****)
22 inductive cwhx (h) (o:sd h) (G:genv): relation2 lenv term ≝
23 | cwhx_sort: ∀L,s. cwhx h o G L (⋆s)
24 | cwhx_abst: ∀p,L,W,T. cwhx h o G L (ⓛ{p}W.T)
25 | cwhx_neg : ∀L,V,T. cwhx h o G (L.ⓓV) T → cwhx h o G L (-ⓓV.T)
29 "whd normality for unbound context-sensitive parallel rt-transition (term)"
30 'PRedTyWHead h o G L T = (cwhx h o G L T).
32 (* Basic inversion lemmas ***************************************************)
34 fact cwhx_inv_lref_aux (h) (o) (G):
35 ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃X⦄ →
37 #h #o #G #Y #X * - X -Y
38 [ #L #s #i #H destruct
39 | #p #L #W #T #i #H destruct
40 | #L #V #T #_ #i #H destruct
44 lemma cwhx_inv_lref (h) (o) (G):
45 ∀L,i. ⦃G,L⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃#i⦄ → ⊥.
46 /2 width=8 by cwhx_inv_lref_aux/ qed-.
48 fact cwhx_inv_gref_aux (h) (o) (G):
49 ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃X⦄ →
51 #h #o #G #Y #X * - X -Y
52 [ #L #s #l #H destruct
53 | #p #L #W #T #l #H destruct
54 | #L #V #T #_ #l #H destruct
58 lemma cwhx_inv_gref (h) (o) (G):
59 ∀L,l. ⦃G,L⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃§l⦄ → ⊥.
60 /2 width=8 by cwhx_inv_gref_aux/ qed-.
62 fact cwhx_inv_pos_aux (h) (o) (G):
63 ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃X⦄ →
65 #h #o #G #Y #X * - X -Y
66 [ #L #s #X1 #X2 #H destruct
67 | #p #L #W #T #X1 #X2 #H destruct
68 | #L #V #T #_ #X1 #X2 #H destruct
72 lemma cwhx_inv_pos (h) (o) (G):
73 ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃+ⓓV.T⦄ → ⊥.
74 /2 width=9 by cwhx_inv_pos_aux/ qed-.