---

Step * 2 of Lemma l-ordered-decomp2


1. T : Type
2. R : T ⟶ T ⟶ 𝔹
3. x : T
4. StAntiSym(T;x,y.↑R[x;y])
5. Irrefl(T;x,y.↑R[x;y])
6. Trans(T;x,y.↑R[x;y])
7. u : T
8. ¬↑R[x;u]
9. v : T List
10. (v = (filter(λy.R[y;x];v) @ [x / filter(λy.R[x;y];v)]) ∈ (T List)) supposing 
       (l-ordered(T;x,y.↑R[x;y];v) and 
       (x ∈ v))
11. ↑R[u;x]
12. (x ∈ v)
13. l-ordered(T;x,y.↑R[x;y];v)
14. ∀y:T. ((y ∈ v) ⇒ (↑R[u;y]))
⊢ [u / v] = [u / (filter(λy.R[y;x];v) @ [x / filter(λy.R[x;y];v)])] ∈ (T List)
BY
{ (EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
3.  x  :  T
4.  StAntiSym(T;x,y.\muparrow{}R[x;y])
5.  Irrefl(T;x,y.\muparrow{}R[x;y])
6.  Trans(T;x,y.\muparrow{}R[x;y])
7.  u  :  T
8.  \mneg{}\muparrow{}R[x;u]
9.  v  :  T  List
10.  (v  =  (filter(\mlambda{}y.R[y;x];v)  @  [x  /  filter(\mlambda{}y.R[x;y];v)]))  supposing 
              (l-ordered(T;x,y.\muparrow{}R[x;y];v)  and 
              (x  \mmember{}  v))
11.  \muparrow{}R[u;x]
12.  (x  \mmember{}  v)
13.  l-ordered(T;x,y.\muparrow{}R[x;y];v)
14.  \mforall{}y:T.  ((y  \mmember{}  v)  {}\mRightarrow{}  (\muparrow{}R[u;y]))
\mvdash{}  [u  /  v]  =  [u  /  (filter(\mlambda{}y.R[y;x];v)  @  [x  /  filter(\mlambda{}y.R[x;y];v)])]


By

---

Latex:
(EqCD  THEN  Auto)

---

Home Index