csuba/getl csuba_getl_abst_rev
csuba/getl csuba_getl_abbr_rev
csuba/props csuba_refl
+
+# check #############################################################
+
csubc/arity csubc_arity_conf
csubc/arity csubc_arity_trans
csubc/clear csubc_clear_conf
csubc/fwd csubc_gen_head_r
csubc/getl csubc_getl_conf
csubc/props csubc_refl
+
+# waiting ####################################################################
+
csubt/clear csubt_clear_conf
csubt/csuba csubt_csuba
csubt/drop csubt_drop_flat
csubv/props csubv_refl
drop1/fwd drop1_gen_pnil
drop1/fwd drop1_gen_pcons
-drop1/getl drop1_getl_trans
drop1/props drop1_skip_bind
drop1/props drop1_cons_tail
-drop1/props drop1_trans
drop/props drop_ctail
ex0/props aplus_gz_le
ex0/props aplus_gz_ge
leq/props leq_trans
leq/props leq_ahead_false_1
leq/props leq_ahead_false_2
-lift1/fwd lift1_sort
-lift1/fwd lift1_lref
-lift1/fwd lift1_bind
-lift1/fwd lift1_flat
lift1/fwd lift1_cons_tail
lift1/fwd lifts1_flat
lift1/fwd lifts1_nil
(* *)
(**************************************************************************)
+include "Basic_2/unfold/lifts_lifts.ma".
+include "Basic_2/unfold/ldrops_ldrops.ma".
include "Basic_2/static/aaa.ma".
include "Basic_2/computation/lsubc.ma".
-(*
-axiom lsubc_ldrops_trans: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀K2,des. ⇩[des] L2 ≡ K2 →
- ∃∃K1. ⇩[des] L1 ≡ K1 & K1 [RP] ⊑ K2.
-*)
+
+(* NOTE: The constant (0) can not be generalized *)
+axiom lsubc_ldrop_trans: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+ ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 [RP] ⊑ K2.
+
axiom ldrops_lsubc_trans: ∀RP,L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 →
∃∃L2. L1 [RP] ⊑ L2 & ⇩*[des] L2 ≡ K2.
-axiom ldrops_trans: ∀L1,L,des1. ⇩*[des1] L1 ≡ L → ∀L2,des2. ⇩*[des2] L ≡ L2 →
- ⇩*[des2 @ des1] L1 ≡ L2.
-
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
(* Main propertis ***********************************************************)
-axiom aacr_aaa_csubc_lifts: ∀RR,RS,RP.
+axiom aacr_aaa_csubc_lifts: ∀RR,RS,RP.
acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
∀L1,T,A. L1 ⊢ T ÷ A → ∀L0,des. ⇩*[des] L0 ≡ L1 →
∀T0. ⇧*[des] T ≡ T0 → ∀L2. L2 [RP] ⊑ L0 →
⦃L2, T0⦄ [RP] ϵ 〚A〛.
(*
#RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A
-[ (*#L #k #L2 #HL2
+[ #L #k #L0 #des #HL0 #X #H #L2 #HL20
+ >(lifts_inv_sort1 … H) -H
lapply (aacr_acr … H1RP H2RP 𝕒) #HAtom
- @(s2 … HAtom … ◊) // /2 width=2/ *)
-| (* * #L #K #V #B #i #HLK #_ #IHB #L2 #HL2
+ @(s2 … HAtom … ◊) // /2 width=2/
+| * #L #K #V #B #i #HLK #_ #IHB #L0 #des #HL0 #X #H #L2 #HL20
+ elim (lifts_inv_lref1 … H) -H #i0 #Hi0 #H destruct
+ elim (ldrops_ldrop_trans … HL0 … HLK) -L #L #des1 #i1 #HL0 #HLK #Hi1 #Hdes1
+
+ elim (lsubc_ldrop_trans … HL20 … HL0) -L0 #L0 #HL20 #HL0
[
| lapply (aacr_acr … H1RP H2RP B) #HB
@(s2 … HB … ◊) //
-(* @(cp2 … H1RP) *)
- ] *)
-| (* #L #V #T #B #A #_ #_ #IHB #IHA #L2 #HL2
+ @(cp2 … H1RP)
+ ]
+
+| #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
+ elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
lapply (aacr_acr … H1RP H2RP A) #HA
lapply (aacr_acr … H1RP H2RP B) #HB
lapply (s1 … HB) -HB #HB
- @(s5 … HA … ◊ ◊) // /3 width=1/ *)
+ @(s5 … HA … ◊ ◊) // /3 width=5/
| #L #W #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02
elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
@(aacr_abst … H1RP H2RP)
@(IHA (L2. 𝕓{Abst} W2) … (ss des @ ss des3))
/2 width=3/ /3 width=5/ /4 width=6/
]
-| /3 width=1/
-| #L #V #T #A #_ #_ #IH1A #IH2A #L2 #HL2
+| #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
+ elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
+ /3 width=10/
+| #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20
+ elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
lapply (aacr_acr … H1RP H2RP A) #HA
lapply (s1 … HA) #H
- @(s6 … HA … ◊) /2 width=1/ /3 width=1/
+ @(s6 … HA … ◊) /2 width=5/ /3 width=5/
]
*)
lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
(**************************************************************************)
include "Basic_2/grammar/aarity.ma".
-include "Basic_2/unfold/lifts_lifts_vector.ma".
+include "Basic_2/unfold/lifts_lift_vector.ma".
include "Basic_2/computation/acp.ma".
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
elim (lift_total V10 0 1) #V20 #HV120
elim (liftv_total 0 1 V10s) #V20s #HV120s
@(s5 … IHA … (V10 :: V10s) (V20 :: V20s)) /2 width=1/ /2 width=6 by rp_lifts/
- @(HA … (ss des)) /2 width=1/
+ @(HA … (des + 1)) /2 width=1/
[ @(s7 … IHB … HB … HV120) /2 width=1/
| @liftsv_applv //
elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s
lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
∀L,W,T,A,B. RP L W → (
- ∀L0,V0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[ss des] T ≡ T0 →
+ ∀L0,V0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des + 1] T ≡ T0 →
⦃L0, V0⦄ [RP] ϵ 〚B〛 → ⦃L0. 𝕓{Abbr} V0, T0⦄ [RP] ϵ 〚A〛
) →
⦃L, 𝕓{Abst} W. T⦄ [RP] ϵ 〚𝕔 B. A〛.
(* Unfold *******************************************************************)
+notation "hvbox( @ [ T1 ] break f ≡ break T2 )"
+ non associative with precedence 45
+ for @{ 'RAt $T1 $f $T2 }.
+
+notation "hvbox( T1 ▭ break T2 ≡ break T )"
+ non associative with precedence 45
+ for @{ 'RMinus $T1 $T2 $T }.
+
notation "hvbox( ⇧ * [ e ] break T1 ≡ break T2 )"
non associative with precedence 45
for @{ 'RLiftStar $e $T1 $T2 }.
include "Basic_2/grammar/term_weight.ma".
include "Basic_2/grammar/term_simple.ma".
-(* RELOCATION ***************************************************************)
+(* BASIC TERM RELOCATION ****************************************************)
(* Basic_1: includes:
lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat
include "Basic_2/substitution/lift.ma".
-(* RELOCATION ***************************************************************)
+(* BASIC TERM RELOCATION ****************************************************)
(* Main properies ***********************************************************)
include "Basic_2/substitution/lift_lift.ma".
include "Basic_2/substitution/lift_vector.ma".
-(* RELOCATION ***************************************************************)
+(* BASIC TERM VECTOR RELOCATION *********************************************)
(* Main properies ***********************************************************)
include "Basic_2/grammar/term_vector.ma".
include "Basic_2/substitution/lift.ma".
-(* RELOCATION ***************************************************************)
+(* BASIC TERM VECTOR RELOCATION *********************************************)
inductive liftv (d,e:nat) : relation (list term) ≝
| liftv_nil : liftv d e ◊ ◊
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/grammar/term_vector.ma".
+
+(* GENERIC RELOCATION WITH PAIRS ********************************************)
+
+let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with
+[ nil2 ⇒ ⟠
+| cons2 d e des ⇒ {d + i, e} :: pluss des i
+].
+
+interpretation "plus (generic relocation with pairs)"
+ 'plus x y = (pluss x y).
+
+inductive at: list2 nat nat → relation nat ≝
+| at_nil: ∀i. at ⟠ i i
+| at_lt : ∀des,d,e,i1,i2. i1 < d →
+ at des i1 i2 → at ({d, e} :: des) i1 i2
+| at_ge : ∀des,d,e,i1,i2. d ≤ i1 →
+ at des (i1 + e) i2 → at ({d, e} :: des) i1 i2
+.
+
+interpretation "application (generic relocation with pairs)"
+ 'RAt i1 des i2 = (at des i1 i2).
+
+inductive minuss: nat → relation (list2 nat nat) ≝
+| minuss_nil: ∀i. minuss i ⟠ ⟠
+| minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 →
+ minuss i ({d, e} :: des1) ({d - i, e} :: des2)
+| minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 →
+ minuss i ({d, e} :: des1) des2
+.
+
+interpretation "minus (generic relocation with pairs)"
+ 'RMinus des1 i des2 = (minuss i des1 des2).
(* Basic properties *********************************************************)
lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 ≡ V1 →
- ∀I. ⇩*[ss des] L1. 𝕓{I} V1 ≡ L2. 𝕓{I} V2.
+ ∀I. ⇩*[des + 1] L1. 𝕓{I} V1 ≡ L2. 𝕓{I} V2.
#L1 #L2 #des #H elim H -L1 -L2 -des
[ #L #V1 #V2 #HV12 #I
>(lifts_inv_nil … HV12) -HV12 //
elim (lifts_inv_cons … H) -H /3 width=5/
].
qed.
+
+(* Basic_1: removed theorems 1: drop1_getl_trans
+*)
+(*
+lemma ldrops_inv_skip2: ∀des2,L1,I,K2,V2. ⇩*[des2] L1 ≡ K2. 𝕓{I} V2 →
+ ∀des,i. des ▭ i ≡ des2 →
+ ∃∃K1,V1,des1. des ▭ (i + 1) ≡ des1 &
+ ⇩*[des1] K1 ≡ K2 &
+ ⇧*[des1] V2 ≡ V1 &
+ L1 = K1. 𝕓{I} V1.
+*)
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/substitution/ldrop_ldrop.ma".
+include "Basic_2/unfold/ldrops.ma".
+
+(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
+
+(* Properties concerning basic local environment slicing ********************)
+
+lemma ldrops_ldrop_trans: ∀L1,L,des. ⇩*[des] L1 ≡ L → ∀L2,i. ⇩[0, i] L ≡ L2 →
+ ∃∃L0,des0,i0. ⇩[0, i0] L1 ≡ L0 & ⇩*[des0] L0 ≡ L2 &
+ @[i] des ≡ i0 & des ▭ i ≡ des0.
+#L1 #L #des #H elim H -L1 -L -des
+[ /2 width=7/
+| #L1 #L3 #L #des3 #d #e #_ #HL3 #IHL13 #L2 #i #HL2
+ elim (lt_or_ge i d) #Hid
+ [ elim (ldrop_trans_le … HL3 … HL2 ?) -L /2 width=2/ #L #HL3 #HL2
+ elim (IHL13 … HL3) -L3 /3 width=7/
+ | lapply (ldrop_trans_ge … HL3 … HL2 ?) -L // #HL32
+ elim (IHL13 … HL32) -L3 /3 width=7/
+ ]
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/unfold/ldrops_ldrop.ma".
+
+(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
+
+(* Main properties **********************************************************)
+
+(* Basic_1: was: drop1_trans *)
+theorem ldrops_trans: ∀L,L2,des2. ⇩*[des2] L ≡ L2 → ∀L1,des1. ⇩*[des1] L1 ≡ L →
+ ⇩*[des2 @ des1] L1 ≡ L2.
+#L #L2 #des2 #H elim H -L -L2 -des2 // /3 width=3/
+qed.
(* *)
(**************************************************************************)
-include "Basic_2/grammar/term_vector.ma".
include "Basic_2/substitution/lift.ma".
+include "Basic_2/unfold/gr2.ma".
-(* GENERIC RELOCATION *******************************************************)
-
-let rec ss (des:list2 nat nat) ≝ match des with
-[ nil2 ⇒ ⟠
-| cons2 d e des ⇒ {d + 1, e} :: ss des
-].
+(* GENERIC TERM RELOCATION **************************************************)
inductive lifts: list2 nat nat → relation term ≝
| lifts_nil : ∀T. lifts ⟠ T T
⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} :: des) T1 T2
.
-interpretation "generic relocation"
+interpretation "generic relocation (term)"
'RLiftStar des T1 T2 = (lifts des T1 T2).
(* Basic inversion lemmas ***************************************************)
∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[des] T ≡ T2.
/2 width=3/ qed-.
+(* Basic_1: was: lift1_sort *)
+lemma lifts_inv_sort1: ∀T2,k,des. ⇧*[des] ⋆k ≡ T2 → T2 = ⋆k.
+#T2 #k #des elim des -des
+[ #H <(lifts_inv_nil … H) -H //
+| #d #e #des #IH #H
+ elim (lifts_inv_cons … H) -H #X #H
+ >(lift_inv_sort1 … H) -H /2 width=1/
+]
+qed-.
+
+(* Basic_1: was: lift1_lref *)
+lemma lifts_inv_lref1: ∀T2,des,i1. ⇧*[des] #i1 ≡ T2 →
+ ∃∃i2. @[i1] des ≡ i2 & T2 = #i2.
+#T2 #des elim des -des
+[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3/
+| #d #e #des #IH #i1 #H
+ elim (lifts_inv_cons … H) -H #X #H1 #H2
+ elim (lift_inv_lref1 … H1) -H1 * #Hdi1 #H destruct
+ elim (IH … H2) -IH -H2 /3 width=3/
+]
+qed-.
+
+lemma lifts_inv_gref1: ∀T2,p,des. ⇧*[des] §p ≡ T2 → T2 = §p.
+#T2 #p #des elim des -des
+[ #H <(lifts_inv_nil … H) -H //
+| #d #e #des #IH #H
+ elim (lifts_inv_cons … H) -H #X #H
+ >(lift_inv_gref1 … H) -H /2 width=1/
+]
+qed-.
+
+(* Basic_1: was: lift1_bind *)
lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇧*[des] 𝕓{I} V1. U1 ≡ T2 →
- ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[ss des] U1 ≡ U2 &
+ ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des + 1] U1 ≡ U2 &
T2 = 𝕓{I} V2. U2.
#I #T2 #des elim des -des
[ #V1 #U1 #H
]
qed-.
+(* Basic_1: was: lift1_flat *)
lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇧*[des] 𝕗{I} V1. U1 ≡ T2 →
∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des] U1 ≡ U2 &
T2 = 𝕗{I} V2. U2.
(* Basic properties *********************************************************)
lemma lifts_bind: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
- ∀T1. ⇧*[ss des] T1 ≡ T2 →
+ ∀T1. ⇧*[des + 1] T1 ≡ T2 →
⇧*[des] 𝕓{I} V1. T1 ≡ 𝕓{I} V2. T2.
#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
[ #V #T1 #H >(lifts_inv_nil … H) -H //
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/substitution/lift_lift.ma".
+include "Basic_2/unfold/lifts.ma".
+
+(* GENERIC TERM RELOCATION **************************************************)
+
+(* Properties concerning basic term relocation ******************************)
+
+(* Basic_1: was: lift1_xhg *)
+lemma lifts_lift_trans_le: ∀T1,T,des. ⇧*[des] T1 ≡ T → ∀T2. ⇧[0, 1] T ≡ T2 →
+ ∃∃T0. ⇧[0, 1] T1 ≡ T0 & ⇧*[des + 1] T0 ≡ T2.
+#T1 #T #des #H elim H -T1 -T -des
+[ /2 width=3/
+| #T1 #T3 #T #des #d #e #HT13 #_ #IHT13 #T2 #HT2
+ elim (IHT13 … HT2) -T #T #HT3 #HT2
+ elim (lift_trans_le … HT13 … HT3 ?) -T3 // /3 width=5/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/substitution/lift_lift_vector.ma".
+include "Basic_2/unfold/lifts_lift.ma".
+include "Basic_2/unfold/lifts_vector.ma".
+
+(* GENERIC RELOCATION *******************************************************)
+
+(* Main properties **********************************************************)
+
+(* Basic_1: was: lifts1_xhg *)
+lemma liftsv_liftv_trans_le: ∀T1s,Ts,des. ⇧*[des] T1s ≡ Ts →
+ ∀T2s:list term. ⇧[0, 1] Ts ≡ T2s →
+ ∃∃T0s. ⇧[0, 1] T1s ≡ T0s & ⇧*[des + 1] T0s ≡ T2s.
+#T1s #Ts #des #H elim H -T1s -Ts
+[ #T1s #H
+ >(liftv_inv_nil1 … H) -T1s /2 width=3/
+| #T1s #Ts #T1 #T #HT1 #_ #IHT1s #X #H
+ elim (liftv_inv_cons1 … H) -H #T2 #T2s #HT2 #HT2s #H destruct
+ elim (IHT1s … HT2s) -Ts #Ts #HT1s #HT2s
+ elim (lifts_lift_trans_le … HT1 … HT2) -T /3 width=5/
+]
+qed-.
(* *)
(**************************************************************************)
-include "Basic_2/substitution/lift_lift.ma".
-include "Basic_2/unfold/lifts.ma".
+include "Basic_2/unfold/lifts_lift.ma".
(* GENERIC RELOCATION *******************************************************)
(* Main properties **********************************************************)
-(* Basic_1: was: lift1_xhg *)
-lemma lifts_lift_trans_le: ∀T1,T,des. ⇧*[des] T1 ≡ T → ∀T2. ⇧[0, 1] T ≡ T2 →
- ∃∃T0. ⇧[0, 1] T1 ≡ T0 & ⇧*[ss des] T0 ≡ T2.
-#T1 #T #des #H elim H -T1 -T -des
-[ /2 width=3/
-| #T1 #T3 #T #des #d #e #HT13 #_ #IHT13 #T2 #HT2
- elim (IHT13 … HT2) -T #T #HT3 #HT2
- elim (lift_trans_le … HT13 … HT3 ?) -T3 // /3 width=5/
-]
-qed-.
-
(* Basic_1: was: lift1_lift1 *)
theorem lifts_trans: ∀T1,T,des1. ⇧*[des1] T1 ≡ T → ∀T2:term. ∀des2. ⇧*[des2] T ≡ T2 →
⇧*[des1 @ des2] T1 ≡ T2.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "Basic_2/substitution/lift_lift_vector.ma".
-include "Basic_2/unfold/lifts_lifts.ma".
-include "Basic_2/unfold/lifts_vector.ma".
-
-(* GENERIC RELOCATION *******************************************************)
-
-(* Main properties **********************************************************)
-
-(* Basic_1: was: lifts1_xhg *)
-lemma liftsv_liftv_trans_le: ∀T1s,Ts,des. ⇧*[des] T1s ≡ Ts →
- ∀T2s:list term. ⇧[0, 1] Ts ≡ T2s →
- ∃∃T0s. ⇧[0, 1] T1s ≡ T0s & ⇧*[ss des] T0s ≡ T2s.
-#T1s #Ts #des #H elim H -T1s -Ts
-[ #T1s #H
- >(liftv_inv_nil1 … H) -T1s /2 width=3/
-| #T1s #Ts #T1 #T #HT1 #_ #IHT1s #X #H
- elim (liftv_inv_cons1 … H) -H #T2 #T2s #HT2 #HT2s #H destruct
- elim (IHT1s … HT2s) -Ts #Ts #HT1s #HT2s
- elim (lifts_lift_trans_le … HT1 … HT2) -T /3 width=5/
-]
-qed-.
include "Basic_2/substitution/lift_vector.ma".
include "Basic_2/unfold/lifts.ma".
-(* GENERIC RELOCATION *******************************************************)
+(* GENERIC TERM VECTOR RELOCATION *******************************************)
inductive liftsv (des:list2 nat nat) : relation (list term) ≝
| liftsv_nil : liftsv des ◊ ◊
(* ARITHMETICAL PROPERTIES **************************************************)
-(* equations ****************************************************************)
+(* Equations ****************************************************************)
lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p).
/2 by plus_minus/ qed.
(*
lemma pippo: ∀x,y,z. x < z → y < z - x → x + y < z.
/3 width=2/
+
+lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
+#m #n elim (lt_or_ge m n) /2 width=1/ /3 width=2/
+qed-.
*)
projects / helm.git / commitdiff