-fact cnv_cpms_conf_lpr_step_tdneq_sub (a) (h) (G0) (L0) (T0) (m11) (m12) (m21) (m22):
- (â\88\80G,L,T. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G,L,Tâ¦\84 â\86\92 IH_cnv_cpm_trans_lpr a h G L T) →
- (â\88\80G,L,T. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G,L,Tâ¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G L T) →
- â¦\83G0,L0â¦\84 â\8a¢ T0 ![a,h] →
- â\88\80X1. â¦\83G0,L0â¦\84 â\8a¢ T0 â\9e¡[m11,h] X1 â\86\92 T0 â\89\9b X1 â\86\92 â\88\80T1. â¦\83G0,L0â¦\84 â\8a¢ X1 â\9e¡*[m12,h] T1 â\86\92 X1 â\89\9b T1 →
- â\88\80X2. â¦\83G0,L0â¦\84 â\8a¢ T0 â\9e¡[m21,h] X2 â\86\92 (T0 â\89\9b X2 â\86\92 â\8a¥) â\86\92 â\88\80T2. â¦\83G0,L0â¦\84 â\8a¢ X2 â\9e¡*[m22,h] T2 →
- â\88\80L1. â¦\83G0,L0â¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G0,L0â¦\84 â\8a¢ â\9e¡[h] L2 →
- ((â\88\80G,L,T. â¦\83G0,L0,X1â¦\84 >[h] â¦\83G,L,Tâ¦\84 â\86\92 IH_cnv_cpm_trans_lpr a h G L T) →
- (∀G,L,T. ⦃G0,L0,X1⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) →
- ∀m21,m22.
- ∀X2. ⦃G0,L0⦄ ⊢ X1 ➡[m21,h] X2 → (X1 ≛ X2 → ⊥) →
- ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 →
- ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-m12,h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[m12-(m21+m22),h]T
+fact cnv_cpms_conf_lpr_step_tneqx_sub (h) (a) (G0) (L0) (T0) (m11) (m12) (m21) (m22):
+ (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« > â\9dªG,L,Tâ\9d« â\86\92 IH_cnv_cpm_trans_lpr h a G L T) →
+ (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« > â\9dªG,L,Tâ\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G L T) →
+ â\9dªG0,L0â\9d« â\8a¢ T0 ![h,a] →
+ â\88\80X1. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[h,m11] X1 â\86\92 T0 â\89\85 X1 â\86\92 â\88\80T1. â\9dªG0,L0â\9d« â\8a¢ X1 â\9e¡*[h,m12] T1 â\86\92 X1 â\89\85 T1 →
+ â\88\80X2. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[h,m21] X2 â\86\92 (T0 â\89\85 X2 â\86\92 â\8a¥) â\86\92 â\88\80T2. â\9dªG0,L0â\9d« â\8a¢ X2 â\9e¡*[h,m22] T2 →
+ â\88\80L1. â\9dªG0,L0â\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG0,L0â\9d« â\8a¢ â\9e¡[h,0] L2 →
+ ((â\88\80G,L,T. â\9dªG0,L0,X1â\9d« > â\9dªG,L,Tâ\9d« â\86\92 IH_cnv_cpm_trans_lpr h a G L T) →
+ (∀G,L,T. ❪G0,L0,X1❫ > ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) →
+ ∀m21,m22.
+ ∀X2. ❪G0,L0❫ ⊢ X1 ➡[h,m21] X2 → (X1 ≅ X2 → ⊥) →
+ ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 →
+ ∀L1. ❪G0,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h,0] L2 →
+ ∃∃T. ❪G0,L1❫ ⊢ T1 ➡*[h,m21+m22-m12] T & ❪G0,L2❫ ⊢ T2 ➡*[h,m12-(m21+m22)]T