#RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A
[ #L #k #L0 #des #HL0 #X #H #L2 #HL20
>(lifts_inv_sort1 … H) -H
- lapply (aacr_acr … H1RP H2RP ⓪) #HAtom
+ lapply (aacr_acr … H1RP H2RP (⓪)) #HAtom
@(s2 … HAtom … ◊) // /2 width=2/
| #I #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20
lapply (aacr_acr … H1RP H2RP B) #HB
fact snv_ssta_conf_aux: ∀h,g,L,T. (
∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] →
∀U0,l. ⦃h, L0⦄ ⊢ T0 •[g, l + 1] U0 →
- #{L0, T0} < #{L, T} → ⦃h, L0⦄ ⊩ U0 :[g]
+ ♯{L0, T0} < ♯{L, T} → ⦃h, L0⦄ ⊩ U0 :[g]
) →
∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] →
∀U0,l. ⦃h, L0⦄ ⊢ T0 •[g, l + 1] U0 →
(* WEIGHT OF A CLOSURE ******************************************************)
-definition fw: lenv → term → ? ≝ λL,T. #{L} + #{T}.
+definition fw: lenv → term → ? ≝ λL,T. ♯{L} + ♯{T}.
interpretation "weight (closure)" 'Weight L T = (fw L T).
(* Basic properties *********************************************************)
(* Basic_1: was: flt_shift *)
-lemma fw_shift: ∀a,K,I,V,T. #{K. ⓑ{I} V, T} < #{K, ⓑ{a,I} V. T}.
+lemma fw_shift: ∀a,K,I,V,T. ♯{K. ⓑ{I} V, T} < ♯{K, ⓑ{a,I} V. T}.
normalize //
qed.
-lemma tw_shift: ∀L,T. #{L, T} ≤ #{L @@ T}.
+lemma tw_shift: ∀L,T. ♯{L, T} ≤ ♯{L @@ T}.
#L elim L //
#K #I #V #IHL #T
@transitive_le [3: @IHL |2: /2 width=2/ | skip ]
qed.
-lemma fw_tpair_sn: ∀I,L,V,T. #{L, V} < #{L, ②{I}V.T}.
+lemma fw_tpair_sn: ∀I,L,V,T. ♯{L, V} < ♯{L, ②{I}V.T}.
normalize in ⊢ (?→?→?→?→?%%); //
qed.
-lemma fw_tpair_dx: ∀I,L,V,T. #{L, T} < #{L, ②{I}V.T}.
+lemma fw_tpair_dx: ∀I,L,V,T. ♯{L, T} < ♯{L, ②{I}V.T}.
normalize in ⊢ (?→?→?→?→?%%); //
qed.
-lemma fw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. #{L, V2} < #{L, ②{I1}V1.②{I2}V2.T}.
+lemma fw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. ♯{L, V2} < ♯{L, ②{I1}V1.②{I2}V2.T}.
normalize in ⊢ (?→?→?→?→?→?→?%%); /2 width=1/
qed.
lemma fw_tpair_sn_sn_shift: ∀I,I1,I2,L,V1,V2,T.
- #{L.ⓑ{I}V1, T} < #{L, ②{I1}V1.②{I2}V2.T}.
-normalize in ⊢ (?→?→?→?→?→?→?→?%%); /3 width=1/
+ ♯{L.ⓑ{I}V1, T} < ♯{L, ②{I1}V1.②{I2}V2.T}.
+normalize in ⊢ (?→?→?→?→?→?→?→?%%); /3 width=1/
qed.
lemma fw_tpair_sn_dx_shift: ∀I,I1,I2,L,V1,V2,T.
- #{L.ⓑ{I}V2, T} < #{L, ②{I1}V1.②{I2}V2.T}.
+ ♯{L.ⓑ{I}V2, T} < ♯{L, ②{I1}V1.②{I2}V2.T}.
normalize in ⊢ (?→?→?→?→?→?→?→?%%); /2 width=1/
qed.
(* Basic_eliminators ********************************************************)
-fact lenv_ind_dx_aux: ∀R:predicate lenv. R ⋆ →
+fact lenv_ind_dx_aux: ∀R:predicate lenv. R (⋆) →
(∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) →
∀d,L. |L| = d → R L.
#R #Hatom #Hpair #d @(nat_ind_plus … d) -d
]
qed-.
-lemma lenv_ind_dx: ∀R:predicate lenv. R ⋆ →
+lemma lenv_ind_dx: ∀R:predicate lenv. R (⋆) →
(∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) →
∀L. R L.
/3 width=2 by lenv_ind_dx_aux/ qed-.
let rec lw L ≝ match L with
[ LAtom ⇒ 0
-| LPair L _ V ⇒ lw L + #{V}
+| LPair L _ V ⇒ lw L + ♯{V}
].
interpretation "weight (local environment)" 'Weight L = (lw L).
(* Basic properties *********************************************************)
-lemma lw_pair: ∀I,L,V. #{L} < #{(L.ⓑ{I}V)}.
+lemma lw_pair: ∀I,L,V. ♯{L} < ♯{L.ⓑ{I}V}.
/3 width=1/ qed.
(* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *)
(* Basic properties *********************************************************)
(* Basic_1: was: tweight_lt *)
-lemma tw_pos: ∀T. 1 ≤ #{T}.
+lemma tw_pos: ∀T. 1 ≤ ♯{T}.
#T elim T -T //
qed.
(* Grammar ******************************************************************)
notation "⓪"
- non associative with precedence 90
+ non associative with precedence 55
for @{ 'Item0 }.
notation "hvbox( ⓪ { term 46 I } )"
- non associative with precedence 90
+ non associative with precedence 55
for @{ 'Item0 $I }.
notation "⋆"
- non associative with precedence 90
+ non associative with precedence 46
for @{ 'Star }.
notation "hvbox( ⋆ term 90 k )"
- non associative with precedence 90
+ non associative with precedence 55
for @{ 'Star $k }.
notation "hvbox( # term 90 i )"
- non associative with precedence 90
+ non associative with precedence 55
for @{ 'LRef $i }.
notation "hvbox( § term 90 p )"
- non associative with precedence 90
+ non associative with precedence 55
for @{ 'GRef $p }.
notation "hvbox( ② term 55 T1 . break term 55 T )"
non associative with precedence 50
for @{ 'DxItem4 $T $I $T1 $T2 $T3 }.
-notation "hvbox( # { term 46 x } )"
+notation "hvbox( ♯ { term 46 x } )"
non associative with precedence 90
for @{ 'Weight $x }.
-notation "hvbox( # { term 46 x , break term 46 y } )"
+notation "hvbox( ♯ { term 46 x , break term 46 y } )"
non associative with precedence 90
for @{ 'Weight $x $y }.
fact tpr_conf_flat_flat:
∀I,V0,V1,T0,T1,V2,T2. (
- ∀X0:term. #{X0} < #{V0} + #{T0} + 1 →
+ ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
fact tpr_conf_flat_beta:
∀a,V0,V1,T1,V2,W0,U0,T2. (
- ∀X0:term. #{X0} < #{V0} + (#{W0} + #{U0} + 1) + 1 →
+ ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{U0} + 1) + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
*)
fact tpr_conf_flat_theta:
∀a,V0,V1,T1,V2,V,W0,W2,U0,U2. (
- ∀X0:term. #{X0} < #{V0} + (#{W0} + #{U0} + 1) + 1 →
+ ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{U0} + 1) + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
fact tpr_conf_flat_cast:
∀X2,V0,V1,T0,T1. (
- ∀X0:term. #{X0} < #{V0} + #{T0} + 1 →
+ ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
fact tpr_conf_beta_beta:
∀a. ∀W0:term. ∀V0,V1,T0,T1,V2,T2. (
- ∀X0:term. #{X0} < #{V0} + (#{W0} + #{T0} + 1) + 1 →
+ ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{T0} + 1) + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
(* Basic_1: was: pr0_cong_delta pr0_delta_delta *)
fact tpr_conf_delta_delta:
∀a,I1,V0,V1,T0,T1,TT1,V2,T2,TT2. (
- ∀X0:term. #{X0} < #{V0} + #{T0} + 1 →
+ ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
fact tpr_conf_delta_zeta:
∀X2,V0,V1,T0,T1,TT1,T2. (
- ∀X0:term. #{X0} < #{V0} + #{T0} + 1 →
+ ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
(* Basic_1: was: pr0_upsilon_upsilon *)
fact tpr_conf_theta_theta:
∀a,VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. (
- ∀X0:term. #{X0} < #{V0} + (#{W0} + #{T0} + 1) + 1 →
+ ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{T0} + 1) + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
fact tpr_conf_zeta_zeta:
∀V0:term. ∀X2,TT0,T0,T1,TT2. (
- ∀X0:term. #{X0} < #{V0} + #{TT0} + 1 →
+ ∀X0:term. ♯{X0} < ♯{V0} + ♯{TT0} + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
fact tpr_conf_tau_tau:
∀V0,T0:term. ∀X2,T1. (
- ∀X0:term. #{X0} < #{V0} + #{T0} + 1 →
+ ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
inductive aaa: lenv → term → predicate aarity ≝
-| aaa_sort: ∀L,k. aaa L (⋆k) ⓪
+| aaa_sort: ∀L,k. aaa L (⋆k) (⓪)
| aaa_lref: ∀I,L,K,V,B,i. ⇩[0, i] L ≡ K. ⓑ{I} V → aaa K V B → aaa L (#i) B
| aaa_abbr: ∀a,L,V,T,B,A.
aaa L V B → aaa (L. ⓓV) T A → aaa L (ⓓ{a}V. T) A
(* Basic forward lemmas *****************************************************)
-lemma frsup_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}.
+lemma frsup_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/
qed-.
-lemma frsup_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → #{L1} ≤ #{L2}.
+lemma frsup_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ♯{L1} ≤ ♯{L2}.
#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/
qed-.
-lemma frsup_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → #{T2} < #{T1}.
+lemma frsup_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ♯{T2} < ♯{T1}.
#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ /2 width=1 by le_minus_to_plus/
qed-.
]
qed-.
-lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #{L2} ≤ #{L1}.
+lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize
[ /2 width=3/
| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12
qed-.
lemma ldrop_pair2_fwd_fw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V →
- ∀T. #{K, V} < #{L, T}.
+ ∀T. ♯{K, V} < ♯{L, T}.
#I #L #K #V #d #e #H #T
lapply (ldrop_fwd_lw … H) -H #H
@(le_to_lt_to_lt … H) -H /3 width=1/
(* Basic forward lemmas *****************************************************)
-lemma tw_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → #{T1} = #{T2}.
+lemma tw_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ♯{T1} = ♯{T2}.
#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
qed-.
(* Basic forward lemmas *****************************************************)
-lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → #{T1} ≤ #{T2}.
+lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ♯{T1} ≤ ♯{T2}.
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e normalize
/3 by monotonic_le_plus_l, le_plus/ (**) (* just /3 width=1/ is too slow *)
qed-.
(* Basic forward lemmas *****************************************************)
-lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → #{T1} ≤ #{T2}.
+lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → ♯{T1} ≤ ♯{T2}.
#L #T1 #T2 #d #e * #T #HT1 #HT2
->(tw_lift … HT2) -T2 /2 width=4 by tpss_fwd_tw /
+>(tw_lift … HT2) -T2 /2 width=4 by tpss_fwd_tw/
qed-.
(∀L,d,e,i. i < d → R d e L (#i) (#i)) →
(∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
⇩[O, i] L ≡ K.ⓓV1 → K ⊢ ▼*[O, d + e - i - 1] V1 ≡ V2 →
- ⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2
+ ⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L (#i) W2
) →
(∀L,d,e,i. d + e ≤ i → R d e L (#i) (#(i - e))) →
(∀L,d,e,p. R d e L (§p) (§p)) →
(* Basic forward lemmas *****************************************************)
-lemma frsupp_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}.
+lemma frsupp_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2
/3 width=3 by frsup_fwd_fw, transitive_lt/
qed-.
-lemma frsupp_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → #{L1} ≤ #{L2}.
+lemma frsupp_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{L1} ≤ ♯{L2}.
#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2
/2 width=3 by frsup_fwd_lw/ (**) (* /3 width=5 by frsup_fwd_lw, transitive_le/ is too slow *)
#L #T #L2 #T2 #_ #HL2 #HL1
lapply (frsup_fwd_lw … HL2) -HL2 /2 width=3 by transitive_le/
qed-.
-lemma frsupp_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → #{T2} < #{T1}.
+lemma frsupp_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{T2} < ♯{T1}.
#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2
/3 width=3 by frsup_fwd_tw, transitive_lt/
qed-.
(* Basic forward lemmas *****************************************************)
-lemma frsups_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → #{L2, T2} ≤ #{L1, T1}.
+lemma frsups_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → ♯{L2, T2} ≤ ♯{L1, T1}.
#L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H [ * // ]
/3 width=1 by frsupp_fwd_fw, lt_to_le/
qed-.
-lemma frsups_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → #{L1} ≤ #{L2}.
+lemma frsups_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → ♯{L1} ≤ ♯{L2}.
#L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H [ * // ]
/2 width=3 by frsupp_fwd_lw/
qed-.
-lemma frsups_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → #{T2} ≤ #{T1}.
+lemma frsups_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → ♯{T2} ≤ ♯{T1}.
#L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H [ * // ]
/3 width=3 by frsupp_fwd_tw, lt_to_le/
qed-.
elim (ltpss_dx_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0
elim (ltpss_dx_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
lapply (tpss_fwd_tw … HV01) #H2
- lapply (transitive_le (#{K1} + #{V0}) … H1) -H1 /2 width=1/ -H2 #H
+ lapply (transitive_le (♯{K1} + ♯{V0}) … H1) -H1 /2 width=1/ -H2 #H
lapply (tpss_trans_eq … HV01 HV12) -V1 #HV02
lapply (IH … HV02 … HK01) -IH -HV02 -HK01
[ normalize /2 width=1/ | /2 width=6/ ]
(* Basic forward lemmas *****************************************************)
-lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #{T1} ≤ #{T2}.
+lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → ♯{T1} ≤ ♯{T2}.
#L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 //
#T #T2 #_ #HT2 #IHT1
lapply (tps_fwd_tw … HT2) -HT2 #HT2
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=6/
qed-.
-lemma tpss_ind_alt: ∀R:ℕ→ℕ→lenv→relation term.
+lemma tpss_ind_alt: ∀R:nat→nat→lenv→relation term.
(∀L,I,d,e. R d e L (⓪{I}) (⓪{I})) →
(∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 ▶* [O, d + e - i - 1] V2 →
- ⇧[O, i + 1] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2
+ ⇧[O, i + 1] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L (#i) W2
) →
(∀L,a,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▶* [d, e] V2 →
L.ⓑ{I}V2 ⊢ T1 ▶* [d + 1, e] T2 → R d e L V1 V2 →
projects / helm.git / commitdiff