X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fmodels%2Ftm_props.ma;h=280bd8e51086a20e3738cf54996ee13e9a0a31aa;hp=260d2415aba20c8f56688c92f045c1a3ba02808d;hb=cc600ed1e115d5566947288d532a1e89d989227f;hpb=ea918ec7701db4458c5ca25885e80abc6fed1be7

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma
index 260d2415a..280bd8e51 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma
@@ -12,43 +12,72 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/rt_equivalence/cpcs_drops.ma".
 include "basic_2/rt_equivalence/cpcs_cpcs.ma".
+include "apps_2/functional/mf_lifts.ma".
+include "apps_2/functional/mf_cpr.ma".
 include "apps_2/models/model_props.ma".
-include "apps_2/models/tm.ma".
+include "apps_2/models/tm_vpush.ma".
 
 (* TERM MODEL ***************************************************************)
 
-lemma tm_md (h): ∀T,V,gv,lv. ⟦+ⓓV.T⟧[gv,lv] ≗{TM h} ⟦T⟧[gv,⫯[O←⟦V⟧[gv,lv]]lv].
-#h #T elim T *
-[ /4 width=3 by cpc_cpcs, cpm_zeta, or_introl/
-| #i #V #gv #lv
-  elim (eq_or_gt i) #Hi destruct
-  [ elim (lifts_total (⟦V⟧[gv,lv]) (𝐔❴1❵)) #W #HVW
-    >tm_ti_lref >vpush_eq
-    >tm_ti_bind >tm_ti_lref >tm_vpush_eq
-    /5 width=3 by cpc_cpcs, cpm_zeta, cpm_delta, or_introl/
-  | >tm_ti_lref >vpush_gt //
-    >tm_ti_bind >tm_ti_lref >tm_vpush_gt //
-    /4 width=3 by cpc_cpcs, cpm_zeta, or_introl/
-  ]
-| #l #V #gv #lv
-  >tm_ti_bind >tm_ti_gref >tm_ti_gref
-  /4 width=3 by cpc_cpcs, cpm_zeta, or_introl/
-| #p #I #W #T #IHW #IHT #V #gv #lv
-  >tm_ti_bind in ⊢ (???%);
+lemma cpcs_repl (h) (G) (L): replace_2 … (cpcs h G L) (cpcs h G L) (cpcs h G L).
+/3 width=5 by cpcs_trans, cpcs_sym/ qed-.
 (*
-  
-  >tm_ti_bind >tm_ti_bind
-  @cpc_cpcs @or_introl
-  @cpm_bind 
-  
-  /4 width=3 by cpc_cpcs, cpm_zeta, or_introl/
+lemma pippo (h) (gv) (lv) (T): ●[gv,lv]T = ⟦T⟧{TM h}[gv,lv].
+// qed.
+
+lemma tm_mi (h) (gv1) (gv2) (lv1) (lv2) (p) (W) (T):
+            ⟦W⟧[gv1,lv1] ≗{TM h} ⟦W⟧[gv2,lv2] →
+            (∀d. ⟦T⟧[gv1,⫯[0←d]lv1] ≗ ⟦T⟧[gv2,⫯[0←d]lv2]) →
+            ⟦ⓛ{p}W.T⟧[gv1,lv1] ≗ ⟦ⓛ{p}W.T⟧[gv2,lv2].
+#h #gv1 #gv2 #lv1 #lv2 #p #W #T #HW #HT
+>tm_ti_bind >tm_ti_bind
+@(cpcs_bind1 … HW)
+
+
+
+<pippo in ⊢ (????%?); >(mf_comp … T) in ⊢ (????%?);
+[2: @@tm_vpush_vlift_join_O
+
+<pippo in ⊢ (????%?);
+
+lapply (HT (#0)) -HT #HT
+*)
+
+lemma tm_md (h) (p) (gv) (lv) (V) (T):
+            ⓓ{p}V.⟦T⟧{TM h}[⇡[0]gv,⇡[0←#0]lv] ≗{TM h} V⊕{TM h}[p]⟦T⟧{TM h}[gv,⫯{TM h}[0←V]lv].
+#h #p #gv #lv #V #T
+>tm_co_rw >(mf_lifts_basic_SO_dx T 0)
+>(mf_comp … T) in ⊢ (???%);
+[2: @tm_vpush_vlift_join_O |4: @exteq_refl |3,5: skip ]
+/6 width=4 by mf_delta_drops, cpcs_bind1, cpc_cpcs, drops_refl, or_introl/
+qed.
+
+lemma tm_mz (h) (V) (T): V ⊕[Ⓣ] T ≗{TM h} T.
+/4 width=3 by cpc_cpcs, cpm_zeta, or_introl/ qed.
+
+lemma tm_me (h) (gv) (lv) (U) (T):
+            ⟦ⓝU.T⟧[gv,lv] ≗{TM h} ⟦T⟧[gv,lv].
+/4 width=1 by cpc_cpcs, cpm_eps, or_introl/ qed.
+
+lemma tm_mb (h) (p) (gv) (lv) (d) (W) (T):
+            d@⟦ⓛ{p}W.T⟧[gv,lv] ≗{TM h} d⊕[p]⟦T⟧[gv,⫯[0←d]lv].
+#h #p #gv #lv #d #W #T
+@cpcs_repl [5: @tm_md |4: /4 width=2 by cpc_cpcs, cpm_beta, or_intror/ |1,2: skip ]
+/5 width=1 by cpcs_bind1, cpc_cpcs, cpm_eps, or_introl/
+qed.
+
+lemma ti_mh (h) (p) (d1) (d2) (d3):
+            d1@(d2⊕[p]d3) ≗{TM h} d2⊕[p](d1@d3).
+/4 width=3 by cpc_cpcs, cpm_theta, or_introl/ qed.
 
 definition is_tm (h): is_model (TM h) ≝ mk_is_model …. //
-[ 
+[ @cpcs_repl
+| #p #V1 #V2 #HV #T1 #T2 #HT
+  @(cpcs_bind1 … HV) @(cpcs_lifts_bi … HT)
+  /2 width=5 by drops_drop/
+| #V1 #V2 #HV #T1 #T2 #HT
+  @(cpcs_flat … HV … HT)
 |
-| #gv #lv #p #V #T
-  @cpcs_cprs_dx
-  @cprs_step_sn
-  [2: @cpm_bind // | skip ]  
-*)
+].