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/static/aaa.ma".
16 include "Basic_2/computation/lsubc.ma".
18 axiom lsubc_ldrops_trans: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀K2,des. ⇓[des] L2 ≡ K2 →
19 ∃∃K1. ⇓[des] L1 ≡ K1 & K1 [RP] ⊑ K2.
21 axiom ldrops_lsubc_trans: ∀RP,L1,K1,des. ⇓[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 →
22 ∃∃L2. L1 [RP] ⊑ L2 & ⇓[des] L2 ≡ K2.
24 axiom lifts_trans: ∀T1,T,des1. ⇑[des1] T1 ≡ T → ∀T2:term. ∀des2. ⇑[des2] T ≡ T2 →
25 ⇑[des1 @ des2] T1 ≡ T2.
27 axiom ldrops_trans: ∀L1,L,des1. ⇓[des1] L1 ≡ L → ∀L2,des2. ⇓[des2] L ≡ L2 →
28 ⇓[des2 @ des1] L1 ≡ L2.
30 (* ABSTRACT COMPUTATION PROPERTIES ******************************************)
32 (* Main propertis ***********************************************************)
34 axiom aacr_aaa_csubc_lifts: ∀RR,RS,RP.
35 acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
36 ∀L1,T,A. L1 ⊢ T ÷ A → ∀L0,des. ⇓[des] L0 ≡ L1 →
37 ∀T0. ⇑[des] T ≡ T0 → ∀L2. L2 [RP] ⊑ L0 →
40 #RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A
42 lapply (aacr_acr … H1RP H2RP 𝕒) #HAtom
43 @(s2 … HAtom … ◊) // /2 width=2/ *)
44 | (* * #L #K #V #B #i #HLK #_ #IHB #L2 #HL2
46 | lapply (aacr_acr … H1RP H2RP B) #HB
50 | (* #L #V #T #B #A #_ #_ #IHB #IHA #L2 #HL2
51 lapply (aacr_acr … H1RP H2RP A) #HA
52 lapply (aacr_acr … H1RP H2RP B) #HB
53 lapply (s1 … HB) -HB #HB
54 @(s5 … HA … ◊ ◊) // /3 width=1/ *)
55 | #L #W #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02
56 elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
57 @(aacr_abst … H1RP H2RP)
58 [ lapply (aacr_acr … H1RP H2RP B) #HB
59 @(s1 … HB) /2 width=5/
60 | #L3 #V3 #T3 #des3 #HL32 #HT03 #HB
61 elim (lifts_total des3 W0) #W2 #HW02
62 elim (ldrops_lsubc_trans … HL32 … HL02) -L2 #L2 #HL32 #HL20
63 @(IHA (L2. 𝕓{Abst} W2) … (ss des @ ss des3))
64 /2 width=3/ /3 width=5/ /4 width=6/
67 | #L #V #T #A #_ #_ #IH1A #IH2A #L2 #HL2
68 lapply (aacr_acr … H1RP H2RP A) #HA
70 @(s6 … HA … ◊) /2 width=1/ /3 width=1/
73 lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
74 ∀L,T,A. L ⊢ T ÷ A → RP L T.
75 #RR #RS #RP #H1RP #H2RP #L #T #A #HT
76 lapply (aacr_acr … H1RP H2RP A) #HA
77 @(s1 … HA) /2 width=8/