(* *)
(**************************************************************************)
-include "basic_2/rt_computation/fpbg_fqup.ma".
+include "basic_2/rt_computation/fpbg_fqus.ma".
include "basic_2/rt_computation/fpbs_cpxs.ma".
include "basic_2/rt_computation/fpbg_fpbs.ma".
include "ground/xoa/ex_8_5.ma".
include "ground/xoa/ex_9_3.ma".
include "basic_2/rt_transition/cpm_teqx.ma".
-include "basic_2/rt_computation/fpbg_fqup.ma".
+include "basic_2/rt_computation/fpbg_cpm.ma".
include "basic_2/dynamic/cnv_fsb.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
/3 width=3 by eq_f2/
| #G #K #V #T1 #X1 #X2 #HXT1 #HX12 #_ #H1 #H2
elim (cnv_fpbg_refl_false … H2) -a
- @(fpbg_teqx_div … H1) -H1
- /3 width=9 by cpm_tneqx_cpm_fpbg, cpm_zeta, teqx_lifts_inv_pair_sn/
+ @(fpbg_teqg_div … H1) -H1
+ /3 width=9 by cpm_tneqx_cpm_fpbg, cpm_zeta, teqg_lifts_inv_pair_sn/
| #G #L #U #T1 #T2 #HT12 #_ #H1 #H2
elim (cnv_fpbg_refl_false … H2) -a
- @(fpbg_teqx_div … H1) -H1
+ @(fpbg_teqg_div … H1) -H1
/3 width=7 by cpm_tneqx_cpm_fpbg, cpm_eps, teqg_inv_pair_xy_y/
| #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H1 #_
elim (teqx_inv_pair … H1) -H1 #H #_ #_ destruct
/2 width=4 by ex5_intro/
| #X1 #HXT1 #HX1 #H1 #H destruct
elim (cnv_fpbg_refl_false … H0) -a
- @(fpbg_teqx_div … H2) -H2
+ @(fpbg_teqg_div … H2) -H2
/3 width=9 by cpm_tneqx_cpm_fpbg, cpm_zeta, teqx_lifts_inv_pair_sn/
]
qed-.
/2 width=7 by ex9_3_intro/
| #HT1X
elim (cnv_fpbg_refl_false … H0) -a
- @(fpbg_teqx_div … H2) -H2
+ @(fpbg_teqg_div … H2) -H2
/3 width=7 by cpm_tneqx_cpm_fpbg, cpm_eps, teqg_inv_pair_xy_y/
| #m #HU1X #H destruct
elim (cnv_fpbg_refl_false … H0) -a
- @(fpbg_teqx_div … H2) -H2
+ @(fpbg_teqg_div … H2) -H2
/3 width=7 by cpm_tneqx_cpm_fpbg, cpm_ee, teqg_inv_pair_xy_x/
]
qed-.
(**************************************************************************)
include "ground/xoa/ex_4_1_props.ma".
+include "basic_2/rt_computation/fpbg_fqus.ma".
include "basic_2/dynamic/cnv_cpm_teqx.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2
elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX02 … 0 T0 … L0 … HL01) //
<minus_n_O <minus_O_n #Y1 #HXY1 #HTY1
-elim (cnv_cpms_strip_lpr_sub … IH1 … HXT2 0 X2 … HL02 L0) [|*: /4 width=3 by fpb_fpbg, cpm_fpb/ ]
+elim (cnv_cpms_strip_lpr_sub … IH1 … HXT2 0 X2 … HL02 L0) [|*: /4 width=3 by fpbc_fpbg, cpm_fwd_fpbc/ ]
<minus_n_O <minus_O_n #Y2 #HTY2 #HXY2 -HXT2
-elim (IH1 … HXY1 … HXY2 … HL01 … HL02) [|*: /4 width=3 by fpb_fpbg, cpm_fpb/ ]
+elim (IH1 … HXY1 … HXY2 … HL01 … HL02) [|*: /4 width=3 by fpbc_fpbg, cpm_fwd_fpbc/ ]
-a -L0 -X2 <minus_n_O <minus_O_n #Y #HY1 #HY2
lapply (cpms_trans … HTY1 … HY1) -Y1 #HT0Y
lapply (cpms_trans … HTY2 … HY2) -Y2 #HT2Y
lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … H1X01 … L0 ?) // #HX1
lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … H1X02 … L0 ?) // #HX2
elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … H1X01 … H1X02 … L0 … L0) // #Z0 #HXZ10 #HXZ20
-cut (❪G0, L0, T0❫ > ❪G0, L0, X2❫) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *)
-lapply (fpbg_fpbs_trans ? G0 ? L0 ? Z0 ? … H1fpbg) [ /2 width=3 by cpms_fwd_fpbs/ ] #H2fpbg
+cut (❪G0, L0, T0❫ > ❪G0, L0, X2❫) [ /4 width=5 by cpms_fwd_fpbs, cpm_fwd_fpbc, fpbc_fpbs_fpbg/ ] #H1fpbg (**) (* cut *)
+lapply (fpbg_fpbs_trans … H1fpbg G0 L0 Z0 ?) [ /2 width=3 by cpms_fwd_fpbs/ ] #H2fpbg
lapply (cnv_cpms_trans_lpr_sub … IH2 … HXZ20 … L0 ?) // #HZ0
-elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02
+elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=2 by fpbc_fpbg, cpm_fwd_fpbc/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02
elim (teqx_dec X1 Z0) #H2XZ
[ -IH
- elim (cnv_cpms_conf_lpr_teqx_teqx_aux … HX1 … H1XT1 H2XT1 … HXZ10 H2XZ … L1 … L0) [2,3: // |4,5: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ]
+ elim (cnv_cpms_conf_lpr_teqx_teqx_aux … HX1 … H1XT1 H2XT1 … HXZ10 H2XZ … L1 … L0)
+ [2,3: // |4,5: /4 width=5 by cpm_fwd_fpb, fpb_fpbg_trans/ ]
| -H1XT1 -H2XT1
- elim (cpms_tneqx_fwd_step_sn_aux … HXZ10 HX1 H2XZ) [|*: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ]
+ elim (cpms_tneqx_fwd_step_sn_aux … HXZ10 HX1 H2XZ) [|*: /4 width=5 by cpm_fwd_fpb, fpb_fpbg_trans/ ]
-HXZ10 -H2XZ #n1 #n2 #X0 #H1X10 #H2X10 #HXZ0 #Hn
- elim (IH … H1X10 H2X10 … HXZ0 … L1 … L0) [2,3: // |4,5: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ]
+ elim (IH … H1X10 H2X10 … HXZ0 … L1 … L0) [2,3: // |4,5: /4 width=5 by cpm_fwd_fpb, fpb_fpbg_trans/ ]
>Hn -n1 -n2 -X0 -IH
]
#Z1 #HTZ1 #HZ01
lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX01 … L0 ?) // #HX1
lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2
elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX01 … HX02 … L0 … L0) // #Z0 #HXZ10 #HXZ20
-cut (❪G0, L0, T0❫ > ❪G0, L0, X1❫) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *)
-lapply (fpbg_fpbs_trans ? G0 ? L0 ? Z0 ? … H1fpbg) [ /2 width=3 by cpms_fwd_fpbs/ ] #H2fpbg
+cut (❪G0, L0, T0❫ > ❪G0, L0, X1❫) [ /4 width=5 by cpms_fwd_fpbs, cpm_fwd_fpbc, fpbc_fpbs_fpbg/ ] #H1fpbg (**) (* cut *)
+lapply (fpbg_fpbs_trans … H1fpbg G0 L0 Z0 ?) [ /2 width=3 by cpms_fwd_fpbs/ ] #H2fpbg
lapply (cnv_cpms_trans_lpr_sub … IH2 … HXZ10 … L0 ?) // #HZ0
-elim (IH1 … HXT1 … HXZ10 … L1 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT1 -HXZ10 #Z1 #HTZ1 #HZ01
-elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=3 by fpb_fpbg, cpm_fpb/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02
+elim (IH1 … HXT1 … HXZ10 … L1 … L0) [|*: /4 width=2 by fpbc_fpbg, cpm_fwd_fpbc/ ] -HXT1 -HXZ10 #Z1 #HTZ1 #HZ01
+elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=3 by fpbc_fpbg, cpm_fwd_fpbc/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02
elim (IH1 … HZ01 … HZ02 L1 … L2) // -L0 -T0 -X1 -X2 -Z0 #Z #HZ01 #HZ02
lapply (cpms_trans … HTZ1 … HZ01) -Z1 <arith_l4 #HT1Z
lapply (cpms_trans … HTZ2 … HZ02) -Z2 <arith_l4 #HT2Z
[ elim (teqx_dec T T2) #H2T2
[ -IH -IH2 -IH1 -H0T1 /4 width=7 by teqx_trans, ex4_3_intro/
| lapply (cnv_cpm_trans_lpr_aux … IH2 IH1 … H1T1 L ?) [6:|*: // ] -H1T2 -H2T12 #H0T
- elim (IH H0T H2T2) [|*: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] -IH -IH2 -H0T -H2T2 (**)
+ elim (IH H0T H2T2) [|*: /4 width=5 by cpm_fwd_fpb, fpb_fpbg_trans/ ] -IH -IH2 -H0T -H2T2 (**)
#m1 #m2 #T0 #H1T0 #H2T0 #H1T02 #H destruct
elim (cnv_cpm_teqx_cpm_trans_aux … IH1 … H0T1 … H1T1 H2T1 … H1T0) -IH1 -H0T1 -H1T1 -H1T0
#T3 #H1T13 #H1T30 #H2T30
elim (teqx_dec T1 T) #H2T1
[ lapply (cnv_cpm_trans_lpr_aux … IH2 IH1 … H1T1 L ?) [6:|*: // ] #H0T
lapply (teqx_canc_sn … H2T1 … H2T12) -H2T12 #H2T2
- /6 width=7 by cpm_fpbq, fpbq_fpbg_trans/ (**)
+ /6 width=7 by cpm_fwd_fpb, fpb_fpbg_trans/ (**)
| -IB2 -IH -IH2 -IH1
elim (cnv_fpbg_refl_false … H0T1) -a -Q
/3 width=9 by cpm_tneqx_cpm_cpms_teqx_sym_fwd_fpbg/
#n2 #T2 #H1T02 #H2T02 #L1 #HL01 #L2 #HL02
elim (cnv_cpms_teqx_strip_lpr_aux … IH2 IH1 … H1T02 H0T0 H2T02 … H1T03 H2T03 … HL02 L0) -H0T0 -H2T03 //
#T4 #H1T24 #H2T24 #H1T34 #H2T34
- elim (IH … H1T34 H2T34 … HL01 … HL02) [|*: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] -L0 -T0 -T3 (**)
+ elim (IH … H1T34 H2T34 … HL01 … HL02) [|*: /4 width=5 by cpm_fwd_fpb, fpb_fpbg_trans/ ] -L0 -T0 -T3 (**)
#T3 #H1T13 #H2T13 #H1T43 #H2T43
<minus_plus >arith_l3
/3 width=7 by cpms_step_sn, teqx_trans, ex4_intro/
(* *)
(**************************************************************************)
+include "basic_2/rt_transition/lpr.ma".
include "basic_2/rt_computation/cpms_fpbg.ma".
include "basic_2/dynamic/cnv.ma".
(* Inductive premises for the preservation results **************************)
definition IH_cnv_cpm_trans_lpr (h) (a): relation3 genv lenv term ≝
- λG,L1,T1. ❪G,L1❫ ⊢ T1 ![h,a] →
- ∀n,T2. ❪G,L1❫ ⊢ T1 ➡[h,n] T2 →
- ∀L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L2❫ ⊢ T2 ![h,a].
+ λG,L1,T1. ❪G,L1❫ ⊢ T1 ![h,a] →
+ ∀n,T2. ❪G,L1❫ ⊢ T1 ➡[h,n] T2 →
+ ∀L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L2❫ ⊢ T2 ![h,a].
definition IH_cnv_cpms_trans_lpr (h) (a): relation3 genv lenv term ≝
- λG,L1,T1. ❪G,L1❫ ⊢ T1 ![h,a] →
- ∀n,T2. ❪G,L1❫ ⊢ T1 ➡*[h,n] T2 →
- ∀L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L2❫ ⊢ T2 ![h,a].
+ λG,L1,T1. ❪G,L1❫ ⊢ T1 ![h,a] →
+ ∀n,T2. ❪G,L1❫ ⊢ T1 ➡*[h,n] T2 →
+ ∀L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L2❫ ⊢ T2 ![h,a].
definition IH_cnv_cpm_conf_lpr (h) (a): relation3 genv lenv term ≝
- λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] →
- ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡[h,n2] T2 →
- ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 →
- ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T.
+ λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] →
+ ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡[h,n2] T2 →
+ ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 →
+ ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T.
definition IH_cnv_cpms_strip_lpr (h) (a): relation3 genv lenv term ≝
- λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] →
- ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡*[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡[h,n2] T2 →
- ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 →
- ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T.
+ λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] →
+ ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡*[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡[h,n2] T2 →
+ ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 →
+ ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T.
definition IH_cnv_cpms_conf_lpr (h) (a): relation3 genv lenv term ≝
- λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] →
- ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡*[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡*[h,n2] T2 →
- ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 →
- ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T.
+ λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] →
+ ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡*[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡*[h,n2] T2 →
+ ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 →
+ ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T.
(* Auxiliary properties for preservation ************************************)
--- /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 "static_2/static/reqg_fqus.ma".
+include "basic_2/rt_transition/cpx_reqg.ma".
+include "basic_2/rt_transition/lpx_reqg.ma".
+include "basic_2/rt_transition/fpbc.ma".
+
+(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************)
+
+(* Properties with generic equivalence for local environments ***************)
+
+(* Basic_2A1: was: teqg_fpb_trans *)
+lemma teqg_fpbc_trans (S):
+ reflexive … S → symmetric … S →
+ ∀U2,U1. U2 ≛[S] U1 →
+ ∀G1,G2,L1,L2,T1. ❪G1,L1,U1❫ ≻ ❪G2,L2,T1❫ →
+ ∃∃L,T2. ❪G1,L1,U2❫ ≻ ❪G2,L,T2❫ & T2 ≛[S] T1 & L ≛[S,T1] L2.
+#S #H1S #H2S #U2 #U1 #HU21 #G1 #G2 #L1 #L2 #T1 #H
+elim (fpbc_inv_gen S … H) -H #H12 #Hn12
+
+(* Basic_2A1: was just: lleq_fpb_trans *)
+lemma reqg_fpb_trans (S):
+ reflexive … S → symmetric … S →
+ ∀F,K1,K2,T. K1 ≛[S,T] K2 →
+ ∀G,L2,U. ❪F,K2,T❫ ≻ ❪G,L2,U❫ →
+ ∃∃L1,U0. ❪F,K1,T❫ ≻ ❪G,L1,U0❫ & U0 ≛[S] U & L1 ≛[S,U] L2.
+#S #H1S #H2S #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U
+[ #G #L2 #U #H2 elim (reqg_fqu_trans … H2 … HT) -K2
+ /3 width=5 by fpb_fqu, ex3_2_intro/
+| #U #HTU #HnTU lapply (reqg_cpx_trans … HT … HTU) -HTU //
+ /4 width=8 by fpb_cpx, cpx_reqg_conf_sn, teqg_refl, ex3_2_intro/
+| #L2 #HKL2 #HnKL2 elim (reqg_lpx_trans … HKL2 … HT) -HKL2 //
+ /6 width=9 by fpb_lpx, reqg_reqx, reqg_repl, teqg_refl, ex3_2_intro/
+]
+qed-.
--- /dev/null
+lemma fpbg_fqu_trans:
+ ∀G1,G,G2,L1,L,L2,T1,T,T2.
+ ❪G1,L1,T1❫ > ❪G,L,T❫ → ❪G,L,T❫ ⬂ ❪G2,L2,T2❫ →
+ ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+#G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2
+/4 width=5 by fpbg_fpbq_trans, fpbq_fquq, fqu_fquq/
+qed-.
+
+lemma fpbq_fpbg_trans:
+ ∀G1,G,G2,L1,L,L2,T1,T,T2.
+ ❪G1,L1,T1❫ ≻ ❪G,L,T❫ → ❪G,L,T❫ > ❪G2,L2,T2❫ →
+ ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+/3 width=5 by fpbg_fwd_fpbs, ex2_3_intro/ 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 "static_2/static/feqx.ma".
+include "basic_2/rt_transition/rpx_reqx.ma".
+include "basic_2/rt_transition/fpbq.ma".
+
+(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************)
+
+(* Basic_2A1: includes: fleq_fpbq fpbq_lleq *)
+lemma fpbq_feqx (G1) (G2):
+ ∀L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫.
+#G1 #G2 #L1 #L2 #T1 #T2 #H
+elim (feqx_inv_gen_sn … H) #H #HL12 #HT12 destruct
+/3 width=3 by fpbq_rcpx, reqx_rpx_trans, teqx_cpx_trans/
+qed.
(* *)
(**************************************************************************)
-include "basic_2/rt_computation/fpbg_fqup.ma".
+include "basic_2/rt_transition/cpm_fpbc.ma".
+include "basic_2/rt_computation/fpbg_fqus.ma".
include "basic_2/rt_computation/fpbg_cpxs.ma".
include "basic_2/rt_computation/cpms_fpbs.ma".
∀n1,T. ❪G,L❫ ⊢ T1 ➡[h,n1] T → (T1 ≅ T → ⊥) →
∀n2,T2. ❪G,L❫⊢ T ➡*[h,n2] T2 → T1 ≅ T2 → ❪G,L,T1❫ > ❪G,L,T1❫.
#h #G #L #T1 #n1 #T #H1T1 #H2T1 #n2 #T2 #H1T2 #H2T12
-/4 width=7 by cpms_fwd_fpbs, cpm_fpb, fpbs_teqx_trans, teqx_sym, ex2_3_intro/
+/4 width=10 by fpbc_fpbs_fpbg, cpms_fwd_fpbs, fpbs_teqg_trans, cpm_fwd_fpbc, teqx_sym/
qed-.
(* Properties with generic equivalence for closures *************************)
-(* to be updated *)
+(* to update *)
lemma feqg_cpxs_trans (S):
reflexive … S → symmetric … S →
∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T❫ →
(* Note: a proof based on fqu_cpx_trans_tneqx might exist *)
(* Basic_2A1: uses: fqu_cpxs_trans_neq *)
-lemma fqu_cpxs_trans_tneqx (b):
+lemma fqu_cpxs_trans_tneqg (S) (b):
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ →
- â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\85 U2 → ⊥) →
- â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\85 U1 → ⊥ & ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,U2❫.
-#b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+ â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\9b[S] U2 → ⊥) →
+ â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\9b[S] U1 → ⊥ & ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,U2❫.
+#S #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ #I #G #L #V1 #V2 #HV12 #_ elim (lifts_total V2 𝐔❨1❩)
#U2 #HVU2 @(ex3_intro … U2)
[1,3: /3 width=7 by cpxs_delta, fqu_drop/
]
| #I #G #L #V1 #T #V2 #HV12 #H0 @(ex3_intro … (②[I]V2.T))
[1,3: /2 width=4 by fqu_pair_sn, cpxs_pair_sn/
- | #H elim (teqx_inv_pair … H) -H /2 width=1 by/
+ | #H elim (teqg_inv_pair … H) -H /2 width=1 by/
]
| #p #I #G #L #V #T1 #Hb #T2 #HT12 #H0 @(ex3_intro … (ⓑ[p,I]V.T2))
[1,3: /2 width=4 by fqu_bind_dx, cpxs_bind/
- | #H elim (teqx_inv_pair … H) -H /2 width=1 by/
+ | #H elim (teqg_inv_pair … H) -H /2 width=1 by/
]
| #p #I #G #L #V #T1 #Hb #T2 #HT12 #H0 @(ex3_intro … (ⓑ[p,I]V.T2))
[1,3: /4 width=4 by lsubr_cpxs_trans, cpxs_bind, lsubr_unit, fqu_clear/
- | #H elim (teqx_inv_pair … H) -H /2 width=1 by/
+ | #H elim (teqg_inv_pair … H) -H /2 width=1 by/
]
| #I #G #L #V #T1 #T2 #HT12 #H0 @(ex3_intro … (ⓕ[I]V.T2))
[1,3: /2 width=4 by fqu_flat_dx, cpxs_flat/
- | #H elim (teqx_inv_pair … H) -H /2 width=1 by/
+ | #H elim (teqg_inv_pair … H) -H /2 width=1 by/
]
| #I #G #L #T1 #U1 #HTU1 #T2 #HT12 #H0
elim (cpxs_lifts_sn … HT12 (Ⓣ) … (L.ⓘ[I]) … HTU1) -HT12
- /4 width=6 by fqu_drop, drops_refl, drops_drop, teqx_inv_lifts_bi, ex3_intro/
+ /4 width=6 by fqu_drop, drops_refl, drops_drop, teqg_inv_lifts_bi, ex3_intro/
]
qed-.
(* Basic_2A1: uses: fquq_cpxs_trans_neq *)
-lemma fquq_cpxs_trans_tneqx (b):
+lemma fquq_cpxs_trans_tneqg (S) (b):
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂⸮[b] ❪G2,L2,T2❫ →
- â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\85 U2 → ⊥) →
- â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\85 U1 → ⊥ & ❪G1,L1,U1❫ ⬂⸮[b] ❪G2,L2,U2❫.
-#b #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12
-[ #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_tneqx … H12 … HTU2 H) -T2
+ â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\9b[S] U2 → ⊥) →
+ â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\9b[S] U1 → ⊥ & ❪G1,L1,U1❫ ⬂⸮[b] ❪G2,L2,U2❫.
+#S #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12
+[ #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_tneqg … H12 … HTU2 H) -T2
/3 width=4 by fqu_fquq, ex3_intro/
| * #HG #HL #HT destruct /3 width=4 by ex3_intro/
]
qed-.
(* Basic_2A1: uses: fqup_cpxs_trans_neq *)
-lemma fqup_cpxs_trans_tneqx (b):
+lemma fqup_cpxs_trans_tneqg (S) (b):
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+[b] ❪G2,L2,T2❫ →
- â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\85 U2 → ⊥) →
- â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\85 U1 → ⊥ & ❪G1,L1,U1❫ ⬂+[b] ❪G2,L2,U2❫.
-#b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1
-[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_tneqx … H12 … HTU2 H) -T2
+ â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\9b[S] U2 → ⊥) →
+ â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\9b[S] U1 → ⊥ & ❪G1,L1,U1❫ ⬂+[b] ❪G2,L2,U2❫.
+#S #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1
+[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_tneqg … H12 … HTU2 H) -T2
/3 width=4 by fqu_fqup, ex3_intro/
| #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2
- #U1 #HTU1 #H #H12 elim (fqu_cpxs_trans_tneqx … H1 … HTU1 H) -T1
+ #U1 #HTU1 #H #H12 elim (fqu_cpxs_trans_tneqg … H1 … HTU1 H) -T1
/3 width=8 by fqup_strap2, ex3_intro/
]
qed-.
(* Basic_2A1: uses: fqus_cpxs_trans_neq *)
-lemma fqus_cpxs_trans_tneqx (b):
+lemma fqus_cpxs_trans_tneqg (S) (b):
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂*[b] ❪G2,L2,T2❫ →
- â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\85 U2 → ⊥) →
- â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\85 U1 → ⊥ & ❪G1,L1,U1❫ ⬂*[b] ❪G2,L2,U2❫.
-#b #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12
-[ #H12 elim (fqup_cpxs_trans_tneqx … H12 … HTU2 H) -T2
+ â\88\80U2. â\9dªG2,L2â\9d« â\8a¢ T2 â¬\88* U2 â\86\92 (T2 â\89\9b[S] U2 → ⊥) →
+ â\88\83â\88\83U1. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* U1 & T1 â\89\9b[S] U1 → ⊥ & ❪G1,L1,U1❫ ⬂*[b] ❪G2,L2,U2❫.
+#S #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12
+[ #H12 elim (fqup_cpxs_trans_tneqg … H12 … HTU2 H) -T2
/3 width=4 by fqup_fqus, ex3_intro/
| * #HG #HL #HT destruct /3 width=4 by ex3_intro/
]
(* Eliminators with extended context-sensitive rt-computation for terms *****)
fact csx_ind_cpxs_aux (G) (L):
- ∀Q:predicate term.
- (∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 →
- (∀T2. ❪G,L❫ ⊢ T1 ⬈* T2 → (T1 ≅ T2 → ⊥) → Q T2) → Q T1
- ) →
- ∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 →
- ∀T2. ❪G,L❫ ⊢ T1 ⬈* T2 → Q T2.
+ ∀Q:predicate term.
+ (∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 →
+ (∀T2. ❪G,L❫ ⊢ T1 ⬈* T2 → (T1 ≅ T2 → ⊥) → Q T2) → Q T1
+ ) →
+ ∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 →
+ ∀T2. ❪G,L❫ ⊢ T1 ⬈* T2 → Q T2.
#G #L #Q #IH #T1 #H @(csx_ind … H) -T1
#T1 #HT1 #IH1 #T2 #HT12
@IH -IH /2 width=3 by csx_cpxs_trans/ -HT1 #V2 #HTV2 #HnTV2
elim (teqx_dec T1 T2) #H
[ lapply (teqg_tneqg_trans … H … HnTV2) // -H -HnTV2 #Hn12
lapply (cpxs_trans … HT12 … HTV2) -T2 #H12
- elim (cpxs_tneqg_fwd_step_sn … H12 … Hn12) // -H12 -Hn12
+ elim (cpxs_tneqg_fwd_step_sn … H12 … Hn12) /2 width=1 by sfull_dec/ -H12 -Hn12
/3 width=4 by/
| elim (cpxs_tneqg_fwd_step_sn … HT12 … H) -HT12 -H
- /3 width=6 by cpxs_trans/
+ /3 width=6 by cpxs_trans, sfull_dec/
]
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/rt_transition/fpb_lpx.ma".
+include "basic_2/rt_computation/csx_fqus.ma".
+include "basic_2/rt_computation/csx_reqg.ma".
+include "basic_2/rt_computation/csx_lpx.ma".
+
+(* STRONGLY NORMALIZING TERMS FOR EXTENDED PARALLEL RT-TRANSITION ***********)
+
+(* Properties with parallel rst-transition for closures *********************)
+
+(* Basic_2A1: was: csx_fpb_conf *)
+lemma csx_fpb_conf:
+ ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒 T1 →
+ ∀G2,L2,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*𝐒 T2.
+#G1 #L1 #T1 #HT1 #G2 #L2 #T2 #H
+elim (fpb_inv_req … H) -H #L0 #L #T #H1 #HT2 #HL0 #HL02
+lapply (cpx_reqg_conf … HL0 … HT2) -HT2 // #HT2
+/5 width=8 by csx_fquq_conf, csx_cpx_trans, csx_lpx_conf, csx_reqg_conf/
+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/rt_transition/fpbq.ma".
-include "basic_2/rt_computation/csx_fqus.ma".
-include "basic_2/rt_computation/csx_feqg.ma".
-include "basic_2/rt_computation/csx_lpx.ma".
-
-(* STRONGLY NORMALIZING TERMS FOR EXTENDED PARALLEL RT-TRANSITION ***********)
-
-(* Properties with parallel rst-transition for closures *********************)
-
-(* Basic_2A1: was: csx_fpb_conf *)
-lemma csx_fpbq_conf:
- ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒 T1 →
- ∀G2,L2,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*𝐒 T2.
-#G1 #L1 #T1 #HT1 #G2 #L2 #T2 *
-/2 width=8 by csx_cpx_trans, csx_fquq_conf, csx_lpx_conf, csx_feqg_conf/
-qed-.
(* *)
(**************************************************************************)
-include "ground/xoa/ex_2_3.ma".
+include "ground/xoa/ex_3_6.ma".
include "basic_2/notation/relations/predsubtystarproper_6.ma".
-include "basic_2/rt_transition/fpb.ma".
+include "basic_2/rt_transition/fpbc.ma".
include "basic_2/rt_computation/fpbs.ma".
(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
definition fpbg: tri_relation genv lenv term ≝
λG1,L1,T1,G2,L2,T2.
- ∃∃G,L,T. ❪G1,L1,T1❫ ≻ ❪G,L,T❫ & ❪G,L,T❫ ≥ ❪G2,L2,T2❫.
+ ∃∃G3,L3,T3,G4,L4,T4. ❪G1,L1,T1❫ ≥ ❪G3,L3,T3❫ & ❪G3,L3,T3❫ ≻ ❪G4,L4,T4❫ & ❪G4,L4,T4❫ ≥ ❪G2,L2,T2❫.
-interpretation "proper parallel rst-computation (closure)"
- 'PRedSubTyStarProper G1 L1 T1 G2 L2 T2 = (fpbg G1 L1 T1 G2 L2 T2).
+interpretation
+ "proper parallel rst-computation (closure)"
+ 'PRedSubTyStarProper G1 L1 T1 G2 L2 T2 = (fpbg G1 L1 T1 G2 L2 T2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma fpbg_inv_gen (G1) (G2) (L1) (L2) (T1) (T2):
+ ❪G1,L1,T1❫ > ❪G2,L2,T2❫ →
+ ∃∃G3,L3,T3,G4,L4,T4. ❪G1,L1,T1❫ ≥ ❪G3,L3,T3❫ & ❪G3,L3,T3❫ ≻ ❪G4,L4,T4❫ & ❪G4,L4,T4❫ ≥ ❪G2,L2,T2❫.
+// qed-.
(* Basic properties *********************************************************)
-lemma fpb_fpbg:
- ∀G1,G2,L1,L2,T1,T2.
- ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
-/2 width=5 by ex2_3_intro/ qed.
+lemma fpbg_intro (G3) (G4) (L3) (L4) (T3) (T4):
+ ∀G1,L1,T1,G2,L2,T2.
+ ❪G1,L1,T1❫ ≥ ❪G3,L3,T3❫ → ❪G3,L3,T3❫ ≻ ❪G4,L4,T4❫ →
+ ❪G4,L4,T4❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+/2 width=9 by ex3_6_intro/ qed.
-lemma fpbg_fpbq_trans:
+(* Basic_2A1: was: fpbg_fpbq_trans *)
+lemma fpbg_fpb_trans:
∀G1,G,G2,L1,L,L2,T1,T,T2.
❪G1,L1,T1❫ > ❪G,L,T❫ → ❪G,L,T❫ ≽ ❪G2,L2,T2❫ →
❪G1,L1,T1❫ > ❪G2,L2,T2❫.
-#G1 #G #G2 #L1 #L #L2 #T1 #T #T2 *
-/3 width=9 by fpbs_strap1, ex2_3_intro/
+#G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2
+elim (fpbg_inv_gen … H1) -H1
+/3 width=13 by fpbs_strap1, fpbg_intro/
qed-.
-lemma fpbg_fqu_trans:
+(* Basic_2A1: was: fpbq_fpbg_trans *)
+lemma fpb_fpbg_trans:
∀G1,G,G2,L1,L,L2,T1,T,T2.
- ❪G1,L1,T1❫ > ❪G,L,T❫ → ❪G,L,T❫ ⬂ ❪G2,L2,T2❫ →
+ ❪G1,L1,T1❫ ≽ ❪G,L,T❫ → ❪G,L,T❫ > ❪G2,L2,T2❫ →
❪G1,L1,T1❫ > ❪G2,L2,T2❫.
#G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2
-/4 width=5 by fpbg_fpbq_trans, fpbq_fquq, fqu_fquq/
-qed-.
-
-(* Note: this is used in the closure proof *)
-lemma fpbg_fpbs_trans:
- ∀G,G2,L,L2,T,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ →
- ∀G1,L1,T1. ❪G1,L1,T1❫ > ❪G,L,T❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
-#G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpbq_trans/
+elim (fpbg_inv_gen … H2) -H2
+/3 width=13 by fpbs_strap2, fpbg_intro/
qed-.
-
-(* Basic_2A1: uses: fpbg_fleq_trans *)
-lemma fpbg_feqx_trans:
- ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ > ❪G,L,T❫ →
- ∀G2,L2,T2. ❪G,L,T❫ ≅ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
-/3 width=5 by fpbg_fpbq_trans, fpbq_feqx/ qed-.
-
-(* Properties with t-bound rt-transition for terms **************************)
-
-lemma cpm_tneqx_cpm_fpbg (h) (G) (L):
- ∀n1,T1,T. ❪G,L❫ ⊢ T1 ➡[h,n1] T → (T1 ≅ T → ⊥) →
- ∀n2,T2. ❪G,L❫ ⊢ T ➡[h,n2] T2 → ❪G,L,T1❫ > ❪G,L,T2❫.
-/4 width=5 by fpbq_fpbs, cpm_fpbq, cpm_fpb, ex2_3_intro/ 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/rt_transition/cpm_fpb.ma".
+include "basic_2/rt_transition/cpm_fpbc.ma".
+include "basic_2/rt_computation/fpbg_fqup.ma".
+
+(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
+
+(* Properties with t-bound rt-transition for terms **************************)
+
+lemma cpm_tneqx_cpm_fpbg (h) (G) (L):
+ ∀n1,T1,T. ❪G,L❫ ⊢ T1 ➡[h,n1] T → (T1 ≅ T → ⊥) →
+ ∀n2,T2. ❪G,L❫ ⊢ T ➡[h,n2] T2 → ❪G,L,T1❫ > ❪G,L,T2❫.
+/4 width=5 by fpbc_fpbs_fpbg, fpb_fpbs, cpm_fwd_fpbc, cpm_fwd_fpb/
+qed.
(* *)
(**************************************************************************)
+include "basic_2/rt_transition/fpbc_fqup.ma".
include "basic_2/rt_computation/cpxs_teqg.ma".
include "basic_2/rt_computation/fpbs_cpxs.ma".
+include "basic_2/rt_computation/fpbg_fqup.ma".
include "basic_2/rt_computation/fpbg_fpbs.ma".
(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
(T1 ≅ T2 → ⊥) → ❪G,L,T1❫ > ❪G,L,T2❫.
#G #L #T1 #T2 #H #H0
elim (cpxs_tneqg_fwd_step_sn … H … H0) -H -H0
-/4 width=5 by cpxs_teqx_fpbs, fpb_cpx, ex2_3_intro/
+/4 width=5 by fpbc_fpbs_fpbg, cpxs_fpbs, cpx_fpbc, sfull_dec/
qed.
lemma cpxs_fpbg_trans:
--- /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/rt_computation/fpbs_fpbc.ma".
+include "basic_2/rt_computation/fpbg_fpbs.ma".
+
+(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
+
+(* Properties with generic equivalence for closures *************************)
+
+(* Basic_2A1: uses: fpbg_fleq_trans *)
+lemma fpbg_feqg_trans (S) (G) (L) (T):
+ reflexive … S → symmetric … S →
+ ∀G1,L1,T1. ❪G1,L1,T1❫ > ❪G,L,T❫ →
+ ∀G2,L2,T2. ❪G,L,T❫ ≛[S] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+/3 width=8 by fpbg_fpb_trans, feqg_fpb/ qed-.
+
+(* Basic_2A1: uses: fleq_fpbg_trans *)
+lemma feqg_fpbg_trans (S) (G) (L) (T):
+ reflexive … S → symmetric … S →
+ ∀G1,L1,T1. ❪G1,L1,T1❫ ≛[S] ❪G,L,T❫ →
+ ∀G2,L2,T2. ❪G,L,T❫ > ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+/3 width=8 by fpb_fpbg_trans, feqg_fpb/ qed-.
+
+(* Properties with generic equivalence for terms ****************************)
+
+lemma fpbg_teqg_div (S):
+ reflexive … S → symmetric … S →
+ ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ > ❪G2,L2,T❫ →
+ ∀T2. T2 ≛[S] T → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+/4 width=8 by fpbg_feqg_trans, teqg_feqg, teqg_sym/ qed-.
+
+(* Advanced inversion lemmas of parallel rst-computation on closures ********)
+
+(* Basic_2A1: was: fpbs_fpbg *)
+lemma fpbs_inv_fpbg:
+ ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ →
+ ∨∨ ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫
+ | ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+#G1 #G2 #L1 #L2 #T1 #T2 #H
+elim (fpbs_inv_fpbc_sn … H) -H
+[ /2 width=1 by or_introl/
+| * #G #L #T #H1 #H2
+ /3 width=9 by fpbg_intro, or_intror/
+]
+qed-.
+
+(* Basic_2A1: this was the definition of fpbg *)
+lemma fpbg_inv_fpbc_fpbs (G1) (G2) (L1) (L2) (T1) (T2):
+ ❪G1,L1,T1❫ > ❪G2,L2,T2❫ →
+ ∃∃G,L,T. ❪G1,L1,T1❫ ≻ ❪G,L,T❫ & ❪G,L,T❫ ≥ ❪G2,L2,T2❫.
+#G1 #G2 #L1 #L2 #T1 #T2 #H
+elim (fpbg_inv_gen … H) -H #G3 #L3 #T3 #G4 #L4 #T4 #H13 #H34 #H42
+elim (fpbs_inv_fpbc_sn … H13) -H13
+[ /3 width=9 by feqg_fpbc_trans, ex2_3_intro/
+| * #G #L #T #H1 #H3
+ /4 width=13 by fpbg_fwd_fpbs,fpbg_intro, ex2_3_intro/
+]
+qed-.
+
+(* Advanced properties of parallel rst-computation on closures **************)
+
+lemma fpbs_fpb_trans:
+ ∀F1,F2,K1,K2,T1,T2. ❪F1,K1,T1❫ ≥ ❪F2,K2,T2❫ →
+ ∀G2,L2,U2. ❪F2,K2,T2❫ ≻ ❪G2,L2,U2❫ →
+ ∃∃G1,L1,U1. ❪F1,K1,T1❫ ≻ ❪G1,L1,U1❫ & ❪G1,L1,U1❫ ≥ ❪G2,L2,U2❫.
+#F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_inv_fpbg … H) -H
+[ #H12 #G2 #L2 #U2 #H22
+ lapply (feqg_fpbc_trans … H12 … H22) -F2 -K2 -T2
+ /3 width=5 by feqg_fpbs, ex2_3_intro/
+| #H12 #G2 #L2 #U2 #H22
+ elim (fpbg_inv_fpbc_fpbs … H12) -H12 #F #K #T #H1 #H2
+ /4 width=9 by fpbs_strap1, fpbc_fwd_fpb, ex2_3_intro/
+]
+qed-.
(* *)
(**************************************************************************)
-include "static_2/static/feqg_fqup.ma".
-include "static_2/static/feqg_feqg.ma".
-include "basic_2/rt_transition/fpbq_fpb.ma".
-include "basic_2/rt_computation/fpbs_fqup.ma".
+include "basic_2/rt_computation/fpbs_fpbs.ma".
include "basic_2/rt_computation/fpbg.ma".
(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
(* Advanced forward lemmas **************************************************)
-lemma fpbg_fwd_fpbs:
- ∀G1,G2,L1,L2,T1,T2.
+lemma fpbg_fwd_fpbs (G1) (G2) (L1) (L2) (T1) (T2):
❪G1,L1,T1❫ > ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
-#G1 #G2 #L1 #L2 #T1 #T2 *
-/3 width=5 by fpbs_strap2, fpb_fpbq/
+#G1 #G2 #L1 #L2 #T1 #T2 #H
+elim (fpbg_inv_gen … H) -H
+/4 width=9 by fpbs_trans, fpbs_strap2, fpbc_fwd_fpb/
qed-.
-(* Advanced properties with sort-irrelevant equivalence on closures *********)
+(* Advanced properties ******************************************************)
-(* Basic_2A1: uses: fleq_fpbg_trans *)
-lemma feqx_fpbg_trans:
- ∀G,G2,L,L2,T,T2. ❪G,L,T❫ > ❪G2,L2,T2❫ →
- ∀G1,L1,T1. ❪G1,L1,T1❫ ≅ ❪G,L,T❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
-#G #G2 #L #L2 #T #T2 * #G0 #L0 #T0 #H0 #H02 #G1 #L1 #T1 #H1
-elim (feqg_fpb_trans … H1 … H0) -G -L -T
-/4 width=9 by fpbs_strap2, fpbq_feqx, ex2_3_intro/
-qed-.
-
-(* Properties with parallel proper rst-reduction on closures ****************)
-
-lemma fpb_fpbg_trans:
- ∀G1,G,G2,L1,L,L2,T1,T,T2.
- ❪G1,L1,T1❫ ≻ ❪G,L,T❫ → ❪G,L,T❫ > ❪G2,L2,T2❫ →
- ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
-/3 width=5 by fpbg_fwd_fpbs, ex2_3_intro/ qed-.
-
-(* Properties with parallel rst-reduction on closures ***********************)
-
-lemma fpbq_fpbg_trans:
- ∀G1,G,G2,L1,L,L2,T1,T,T2.
- ❪G1,L1,T1❫ ≽ ❪G,L,T❫ → ❪G,L,T❫ > ❪G2,L2,T2❫ →
- ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
-#G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2
-elim (fpbq_inv_fpb … H1) -H1
-/2 width=5 by feqx_fpbg_trans, fpb_fpbg_trans/
-qed-.
-
-(* Properties with parallel rst-compuutation on closures ********************)
-
-lemma fpbs_fpbg_trans:
- ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ →
+lemma fpbs_fpbg_trans (G) (L) (T):
+ ∀G1,L1,T1. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ →
∀G2,L2,T2. ❪G,L,T❫ > ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
-#G1 #G #L1 #L #T1 #T #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpbq_fpbg_trans/
+#G #L #T #G1 #L1 #T1 #H1 #G2 #L2 #T2 #H2
+elim (fpbg_inv_gen … H2) -H2
+/3 width=13 by fpbg_intro, fpbs_trans/
qed-.
-(* Advanced properties with plus-iterated structural successor for closures *)
-
-lemma fqup_fpbg_trans:
- ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ⬂+ ❪G,L,T❫ →
- ∀G2,L2,T2. ❪G,L,T❫ > ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
-/3 width=5 by fpbs_fpbg_trans, fqup_fpbs/ qed-.
-
-(* Advanced inversion lemmas of parallel rst-computation on closures ********)
-
-(* Basic_2A1: was: fpbs_fpbg *)
-lemma fpbs_inv_fpbg:
- ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ →
- ∨∨ ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫
- | ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
-#G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2
-[ /3 width=1 by feqg_refl, or_introl/
-| #G #G2 #L #L2 #T #T2 #_ #H2 * #H1
- elim (fpbq_inv_fpb … H2) -H2 #H2
- [ /3 width=5 by feqg_trans, or_introl/
- | elim (feqg_fpb_trans … H1 … H2) -G -L -T
- /4 width=5 by ex2_3_intro, or_intror, feqx_fpbs/
- | /3 width=5 by fpbg_feqx_trans, or_intror/
- | /4 width=5 by fpbg_fpbq_trans, fpb_fpbq, or_intror/
- ]
-]
-qed-.
-
-(* Advanced properties of parallel rst-computation on closures **************)
-
-lemma fpbs_fpb_trans:
- ∀F1,F2,K1,K2,T1,T2. ❪F1,K1,T1❫ ≥ ❪F2,K2,T2❫ →
- ∀G2,L2,U2. ❪F2,K2,T2❫ ≻ ❪G2,L2,U2❫ →
- ∃∃G1,L1,U1. ❪F1,K1,T1❫ ≻ ❪G1,L1,U1❫ & ❪G1,L1,U1❫ ≥ ❪G2,L2,U2❫.
-#F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_inv_fpbg … H) -H
-[ #H12 #G2 #L2 #U2 #H2 elim (feqg_fpb_trans … H12 … H2) -F2 -K2 -T2
- /3 width=5 by feqx_fpbs, ex2_3_intro/
-| * #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
- @(ex2_3_intro … H4) -H4 /3 width=5 by fpbs_strap1, fpb_fpbq/
-]
+(* Note: this is used in the closure proof *)
+lemma fpbg_fpbs_trans (G) (L) (T):
+ ∀G1,L1,T1. ❪G1,L1,T1❫ > ❪G,L,T❫ →
+ ∀G2,L2,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+#G #L #T #G1 #L1 #T1 #H1 #G2 #L2 #T2 #H2
+elim (fpbg_inv_gen … H1) -H1
+/3 width=13 by fpbg_intro, fpbs_trans/
qed-.
(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
-(* Advanced properties with sort-irrelevant equivalence for terms ***********)
+(* Advanced properties ******************************************************)
-lemma fpbg_teqx_div:
- ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ > ❪G2,L2,T❫ →
- ∀T2. T2 ≅ T → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
-/4 width=5 by fpbg_feqx_trans, teqg_feqg, teqx_sym/ qed-.
+lemma fpbc_fpbg (G1) (G2) (L1) (L2) (T1) (T2):
+ ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+/3 width=13 by fpbg_intro, fpb_fpbs/ qed.
-(* Properties with plus-iterated structural successor for closures **********)
-
-(* Note: this is used in the closure proof *)
-lemma fqup_fpbg:
- ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H
-/3 width=5 by fqus_fpbs, fpb_fqu, ex2_3_intro/
-qed.
+lemma fpbc_fpbs_fpbg (G) (L) (T):
+ ∀G1,L1,T1. ❪G1,L1,T1❫ ≻ ❪G,L,T❫ →
+ ∀G2,L2,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+/2 width=9 by fpbg_intro/ 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 "static_2/s_computation/fqus_fqup.ma".
+include "basic_2/rt_transition/fpbc_fqup.ma".
+include "basic_2/rt_computation/fpbs_fqus.ma".
+include "basic_2/rt_computation/fpbg_fqup.ma".
+include "basic_2/rt_computation/fpbg_fpbs.ma".
+
+(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
+
+(* Properties with plus-iterated structural successor for closures **********)
+
+(* Note: this is used in the closure proof *)
+lemma fqup_fpbg:
+ ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H
+/3 width=5 by fpbc_fpbs_fpbg, fqus_fpbs, fqu_fpbc/
+qed.
+
+(* Note: this is used in the closure proof *)
+lemma fqup_fpbg_trans (G) (L) (T):
+ ∀G1,L1,T1. ❪G1,L1,T1❫ ⬂+ ❪G,L,T❫ →
+ ∀G2,L2,T2. ❪G,L,T❫ > ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+/3 width=5 by fpbs_fpbg_trans, fqup_fpbs/ qed-.
(* *)
(**************************************************************************)
+include "basic_2/rt_transition/fpbc_lpx.ma".
include "basic_2/rt_computation/fpbs_lpxs.ma".
-include "basic_2/rt_computation/fpbg.ma".
+include "basic_2/rt_computation/fpbg_fqup.ma".
(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
(L1 ≅[T] L2 → ⊥) → ❪G,L1,T❫ > ❪G,L2,T❫.
#G #L1 #L2 #T #H #H0
elim (lpxs_rneqg_inv_step_sn … H … H0) -H -H0
-/4 width=7 by fpb_lpx, lpxs_feqx_fpbs, feqg_intro_sn, ex2_3_intro/
+/4 width=10 by fpbc_fpbs_fpbg, lpxs_feqg_fpbs, lpx_fpbc, feqg_intro_sn, sfull_dec/
qed.
include "ground/lib/star.ma".
include "basic_2/notation/relations/predsubtystar_6.ma".
-include "static_2/static/reqx.ma".
-include "basic_2/rt_transition/fpbq.ma".
+include "basic_2/rt_transition/fpb.ma".
(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
definition fpbs: tri_relation genv lenv term ≝
- tri_TC … fpbq.
+ tri_TC … fpb.
interpretation
"parallel rst-computation (closure)"
'PRedSubTyStar G1 L1 T1 G2 L2 T2 = (fpbs G1 L1 T1 G2 L2 T2).
-(* Basic eliminators ********************************************************)
-
-lemma fpbs_ind:
- ∀G1,L1,T1. ∀Q:relation3 genv lenv term. Q G1 L1 T1 →
- (∀G,G2,L,L2,T,T2. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ → ❪G,L,T❫ ≽ ❪G2,L2,T2❫ → Q G L T → Q G2 L2 T2) →
- ∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → Q G2 L2 T2.
-/3 width=8 by tri_TC_star_ind/ qed-.
-
-lemma fpbs_ind_dx:
- ∀G2,L2,T2. ∀Q:relation3 genv lenv term. Q G2 L2 T2 →
- (∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≽ ❪G,L,T❫ → ❪G,L,T❫ ≥ ❪G2,L2,T2❫ → Q G L T → Q G1 L1 T1) →
- ∀G1,L1,T1. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → Q G1 L1 T1.
-/3 width=8 by tri_TC_star_ind_dx/ qed-.
(* Basic properties *********************************************************)
-lemma fpbs_refl:
- tri_reflexive … fpbs.
-/2 width=1 by tri_inj/ qed.
-
-lemma fpbq_fpbs:
+(* Basic_2A1: uses: fpbq_fpbs *)
+lemma fpb_fpbs:
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ →
❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
/2 width=1 by tri_inj/ qed.
❪G,L,T❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
/2 width=5 by tri_TC_strap/ qed-.
-(* Basic_2A1: uses: lleq_fpbs fleq_fpbs *)
-lemma feqx_fpbs:
- ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
-/3 width=1 by fpbq_fpbs, fpbq_feqx/ qed.
-
-(* Basic_2A1: uses: fpbs_lleq_trans *)
-lemma fpbs_feqx_trans:
- ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ →
- ∀G2,L2,T2. ❪G,L,T❫ ≅ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
-/3 width=9 by fpbs_strap1, fpbq_feqx/ qed-.
-
-(* Basic_2A1: uses: lleq_fpbs_trans *)
-lemma feqx_fpbs_trans:
- ∀G,G2,L,L2,T,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ →
- ∀G1,L1,T1. ❪G1,L1,T1❫ ≅ ❪G,L,T❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
-/3 width=5 by fpbs_strap2, fpbq_feqx/ qed-.
-
-lemma teqx_reqx_lpx_fpbs:
- ∀T1,T2. T1 ≅ T2 → ∀L1,L0. L1 ≅[T2] L0 →
- ∀G,L2. ❪G,L0❫ ⊢ ⬈ L2 → ❪G,L1,T1❫ ≥ ❪G,L2,T2❫.
-/4 width=5 by feqx_fpbs, fpbs_strap1, fpbq_lpx, feqg_intro_dx/ qed.
-
(* Basic_2A1: removed theorems 3:
fpb_fpbsa_trans fpbs_fpbsa fpbsa_inv_fpbs
*)
(* *)
(**************************************************************************)
-include "basic_2/rt_transition/fpbq_aaa.ma".
-include "basic_2/rt_computation/fpbs.ma".
+include "basic_2/rt_transition/fpb_aaa.ma".
+include "basic_2/rt_computation/fpbs_fqup.ma".
(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
lemma fpbs_aaa_conf:
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ →
∀A1. ❪G1,L1❫ ⊢ T1 ⁝ A1 → ∃A2. ❪G2,L2❫ ⊢ T2 ⁝ A2.
-#G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 /2 width=2 by ex_intro/
-#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #A #HA elim (IH1 … HA) -IH1 -A
-/2 width=8 by fpbq_aaa_conf/
+#G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2
+[ /2 width=2 by ex_intro/
+| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #A #HA elim (IH1 … HA) -IH1 -A
+ /2 width=8 by fpb_aaa_conf/
+]
qed-.
(* *)
(**************************************************************************)
-include "basic_2/rt_transition/cpx_feqg.ma".
include "basic_2/rt_computation/lpxs_cpxs.ma".
include "basic_2/rt_computation/fpbs_lpxs.ma".
(* Properties with extended context-sensitive parallel rt-transition ********)
(* Basic_2A1: uses: fpbs_cpx_trans_neq *)
-lemma fpbs_cpx_tneqx_trans:
+lemma fpbs_cpx_tneqg_trans (S):
+ reflexive … S → symmetric … S → Transitive … S →
+ (∀s1,s2. Decidable (S s1 s2)) →
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ →
- ∀U2. ❪G2,L2❫ ⊢ T2 ⬈ U2 → (T2 ≅ U2 → ⊥) →
- ∃∃U1. ❪G1,L1❫ ⊢ T1 ⬈ U1 & T1 ≅ U1 → ⊥ & ❪G1,L1,U1❫ ≥ ❪G2,L2,U2❫.
-#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2
-elim (fpbs_inv_star … H) -H #G0 #L0 #L3 #T0 #T3 #HT10 #H10 #HL03 #H32
-elim (feqg_cpx_trans … H32 … HTU2) -HTU2 // #T4 #HT34 #H42
-lapply (feqg_tneqg_repl_dx … H32 … H42 … HnTU2) -T2 // #HnT34
-lapply (lpxs_cpx_trans … HT34 … HL03) -HT34 #HT34
-elim (fqus_cpxs_trans_tneqx … H10 … HT34 HnT34) -T3 #T2 #HT02 #HnT02 #H24
-elim (teqx_dec T1 T0) [ #H10 | -HnT02 #HnT10 ]
+ ∀U2. ❪G2,L2❫ ⊢ T2 ⬈ U2 → (T2 ≛[S] U2 → ⊥) →
+ ∃∃U1. ❪G1,L1❫ ⊢ T1 ⬈ U1 & T1 ≛[S] U1 → ⊥ & ❪G1,L1,U1❫ ≥ ❪G2,L2,U2❫.
+#S #H1S #H2S #H3S #H4S #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2
+elim (fpbs_inv_star S … H) -H // #G0 #L0 #L3 #T0 #T3 #HT10 #H10 #HL03 #H32
+lapply (feqg_cpx_trans_cpx … H32 … HTU2) // #HTU32
+lapply (feqg_tneqg_trans … H32 … HnTU2) -HnTU2 // #HnTU34
+lapply (feqg_cpx_trans_feqg … H32 … HTU2) // -T2 #H32
+lapply (lpxs_cpx_trans … HTU32 … HL03) -HTU32 #HTU32
+elim (fqus_cpxs_trans_tneqg … H10 … HTU32 HnTU34) -T3 #T2 #HT02 #HnT02 #H2
+elim (teqg_dec S … T1 T0) [ #H10 | -HnT02 #HnT10 | // ]
[ lapply (cpxs_trans … HT10 … HT02) -HT10 -HT02 #HT12
elim (cpxs_tneqg_fwd_step_sn … HT12)
- [2,7: /3 width=3 by teqg_canc_sn/ ] -T0 -HT12 //
-| elim (cpxs_tneqg_fwd_step_sn … HT10 … HnT10) -HT10 -HnT10 //
+ [2,7: /3 width=3 by teqg_canc_sn/ ] -T0 -HT12 /2 width=1 by sfull_dec/
+ /3 width=15 by fpbs_intro_star, ex3_intro/
+| elim (cpxs_tneqg_fwd_step_sn … HT10 … HnT10) -HT10 -HnT10 /2 width=1 by sfull_dec/
+ /4 width=15 by fpbs_intro_star, cpxs_trans, ex3_intro/
]
-/4 width=16 by fpbs_intro_star, cpxs_teqx_fpbs_trans, ex3_intro/
qed-.
(**************************************************************************)
include "basic_2/rt_computation/cpxs.ma".
-include "basic_2/rt_computation/fpbs_fqup.ma".
+include "basic_2/rt_computation/fpbs_feqg.ma".
+include "basic_2/rt_computation/fpbs_fqus.ma".
(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
lemma cpxs_fpbs:
∀G,L,T1,T2. ❪G,L❫ ⊢ T1 ⬈* T2 → ❪G,L,T1❫ ≥ ❪G,L,T2❫.
#G #L #T1 #T2 #H @(cpxs_ind … H) -T2
-/3 width=5 by fpbq_cpx, fpbs_strap1/
+/3 width=5 by cpx_fpb, fpbs_strap1/
qed.
lemma fpbs_cpxs_trans:
∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ →
∀T2. ❪G,L❫ ⊢ T ⬈* T2 → ❪G1,L1,T1❫ ≥ ❪G,L,T2❫.
#G1 #G #L1 #L #T1 #T #H1 #T2 #H @(cpxs_ind … H) -T2
-/3 width=5 by fpbs_strap1, fpbq_cpx/
+/3 width=5 by fpbs_strap1, cpx_fpb/
qed-.
lemma cpxs_fpbs_trans:
∀G1,G2,L1,L2,T,T2. ❪G1,L1,T❫ ≥ ❪G2,L2,T2❫ →
∀T1. ❪G1,L1❫ ⊢ T1 ⬈* T → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
#G1 #G2 #L1 #L2 #T #T2 #H1 #T1 #H @(cpxs_ind_dx … H) -T1
-/3 width=5 by fpbs_strap2, fpbq_cpx/
+/3 width=5 by fpbs_strap2, cpx_fpb/
qed-.
-lemma cpxs_teqx_fpbs_trans:
- ∀G1,L1,T1,T. ❪G1,L1❫ ⊢ T1 ⬈* T → ∀T0. T ≅ T0 →
+lemma cpxs_teqg_fpbs_trans (S):
+ reflexive … S → symmetric … S →
+ ∀G1,L1,T1,T. ❪G1,L1❫ ⊢ T1 ⬈* T → ∀T0. T ≛[S] T0 →
∀G2,L2,T2. ❪G1,L1,T0❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
-/3 width=3 by cpxs_fpbs_trans, teqx_fpbs_trans/ qed-.
+/3 width=6 by cpxs_fpbs_trans, teqg_fpbs_trans/ qed-.
-lemma cpxs_teqx_fpbs:
+lemma cpxs_teqg_fpbs (S):
+ reflexive … S → symmetric … S →
∀G,L,T1,T. ❪G,L❫ ⊢ T1 ⬈* T →
- ∀T2. T ≅ T2 → ❪G,L,T1❫ ≥ ❪G,L,T2❫.
-/4 width=3 by cpxs_fpbs_trans, feqx_fpbs, teqg_feqg/ qed.
-
-(* Properties with star-iterated structural successor for closures **********)
-
-lemma cpxs_fqus_fpbs:
- ∀G1,L1,T1,T. ❪G1,L1❫ ⊢ T1 ⬈* T →
- ∀G2,L2,T2. ❪G1,L1,T❫ ⬂* ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
-/3 width=5 by fpbs_fqus_trans, cpxs_fpbs/ qed.
+ ∀T2. T ≛[S] T2 → ❪G,L,T1❫ ≥ ❪G,L,T2❫.
+/4 width=5 by cpxs_fpbs_trans, feqg_fpbs, teqg_feqg/ qed.
(* Properties with plus-iterated structural successor for closures **********)
∀G1,L1,T1,T. ❪G1,L1❫ ⊢ T1 ⬈* T →
∀G2,L2,T2. ❪G1,L1,T❫ ⬂+ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
/3 width=5 by fpbs_fqup_trans, cpxs_fpbs/ qed.
+
+(* Properties with star-iterated structural successor for closures **********)
+
+lemma cpxs_fqus_fpbs:
+ ∀G1,L1,T1,T. ❪G1,L1❫ ⊢ T1 ⬈* T →
+ ∀G2,L2,T2. ❪G1,L1,T❫ ⬂* ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
+/3 width=5 by fpbs_fqus_trans, cpxs_fpbs/ qed.
(* *)
(**************************************************************************)
-include "basic_2/rt_computation/csx_fpbq.ma".
-include "basic_2/rt_computation/fpbs.ma".
+include "basic_2/rt_computation/csx_fpb.ma".
+include "basic_2/rt_computation/fpbs_fqup.ma".
(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒 T1 →
∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*𝐒 T2.
#G1 #L1 #T1 #HT1 #G2 #L2 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2
-/2 width=5 by csx_fpbq_conf/
+/2 width=5 by csx_fpb_conf/
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 "static_2/static/feqg_fqup.ma".
+include "basic_2/rt_transition/fpb_feqg.ma".
+include "basic_2/rt_computation/fpbs_fqup.ma".
+
+(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
+
+(* Propreties with generic equivalence on referred closures *****************)
+
+(* Basic_2A1: uses: lleq_fpbs fleq_fpbs *)
+lemma feqg_fpbs (S) (G1) (G2) (L1) (L2) (T1) (T2):
+ reflexive … S → symmetric … S →
+ ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
+/3 width=5 by fpb_fpbs, feqg_fpb/ qed.
+
+(* Basic_2A1: uses: fpbs_lleq_trans *)
+lemma fpbs_feqg_trans (S) (G) (L) (T):
+ reflexive … S → symmetric … S →
+ ∀G1,L1,T1. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ →
+ ∀G2,L2,T2. ❪G,L,T❫ ≛[S] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
+/3 width=9 by fpbs_strap1, feqg_fpb/ qed-.
+
+(* Basic_2A1: uses: lleq_fpbs_trans *)
+lemma feqg_fpbs_trans (S) (G) (L) (T):
+ reflexive … S → symmetric … S →
+ ∀G2,L2,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ →
+ ∀G1,L1,T1. ❪G1,L1,T1❫ ≛[S] ❪G,L,T❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
+/3 width=5 by fpbs_strap2, feqg_fpb/ qed-.
+
+lemma teqg_fpbs_trans (S) (T):
+ reflexive … S → symmetric … S →
+ ∀T1. T1 ≛[S] T →
+ ∀G1,G2,L1,L2,T2. ❪G1,L1,T❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
+/3 width=8 by feqg_fpbs_trans, teqg_feqg/ qed-.
+
+lemma fpbs_teqg_trans (S) (T):
+ reflexive … S → symmetric … S →
+ ∀G1,G2,L1,L2,T1. ❪G1,L1,T1❫ ≥ ❪G2,L2,T❫ →
+ ∀T2. T ≛[S] T2 → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
+/3 width=8 by fpbs_feqg_trans, teqg_feqg/ 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/rt_transition/fpbq_fpb.ma".
-include "basic_2/rt_computation/fpbs.ma".
-
-(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
-
-(* Properties with proper parallel rst-reduction on closures ****************)
-
-lemma fpb_fpbs:
- ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ →
- ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
-/3 width=1 by fpbq_fpbs, fpb_fpbq/ 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/rt_transition/fpbc_feqg.ma".
+include "basic_2/rt_transition/fpbc_fpb.ma".
+include "basic_2/rt_computation/fpbs_feqg.ma".
+
+(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
+
+(* Properties with proper parallel rst-reduction on closures ****************)
+
+lemma fpbc_fpbs:
+ ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ →
+ ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
+/3 width=1 by fpb_fpbs, fpbc_fwd_fpb/ qed.
+
+(* Inversion lemmas with proper parallel rst-reduction on closures **********)
+
+lemma fpbs_inv_fpbc_sn:
+ ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ →
+ ∨∨ ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫
+ | ∃∃G,L,T. ❪G1,L1,T1❫ ≻ ❪G,L,T❫ & ❪G,L,T❫ ≥ ❪G2,L2,T2❫.
+#G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2
+[ /3 width=1 by feqg_refl, or_introl/
+| #G #G2 #L #L2 #T #T2 #_ #H2 * [ #H1 | * #G0 #L0 #T0 #H10 #H0 ]
+ elim (fpb_inv_fpbc … H2) -H2 #H2
+ [ /3 width=5 by feqg_trans, or_introl/
+ | lapply (feqg_fpbc_trans … H1 … H2) -G -L -T //
+ /3 width=5 by fpb_fpbs, ex2_3_intro, or_intror/
+ | /4 width=12 by fpbs_feqg_trans, ex2_3_intro, or_intror/
+ | /5 width=9 by fpbs_strap1, fpbc_fwd_fpb, ex2_3_intro, or_intror/
+ ]
+]
+qed-.
(* *)
(**************************************************************************)
-include "static_2/s_computation/fqus_fqup.ma".
-include "static_2/static/feqg_fqup.ma".
-include "basic_2/rt_computation/fpbs_fqus.ma".
+include "basic_2/rt_transition/fpb_fqup.ma".
+include "basic_2/rt_computation/fpbs.ma".
(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
-(* Advanced properties ******************************************************)
+(* Advanced eliminators *****************************************************)
+
+lemma fpbs_ind:
+ ∀G1,L1,T1. ∀Q:relation3 genv lenv term. Q G1 L1 T1 →
+ (∀G,G2,L,L2,T,T2. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ → ❪G,L,T❫ ≽ ❪G2,L2,T2❫ → Q G L T → Q G2 L2 T2) →
+ ∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → Q G2 L2 T2.
+/3 width=8 by tri_TC_star_ind/ qed-.
-lemma teqx_fpbs_trans:
- ∀T1,T. T1 ≅ T →
- ∀G1,G2,L1,L2,T2. ❪G1,L1,T❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
-/3 width=5 by feqx_fpbs_trans, teqg_feqg/ qed-.
+lemma fpbs_ind_dx:
+ ∀G2,L2,T2. ∀Q:relation3 genv lenv term. Q G2 L2 T2 →
+ (∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≽ ❪G,L,T❫ → ❪G,L,T❫ ≥ ❪G2,L2,T2❫ → Q G L T → Q G1 L1 T1) →
+ ∀G1,L1,T1. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → Q G1 L1 T1.
+/3 width=8 by tri_TC_star_ind_dx/ qed-.
+
+(* Advanced properties ******************************************************)
-lemma fpbs_teqx_trans:
- ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ ≥ ❪G2,L2,T❫ →
- ∀T2. T ≅ T2 → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
-/3 width=5 by fpbs_feqx_trans, teqg_feqg/ qed-.
+lemma fpbs_refl:
+ tri_reflexive … fpbs.
+/2 width=1 by tri_inj/ qed.
(* Properties with plus-iterated structural successor for closures **********)
lemma fqup_fpbs:
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
-/4 width=5 by fqu_fquq, fpbq_fquq, tri_step/
+/4 width=5 by fqu_fquq, fquq_fpb, tri_step/
qed.
lemma fpbs_fqup_trans:
∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ →
∀G2,L2,T2. ❪G,L,T❫ ⬂+ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
-/3 width=5 by fpbs_fqus_trans, fqup_fqus/ qed-.
+#G1 #G #L1 #L #T1 #T #H1 #G2 #L2 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+/3 width=5 by fpbs_strap1, fqu_fpb/
+qed-.
lemma fqup_fpbs_trans:
∀G,G2,L,L2,T,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ →
∀G1,L1,T1. ❪G1,L1,T1❫ ⬂+ ❪G,L,T❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
-/3 width=5 by fqus_fpbs_trans, fqup_fqus/ qed-.
+#G #G2 #L #L2 #T #T2 #H1 #G1 #L1 #T1 #H @(fqup_ind_dx … H) -G1 -L1 -T1
+/3 width=9 by fpbs_strap2, fqu_fpb/
+qed-.
\ No newline at end of file
(**************************************************************************)
include "static_2/s_computation/fqus.ma".
-include "basic_2/rt_computation/fpbs.ma".
+include "basic_2/rt_computation/fpbs_fqup.ma".
(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂* ❪G2,L2,T2❫ →
❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2
-/3 width=5 by fpbq_fquq, tri_step/
+/3 width=5 by fquq_fpb, fpbs_strap1/
qed.
lemma fpbs_fqus_trans:
∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ →
∀G2,L2,T2. ❪G,L,T❫ ⬂* ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
#G1 #G #L1 #L #T1 #T #H1 #G2 #L2 #T2 #H @(fqus_ind … H) -G2 -L2 -T2
-/3 width=5 by fpbs_strap1, fpbq_fquq/
+/3 width=5 by fpbs_strap1, fquq_fpb/
qed-.
lemma fqus_fpbs_trans:
∀G,G2,L,L2,T,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ →
∀G1,L1,T1. ❪G1,L1,T1❫ ⬂* ❪G,L,T❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
#G #G2 #L #L2 #T #T2 #H1 #G1 #L1 #T1 #H @(fqus_ind_dx … H) -G1 -L1 -T1
-/3 width=5 by fpbs_strap2, fpbq_fquq/
+/3 width=5 by fpbs_strap2, fquq_fpb/
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/rt_transition/fpb_lpx.ma".
+include "basic_2/rt_computation/fpbs_feqg.ma".
+
+(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
+
+(* Properties with extended rt-transition on full local environments *******)
+
+lemma fpbs_lpx_trans (L):
+ ∀G1,G2,L1,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L,T2❫ →
+ ∀L2. ❪G2,L❫ ⊢ ⬈ L2 → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
+/3 width=5 by fpbs_strap1, lpx_fpb/ qed-.
+
+lemma teqg_reqg_lpx_fpbs (S):
+ reflexive … S → symmetric … S →
+ ∀T1,T2. T1 ≛[S] T2 → ∀L1,L0. L1 ≛[S,T2] L0 →
+ ∀G,L2. ❪G,L0❫ ⊢ ⬈ L2 → ❪G,L1,T1❫ ≥ ❪G,L2,T2❫.
+/4 width=7 by feqg_fpbs, fpbs_strap1, lpx_fpb, feqg_intro_dx/ qed.
(* *)
(**************************************************************************)
-include "static_2/static/feqg_fqus.ma".
-include "static_2/static/feqg_feqg.ma".
include "basic_2/rt_computation/cpxs_fqus.ma".
-include "basic_2/rt_computation/cpxs_feqg.ma".
+include "basic_2/rt_computation/cpxs_reqg.ma".
include "basic_2/rt_computation/lpxs_feqg.ma".
+include "basic_2/rt_computation/fpbs_lpx.ma".
include "basic_2/rt_computation/fpbs_cpxs.ma".
(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
lemma lpxs_fpbs:
∀G,L1,L2,T. ❪G,L1❫ ⊢ ⬈* L2 → ❪G,L1,T❫ ≥ ❪G,L2,T❫.
#G #L1 #L2 #T #H @(lpxs_ind_dx … H) -L2
-/3 width=5 by fpbq_lpx, fpbs_strap1/
+/3 width=5 by lpx_fpb, fpbs_strap1/
qed.
lemma fpbs_lpxs_trans:
∀G1,G2,L1,L,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L,T2❫ →
∀L2. ❪G2,L❫ ⊢ ⬈* L2 → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
#G1 #G2 #L1 #L #T1 #T2 #H1 #L2 #H @(lpxs_ind_dx … H) -L2
-/3 width=5 by fpbs_strap1, fpbq_lpx/
+/3 width=5 by fpbs_strap1, lpx_fpb/
qed-.
lemma lpxs_fpbs_trans:
∀G1,G2,L,L2,T1,T2. ❪G1,L,T1❫ ≥ ❪G2,L2,T2❫ →
∀L1. ❪G1,L1❫ ⊢ ⬈* L → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
#G1 #G2 #L #L2 #T1 #T2 #H1 #L1 #H @(lpxs_ind_sn … H) -L1
-/3 width=5 by fpbs_strap2, fpbq_lpx/
+/3 width=5 by fpbs_strap2, lpx_fpb/
qed-.
(* Basic_2A1: uses: lpxs_lleq_fpbs *)
-lemma lpxs_feqx_fpbs:
- ∀G1,L1,L,T1. ❪G1,L1❫ ⊢ ⬈* L →
- ∀G2,L2,T2. ❪G1,L,T1❫ ≅ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
-/3 width=3 by lpxs_fpbs_trans, feqx_fpbs/ qed.
-
-lemma fpbs_lpx_trans:
- ∀G1,G2,L1,L,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L,T2❫ →
- ∀L2. ❪G2,L❫ ⊢ ⬈ L2 → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
-/3 width=3 by fpbs_lpxs_trans, lpx_lpxs/ qed-.
+lemma lpxs_feqg_fpbs (S) (L):
+ reflexive … S → symmetric … S →
+ ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈* L →
+ ∀G2,L2,T2. ❪G1,L,T1❫ ≛[S] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
+/3 width=4 by lpxs_fpbs_trans, feqg_fpbs/ qed.
(* Properties with star-iterated structural successor for closures **********)
∀L2.❪G2,L❫ ⊢ ⬈* L2 → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
/3 width=5 by cpxs_fqus_fpbs, fpbs_lpxs_trans/ qed.
-lemma fpbs_cpxs_teqx_fqup_lpx_trans:
+lemma fpbs_cpxs_teqg_fqup_lpx_trans (S):
+ reflexive … S → symmetric … S →
∀G1,G3,L1,L3,T1,T3. ❪G1,L1,T1❫ ≥ ❪G3,L3,T3❫ →
- â\88\80T4. â\9dªG3,L3â\9d« â\8a¢ T3 â¬\88* T4 â\86\92 â\88\80T5. T4 â\89\85 T5 →
+ â\88\80T4. â\9dªG3,L3â\9d« â\8a¢ T3 â¬\88* T4 â\86\92 â\88\80T5. T4 â\89\9b[S] T5 →
∀G2,L4,T2. ❪G3,L3,T5❫ ⬂+ ❪G2,L4,T2❫ →
∀L2. ❪G2,L4❫ ⊢ ⬈ L2 → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
-#G1 #G3 #L1 #L3 #T1 #T3 #H13 #T4 #HT34 #T5 #HT45 #G2 #L4 #T2 #H34 #L2 #HL42
+#S #H1S #H2S #G1 #G3 #L1 #L3 #T1 #T3 #H13 #T4 #HT34 #T5 #HT45 #G2 #L4 #T2 #H34 #L2 #HL42
@(fpbs_lpx_trans … HL42) -L2 (**) (* full auto too slow *)
@(fpbs_fqup_trans … H34) -G2 -L4 -T2
-/3 width=3 by fpbs_cpxs_trans, fpbs_teqx_trans/
+/3 width=6 by fpbs_cpxs_trans, fpbs_teqg_trans/
qed-.
(* Advanced properties ******************************************************)
(* Basic_2A1: uses: fpbs_intro_alt *)
-lemma fpbs_intro_star:
- ∀G1,L1,T1,T. ❪G1,L1❫ ⊢ T1 ⬈* T →
- ∀G,L,T0. ❪G1,L1,T❫ ⬂* ❪G,L,T0❫ →
- â\88\80L0. ❪G,L❫ ⊢ ⬈* L0 →
- â\88\80G2,L2,T2. â\9dªG,L0,T0â\9d« â\89\85 â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« â\89¥ â\9dªG2,L2,T2â\9d« .
-/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpbq_feqx/ qed.
+lemma fpbs_intro_star (S) (G) (T) (T0) (L) (L0):
+ reflexive … S → symmetric … S →
+ ∀G1,L1,T1. ❪G1,L1❫ ⊢ T1 ⬈* T →
+ â\9dªG1,L1,Tâ\9d« â¬\82* â\9dªG,L,T0â\9d« â\86\92 ❪G,L❫ ⊢ ⬈* L0 →
+ â\88\80G2,L2,T2. â\9dªG,L0,T0â\9d« â\89\9b[S] â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« â\89¥ â\9dªG2,L2,T2â\9d«.
+/3 width=8 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, feqg_fpb/ qed.
(* Advanced inversion lemmas *************************************************)
(* Basic_2A1: uses: fpbs_inv_alt *)
-lemma fpbs_inv_star:
+lemma fpbs_inv_star (S):
+ reflexive … S → symmetric … S → Transitive … S →
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ →
- â\88\83â\88\83G,L,L0,T,T0. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* T & â\9dªG1,L1,Tâ\9d« â¬\82* â\9dªG,L,T0â\9d« & â\9dªG,Lâ\9d« â\8a¢ â¬\88* L0 & â\9dªG,L0,T0â\9d« â\89\85 ❪G2,L2,T2❫.
-#G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1
+ â\88\83â\88\83G,L,L0,T,T0. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* T & â\9dªG1,L1,Tâ\9d« â¬\82* â\9dªG,L,T0â\9d« & â\9dªG,Lâ\9d« â\8a¢ â¬\88* L0 & â\9dªG,L0,T0â\9d« â\89\9b[S] ❪G2,L2,T2❫.
+#S #H1S #H2S #H3S #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1
[ /3 width=9 by feqg_refl, ex4_5_intro/
-| #G1 #G0 #L1 #L0 #T1 #T0 * -G0 -L0 -T0
- [ #G0 #L0 #T0 #H10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
- elim (fquq_cpxs_trans … HT03 … H10) -T0
- /3 width=9 by fqus_strap2, ex4_5_intro/
- | #T0 #HT10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
- /3 width=9 by cpxs_strap2, ex4_5_intro/
- | #L0 #HL10 #_ * #G3 #L3 #L4 #T3 #T4 #HT13 #H34 #HL34 #H42
- lapply (lpx_cpxs_trans … HT13 … HL10) -HT13 #HT13
- elim (lpx_fqus_trans … H34 … HL10) -L0
- /3 width=9 by lpxs_step_sn, cpxs_trans, ex4_5_intro/
- | #G0 #L0 #T0 #H10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
- elim (feqg_cpxs_trans … H10 … HT03) -T0 // #T0 #HT10 #H03
- elim (feqg_fqus_trans … H03 … H34) -G0 -L0 -T3 // #G0 #L0 #T3 #H03 #H34
- elim (feqg_lpxs_trans … H34 … HL34) -L3 // #L3 #HL03 #H34
- /3 width=13 by feqg_trans, ex4_5_intro/
- ]
+| #G1 #G0 #L1 #L0 #T1 #T0 *
+ #L3 #T3 #H13 #HT30 #HL30 #_ *
+ #G4 #L4 #L5 #T4 #T5 #HT04 #H45 #HL45 #H52
+ lapply (rpx_cpx_conf_sn … HT30 … HL30) -HL30 #HL30
+ elim (fquq_cpx_trans … H13 … HT30) -T3 #T3 #HT13 #H30
+ elim (rpx_fwd_lpx_reqg S … HL30) -HL30 // #L #HL3 #HL0
+ lapply (reqg_cpxs_trans … HT04 … HL0) -HT04 // #HT04
+ lapply (cpxs_reqg_conf_sn … HT04 … HL0) -HL0 #HL0
+ lapply (lpx_cpxs_trans … HT04 … HL3) -HT04 #HT04
+ elim (fquq_cpxs_trans … HT04 … H30) -T0 #T0 #HT30 #H04
+ lapply (cpxs_strap2 … HT13 … HT30) -T3 #HT10
+ elim (reqg_fqus_trans … H45 … HL0) -L0 // #L0 #T3 #H43 #HT35 #HL04
+ lapply (feqg_intro_dx … G4 … HL04 … HT35) -HL04 -HT35 // #H35
+ elim (lpx_fqus_trans … H43 … HL3) -L #L #T #HT4 #H3 #HL0
+ elim (fquq_cpxs_trans … HT4 … H04) -T4 #T4 #HT04 #H4
+ lapply (cpxs_trans … HT10 … HT04) -T0 #HT14
+ lapply (fqus_strap2 … H4 … H3) -G0 -L3 -T #H43
+ elim (feqg_lpxs_trans … H35 … HL45) -L4 // #L4 #HL04 #H35
+ lapply (lpxs_step_sn … HL0 … HL04) -L0 #HL4
+ lapply (feqg_trans … H35 … H52) -L5 -T5 // #H32
+ /2 width=9 by ex4_5_intro/
]
qed-.
(**************************************************************************)
include "basic_2/notation/relations/predsubtystrong_3.ma".
-include "basic_2/rt_transition/fpb.ma".
+include "basic_2/rt_transition/fpbc.ma".
(* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************)
include "basic_2/rt_computation/csx_aaa.ma".
include "basic_2/rt_computation/fpbs_aaa.ma".
-include "basic_2/rt_computation/fpbs_fpb.ma".
include "basic_2/rt_computation/fsb_csx.ma".
(* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************)
(* Main properties with atomic arity assignment for terms *******************)
-theorem aaa_fsb:
- â\88\80G,L,T,A. â\9dªG,Lâ\9d« â\8a¢ T â\81\9d A â\86\92 â\89¥ð\9d\90\92 â\9dªG,L,Tâ\9d«.
+theorem aaa_fsb (G) (L) (T) (A):
+ ❪G,L❫ ⊢ T ⁝ A → ≥𝐒 ❪G,L,T❫.
/3 width=2 by aaa_csx, csx_fsb/ qed.
(* Advanced eliminators with atomic arity assignment for terms **************)
-fact aaa_ind_fpb_aux (Q:relation3 …):
+fact aaa_ind_fpbc_aux (Q:relation3 …):
(∀G1,L1,T1,A.
❪G1,L1❫ ⊢ T1 ⁝ A →
(∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → Q G2 L2 T2) →
Q G1 L1 T1
) →
∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒 T → ∀A. ❪G,L❫ ⊢ T ⁝ A → Q G L T.
-#R #IH #G #L #T #H @(csx_ind_fpb … H) -G -L -T
+#R #IH #G #L #T #H @(csx_ind_fpbc … H) -G -L -T
#G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH //
#G2 #L2 #T2 #H12 elim (fpbs_aaa_conf … G2 … L2 … T2 … HTA1) -A1
-/2 width=2 by fpb_fpbs/
+/2 width=2 by fpbc_fpbs/
qed-.
-lemma aaa_ind_fpb (Q:relation3 …):
+lemma aaa_ind_fpbc (Q:relation3 …):
(∀G1,L1,T1,A.
❪G1,L1❫ ⊢ T1 ⁝ A →
(∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → Q G2 L2 T2) →
Q G1 L1 T1
) →
∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → Q G L T.
-/4 width=4 by aaa_ind_fpb_aux, aaa_csx/ qed-.
+/4 width=4 by aaa_ind_fpbc_aux, aaa_csx/ qed-.
fact aaa_ind_fpbg_aux (Q:relation3 …):
(∀G1,L1,T1,A.
(* *)
(**************************************************************************)
+include "basic_2/rt_transition/fpbc_fqup.ma".
+include "basic_2/rt_transition/fpbc_lpx.ma".
include "basic_2/rt_computation/rsx_csx.ma".
include "basic_2/rt_computation/fpbs_cpx.ma".
include "basic_2/rt_computation/fpbs_csx.ma".
lemma fsb_inv_csx:
∀G,L,T. ≥𝐒 ❪G,L,T❫ → ❪G,L❫ ⊢ ⬈*𝐒 T.
-#G #L #T #H @(fsb_ind_alt … H) -G -L -T /5 width=1 by csx_intro, fpb_cpx/
+#G #L #T #H @(fsb_ind_alt … H) -G -L -T
+/5 width=1 by csx_intro, cpx_fpbc/
qed-.
(* Propreties with context-sensitive stringly rt-normalizing terms **********)
#G0 #L0 #T0 #IHu #H10
lapply (fpbs_csx_conf … H10) // -HT1 #HT0
generalize in match IHu; -IHu generalize in match H10; -H10
-@(rsx_ind … (csx_rsx … HT0)) -L0
-#L0 #_ #IHd #H10 #IHu @fsb_intro
-#G2 #L2 #T2 * -G2 -L2 -T2 [ -IHd -IHc | -IHu -IHd | ]
-[ /4 width=5 by fpbs_fqup_trans, fqu_fqup/
-| #T2 #HT02 #HnT02
- elim (fpbs_cpx_tneqx_trans … H10 … HT02 HnT02) -T0
- /3 width=4 by/
-| #L2 #HL02 #HnL02 @(IHd … HL02 HnL02) -IHd -HnL02 [ -IHu -IHc | ]
+@(rsx_ind … (csx_rsx … HT0)) -L0 #L0 #_ #IHd #H10 #IHu
+@fsb_intro #G2 #L2 #T2 #H
+elim (fpbc_fwd_lpx … H) -H * [ -IHd -IHc | -IHu -IHd |]
+[ /5 width=5 by fsb_fpb_trans, fpbs_fqup_trans, fqu_fqup/
+| #T3 #HT03 #HnT03 #H32
+ elim (fpbs_cpx_tneqg_trans … H10 … HT03 HnT03) -T0
+ /4 width=5 by fsb_fpb_trans, sfull_dec/
+| #L3 #HL03 #HnL03 #HL32
+ @(fsb_fpb_trans … HL32) -L2
+ @(IHd … HL03 HnL03) -IHd -HnL03 [ -IHu -IHc |]
[ /3 width=3 by fpbs_lpxs_trans, lpx_lpxs/
- | #G3 #L3 #T3 #H03 #_
- elim (lpx_fqup_trans … H03 … HL02) -L2 #L4 #T4 #HT04 #H43 #HL43
- elim (teqx_dec T0 T4) [ -IHc -HT04 #HT04 | -IHu #HnT04 ]
- [ elim (teqg_fqup_trans … H43 … HT04) -T4 // #L2 #T4 #H04 #HT43 #HL24
- /4 width=7 by fsb_fpbs_trans, teqx_reqx_lpx_fpbs, fpbs_fqup_trans/
- | elim (cpxs_tneqg_fwd_step_sn … HT04 HnT04) -HT04 -HnT04 // #T2 #HT02 #HnT02 #HT24
- elim (fpbs_cpx_tneqx_trans … H10 … HT02 HnT02) -T0 #T0 #HT10 #HnT10 #H02
- /3 width=14 by fpbs_cpxs_teqx_fqup_lpx_trans/
+ | #G4 #L4 #T4 #H04 #_
+ elim (lpx_fqup_trans … H04 … HL03) -L3 #L3 #T3 #HT03 #H34 #HL34
+ elim (teqx_dec T0 T3) [ -IHc -HT03 #HT03 | -IHu #HnT03 ]
+ [ elim (teqg_fqup_trans … H34 … HT03) -T3 // #L2 #T3 #H03 #HT34 #HL23
+ /4 width=10 by fsb_fpbs_trans, teqg_reqg_lpx_fpbs, fpbs_fqup_trans/
+ | elim (cpxs_tneqg_fwd_step_sn … HT03 HnT03) -HT03 -HnT03 /2 width=1 by sfull_dec/ #T2 #HT02 #HnT02 #HT23
+ elim (fpbs_cpx_tneqg_trans … H10 … HT02 HnT02) -T0 /2 width=1 by sfull_dec/ #T0 #HT10 #HnT10 #H02
+ /3 width=17 by fpbs_cpxs_teqg_fqup_lpx_trans/
]
]
]
qed.
-lemma csx_fsb:
- â\88\80G,L,T. â\9dªG,Lâ\9d« â\8a¢ â¬\88*ð\9d\90\92 T â\86\92 â\89¥ð\9d\90\92 â\9dªG,L,Tâ\9d«.
+lemma csx_fsb (G) (L) (T):
+ ❪G,L❫ ⊢ ⬈*𝐒 T → ≥𝐒 ❪G,L,T❫.
/2 width=5 by csx_fsb_fpbs/ qed.
(* Advanced eliminators *****************************************************)
-lemma csx_ind_fpb (Q:relation3 …):
+lemma csx_ind_fpbc (Q:relation3 …):
(∀G1,L1,T1.
❪G1,L1❫ ⊢ ⬈*𝐒 T1 →
(∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → Q G2 L2 T2) →
(* *)
(**************************************************************************)
-include "basic_2/rt_transition/fpb_feqg.ma".
+include "static_2/static/feqg_fqup.ma".
+include "basic_2/rt_transition/fpbc_feqg.ma".
include "basic_2/rt_computation/fsb.ma".
(* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************)
#S #H1S #H2S #H3S #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
#G1 #L1 #T1 #_ #IH #G2 #L2 #T2 #H12
@fsb_intro #G #L #T #H2
-elim (feqg_fpb_trans … H12 … H2) -G2 -L2 -T2
-/2 width=5 by/
+elim (feqg_fpbc_trans … H12 … H2) -G2 -L2 -T2
+/4 width=5 by fpbc_intro, feqg_refl/
qed-.
(* *)
(**************************************************************************)
-include "basic_2/rt_computation/fpbg_fpbs.ma".
+include "basic_2/rt_computation/fpbg_fqup.ma".
+include "basic_2/rt_computation/fpbg_feqg.ma".
include "basic_2/rt_computation/fsb_feqg.ma".
(* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************)
#G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
elim (fpbs_inv_fpbg … H12) -H12
[ -IH /2 width=9 by fsb_feqg_trans/
-| -H1 * /2 width=5 by/
+| -H1 #H elim (fpbg_inv_fpbc_fpbs … H)
+ /2 width=5 by/
]
qed-.
+(* Properties with parallel rst-transition for closures *********************)
+
+lemma fsb_fpb_trans:
+ ∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
+ ∀G2,L2,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫.
+/3 width=5 by fsb_fpbs_trans, fpb_fpbs/ qed-.
+
(* Properties with proper parallel rst-computation for closures *************)
lemma fsb_intro_fpbg:
∀G1,L1,T1.
(∀G2,L2,T2. ❪G1,L1,T1❫ > ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫) →
≥𝐒 ❪G1,L1,T1❫.
-/4 width=1 by fsb_intro, fpb_fpbg/ qed.
+/4 width=1 by fsb_intro, fpbc_fpbg/ qed.
(* Eliminators with proper parallel rst-computation for closures ************)
@IH1 -IH1
[ -IH /2 width=5 by fsb_fpbs_trans/
| -H1 #G0 #L0 #T0 #H10
- elim (fpbs_fpbg_trans … H12 … H10) -G2 -L2 -T2
+ lapply (fpbs_fpbg_trans … H12 … H10) -G2 -L2 -T2 #H
+ elim (fpbg_inv_fpbc_fpbs … H) -H #G #L #T #H1 #H0
/2 width=5 by/
]
qed-.
[ lapply (reqg_rneqg_trans … H … HnLK0) -H -HnLK0 // #Hn10
lapply (lpxs_trans … HL10 … HLK0) -L0 #H10
elim (lpxs_rneqg_inv_step_sn … H10 … Hn10) -H10 -Hn10
- /3 width=8 by reqg_trans/
-| elim (lpxs_rneqg_inv_step_sn … HL10 … H) -HL10 -H // #L #K #HL1 #HnL1 #HLK #HKL0
+ /3 width=8 by reqg_trans, sfull_dec/
+| elim (lpxs_rneqg_inv_step_sn … HL10 … H) -HL10 -H /2 width=1 by sfull_dec/ #L #K #HL1 #HnL1 #HLK #HKL0
elim (reqg_lpxs_trans … HLK0 … HKL0) -L0
/3 width=8 by lpxs_trans, reqg_trans/
]
#Y #HY #IHY #L2 #H #HL12 destruct
@rsx_intro_lpxs #L0 #HL20
lapply (lpxs_trans … HL12 … HL20) #HL10 #H
-elim (rneqg_inv_bind … H) -H // [ -IHY | -HY -IHL1 -HL12 ]
+elim (rneqg_inv_bind … H) -H /2 width=1 by sfull_dec/ [ -IHY | -HY -IHL1 -HL12 ]
[ #HnV elim (reqx_dec L1 L2 V)
[ #HV @(IHL1 … HL10) -IHL1 -HL12 -HL10
/3 width=4 by rsx_lpxs_trans, lpxs_bind_refl_dx, reqg_canc_sn/ (**) (* full auto too slow *)
#L1 #HL1 #IHL1 #L2 #T #H @(rsx_ind_lpxs … H) -L2
#L2 #HL2 #IHL2 #HL12 @rsx_intro_lpxs
#L0 #HL20 lapply (lpxs_trans … HL12 … HL20)
-#HL10 #H elim (rneqg_inv_flat … H) -H // [ -HL1 -IHL2 | -HL2 -IHL1 ]
+#HL10 #H elim (rneqg_inv_flat … H) -H /2 width=1 by sfull_dec/ [ -HL1 -IHL2 | -HL2 -IHL1 ]
[ #HnV elim (reqx_dec L1 L2 V)
[ #HV @(IHL1 … HL10) -IHL1 -HL12 -HL10
/3 width=5 by rsx_lpxs_trans, reqg_canc_sn/ (**) (* full auto too slow: 47s *)
#Y #HY #IHY #L2 #H #HL12 destruct
@rsx_intro_lpxs #L0 #HL20
lapply (lpxs_trans … HL12 … HL20) #HL10 #H
-elim (rneqg_inv_bind_void … H) -H // [ -IHY | -HY -IHL1 -HL12 ]
+elim (rneqg_inv_bind_void … H) -H /2 width=1 by sfull_dec/ [ -IHY | -HY -IHL1 -HL12 ]
[ #HnV elim (reqx_dec L1 L2 V)
[ #HV @(IHL1 … HL10) -IHL1 -HL12 -HL10
/3 width=6 by rsx_lpxs_trans, lpxs_bind_refl_dx, reqg_canc_sn/ (**) (* full auto too slow *)
(* *)
(**************************************************************************)
-include "static_2/syntax/teqx.ma".
-include "basic_2/rt_transition/cnr_teqg.ma".
+include "basic_2/rt_transition/cnr_teqg.ma". (**) (* one dependence *)
(* NORMAL TERMS FOR CONTEXT-SENSITIVE R-TRANSITION **************************)
--- /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/rt_transition/fpb_fqup.ma".
+include "basic_2/rt_transition/cpm_cpx.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+
+(* Forward lemmas with rst-transition for closures **************************)
+
+(* Basic_2A1: includes: cpr_fpbq *)
+(* Basic_2A1: uses: cpm_fpbq *)
+lemma cpm_fwd_fpb (h) (n) (G) (L):
+ ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[h,n] T2 → ❪G,L,T1❫ ≽ ❪G,L,T2❫.
+/3 width=3 by cpx_fpb, cpm_fwd_cpx/ 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/rt_transition/fpbc_fqup.ma".
+include "basic_2/rt_transition/cpm_cpx.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+
+(* Forward lemmas with proper rst-transition for closures *******************)
+
+(* Basic_2A1: includes: cpr_fpb *)
+(* Basic_2A1: uses: cpm_fpb *)
+lemma cpm_fwd_fpbc (h) (n) (G) (L):
+ ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[h,n] T2 → (T1 ≅ T2 → ⊥) → ❪G,L,T1❫ ≻ ❪G,L,T2❫.
+/3 width=3 by cpx_fpbc, cpm_fwd_cpx/ qed-.
(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS **************)
-definition sort_eq_f: relation nat ≝ λs1,s2. ⊤.
-
definition cpx (G) (L): relation2 term term ≝
- λT1,T2. ∃c. ❪G,L❫ ⊢ T1 ⬈[sort_eq_f,rtc_eq_f,c] T2.
+ λT1,T2. ∃c. ❪G,L❫ ⊢ T1 ⬈[sfull,rtc_eq_f,c] T2.
interpretation
"extended context-sensitive parallel rt-transition (term)"
(* Properties with generic equivalence for closures *************************)
-(**) (* to update *)
-lemma feqg_cpx_trans (S):
+lemma feqg_cpx_trans_cpx (S):
reflexive … S → symmetric … S →
∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T❫ →
- ∀T2. ❪G2,L2❫ ⊢ T ⬈ T2 →
- ∃∃T0. ❪G1,L1❫ ⊢ T1 ⬈ T0 & ❪G1,L1,T0❫ ≛[S] ❪G2,L2,T2❫.
+ ∀T2. ❪G2,L2❫ ⊢ T ⬈ T2 → ❪G1,L1❫ ⊢ T1 ⬈ T2.
#S #H1S #H2S #G1 #G2 #L1 #L2 #T1 #T #H #T2 #HT2
elim (feqg_inv_gen_dx … H) -H // #H #HL12 #HT1 destruct
-lapply (reqg_cpx_trans … HL12 … HT2) // #H
+@(cpx_teqg_repl_reqg … HT2)
+/2 width=7 by reqg_sym, teqg_sym, teqg_refl/
+qed-.
+
+lemma feqg_cpx_trans_feqg (S):
+ reflexive … S → symmetric … S →
+ ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T❫ →
+ ∀T2. ❪G2,L2❫ ⊢ T ⬈ T2 → ❪G1,L1,T2❫ ≛[S] ❪G2,L2,T2❫.
+#S #H1S #H2S #G1 #G2 #L1 #L2 #T1 #T #H #T2 #HT2
+elim (feqg_inv_gen_dx … H) -H // #H #HL12 #_ destruct
lapply (cpx_reqg_conf_dx … HT2 … HL12) -HT2 -HL12 // #HL12
-lapply (teqg_cpx_trans … HT1 … H) -T // #HT12
-/4 width=4 by feqg_intro_sn, teqg_refl, ex2_intro/
+/3 width=1 by feqg_intro_sn, teqg_refl/
qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/predsubtyproper_6.ma".
-include "static_2/s_transition/fqu.ma".
-include "static_2/static/reqx.ma".
-include "basic_2/rt_transition/lpr_lpx.ma".
+include "basic_2/notation/relations/predsubty_6.ma".
+include "static_2/s_transition/fquq.ma".
+include "basic_2/rt_transition/rpx.ma".
-(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************)
+(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************)
-inductive fpb (G1) (L1) (T1): relation3 genv lenv term ≝
-| fpb_fqu: ∀G2,L2,T2. ❪G1,L1,T1❫ ⬂ ❪G2,L2,T2❫ → fpb G1 L1 T1 G2 L2 T2
-| fpb_cpx: ∀T2. ❪G1,L1❫ ⊢ T1 ⬈ T2 → (T1 ≅ T2 → ⊥) → fpb G1 L1 T1 G1 L1 T2
-| fpb_lpx: ∀L2. ❪G1,L1❫ ⊢ ⬈ L2 → (L1 ≅[T1] L2 → ⊥) → fpb G1 L1 T1 G1 L2 T1
-.
+(* Basic_2A1: uses: fpbq *)
+definition fpb (G1) (L1) (T1) (G2) (L2) (T2): Prop ≝
+ ∃∃L,T. ❪G1,L1,T1❫ ⬂⸮ ❪G2,L,T❫ & ❪G2,L❫ ⊢ T ⬈ T2 & ❪G2,L❫ ⊢ ⬈[T] L2.
interpretation
- "proper parallel rst-transition (closure)"
- 'PRedSubTyProper G1 L1 T1 G2 L2 T2 = (fpb G1 L1 T1 G2 L2 T2).
+ "parallel rst-transition (closure)"
+ 'PRedSubTy G1 L1 T1 G2 L2 T2 = (fpb G1 L1 T1 G2 L2 T2).
(* Basic properties *********************************************************)
-(* Basic_2A1: includes: cpr_fpb *)
-lemma cpm_fpb (h) (n) (G) (L):
- â\88\80T1,T2. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡[h,n] T2 â\86\92 (T1 â\89\85 T2 â\86\92 â\8a¥) â\86\92 â\9dªG,L,T1â\9d« â\89» â\9dªG,L,T2❫.
-/3 width=3 by fpb_cpx, cpm_fwd_cpx/ qed.
+lemma fpb_intro (G1) (L1) (T1) (G2) (L2) (T2):
+ ∀L,T. ❪G1,L1,T1❫ ⬂⸮ ❪G2,L,T❫ → ❪G2,L❫ ⊢ T ⬈ T2 →
+ â\9dªG2,Lâ\9d« â\8a¢ â¬\88[T] L2 â\86\92 â\9dªG1,L1,T1â\9d« â\89½ â\9dªG2,L2,T2❫.
+/2 width=5 by ex3_2_intro/ qed.
-lemma lpr_fpb (h) (G) (T):
- ∀L1,L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → (L1 ≅[T] L2 → ⊥) → ❪G,L1,T❫ ≻ ❪G,L2,T❫.
-/3 width=2 by fpb_lpx, lpr_fwd_lpx/ qed.
+lemma rpx_fpb (G) (T):
+ ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 → ❪G,L1,T❫ ≽ ❪G,L2,T❫.
+/2 width=5 by fpb_intro/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma fpb_inv_gen (G1) (L1) (T1) (G2) (L2) (T2):
+ ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ →
+ ∃∃L,T. ❪G1,L1,T1❫ ⬂⸮ ❪G2,L,T❫ & ❪G2,L❫ ⊢ T ⬈ T2 & ❪G2,L❫ ⊢ ⬈[T] L2.
+// qed-.
+
+(* Basic_2A1: removed theorems 2:
+ fpbq_fpbqa fpbqa_inv_fpbq
+*)
--- /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 "static_2/static/aaa_fqus.ma".
+include "static_2/static/aaa_reqg.ma".
+include "basic_2/rt_transition/lpx_aaa.ma".
+include "basic_2/rt_transition/fpb_lpx.ma".
+
+(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************)
+
+(* Properties with atomic arity assignment for terms ************************)
+
+(* Basic_2A1: uses: fpbq_aaa_conf *)
+lemma fpb_aaa_conf:
+ ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ →
+ ∀A1. ❪G1,L1❫ ⊢ T1 ⁝ A1 → ∃A2. ❪G2,L2❫ ⊢ T2 ⁝ A2.
+#G1 #G2 #L1 #L2 #T1 #T2 #H #A1 #HA1
+elim (fpb_inv_req … H) -H #L0 #L #T #H1 #HT2 #HL0 #HL02
+elim (aaa_fquq_conf … H1 … HA1) -G1 -L1 -T1 -A1 #A2 #HA2
+lapply (cpx_reqg_conf … HL0 … HT2) -HT2 // #HT2
+/4 width=6 by cpx_aaa_conf_lpx, aaa_reqg_conf, ex_intro/
+qed-.
(* *)
(**************************************************************************)
-include "static_2/s_transition/fqu_teqg.ma".
-include "static_2/static/feqg.ma".
-include "basic_2/rt_transition/fpb_reqg.ma".
+include "static_2/static/feqg_fqus.ma".
+include "static_2/static/feqg_feqg.ma".
+include "basic_2/rt_transition/cpx_feqg.ma".
+include "basic_2/rt_transition/lpx_reqg.ma".
+include "basic_2/rt_transition/fpb.ma".
-(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************)
+(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************)
-(* Properties with generic equivalence for closures *************************)
+(* Propreties with generic equivalence on referred closures *****************)
-(* Basic_2A1: uses: fleq_fpb_trans *)
-lemma feqg_fpb_trans (S):
- reflexive … S → symmetric … S → Transitive … S →
- ∀F1,F2,K1,K2,T1,T2. ❪F1,K1,T1❫ ≛[S] ❪F2,K2,T2❫ →
- ∀G2,L2,U2. ❪F2,K2,T2❫ ≻ ❪G2,L2,U2❫ →
- ∃∃G1,L1,U1. ❪F1,K1,T1❫ ≻ ❪G1,L1,U1❫ & ❪G1,L1,U1❫ ≛[S] ❪G2,L2,U2❫.
-#S #H1S #H2S #H3S #F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2
-#K2 #T2 #HK12 #HT12 #G2 #L2 #U2 #H12
-elim (teqg_fpb_trans … HT12 … H12) -T2 // #K0 #T0 #H #HT0 #HK0
-elim (reqg_fpb_trans … HK12 … H) -K2 // #L0 #U0 #H #HUT0 #HLK0
-@(ex2_3_intro … H) -H (**) (* full auto too slow *)
-/4 width=5 by feqg_intro_dx, reqg_trans, teqg_reqg_conf_sn, teqg_trans/
-qed-.
+(* Basic_2A1: includes: fleq_fpbq fpbq_lleq *)
+(* Basic_2A1: uses: fpbq_feqx *)
+lemma feqg_fpb (S) (G1) (G2) (L1) (L2) (T1) (T2):
+ reflexive … S → symmetric … S →
+ ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫.
+#S #G1 #G2 #L1 #L2 #T1 #T2 #HS1 #HS2 #H
+elim (feqg_inv_gen_sn … H) -H #H #HL12 #HT12 destruct
+/4 width=8 by reqg_rpx, teqg_cpx, fpb_intro/
+qed.
-(* Inversion lemmas with generic equivalence for closures *******************)
-
-(* Basic_2A1: uses: fpb_inv_fleq *)
-lemma fpb_inv_feqg (S):
- ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ →
- ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ⊥.
-#S #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-[ #G2 #L2 #T2 #H12 #H elim (feqg_inv_gen_sn … H) -H
- /3 width=11 by reqg_fwd_length, fqu_inv_teqg/
-| #T2 #_ #HnT #H elim (feqg_inv_gen_sn … H) -H /3 width=2 by teqg_teqx/
-| #L2 #_ #HnL #H elim (feqg_inv_gen_sn … H) -H /3 width=2 by reqg_reqx/
-]
+lemma feqg_fpb_trans (S) (G) (L) (T):
+ reflexive … S → symmetric … S → Transitive … S →
+ ∀G1,L1,T1. ❪G1,L1,T1❫ ≛[S] ❪G,L,T❫ →
+ ∀G2,L2,T2. ❪G,L,T❫ ≽ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫.
+#S #G #L #T #H1S #H2S #H3S #G1 #L1 #T1 #H1 #G2 #L2 #T2 #H2
+elim (fpb_inv_gen … H2) -H2 #L0 #T0 #H0 #HT02 #H
+elim (rpx_inv_reqg_lpx S … H) -H // #L3 #HL03 #HL32
+elim (feqg_fquq_trans … H1 … H0) -G -L -T // #G #L #T #H1 #H0
+lapply (feqg_cpx_trans_cpx … H0 … HT02) // -HT02 #HT2
+lapply (feqg_reqg_trans … H0 … HL03) -H0 -HL03 // #H
+elim (feqg_inv_gen_sn … H) -H #H #HL3 #_ destruct -T0
+/3 width=10 by fpb_intro, reqg_lpx_trans_rpx/
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/rt_transition/rpx_fqup.ma".
+include "basic_2/rt_transition/fpb.ma".
+
+(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: was: fpbq_refl *)
+lemma fpb_refl: tri_reflexive … fpb.
+/2 width=5 by fpb_intro/ qed.
+
+(* Basic_2A1: uses: fpbq_cpx *)
+lemma cpx_fpb (G) (L):
+ ∀T1,T2. ❪G,L❫ ⊢ T1 ⬈ T2 → ❪G,L,T1❫ ≽ ❪G,L,T2❫.
+/2 width=5 by fpb_intro/ qed.
+
+(* Basic_2A1: uses: fpbq_fquq *)
+lemma fquq_fpb (G1) (G2) (L1) (L2) (T1) (T2):
+ ❪G1,L1,T1❫ ⬂⸮ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫.
+/2 width=5 by fpb_intro/ qed.
+
+lemma fqu_fpb (G1) (G2) (L1) (L2) (T1) (T2):
+ ❪G1,L1,T1❫ ⬂ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫.
+/3 width=5 by fquq_fpb, fqu_fquq/ 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/rt_transition/rpx_lpx.ma".
+include "basic_2/rt_transition/fpb.ma".
+
+(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************)
+
+(* Properties with extended rt-transition for full local envs ***************)
+
+(* Basic_2A1: uses: fpbq_lpx *)
+lemma lpx_fpb (G) (T):
+ ∀L1,L2. ❪G,L1❫ ⊢ ⬈ L2 → ❪G,L1,T❫ ≽ ❪G,L2,T❫.
+/3 width=1 by rpx_fpb, lpx_rpx/ qed.
+
+lemma fpb_intro_req (G1) (G2) (L1) (L2) (T1) (T2):
+ ∀L0,L,T. ❪G1,L1,T1❫ ⬂⸮ ❪G2,L,T❫ → ❪G2,L❫ ⊢ T ⬈ T2 →
+ L ≡[T] L0 → ❪G2,L0❫ ⊢ ⬈ L2 → ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫.
+/4 width=10 by fpb_intro, lpx_rpx, reqg_rpx_trans/ qed.
+
+(* Inversion lemmas with extended rt-transition for full local envs *********)
+
+lemma fpb_inv_req (G1) (G2) (L1) (L2) (T1) (T2):
+ ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ →
+ ∃∃L0,L,T. ❪G1,L1,T1❫ ⬂⸮ ❪G2,L,T❫ & ❪G2,L❫ ⊢ T ⬈ T2 & L ≡[T] L0 & ❪G2,L0❫ ⊢ ⬈ L2.
+#G1 #G2 #L1 #L2 #T1 #T2 * #L #T #H1 #HT2 #HL2
+elim (rpx_inv_req_lpx … HL2) -HL2 #L0 #HL0 #HL02
+/2 width=7 by ex4_3_intro/
+qed-.
+
+(* Forward lemmas with extended rt-transition for full local envs ***********)
+
+lemma fpb_fwd_req (G1) (G2) (L1) (L2) (T1) (T2):
+ ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ →
+ ∃∃L0,L,T. ❪G1,L1,T1❫ ⬂⸮ ❪G2,L,T❫ & ❪G2,L❫ ⊢ T ⬈ T2 & ❪G2,L❫ ⊢ ⬈ L0 & L0 ≡[T] L2.
+#G1 #G2 #L1 #L2 #T1 #T2 * #L #T #H1 #HT2 #HL2
+elim (rpx_fwd_lpx_req … HL2) -HL2 #L0 #HL0 #HL02
+/2 width=7 by ex4_3_intro/
+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 "static_2/static/reqg_fqus.ma".
-include "basic_2/rt_transition/cpx_reqg.ma".
-include "basic_2/rt_transition/lpx_reqg.ma".
-include "basic_2/rt_transition/fpb.ma".
-
-(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************)
-
-(* Properties with generic equivalence for local environments ***************)
-
-lemma teqg_fpb_trans (S):
- reflexive … S → symmetric … S →
- ∀U2,U1. U2 ≛[S] U1 →
- ∀G1,G2,L1,L2,T1. ❪G1,L1,U1❫ ≻ ❪G2,L2,T1❫ →
- ∃∃L,T2. ❪G1,L1,U2❫ ≻ ❪G2,L,T2❫ & T2 ≛[S] T1 & L ≛[S,T1] L2.
-#S #H1S #H2S #U2 #U1 #HU21 #G1 #G2 #L1 #L2 #T1 * -G2 -L2 -T1
-[ #G2 #L2 #T1 #H
- elim (teqg_fqu_trans … H … HU21) -H
- /3 width=5 by fpb_fqu, ex3_2_intro/
-| #T1 #HUT1 #HnUT1
- lapply (teqg_cpx_trans … HU21 … HUT1) -HUT1
- /6 width=5 by fpb_cpx, reqg_refl, teqg_teqx, teqg_canc_sn, teqg_refl, ex3_2_intro/
-| /5 width=5 by fpb_lpx, teqg_reqg_conf_sn, reqg_refl, ex3_2_intro/
-]
-qed-.
-
-(* Basic_2A1: was just: lleq_fpb_trans *)
-lemma reqg_fpb_trans (S):
- reflexive … S → symmetric … S →
- ∀F,K1,K2,T. K1 ≛[S,T] K2 →
- ∀G,L2,U. ❪F,K2,T❫ ≻ ❪G,L2,U❫ →
- ∃∃L1,U0. ❪F,K1,T❫ ≻ ❪G,L1,U0❫ & U0 ≛[S] U & L1 ≛[S,U] L2.
-#S #H1S #H2S #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U
-[ #G #L2 #U #H2 elim (reqg_fqu_trans … H2 … HT) -K2
- /3 width=5 by fpb_fqu, ex3_2_intro/
-| #U #HTU #HnTU lapply (reqg_cpx_trans … HT … HTU) -HTU //
- /4 width=8 by fpb_cpx, cpx_reqg_conf_sn, teqg_refl, ex3_2_intro/
-| #L2 #HKL2 #HnKL2 elim (reqg_lpx_trans … HKL2 … HT) -HKL2 //
- /6 width=9 by fpb_lpx, reqg_reqx, reqg_repl, teqg_refl, ex3_2_intro/
-]
-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/notation/relations/predsubtyproper_6.ma".
+include "static_2/static/feqx.ma".
+include "basic_2/rt_transition/fpb.ma".
+
+(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************)
+
+(* Basic_2A1: uses: fpb *)
+definition fpbc (G1) (L1) (T1) (G2) (L2) (T2): Prop ≝
+ ∧∧ ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫
+ & (❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫ → ⊥).
+
+interpretation
+ "proper parallel rst-transition (closure)"
+ 'PRedSubTyProper G1 L1 T1 G2 L2 T2 = (fpbc G1 L1 T1 G2 L2 T2).
+
+(* Basic properties *********************************************************)
+
+(* Basic_2A1: fpbq_inv_fpb_alt *)
+lemma fpbc_intro (G1) (L1) (T1) (G2) (L2) (T2):
+ ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → (❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫ → ⊥) →
+ ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫.
+/3 width=1 by conj/ qed.
+
+lemma rpx_fpbc (G) (T):
+ ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 → (L1 ≅[T] L2 → ⊥) → ❪G,L1,T❫ ≻ ❪G,L2,T❫.
+/4 width=4 by fpbc_intro, rpx_fpb, feqg_fwd_reqg_sn/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+(* Basic_2A1: uses: fpb_fpbq_alt *)
+lemma fpbc_inv_gen (S):
+ ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ →
+ ∧∧ ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ & (❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ⊥).
+#S #G1 #G2 #L1 #L2 #T1 #T2 *
+/4 width=2 by feqg_feqx, conj/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+(* Basic_2A1: uses: fpb_fpbq *)
+lemma fpbc_fwd_fpb:
+ ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ →
+ ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫.
+#G1 #G2 #L1 #L2 #T1 #T2 * //
+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/rt_transition/fpb_feqg.ma".
+include "basic_2/rt_transition/fpbc.ma".
+
+(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************)
+
+(* Properties with generic equivalence for closures *************************)
+
+(* Basic_2A1: uses: teqg_fpb_trans lleq_fpb_trans fleq_fpb_trans *)
+lemma feqg_fpbc_trans (S) (G) (L) (T):
+ reflexive … S → symmetric … S → Transitive … S →
+ ∀G1,L1,T1. ❪G1,L1,T1❫ ≛[S] ❪G,L,T❫ →
+ ∀G2,L2,T2. ❪G,L,T❫ ≻ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫.
+#S #G #L #T #H1S #H2S #H3S #G1 #L1 #T1 #H1 #G2 #L2 #T2 #H2
+elim (fpbc_inv_gen sfull … H2) -H2 #H2 #Hn2
+/6 width=9 by fpbc_intro, feqg_fpb_trans, feqg_canc_sn, feqg_feqx/
+qed-.
+
+(* Inversion lemmas with generic equivalence for closures *******************)
+
+(* Basic_2A1: uses: fpb_inv_fleq *)
+lemma fpbc_inv_feqg (S):
+ ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ →
+ ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ⊥.
+#S #G1 #G2 #L1 #L2 #T1 #T2 #H #H12
+elim (fpbc_inv_gen S … H) -H #_ #Hn2
+/2 width=1 by/
+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 "static_2/static/feqx_feqx.ma".
+include "basic_2/rt_transition/fpbc.ma".
+
+(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************)
+
+(* Inversrion lemmas with parallel rst-transition for closures **************)
+
+(* Basic_2A1: uses: fpbq_ind_alt *)
+lemma fpb_inv_fpbc:
+ ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ →
+ ∨∨ ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫
+ | ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫.
+#G1 #G2 #L1 #L2 #T1 #T2 #H
+elim (feqx_dec G1 G2 L1 L2 T1 T2)
+/4 width=1 by fpbc_intro, or_intror, or_introl/
+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 "static_2/static/feqg_fqu.ma".
+include "basic_2/rt_transition/fpb_fqup.ma".
+include "basic_2/rt_transition/fpbc.ma".
+
+(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: uses: fpb_cpx *)
+lemma cpx_fpbc (G) (L):
+ ∀T1,T2. ❪G,L❫ ⊢ T1 ⬈ T2 → (T1 ≅ T2 → ⊥) → ❪G,L,T1❫ ≻ ❪G,L,T2❫.
+/4 width=5 by fpbc_intro, cpx_fpb, feqg_fwd_teqg/ qed.
+
+(* Basic_2A1: uses: fpb_fqu *)
+lemma fqu_fpbc (G1) (G2) (L1) (L2) (T1) (T2):
+ ❪G1,L1,T1❫ ⬂ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫.
+/4 width=10 by fpbc_intro, fquq_fpb, fqu_fquq, fqu_fneqg/ 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/rt_transition/lpx_reqg.ma".
+include "basic_2/rt_transition/fpbc.ma".
+
+(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************)
+
+(* Properties with extended rt-transition for full local envs ***************)
+
+(* Basic_2A1: uses: fpb_lpx *)
+lemma lpx_fpbc (G) (T):
+ ∀L1,L2. ❪G,L1❫ ⊢ ⬈ L2 → (L1 ≅[T] L2 → ⊥) → ❪G,L1,T❫ ≻ ❪G,L2,T❫.
+/3 width=1 by rpx_fpbc, lpx_rpx/ qed.
+
+(* Forward lemmas with extended rt-transition for full local envs ***********)
+
+lemma fpbc_fwd_lpx (G1) (G2) (L1) (L2) (T1) (T2):
+ ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ →
+ ∨∨ ∃∃G,L,T. ❪G1,L1,T1❫ ⬂ ❪G,L,T❫ & ❪G,L,T❫ ≽ ❪G2,L2,T2❫
+ | ∃∃T. ❪G1,L1❫ ⊢ T1 ⬈ T & T1 ≅ T → ⊥ & ❪G1,L1,T❫ ≽ ❪G2,L2,T2❫
+ | ∃∃L. ❪G1,L1❫ ⊢ ⬈ L & (L1 ≅[T1] L → ⊥) & ❪G1,L,T1❫ ≽ ❪G2,L2,T2❫.
+#G1 #G2 #L1 #L2 #T1 #T2 #H
+elim (fpbc_inv_gen sfull … H) -H #H12 #Hn12
+elim (fpb_inv_gen … H12) -H12 #L #T #H1 #HT2 #HL2
+elim H1 -H1 [ /4 width=9 by fpb_intro, ex2_3_intro, or3_intro0/ ]
+* #H1 #H2 #H3 destruct
+elim (teqg_dec sfull … T T2)
+[ -HT2 #HT2 |*: /5 width=11 by fpb_intro, cpx_rex_conf_sn, ex3_intro, or3_intro1, sfull_dec/ ]
+elim (rpx_fwd_lpx_reqg sfull … HL2) -HL2 // #L0 #HL0 #HL02
+elim (reqg_dec sfull … L L0 T)
+[ -HL0 #HL0 |*: /5 width=11 by fpb_intro, reqg_rpx, teqg_cpx, ex3_intro, or3_intro2, sfull_dec/ ]
+elim Hn12 -Hn12 /3 width=3 by feqg_intro_sn, reqg_trans/
+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/notation/relations/predsubty_6.ma".
-include "static_2/static/feqx.ma".
-include "static_2/s_transition/fquq.ma".
-include "basic_2/rt_transition/lpr_lpx.ma".
-
-(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************)
-
-(* Basic_2A1: includes: fleq_fpbq fpbq_lleq *)
-inductive fpbq (G1) (L1) (T1): relation3 genv lenv term ≝
-| fpbq_fquq: ∀G2,L2,T2. ❪G1,L1,T1❫ ⬂⸮ ❪G2,L2,T2❫ → fpbq G1 L1 T1 G2 L2 T2
-| fpbq_cpx : ∀T2. ❪G1,L1❫ ⊢ T1 ⬈ T2 → fpbq G1 L1 T1 G1 L1 T2
-| fpbq_lpx : ∀L2. ❪G1,L1❫ ⊢ ⬈ L2 → fpbq G1 L1 T1 G1 L2 T1
-| fpbq_feqx: ∀G2,L2,T2. ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫ → fpbq G1 L1 T1 G2 L2 T2
-.
-
-interpretation
- "parallel rst-transition (closure)"
- 'PRedSubTy G1 L1 T1 G2 L2 T2 = (fpbq G1 L1 T1 G2 L2 T2).
-
-(* Basic properties *********************************************************)
-
-lemma fpbq_refl: tri_reflexive … fpbq.
-/2 width=1 by fpbq_cpx/ qed.
-
-(* Basic_2A1: includes: cpr_fpbq *)
-lemma cpm_fpbq (h) (n) (G) (L):
- ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[h,n] T2 → ❪G,L,T1❫ ≽ ❪G,L,T2❫.
-/3 width=3 by fpbq_cpx, cpm_fwd_cpx/ qed.
-
-lemma lpr_fpbq (h) (G) (T):
- ∀L1,L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L1,T❫ ≽ ❪G,L2,T❫.
-/3 width=2 by fpbq_lpx, lpr_fwd_lpx/ qed.
-
-(* Basic_2A1: removed theorems 2:
- fpbq_fpbqa fpbqa_inv_fpbq
-*)
+++ /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 "static_2/static/aaa_fqus.ma".
-include "static_2/static/aaa_feqg.ma".
-include "basic_2/rt_transition/lpx_aaa.ma".
-include "basic_2/rt_transition/fpbq.ma".
-
-(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************)
-
-(* Properties with atomic arity assignment for terms ************************)
-
-lemma fpbq_aaa_conf:
- ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ →
- ∀A1. ❪G1,L1❫ ⊢ T1 ⁝ A1 → ∃A2. ❪G2,L2❫ ⊢ T2 ⁝ A2.
-#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-/3 width=8 by lpx_aaa_conf, cpx_aaa_conf, aaa_feqg_conf, aaa_fquq_conf, ex_intro/
-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 "static_2/static/feqg_fqup.ma".
-include "static_2/static/feqg_feqg.ma".
-include "basic_2/rt_transition/fpb_feqg.ma".
-include "basic_2/rt_transition/fpbq.ma".
-
-(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************)
-
-(* Properties with proper parallel rst-transition for closures **************)
-
-lemma fpb_fpbq:
- ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ →
- ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫.
-#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-/3 width=1 by fpbq_fquq, fpbq_cpx, fpbq_lpx, fqu_fquq/
-qed.
-
-(* Basic_2A1: fpb_fpbq_alt *)
-lemma fpb_fpbq_fneqx (S):
- ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ →
- ∧∧ ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ & (❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ⊥).
-/3 width=10 by fpb_fpbq, fpb_inv_feqg, conj/ qed-.
-
-(* Inversrion lemmas with proper parallel rst-transition for closures *******)
-
-(* Basic_2A1: fpbq_inv_fpb_alt *)
-lemma fpbq_fneqx_inv_fpb:
- ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ →
- (❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫ → ⊥) → ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫.
-#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-[ #G2 #L2 #T2 * [2: * #H1 #H2 #H3 destruct ]
- [ #H elim H -H /2 width=1 by feqg_refl/
- | /2 width=1 by fpb_fqu/
- ]
-| /4 width=1 by fpb_cpx, teqg_feqg/
-| /4 width=1 by fpb_lpx, feqg_intro_sn/
-| #G2 #L2 #T2 #H12 #Hn12
- elim Hn12 -Hn12 //
-]
-qed-.
-
-(* Basic_2A1: uses: fpbq_ind_alt *)
-lemma fpbq_inv_fpb:
- ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ →
- ∨∨ ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫
- | ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫.
-#G1 #G2 #L1 #L2 #T1 #T2 #H
-elim (feqg_dec sfull … G1 G2 L1 L2 T1 T2) //
-[ /2 width=1 by or_introl/
-| /4 width=1 by fpbq_fneqx_inv_fpb, or_intror/
-]
-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/rt_transition/fpb_lpx.ma".
+include "basic_2/rt_transition/lpr_lpx.ma".
+
+(* PARALLEL R-TRANSITION FOR FULL LOCAL ENVIRONMENTS ************************)
+
+(* Forward lemmas with rst-transition for closures **************************)
+
+(* Basic_2A1: uses: lpr_fpbq *)
+lemma lpr_fwd_fpb (h) (G) (T):
+ ∀L1,L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L1,T❫ ≽ ❪G,L2,T❫.
+/3 width=2 by lpx_fpb, lpr_fwd_lpx/ 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/rt_transition/fpbc_lpx.ma".
+include "basic_2/rt_transition/lpr_lpx.ma".
+
+(* PARALLEL R-TRANSITION FOR FULL LOCAL ENVIRONMENTS ************************)
+
+(* Forward lemmas with proper rst-transition for closures *******************)
+
+(* Basic_2A1: uses: lpr_fpb *)
+lemma lpr_fwd_fpbc (h) (G) (T):
+ ∀L1,L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → (L1 ≅[T] L2 → ⊥) → ❪G,L1,T❫ ≻ ❪G,L2,T❫.
+/3 width=2 by lpx_fpbc, lpr_fwd_lpx/ qed-.
(* *)
(**************************************************************************)
-include "static_2/static/req.ma".
-include "basic_2/rt_transition/rpx_lpx.ma".
+include "basic_2/rt_transition/rpx_lpx.ma". (**) (* one dependence *)
(* EXTENDED PARALLEL RT-TRANSITION FOR FULL LOCAL ENVIRONMENTS **************)
(* Properties with generic equivalence for local environments ***************)
lemma reqg_lpx_trans_rpx (S) (G) (L) (T:term):
- ∀L1. L1 ≛[S,T] L → ∀L2. ❪G,L❫ ⊢ ⬈ L2 → ❪G,L❫ ⊢ ⬈[T] L2.
-/3 width=1 by lpx_rpx, reqg_rpx_trans/ qed.
+ reflexive … S → symmetric … S →
+ ∀L1. L1 ≛[S,T] L → ∀L2. ❪G,L❫ ⊢ ⬈ L2 → ❪G,L1❫ ⊢ ⬈[T] L2.
+/3 width=6 by lpx_rpx, reqg_rpx_trans/ qed.
(* Basic_2A1: uses: lleq_lpx_trans *)
lemma reqg_lpx_trans (S) (G) (T:term):
/3 width=3 by req_fwd_reqg, ex2_intro/
qed-.
-(* Inversion lemmas with sort-irrelevant equivalence for local environments *)
+(* Inversion lemmas with generic equivalence for local environments *********)
lemma rpx_inv_reqg_lpx (S) (G) (T):
reflexive … S →
/3 width=3 by req_fwd_reqg, ex2_intro/
qed-.
-(* Forward lemmas with sort-irrelevant equivalence for local environments ***)
+(* Forward lemmas with generic equivalence for local environments ***********)
lemma rpx_fwd_lpx_reqg (S) (G) (T):
reflexive … S →
</body>
<table name="basic_2_sum"/>
+ <news class="gamma" date="2020-09-25.">
+ Improved rst-transition and related theory.
+ </news>
<news class="gamma" date="2020-04-16.">
Sort hierarchy parameter removed from unbound rt-transition
(anniversary milestone).
]
[ { "extended context-sensitive parallel rst-computation" * } {
[ [ "strongly normalizing for closures" ] "fsb" + "( ≥𝐒 ❪?,?,?❫ )" "fsb_feqg" + "fsb_aaa" + "fsb_csx" + "fsb_fpbg" * ]
- [ [ "proper for closures" ] "fpbg" + "( ❪?,?,?❫ > ❪?,?,?❫ )" "fpbg_fqup" + "fpbg_cpxs" + "fpbg_lpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ]
- [ [ "for closures" ] "fpbs" + "( ❪?,?,?❫ ≥ ❪?,?,?❫ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_aaa" + "fpbs_cpx" + "fpbs_fpb" + "fpbs_cpxs" + "fpbs_lpxs" + "fpbs_csx" + "fpbs_fpbs" * ]
+ [ [ "proper for closures" ] "fpbg" + "( ❪?,?,?❫ > ❪?,?,?❫ )" "fpbg_fqup" + "fpbg_fqus" + "fpbg_feqg" + "fpbg_cpm" + "fpbg_cpxs" + "fpbg_lpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ]
+ [ [ "for closures" ] "fpbs" + "( ❪?,?,?❫ ≥ ❪?,?,?❫ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_feqg" + "fpbs_aaa" + "fpbs_cpx" + "fpbs_fpbc" + "fpbs_cpxs" + "fpbs_lpxs" + "fpbs_csx" + "fpbs_fpbs" * ]
}
]
[ { "extended context-sensitive parallel rt-computation" * } {
[ [ "compatibility for lenvs" ] "jsx" + "( ? ⊢ ? ⊒ ? )" "jsx_drops" + "jsx_lsubr" + "jsx_csx" + "jsx_rsx" + "jsx_jsx" * ]
[ [ "strongly normalizing for lenvs on referred entries" ] "rsx" + "( ? ⊢ ⬈*𝐒[?] ? )" "rsx_length" + "rsx_drops" + "rsx_fqup" + "rsx_cpxs" + "rsx_csx" + "rsx_rsx" * ]
[ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ❪?,?❫ ⊢ ⬈*𝐒 ? )" "csx_cnx_vector" + "csx_csx_vector" * ]
- [ [ "strongly normalizing for terms" ] "csx" + "( ❪?,?❫ ⊢ ⬈*𝐒 ? )" "csx_simple" + "csx_simple_teqo" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_reqg" + "csx_feqg" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ]
+ [ [ "strongly normalizing for terms" ] "csx" + "( ❪?,?❫ ⊢ ⬈*𝐒 ? )" "csx_simple" + "csx_simple_teqo" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_reqg" + "csx_feqg" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpb" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ]
[ [ "for lenvs on all entries" ] "lpxs" + "( ❪?,?❫ ⊢ ⬈* ? )" "lpxs_length" + "lpxs_drops" + "lpxs_reqg" + "lpxs_feqg" + "lpxs_aaa" + "lpxs_lpx" + "lpxs_cpxs" + "lpxs_lpxs" * ]
[ [ "for binders" ] "cpxs_ext" + "( ❪?,?❫ ⊢ ? ⬈* ? )" * ]
[ [ "for terms" ] "cpxs" + "( ❪?,?❫ ⊢ ? ⬈* ? )" "cpxs_teqg" + "cpxs_teqo" + "cpxs_teqo_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_reqg" + "cpxs_feqg" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
]
[ { "context-sensitive parallel r-transition" * } {
[ [ "normal form for terms" ] "cnr ( ❪?,?❫ ⊢ ➡𝐍[?,?] ? )" "cnr_simple" + "cnr_teqg" + "cnr_teqx" + "cnr_drops" * ]
- [ [ "for lenvs on all entries" ] "lpr" + "( ❪?,?❫ ⊢ ➡[?,?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" + "lpr_lpr" * ]
+ [ [ "for lenvs on all entries" ] "lpr" + "( ❪?,?❫ ⊢ ➡[?,?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" + "lpr_fpb" + "lpr_fpbc" + "lpr_lpr" * ]
[ [ "for binders" ] "cpr_ext" * ]
[ [ "for terms" ] "cpr" "cpr_drops" + "cpr_drops_basic" + "cpr_teqg" + "cpr_cpr" * ]
}
]
[ { "t-bound context-sensitive parallel rt-transition" * } {
- [ [ "for terms" ] "cpm" + "( ❪?,?❫ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_teqx" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_aaa" + "cpm_cpx" * ]
+ [ [ "for terms" ] "cpm" + "( ❪?,?❫ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_teqx" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_aaa" + "cpm_cpx" + "cpm_fpb" + "cpm_fpbc" * ]
}
]
[ { "extended parallel rst-transition" * } {
- [ [ "for closures" ] "fpbq" + "( ❪?,?,?❫ ≽ ❪?,?,?❫ )" "fpbq_aaa" + "fpbq_fpb" * ]
- [ [ "proper for closures" ] "fpb" + "( ❪?,?,?❫ ≻ ❪?,?,?❫ )" "fpb_reqg" + "fpb_feqg" * ]
+ [ [ "proper for closures" ] "fpbc" + "( ❪?,?,?❫ ≻ ❪?,?,?❫ )" "fpbc_fqup" + "fpbc_feqg" + "fpbc_lpx" + "fpbc_fpb" * ]
+ [ [ "for closures" ] "fpb" + "( ❪?,?,?❫ ≽ ❪?,?,?❫ )" "fpb_fqup" + "fpb_feqg" + "fpb_aaa" + "fpb_lpx" * ]
}
]
[ { "extended context-sensitive parallel rt-transition" * } {
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* This file was generated by xoa.native: do not edit *********************)
+
+(* multiple existental quantifier (3, 6) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex6 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P2) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex6 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) }.
+
<key name="ex">3 3</key>
<key name="ex">3 4</key>
<key name="ex">3 5</key>
+ <key name="ex">3 6</key>
<key name="ex">4 1</key>
<key name="ex">4 2</key>
<key name="ex">4 3</key>
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* This file was generated by xoa.native: do not edit *********************)
+
+include "basics/pts.ma".
+
+include "ground/notation/xoa/ex_3_6.ma".
+
+(* multiple existental quantifier (3, 6) *)
+
+inductive ex3_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝
+ | ex3_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → ex3_6 ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (3, 6)" 'Ex6 P0 P1 P2 = (ex3_6 ? ? ? ? ? ? P0 P1 P2).
+
+++ /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 "static_2/static/reqx_reqx.ma".
-include "static_2/static/feqx.ma".
-
-(* SORT-IRRELEVANT EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *************)
-
-(* Advanced properties ******************************************************)
-
-lemma feqx_sym: tri_symmetric … feqx.
-#G1 #G2 #L1 #L2 #T1 #T2 * -G1 -L1 -T1
-/3 width=1 by feqx_intro_dx, reqx_sym, teqx_sym/
-qed-.
-
-(* Main properties **********************************************************)
-
-theorem feqx_trans: tri_transitive … feqx.
-#G1 #G #L1 #L #T1 #T * -G -L -T
-#L #T #HL1 #HT1 #G2 #L2 #T2 * -G2 -L2 -T2
-/4 width=5 by feqx_intro_sn, reqx_trans, teqx_reqx_div, teqx_trans/
-qed-.
-
-theorem feqx_canc_sn: ∀G,G1,L,L1,T,T1. ❪G,L,T❫ ≛ ❪G1,L1,T1❫→
- ∀G2,L2,T2. ❪G,L,T❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫.
-/3 width=5 by feqx_trans, feqx_sym/ qed-.
-
-theorem feqx_canc_dx: ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛ ❪G,L,T❫ →
- ∀G2,L2,T2. ❪G2,L2,T2❫ ≛ ❪G,L,T❫ → ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫.
-/3 width=5 by feqx_trans, feqx_sym/ qed-.
-
-(* Main inversion lemmas with degree-based equivalence on terms *************)
-
-theorem feqx_tneqx_repl_dx: ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ →
- ∀U1,U2. ❪G1,L1,U1❫ ≛ ❪G2,L2,U2❫ →
- (T2 ≛ U2 → ⊥) → (T1 ≛ U1 → ⊥).
-#G1 #G2 #L1 #L2 #T1 #T2 #HT #U1 #U2 #HU #HnTU2 #HTU1
-elim (feqx_inv_gen_sn … HT) -HT #_ #_ #HT
-elim (feqx_inv_gen_sn … HU) -HU #_ #_ #HU
-/3 width=5 by teqx_repl/
-qed-.
(* *)
(**************************************************************************)
-include "static_2/static/reqg.ma".
+include "static_2/static/reqg_fqup.ma".
include "static_2/static/aaa.ma".
(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
/3 width=1 by aaa_cast/
]
qed-.
+
+lemma aaa_teqg_conf (S) (G) (L) (A):
+ reflexive … S →
+ ∀T1. ❪G,L❫ ⊢ T1 ⁝ A → ∀T2. T1 ≛[S] T2 → ❪G,L❫ ⊢ T2 ⁝ A.
+/3 width=7 by aaa_teqg_conf_reqg, reqg_refl/ qed-.
+
+lemma aaa_reqg_conf (S) (G) (T) (A):
+ reflexive … S →
+ ∀L1. ❪G,L1❫ ⊢ T ⁝ A → ∀L2. L1 ≛[S,T] L2 → ❪G,L2❫ ⊢ T ⁝ A.
+/3 width=7 by aaa_teqg_conf_reqg, teqg_refl/ qed-.
/3 width=6 by teqg_reqg_conf_sn, and3_intro/
qed-.
+(* Basic forward lemmas *****************************************************)
+
+lemma feqg_fwd_teqg (S):
+ ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → T1 ≛[S] T2.
+#S #G1 #G2 #L1 #L2 #T1 #T2 #H
+elim (feqg_inv_gen_sn … H) -H //
+qed-.
+
+lemma feqg_fwd_reqg_sn (S):
+ ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → L1 ≛[S,T1] L2.
+#S #G1 #G2 #L1 #L2 #T1 #T2 #H
+elim (feqg_inv_gen_sn … H) -H //
+qed-.
+
+lemma feqg_fwd_reqg_dx (S):
+ reflexive … S →
+ ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → L1 ≛[S,T2] L2.
+#S #HS #G1 #G2 #L1 #L2 #T1 #T2 #H
+elim (feqg_inv_gen_dx … H) -H //
+qed-.
+
(* Basic_2A1: removed theorems 6:
fleq_refl fleq_sym fleq_inv_gen
fleq_trans fleq_canc_sn fleq_canc_dx
∀G2,L2,T2. ❪G2,L2,T2❫ ≛[S] ❪G,L,T❫ → ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫.
/3 width=5 by feqg_trans, feqg_sym/ qed-.
-(* Main inversion lemmas with generic equivalence on terms ******************)
+lemma feqg_reqg_trans (S) (G2) (L) (T2):
+ reflexive … S → symmetric … S → Transitive … S →
+ ∀G1,L1,T1. ❪G1,L1,T1❫ ≛[S] ❪G2,L,T2❫ →
+ ∀L2. L ≛[S,T2] L2 → ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫.
+#S #G2 #L #T2 #H1S #H2S #H3S #G1 #L1 #T1 #H1 #L2 #HL2
+/4 width=5 by feqg_trans, feqg_intro_sn, teqg_refl/
+qed-.
-theorem feqg_tneqg_repl_dx (S):
- reflexive … S → symmetric … S → Transitive … S →
- ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ →
- ∀U1,U2. ❪G1,L1,U1❫ ≛[S] ❪G2,L2,U2❫ →
- (T2 ≛[S] U2 → ⊥) → (T1 ≛[S] U1 → ⊥).
-#S #H1S #H2S #H3S #G1 #G2 #L1 #L2 #T1 #T2 #HT #U1 #U2 #HU #HnTU2 #HTU1
-elim (feqg_inv_gen_sn … HT) -HT #_ #_ #HT
-elim (feqg_inv_gen_sn … HU) -HU #_ #_ #HU
-/3 width=5 by teqg_repl/
+(* Inversion lemmas with generic equivalence on terms ***********************)
+
+(* Basic_2A1: uses: feqg_tneqg_repl_dx *)
+lemma feqg_tneqg_trans (S) (G1) (G2) (L1) (L2) (T):
+ reflexive … S → symmetric … S → Transitive … S →
+ ∀T1. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T❫ →
+ ∀T2. (T ≛[S] T2 → ⊥) → (T1 ≛[S] T2 → ⊥).
+#S #G1 #G2 #L1 #L2 #T #H1S #H2S #H3S #T1 #H1 #T2 #HnT2 #HT12
+elim (feqg_inv_gen_sn … H1) -H1 #_ #_ #HnT1 -G1 -G2 -L1 -L2
+/3 width=3 by teqg_canc_sn/
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 "static_2/static/feqg_length.ma".
+
+(* GENERIC EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *********************)
+
+(* Properties with structural successor for closures ************************)
+
+lemma fqu_fneqg (S) (b) (G1) (G2) (L1) (L2) (T1) (T2):
+ ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ⊥.
+#S #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+[ /3 width=8 by feqg_fwd_length, succ_inv_refl_sn/
+| /3 width=9 by teqg_inv_pair_xy_x, feqg_fwd_teqg/
+| /3 width=9 by teqg_inv_pair_xy_y, feqg_fwd_teqg/
+| /3 width=9 by teqg_inv_pair_xy_y, feqg_fwd_teqg/
+| /3 width=9 by teqg_inv_pair_xy_y, feqg_fwd_teqg/
+| /3 width=8 by feqg_fwd_length, succ_inv_refl_sn/
+]
+qed-.
(* Properties with star-iterated structural successor for closures **********)
+lemma feqg_fquq_trans (S) (b):
+ reflexive … S → symmetric … S → Transitive … S →
+ ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛[S] ❪G,L,T❫ →
+ ∀G2,L2,T2. ❪G,L,T❫ ⬂⸮[b] ❪G2,L2,T2❫ →
+ ∃∃G,L0,T0. ❪G1,L1,T1❫ ⬂⸮[b] ❪G,L0,T0❫ & ❪G,L0,T0❫ ≛[S] ❪G2,L2,T2❫.
+#S #b #H1S #H2S #H3S #G1 #G #L1 #L #T1 #T #H1 #G2 #L2 #T2 #H2
+elim(feqg_inv_gen_dx … H1) -H1 // #HG #HL1 #HT1 destruct
+elim (reqg_fquq_trans … H2 … HL1) -L // #L #T0 #H2 #HT02 #HL2
+elim (teqg_fquq_trans … H2 … HT1) -T // #L0 #T #H2 #HT0 #HL0
+lapply (teqg_reqg_conf_sn … HT02 … HL0) -HL0 // #HL0
+/4 width=7 by feqg_intro_dx, reqg_trans, teqg_trans, ex2_3_intro/
+qed-.
+
lemma feqg_fqus_trans (S) (b):
reflexive … S → symmetric … S → Transitive … S →
∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛[S] ❪G,L,T❫ →
--- /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 "static_2/static/reqg_length.ma".
+include "static_2/static/feqg.ma".
+
+(* GENERIC EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *********************)
+
+(* Forward lemmas with length for local environments ************************)
+
+lemma feqg_fwd_length (S) (G1) (G2) (L1) (L2) (T1) (T2):
+ ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → |L1| = |L2|.
+/3 width=6 by feqg_fwd_reqg_sn, reqg_fwd_length/ qed-.
(**************************************************************************)
include "static_2/notation/relations/approxeqsn_6.ma".
-include "static_2/syntax/teqx.ma".
+include "static_2/static/reqx.ma".
include "static_2/static/feqg.ma".
(* SORT-IRRELEVANT EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *************)
-
+(*
definition feqx: relation6 genv lenv term genv lenv term ≝
feqg sfull.
-
+*)
interpretation
"sort-irrelevant equivalence on referred entries (closure)"
- 'ApproxEqSn G1 L1 T1 G2 L2 T2 = (feqx G1 L1 T1 G2 L2 T2).
+ 'ApproxEqSn G1 L1 T1 G2 L2 T2 = (feqg sfull G1 L1 T1 G2 L2 T2).
(* Basic_properties *********************************************************)
-(*
-lemma feqx_intro_dx (G):
- ∀L1,L2,T2. L1 ≛[T2] L2 →
- ∀T1. T1 ≛ T2 → ❪G,L1,T1❫ ≛ ❪G,L2,T2❫.
-/3 width=3 by feqx_intro_sn, teqx_reqx_div/ qed.
-(* Basic inversion lemmas ***************************************************)
-
-lemma feqx_inv_gen_sn:
- ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ →
- ∧∧ G1 = G2 & L1 ≛[T1] L2 & T1 ≛ T2.
-#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and3_intro/
-qed-.
-
-lemma feqx_inv_gen_dx:
- ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ →
- ∧∧ G1 = G2 & L1 ≛[T2] L2 & T1 ≛ T2.
-#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-/3 width=3 by teqx_reqx_conf_sn, and3_intro/
-qed-.
-*)
-(* Basic_2A1: removed theorems 6:
- fleq_refl fleq_sym fleq_inv_gen
- fleq_trans fleq_canc_sn fleq_canc_dx
-*)
+lemma feqg_feqx (S) (G1) (G2) (L1) (L2) (T1) (T2):
+ ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫.
+#S #G1 #G2 #L1 #L2 #T1 #T2 #H
+elim (feqg_inv_gen_sn … H) -H
+/3 width=2 by feqg_intro_sn, reqg_reqx, teqg_teqx/
+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 "static_2/static/feqg_feqg.ma".
+include "static_2/static/feqx.ma".
+
+(* SORT-IRRELEVANT EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *************)
+
+(* Advanced properties ******************************************************)
+
+lemma feqx_dec (G1) (G2) (L1) (L2) (T1) (T2):
+ Decidable (❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫).
+/3 width=1 by feqg_dec, sfull_dec/ qed-.
+(*
+lemma feqx_sym: tri_symmetric … feqx.
+#G1 #G2 #L1 #L2 #T1 #T2 * -G1 -L1 -T1
+/3 width=1 by feqx_intro_dx, reqx_sym, teqx_sym/
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem feqx_trans: tri_transitive … feqx.
+#G1 #G #L1 #L #T1 #T * -G -L -T
+#L #T #HL1 #HT1 #G2 #L2 #T2 * -G2 -L2 -T2
+/4 width=5 by feqx_intro_sn, reqx_trans, teqx_reqx_div, teqx_trans/
+qed-.
+
+theorem feqx_canc_sn: ∀G,G1,L,L1,T,T1. ❪G,L,T❫ ≛ ❪G1,L1,T1❫→
+ ∀G2,L2,T2. ❪G,L,T❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫.
+/3 width=5 by feqx_trans, feqx_sym/ qed-.
+
+theorem feqx_canc_dx: ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛ ❪G,L,T❫ →
+ ∀G2,L2,T2. ❪G2,L2,T2❫ ≛ ❪G,L,T❫ → ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫.
+/3 width=5 by feqx_trans, feqx_sym/ qed-.
+
+(* Main inversion lemmas with degree-based equivalence on terms *************)
+
+theorem feqx_tneqx_repl_dx: ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ →
+ ∀U1,U2. ❪G1,L1,U1❫ ≛ ❪G2,L2,U2❫ →
+ (T2 ≛ U2 → ⊥) → (T1 ≛ U1 → ⊥).
+#G1 #G2 #L1 #L2 #T1 #T2 #HT #U1 #U2 #HU #HnTU2 #HTU1
+elim (feqx_inv_gen_sn … HT) -HT #_ #_ #HT
+elim (feqx_inv_gen_sn … HU) -HU #_ #_ #HU
+/3 width=5 by teqx_repl/
+qed-.
+*)
include "static_2/syntax/ext2_ext2.ma".
include "static_2/syntax/teqg_teqg.ma".
-include "static_2/static/rex_rex.ma".
include "static_2/static/reqg_length.ma".
(* GENERIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***********)
*)
(* Basic_2A1: uses: lleq_dec *)
lemma reqx_dec: ∀L1,L2. ∀T:term. Decidable (L1 ≅[T] L2).
-/2 width=1 by reqg_dec/ qed-.
+/3 width=1 by reqg_dec, sfull_dec/ qed-.
(*
(* Main properties **********************************************************)
(* ITEMS ********************************************************************)
+definition sfull: relation2 nat nat ≝
+ λs1,s2. ⊤.
+
(* atomic items *)
inductive item0: Type[0] ≝
- | Sort: nat → item0 (* sort: starting at 0 *)
- | LRef: nat → item0 (* reference by index: starting at 0 *)
- | GRef: nat → item0 (* reference by position: starting at 0 *)
+| Sort: nat → item0 (* sort: starting at 0 *)
+| LRef: nat → item0 (* reference by index: starting at 0 *)
+| GRef: nat → item0 (* reference by position: starting at 0 *)
.
(* unary binding items *)
inductive bind1: Type[0] ≝
- | Void: bind1 (* exclusion *)
+| Void: bind1 (* exclusion *)
.
(* binary binding items *)
inductive bind2: Type[0] ≝
- | Abbr: bind2 (* abbreviation *)
- | Abst: bind2 (* abstraction *)
+| Abbr: bind2 (* abbreviation *)
+| Abst: bind2 (* abstraction *)
.
(* binary non-binding items *)
inductive flat2: Type[0] ≝
- | Appl: flat2 (* application *)
- | Cast: flat2 (* explicit type annotation *)
+| Appl: flat2 (* application *)
+| Cast: flat2 (* explicit type annotation *)
.
(* binary items *)
inductive item2: Type[0] ≝
- | Bind2: bool → bind2 → item2 (* polarized binding item *)
- | Flat2: flat2 → item2 (* non-binding item *)
+| Bind2: bool → bind2 → item2 (* polarized binding item *)
+| Flat2: flat2 → item2 (* non-binding item *)
.
(* Basic inversion lemmas ***************************************************)
(* Basic properties *********************************************************)
-lemma eq_item0_dec: ∀I1,I2:item0. Decidable (I1 = I2).
+lemma sfull_dec:
+ ∀s1,s2. Decidable (sfull s1 s2).
+/2 width=1 by or_introl/ qed-.
+
+lemma eq_item0_dec:
+ ∀I1,I2:item0. Decidable (I1 = I2).
* #i1 * #i2 [2,3,4,6,7,8: @or_intror #H destruct ]
[2: elim (eq_nat_dec i1 i2) |1,3: elim (eq_nat_dec i1 i2) ] /2 width=1 by or_introl/
#Hni12 @or_intror #H destruct /2 width=1 by/
qed-.
-lemma eq_bind1_dec: ∀I1,I2:bind1. Decidable (I1 = I2).
+lemma eq_bind1_dec:
+ ∀I1,I2:bind1. Decidable (I1 = I2).
* * /2 width=1 by or_introl/
qed-.
(* Basic_1: was: bind_dec *)
-lemma eq_bind2_dec: ∀I1,I2:bind2. Decidable (I1 = I2).
+lemma eq_bind2_dec:
+ ∀I1,I2:bind2. Decidable (I1 = I2).
* * /2 width=1 by or_introl/
@or_intror #H destruct
qed-.
(* Basic_1: was: flat_dec *)
-lemma eq_flat2_dec: ∀I1,I2:flat2. Decidable (I1 = I2).
+lemma eq_flat2_dec:
+ ∀I1,I2:flat2. Decidable (I1 = I2).
* * /2 width=1 by or_introl/
@or_intror #H destruct
qed-.
(* Basic_1: was: kind_dec *)
-lemma eq_item2_dec: ∀I1,I2:item2. Decidable (I1 = I2).
+lemma eq_item2_dec:
+ ∀I1,I2:item2. Decidable (I1 = I2).
* [ #p1 ] #I1 * [1,3: #p2 ] #I2
[2,3: @or_intror #H destruct
| elim (eq_bool_dec p1 p2) #Hp
(* SORT-IRRELEVANT EQUIVALENCE ON TERMS *************************************)
-definition sfull: relation2 nat nat ≝
- λs1,s2. ⊤.
-
definition teqx: relation term ≝
teqg sfull.
(* Basic properties *********************************************************)
-lemma sfull_dec:
- ∀s1,s2. Decidable (sfull s1 s2).
-/2 width=1 by or_introl/ qed.
-
lemma teqx_pair:
∀V1,V2. V1 ≅ V2 → ∀T1,T2. T1 ≅ T2 →
∀I. ②[I]V1.T1 ≅ ②[I]V2.T2.
(**************************************************************************)
(*
-include "static_2/notation/relations/stareq_3.ma".
+include "static_2/notation/relations/approxeq_3.ma".
*)
include "static_2/syntax/teqg_ext.ma".
include "static_2/syntax/teqx.ma".
(* terms *)
inductive term: Type[0] ≝
- | TAtom: item0 → term (* atomic item construction *)
- | TPair: item2 → term → term → term (* binary item construction *)
+| TAtom: item0 → term (* atomic item construction *)
+| TPair: item2 → term → term → term (* binary item construction *)
.
-interpretation "term construction (atomic)"
- 'Item0 I = (TAtom I).
+interpretation
+ "term construction (atomic)"
+ 'Item0 I = (TAtom I).
-interpretation "term construction (binary)"
- 'SnItem2 I T1 T2 = (TPair I T1 T2).
+interpretation
+ "term construction (binary)"
+ 'SnItem2 I T1 T2 = (TPair I T1 T2).
-interpretation "term binding construction (binary)"
- 'SnBind2 p I T1 T2 = (TPair (Bind2 p I) T1 T2).
+interpretation
+ "term binding construction (binary)"
+ 'SnBind2 p I T1 T2 = (TPair (Bind2 p I) T1 T2).
-interpretation "term positive binding construction (binary)"
- 'SnBind2Pos I T1 T2 = (TPair (Bind2 true I) T1 T2).
+interpretation
+ "term positive binding construction (binary)"
+ 'SnBind2Pos I T1 T2 = (TPair (Bind2 true I) T1 T2).
-interpretation "term negative binding construction (binary)"
- 'SnBind2Neg I T1 T2 = (TPair (Bind2 false I) T1 T2).
+interpretation
+ "term negative binding construction (binary)"
+ 'SnBind2Neg I T1 T2 = (TPair (Bind2 false I) T1 T2).
-interpretation "term flat construction (binary)"
- 'SnFlat2 I T1 T2 = (TPair (Flat2 I) T1 T2).
+interpretation
+ "term flat construction (binary)"
+ 'SnFlat2 I T1 T2 = (TPair (Flat2 I) T1 T2).
-interpretation "sort (term)"
- 'Star s = (TAtom (Sort s)).
+interpretation
+ "sort (term)"
+ 'Star s = (TAtom (Sort s)).
-interpretation "local reference (term)"
- 'LRef i = (TAtom (LRef i)).
+interpretation
+ "local reference (term)"
+ 'LRef i = (TAtom (LRef i)).
-interpretation "global reference (term)"
- 'GRef l = (TAtom (GRef l)).
+interpretation
+ "global reference (term)"
+ 'GRef l = (TAtom (GRef l)).
-interpretation "abbreviation (term)"
- 'SnAbbr p T1 T2 = (TPair (Bind2 p Abbr) T1 T2).
+interpretation
+ "abbreviation (term)"
+ 'SnAbbr p T1 T2 = (TPair (Bind2 p Abbr) T1 T2).
-interpretation "positive abbreviation (term)"
- 'SnAbbrPos T1 T2 = (TPair (Bind2 true Abbr) T1 T2).
+interpretation
+ "positive abbreviation (term)"
+ 'SnAbbrPos T1 T2 = (TPair (Bind2 true Abbr) T1 T2).
-interpretation "negative abbreviation (term)"
- 'SnAbbrNeg T1 T2 = (TPair (Bind2 false Abbr) T1 T2).
+interpretation
+ "negative abbreviation (term)"
+ 'SnAbbrNeg T1 T2 = (TPair (Bind2 false Abbr) T1 T2).
-interpretation "abstraction (term)"
- 'SnAbst p T1 T2 = (TPair (Bind2 p Abst) T1 T2).
+interpretation
+ "abstraction (term)"
+ 'SnAbst p T1 T2 = (TPair (Bind2 p Abst) T1 T2).
-interpretation "positive abstraction (term)"
- 'SnAbstPos T1 T2 = (TPair (Bind2 true Abst) T1 T2).
+interpretation
+ "positive abstraction (term)"
+ 'SnAbstPos T1 T2 = (TPair (Bind2 true Abst) T1 T2).
-interpretation "negative abstraction (term)"
- 'SnAbstNeg T1 T2 = (TPair (Bind2 false Abst) T1 T2).
+interpretation
+ "negative abstraction (term)"
+ 'SnAbstNeg T1 T2 = (TPair (Bind2 false Abst) T1 T2).
-interpretation "application (term)"
- 'SnAppl T1 T2 = (TPair (Flat2 Appl) T1 T2).
+interpretation
+ "application (term)"
+ 'SnAppl T1 T2 = (TPair (Flat2 Appl) T1 T2).
-interpretation "native type annotation (term)"
- 'SnCast T1 T2 = (TPair (Flat2 Cast) T1 T2).
+interpretation
+ "native type annotation (term)"
+ 'SnCast T1 T2 = (TPair (Flat2 Cast) T1 T2).
(* Basic properties *********************************************************)
-lemma abst_dec (X): ∨∨ ∃∃p,W,T. X = ⓛ[p]W.T
- | (∀p,W,T. X = ⓛ[p]W.T → ⊥).
+lemma abst_dec (X):
+ ∨∨ ∃∃p,W,T. X = ⓛ[p]W.T
+ | (∀p,W,T. X = ⓛ[p]W.T → ⊥).
* [ #I | * [ #p * | #I ] #V #T ]
[3: /3 width=4 by ex1_3_intro, or_introl/ ]
@or_intror #q #W #U #H destruct
qed-.
(* Basic_1: was: term_dec *)
-lemma eq_term_dec: ∀T1,T2:term. Decidable (T1 = T2).
+lemma eq_term_dec:
+ ∀T1,T2:term. Decidable (T1 = T2).
#T1 elim T1 -T1 #I1 [| #V1 #T1 #IHV1 #IHT1 ] * #I2 [2,4: #V2 #T2 ]
[1,4: @or_intror #H destruct
| elim (eq_item2_dec I1 I2) #HI
(* Basic inversion lemmas ***************************************************)
-fact destruct_tatom_tatom_aux: ∀I1,I2. ⓪[I1] = ⓪[I2] → I1 = I2.
+fact destruct_tatom_tatom_aux:
+ ∀I1,I2. ⓪[I1] = ⓪[I2] → I1 = I2.
#I1 #I2 #H destruct //
qed-.
-fact destruct_tpair_tpair_aux: ∀I1,I2,T1,T2,V1,V2. ②[I1]T1.V1 = ②[I2]T2.V2 →
- ∧∧T1 = T2 & I1 = I2 & V1 = V2.
+fact destruct_tpair_tpair_aux:
+ ∀I1,I2,T1,T2,V1,V2. ②[I1]T1.V1 = ②[I2]T2.V2 →
+ ∧∧ T1 = T2 & I1 = I2 & V1 = V2.
#I1 #I2 #T1 #T2 #V1 #V2 #H destruct /2 width=1 by and3_intro/
qed-.
-lemma discr_tpair_xy_x: ∀I,T,V. ②[I]V.T = V → ⊥.
+lemma discr_tpair_xy_x:
+ ∀I,T,V. ②[I]V.T = V → ⊥.
#I #T #V elim V -V
[ #J #H destruct
| #J #W #U #IHW #_ #H elim (destruct_tpair_tpair_aux … H) -H /2 width=1 by/ (**) (* destruct lemma needed *)
qed-.
(* Basic_1: was: thead_x_y_y *)
-lemma discr_tpair_xy_y: ∀I,V,T. ②[I]V.T = T → ⊥.
+lemma discr_tpair_xy_y:
+ ∀I,V,T. ②[I]V.T = T → ⊥.
#I #V #T elim T -T
[ #J #H destruct
| #J #W #U #_ #IHU #H elim (destruct_tpair_tpair_aux … H) -H /2 width=1 by/ (**) (* destruct lemma needed *)
]
qed-.
-lemma eq_false_inv_tpair_sn: ∀I,V1,T1,V2,T2.
- (②[I]V1.T1 = ②[I]V2.T2 → ⊥) →
- (V1 = V2 → ⊥) ∨ (V1 = V2 ∧ (T1 = T2 → ⊥)).
+lemma eq_false_inv_tpair_sn:
+ ∀I,V1,T1,V2,T2.
+ (②[I]V1.T1 = ②[I]V2.T2 → ⊥) →
+ (V1 = V2 → ⊥) ∨ (V1 = V2 ∧ (T1 = T2 → ⊥)).
#I #V1 #T1 #V2 #T2 #H
elim (eq_term_dec V1 V2) /3 width=1 by or_introl/ #HV12 destruct
@or_intror @conj // #HT12 destruct /2 width=1 by/
qed-.
-lemma eq_false_inv_tpair_dx: ∀I,V1,T1,V2,T2.
- (②[I] V1. T1 = ②[I]V2.T2 → ⊥) →
- (T1 = T2 → ⊥) ∨ (T1 = T2 ∧ (V1 = V2 → ⊥)).
+lemma eq_false_inv_tpair_dx:
+ ∀I,V1,T1,V2,T2.
+ (②[I] V1. T1 = ②[I]V2.T2 → ⊥) →
+ (T1 = T2 → ⊥) ∨ (T1 = T2 ∧ (V1 = V2 → ⊥)).
#I #V1 #T1 #V2 #T2 #H
elim (eq_term_dec T1 T2) /3 width=1 by or_introl/ #HT12 destruct
@or_intror @conj // #HT12 destruct /2 width=1 by/
}
]
[ { "sort-irrelevant equivalence" * } {
- [ [ "for closures on referred entries" ] "feqx" + "( ❪?,?,?❫ ≅ ❪?,?,?❫ )" * ]
+ [ [ "for closures on referred entries" ] "feqx" + "( ❪?,?,?❫ ≅ ❪?,?,?❫ )" "feqx_feqx" * ]
[ [ "for lenvs on referred entries" ] "reqx" + "( ? ≅[?] ? )" "reqx_reqx" * ]
}
]
}
]
[ { "generic equivalence" * } {
- [ [ "for closures on referred entries" ] "feqg" + "( ❪?,?,?❫ ≛[?] ❪?,?,?❫ )" "feqg_fqup" + "feqg_fqus" + "feqg_feqg" * ]
+ [ [ "for closures on referred entries" ] "feqg" + "( ❪?,?,?❫ ≛[?] ❪?,?,?❫ )" "feqg_length" + "feqg_fqu" + "feqg_fqup" + "feqg_fqus" + "feqg_feqg" * ]
[ [ "for lenvs on referred entries" ] "reqg" + "( ? ≛[?,?] ? )" "reqg_length" + "reqg_drops" + "reqg_fqup" + "reqg_fqus" + "reqg_reqg" * ]
}
]
projects / helm.git / commitdiff