]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isi.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_coafter_ist_isi.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "ground/relocation/pr_pat_tls.ma".
16 include "ground/relocation/pr_isi_tls.ma".
17 include "ground/relocation/pr_ist_tls.ma".
18 include "ground/relocation/pr_coafter_nat_tls.ma".
19
20 (* RELATIONAL CO-COMPOSITION FOR PARTIAL RELOCATION MAPS ********************)
21
22 (*** H_coafter_fwd_isid2 *)
23 definition H_pr_coafter_des_ist_sn_isi: predicate pr_map ≝
24            λf1. ∀f2,f. f1 ~⊚ f2 ≘ f → 𝐓❨f1❩ → 𝐈❨f❩ → 𝐈❨f2❩.
25
26 (* Destructions with pr_ist and pr_isi **************************************)
27
28 (*** coafter_fwd_isid2_O_aux *)
29 corec fact pr_coafter_des_ist_sn_isi_unit_aux:
30            ∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1.
31 #f1 #H1f1 #f2 #f #H #H2f1 #Hf
32 cases (pr_pat_inv_unit_bi … H1f1) -H1f1 [ |*: // ] #g1 #H1
33 lapply (pr_ist_inv_push … H2f1 … H1) -H2f1 #H2g1
34 cases (H2g1 (𝟏)) #n #Hn
35 cases (pr_coafter_inv_push_sn … H … H1) -H * #g2 #g #H #H2 #H0
36 [ lapply (pr_isi_inv_push … Hf … H0) -Hf #Hg
37   @(pr_isi_push … H2) -H2
38   /3 width=7 by pr_coafter_tls_sn_tls, pr_pat_unit_succ_tls, pr_ist_tls, pr_isi_tls/
39 | cases (pr_isi_inv_next … Hf … H0)
40 ]
41 qed-.
42
43 (*** coafter_fwd_isid2_aux *)
44 fact pr_coafter_des_ist_sn_isi_aux:
45      (∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1) →
46      ∀i2,f1. @❨𝟏, f1❩ ≘ i2 → H_pr_coafter_des_ist_sn_isi f1.
47 #H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
48 #i2 #IH #f1 #H1f1 #f2 #f #H #H2f1 #Hf
49 elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1
50 elim (pr_coafter_inv_next_sn … H … H1) -H #g #Hg #H0
51 @(IH … Hg1 … Hg) /2 width=3 by pr_ist_inv_next, pr_isi_inv_push/ (* * full auto fails *)
52 qed-.
53
54 (*** coafter_fwd_isid2 *)
55 lemma pr_coafter_des_ist_sn_isi:
56       ∀f1. H_pr_coafter_des_ist_sn_isi f1.
57 #f1 #f2 #f #Hf #H cases (H (𝟏))
58 /3 width=7 by pr_coafter_des_ist_sn_isi_aux, pr_coafter_des_ist_sn_isi_unit_aux/
59 qed-.