(* *)
(**************************************************************************)
-include "Basic-2/substitution/tps_tps.ma".
-include "Basic-2/reduction/tpr_lift.ma".
include "Basic-2/reduction/tpr_tps.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
elim (IH … HT02 … HU01) -HT02 HU01 IH /3 width=5/
qed.
+(* basic-1: was:
+ pr0_cong_upsilon_refl pr0_cong_upsilon_zeta
+ pr0_cong_upsilon_cong pr0_cong_upsilon_delta
+*)
fact tpr_conf_flat_theta:
∀V0,V1,T1,V2,V,W0,W2,U0,U2. (
∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 →
elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/
qed.
+(* Basic-1: was: pr0_cong_delta pr0_delta_delta *)
fact tpr_conf_delta_delta:
∀I1,V0,V1,T0,T1,TT1,V2,T2,TT2. (
∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2
elim (tpr_tps_bind … HV1 HT1 … HTT1) -HT1 HTT1 #U1 #TTU1 #HTU1
elim (tpr_tps_bind … HV2 HT2 … HTT2) -HT2 HTT2 #U2 #TTU2 #HTU2
-elim (tps_conf … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2
+elim (tps_conf_eq … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2
@ex2_1_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *)
qed.
elim (IH … HTX2 … HTT2) -HTX2 HTT2 IH /3/
qed.
+(* Basic-1: was: pr0_upsilon_upsilon *)
fact tpr_conf_theta_theta:
∀VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. (
∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 →
]
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/