- we introduced the pointer_step rc in the perspective of proving

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / reducibility / tpr_tpr.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma
index 8c7f2819e401e9e8ef5ebc0fb85990446a8f28c1..1522d00c0402548f2adf1506fd99c7544b2292fd 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma
@@ -23,7 +23,7 @@ fact tpr_conf_atom_atom: ∀I. ∃∃X. ⓪{I} ➡ X & ⓪{I} ➡ X.
 
 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
    ) →
@@ -36,7 +36,7 @@ qed.
 
 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
    ) →
@@ -55,7 +55,7 @@ qed.
 *)
 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
    ) →
@@ -87,7 +87,7 @@ qed.
 
 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
    ) →
@@ -99,7 +99,7 @@ qed.
 
 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
    ) →
@@ -113,7 +113,7 @@ qed.
 (* 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
    ) →
@@ -132,7 +132,7 @@ qed.
 
 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
    ) →
@@ -149,7 +149,7 @@ qed.
 (* 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
    ) →
@@ -168,7 +168,7 @@ qed.
 
 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
    ) →
@@ -184,7 +184,7 @@ qed.
 
 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
    ) →
@@ -198,7 +198,7 @@ qed.
 
 fact tpr_conf_aux:
    ∀Y0:term. (
-      ∀X0:term. #[X0] < #[Y0] →
+      ∀X0:term. #{X0} < #{Y0} →
       ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
       ∃∃X. X1 ➡ X & X2 ➡ X
          ) →
@@ -279,5 +279,5 @@ qed.
 (* Basic_1: was: pr0_confluence *)
 theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ➡ T1 → T0 ➡ T2 →
                   ∃∃T. T1 ➡ T & T2 ➡ T.
-#T @(tw_wf_ind … T) -T /3 width=6 by tpr_conf_aux/
+#T @(tw_ind … T) -T /3 width=6 by tpr_conf_aux/
 qed.