-definition f_dedropable_sn: predicate (relation3 lenv term term) ≝
- λR. ∀b,f,L1,K1. ⬇*[b,f] L1 ≘ K1 →
- ∀K2,T. K1 ⪤[R,T] K2 → ∀U. ⬆*[f] T ≘ U →
- ∃∃L2. L1 ⪤[R,U] L2 & ⬇*[b,f] L2 ≘ K2 & L1 ≡[f] L2.
-
-definition f_dropable_sn: predicate (relation3 lenv term term) ≝
- λR. ∀b,f,L1,K1. ⬇*[b,f] L1 ≘ K1 → 𝐔⦃f⦄ →
- ∀L2,U. L1 ⪤[R,U] L2 → ∀T. ⬆*[f] T ≘ U →
- ∃∃K2. K1 ⪤[R,T] K2 & ⬇*[b,f] L2 ≘ K2.
-
-definition f_dropable_dx: predicate (relation3 lenv term term) ≝
- λR. ∀L1,L2,U. L1 ⪤[R,U] L2 →
- ∀b,f,K2. ⬇*[b,f] L2 ≘ K2 → 𝐔⦃f⦄ → ∀T. ⬆*[f] T ≘ U →
- ∃∃K1. ⬇*[b,f] L1 ≘ K1 & K1 ⪤[R,T] K2.
-
-definition f_transitive_next: relation3 … ≝ λR1,R2,R3.
- ∀f,L,T. L ⊢ 𝐅+⦃T⦄ ≘ f →
- ∀g,I,K,n. ⬇*[n] L ≘ K.ⓘ{I} → ↑g = ⫱*[n] f →
- sex_transitive (cext2 R1) (cext2 R2) (cext2 R3) (cext2 R1) cfull g K I.
+definition f_dedropable_sn:
+ predicate (relation3 lenv term term) ≝ λR.
+ ∀b,f,L1,K1. ⇩*[b,f] L1 ≘ K1 →
+ ∀K2,T. K1 ⪤[R,T] K2 → ∀U. ⇧*[f] T ≘ U →
+ ∃∃L2. L1 ⪤[R,U] L2 & ⇩*[b,f] L2 ≘ K2 & L1 ≡[f] L2.
+
+definition f_dropable_sn:
+ predicate (relation3 lenv term term) ≝ λR.
+ ∀b,f,L1,K1. ⇩*[b,f] L1 ≘ K1 → 𝐔❨f❩ →
+ ∀L2,U. L1 ⪤[R,U] L2 → ∀T. ⇧*[f] T ≘ U →
+ ∃∃K2. K1 ⪤[R,T] K2 & ⇩*[b,f] L2 ≘ K2.
+
+definition f_dropable_dx:
+ predicate (relation3 lenv term term) ≝ λR.
+ ∀L1,L2,U. L1 ⪤[R,U] L2 →
+ ∀b,f,K2. ⇩*[b,f] L2 ≘ K2 → 𝐔❨f❩ → ∀T. ⇧*[f] T ≘ U →
+ ∃∃K1. ⇩*[b,f] L1 ≘ K1 & K1 ⪤[R,T] K2.
+
+definition f_transitive_next:
+ relation3 … ≝ λR1,R2,R3.
+ ∀f,L,T. L ⊢ 𝐅+❨T❩ ≘ f →
+ ∀g,I,K,i. ⇩[i] L ≘ K.ⓘ[I] → ↑g = ⫰*[i] f →
+ R_pw_transitive_sex (cext2 R1) (cext2 R2) (cext2 R3) (cext2 R1) cfull g K I.
+
+definition f_confluent1_next: relation2 … ≝ λR1,R2.
+ ∀f,L,T. L ⊢ 𝐅+❨T❩ ≘ f →
+ ∀g,I,K,i. ⇩[i] L ≘ K.ⓘ[I] → ↑g = ⫰*[i] f →
+ R_pw_confluent1_sex (cext2 R1) (cext2 R1) (cext2 R2) cfull g K I.