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/functions.ma".
16 include "ground_2/lib/exteq.ma".
17 include "apps_2/models/tm.ma".
19 (* TERM MODEL ***************************************************************)
21 (* Properties with extensional equivalencs of evaluations *******************)
23 lemma tm_gc_id: ∀j. ⇡[j]tm_gc ≐ tm_gc.
26 lemma tm_lc_id: ⇡[0←#0]tm_lc ≐ tm_lc.
27 #i elim (eq_or_gt i) #Hi destruct //
28 >tm_vpush_gt // >(flifts_lref_uni 1) <(S_pred … Hi) in ⊢ (???%); -Hi //
31 lemma tm_vlift_comp (l): compatible_2 … (tm_vlift l) (exteq …) (exteq …).
33 >tm_vlift_rw >tm_vlift_rw //
36 lemma tm_vpush_comp (i): compatible_3 … (tm_vpush i) (eq …) (exteq …) (exteq …).
37 #i #T1 #T2 #HT12 #lv1 #lv2 #Hlv #j
38 elim (lt_or_eq_or_gt j i) #Hij destruct
39 [ >tm_vpush_lt // >tm_vpush_lt //
40 | >tm_vpush_eq >tm_vpush_eq //
41 | >tm_vpush_gt // >tm_vpush_gt //
45 lemma tm_ti_comp (T): compatible_3 … (λgv,lv.tm_ti gv lv T) (exteq …) (exteq …) (eq …).
48 | #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
50 | #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
52 | #p #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
53 whd in ⊢ (??%%); /4 width=1 by tm_vlift_comp, tm_vpush_comp, eq_f3/
54 | #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
55 whd in ⊢ (??%%); /3 width=1 by eq_f3/
59 lemma tm_ti_eq (T): tm_ti tm_gc tm_lc T = T.
61 [ #p #I #V #T #IHV #IHT
62 <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT
63 whd in ⊢ (??%?); /3 width=1 by tm_ti_comp, eq_f3/
65 <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT //