qed-.
fact sex_dropable_dx_aux (RN) (RP):
- â\88\80b,f,L2,K2. â\87©*[b,f] L2 â\89\98 K2 â\86\92 ð\9d\90\94â\9dªfâ\9d« →
+ â\88\80b,f,L2,K2. â\87©*[b,f] L2 â\89\98 K2 â\86\92 ð\9d\90\94â\9d¨fâ\9d© →
∀f2,L1. L1 ⪤[RN,RP,f2] L2 → ∀f1. f ~⊚ f1 ≘ f2 →
∃∃K1. ⇩*[b,f] L1 ≘ K1 & K1 ⪤[RN,RP,f1] K2.
#RN #RP #b #f #L2 #K2 #H elim H -f -L2 -K2
lemma sex_drops_conf_next (RN) (RP):
∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
- â\88\80b,f,I1,K1. â\87©*[b,f] L1 â\89\98 K1.â\93\98[I1] â\86\92 ð\9d\90\94â\9dªfâ\9d« →
+ â\88\80b,f,I1,K1. â\87©*[b,f] L1 â\89\98 K1.â\93\98[I1] â\86\92 ð\9d\90\94â\9d¨fâ\9d© →
∀f1. f ~⊚ ↑f1 ≘ f2 →
∃∃I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] & K1 ⪤[RN,RP,f1] K2 & RN K1 I1 I2.
#RN #RP #f2 #L1 #L2 #HL12 #b #f #I1 #K1 #HLK1 #Hf #f1 #Hf2
lemma sex_drops_conf_push (RN) (RP):
∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
- â\88\80b,f,I1,K1. â\87©*[b,f] L1 â\89\98 K1.â\93\98[I1] â\86\92 ð\9d\90\94â\9dªfâ\9d« →
+ â\88\80b,f,I1,K1. â\87©*[b,f] L1 â\89\98 K1.â\93\98[I1] â\86\92 ð\9d\90\94â\9d¨fâ\9d© →
∀f1. f ~⊚ ⫯f1 ≘ f2 →
∃∃I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] & K1 ⪤[RN,RP,f1] K2 & RP K1 I1 I2.
#RN #RP #f2 #L1 #L2 #HL12 #b #f #I1 #K1 #HLK1 #Hf #f1 #Hf2
lemma sex_drops_trans_next (RN) (RP):
∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
- â\88\80b,f,I2,K2. â\87©*[b,f] L2 â\89\98 K2.â\93\98[I2] â\86\92 ð\9d\90\94â\9dªfâ\9d« →
+ â\88\80b,f,I2,K2. â\87©*[b,f] L2 â\89\98 K2.â\93\98[I2] â\86\92 ð\9d\90\94â\9d¨fâ\9d© →
∀f1. f ~⊚ ↑f1 ≘ f2 →
∃∃I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] & K1 ⪤[RN,RP,f1] K2 & RN K1 I1 I2.
#RN #RP #f2 #L1 #L2 #HL12 #b #f #I2 #K2 #HLK2 #Hf #f1 #Hf2
qed-.
lemma sex_drops_trans_push (RN) (RP): ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
- â\88\80b,f,I2,K2. â\87©*[b,f] L2 â\89\98 K2.â\93\98[I2] â\86\92 ð\9d\90\94â\9dªfâ\9d« →
+ â\88\80b,f,I2,K2. â\87©*[b,f] L2 â\89\98 K2.â\93\98[I2] â\86\92 ð\9d\90\94â\9d¨fâ\9d© →
∀f1. f ~⊚ ⫯f1 ≘ f2 →
∃∃I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] & K1 ⪤[RN,RP,f1] K2 & RP K1 I1 I2.
#RN #RP #f2 #L1 #L2 #HL12 #b #f #I2 #K2 #HLK2 #Hf #f1 #Hf2
qed-.
lemma drops_atom2_sex_conf (RN) (RP):
- â\88\80b,f1,L1. â\87©*[b,f1] L1 â\89\98 â\8b\86 â\86\92 ð\9d\90\94â\9dªf1â\9d« →
+ â\88\80b,f1,L1. â\87©*[b,f1] L1 â\89\98 â\8b\86 â\86\92 ð\9d\90\94â\9d¨f1â\9d© →
∀f,L2. L1 ⪤[RN,RP,f] L2 →
∀f2. f1 ~⊚ f2 ≘f → ⇩*[b,f1] L2 ≘ ⋆.
#RN #RP #b #f1 #L1 #H1 #Hf1 #f #L2 #H2 #f2 #H3