fact cnv_cpm_conf_lpr_atom_delta_aux (h) (a) (G) (L) (i):
(∀G0,L0,T0. ⦃G,L,#i⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
⦃G,L⦄⊢#i![h,a] →
- â\88\80K,V. â¬\87*[i]L ≘ K.ⓓV →
+ â\88\80K,V. â\87©*[i]L ≘ K.ⓓV →
∀n,XV. ⦃G,K⦄ ⊢ V ➡[n,h] XV →
- â\88\80X. â¬\86*[↑i]XV ≘ X →
+ â\88\80X. â\87§*[↑i]XV ≘ X →
∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
∃∃T. ⦃G,L1⦄ ⊢ #i ➡*[n,h] T & ⦃G,L2⦄ ⊢ X ➡*[h] T.
#h #a #G #L #i #IH #HT #K #V #HLK #n #XV #HVX #X #HXV #L1 #HL1 #L2 #HL2
fact cnv_cpm_conf_lpr_atom_ell_aux (h) (a) (G) (L) (i):
(∀G0,L0,T0. ⦃G,L,#i⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
⦃G,L⦄⊢#i![h,a] →
- â\88\80K,W. â¬\87*[i]L ≘ K.ⓛW →
+ â\88\80K,W. â\87©*[i]L ≘ K.ⓛW →
∀n,XW. ⦃G,K⦄ ⊢ W ➡[n,h] XW →
- â\88\80X. â¬\86*[↑i]XW ≘ X →
+ â\88\80X. â\87§*[↑i]XW ≘ X →
∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
∃∃T. ⦃G,L1⦄ ⊢ #i ➡*[↑n,h] T & ⦃G,L2⦄ ⊢ X ➡*[h] T.
#h #a #G #L #i #IH #HT #K #W #HLK #n #XW #HWX #X #HXW #L1 #HL1 #L2 #HL2
fact cnv_cpm_conf_lpr_delta_delta_aux (h) (a) (I) (G) (L) (i):
(∀G0,L0,T0. ⦃G,L,#i⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
⦃G,L⦄⊢#i![h,a] →
- â\88\80K1,V1. â¬\87*[i]L â\89\98 K1.â\93\91{I}V1 â\86\92 â\88\80K2,V2. â¬\87*[i]L ≘ K2.ⓑ{I}V2 →
+ â\88\80K1,V1. â\87©*[i]L â\89\98 K1.â\93\91{I}V1 â\86\92 â\88\80K2,V2. â\87©*[i]L ≘ K2.ⓑ{I}V2 →
∀n1,XV1. ⦃G,K1⦄ ⊢ V1 ➡[n1,h] XV1 → ∀n2,XV2. ⦃G,K2⦄ ⊢ V2 ➡[n2,h] XV2 →
- â\88\80X1. â¬\86*[â\86\91i]XV1 â\89\98 X1 â\86\92 â\88\80X2. â¬\86*[↑i]XV2 ≘ X2 →
+ â\88\80X1. â\87§*[â\86\91i]XV1 â\89\98 X1 â\86\92 â\88\80X2. â\87§*[↑i]XV2 ≘ X2 →
∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
∃∃T. ⦃G,L1⦄ ⊢ X1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ X2 ➡*[n1-n2,h] T.
#h #a #I #G #L #i #IH #HT
qed-.
fact cnv_cpm_conf_lpr_delta_ell_aux (L) (K1) (K2) (V) (W) (i):
- â¬\87*[i]L â\89\98 K1.â\93\93V â\86\92 â¬\87*[i]L ≘ K2.ⓛW → ⊥.
+ â\87©*[i]L â\89\98 K1.â\93\93V â\86\92 â\87©*[i]L ≘ K2.ⓛW → ⊥.
#L #K1 #K2 #V #W #i #HLK1 #HLK2
lapply (drops_mono … HLK2 … HLK1) -L -i #H destruct
qed-.
(∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
⦃G,L⦄ ⊢ +ⓓV.T ![h,a] →
∀V1. ⦃G,L⦄ ⊢V ➡[h] V1 → ∀n1,T1. ⦃G,L.ⓓV⦄ ⊢ T ➡[n1,h] T1 →
- â\88\80T2. â¬\86*[1]T2 ≘ T → ∀n2,XT2. ⦃G,L⦄ ⊢ T2 ➡[n2,h] XT2 →
+ â\88\80T2. â\87§*[1]T2 ≘ T → ∀n2,XT2. ⦃G,L⦄ ⊢ T2 ➡[n2,h] XT2 →
∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
∃∃T. ⦃G,L1⦄ ⊢ +ⓓV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ XT2 ➡*[n1-n2,h] T.
#h #a #G0 #L0 #V0 #T0 #IH #H0
fact cnv_cpm_conf_lpr_zeta_zeta_aux (h) (a) (G) (L) (V) (T):
(∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
⦃G,L⦄ ⊢ +ⓓV.T ![h,a] →
- â\88\80T1. â¬\86*[1]T1 â\89\98 T â\86\92 â\88\80T2. â¬\86*[1]T2 ≘ T →
+ â\88\80T1. â\87§*[1]T1 â\89\98 T â\86\92 â\88\80T2. â\87§*[1]T2 ≘ T →
∀n1,XT1. ⦃G,L⦄ ⊢ T1 ➡[n1,h] XT1 → ∀n2,XT2. ⦃G,L⦄ ⊢ T2 ➡[n2,h] XT2 →
∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
∃∃T. ⦃G,L1⦄ ⊢ XT1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ XT2 ➡*[n1-n2,h] T.
∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 →
∀n1,T1. ⦃G,L⦄ ⊢ ⓓ{p}W.T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓓW⦄ ⊢ T ➡[n2,h] T2 →
- â\88\80U2. â¬\86*[1]V2 ≘ U2 →
+ â\88\80U2. â\87§*[1]V2 ≘ U2 →
∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
∃∃T. ⦃G,L1⦄ ⊢ ⓐV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡*[n1-n2,h] T.
#h #a #p #G0 #L0 #V0 #W0 #T0 #IH #H0
∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
∀W1. ⦃G,L⦄ ⊢ W ➡[h] W1 → ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 →
∀n1,T1. ⦃G,L.ⓓW⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓓW⦄ ⊢ T ➡[n2,h] T2 →
- â\88\80U1. â¬\86*[1]V1 â\89\98 U1 â\86\92 â\88\80U2. â¬\86*[1]V2 ≘ U2 →
+ â\88\80U1. â\87§*[1]V1 â\89\98 U1 â\86\92 â\88\80U2. â\87§*[1]V2 ≘ U2 →
∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
∃∃T. ⦃G,L1⦄ ⊢ ⓓ{p}W1.ⓐU1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡*[n1-n2,h] T.
#h #a #p #G0 #L0 #V0 #W0 #T0 #IH #H0