---

Step * 1 of Lemma l-ordered-reorder


1. [A] : Type
2. R : A ⟶ A ⟶ 𝔹
3. u : A
4. v : A List
5. Trans(A;x,y.↑R[x;y])
6. (∀x∈[u / v].(∀y∈[u / v].(¬↑R[x;y]) ⇒ (↑R[y;x])))
7. L' : A List
8. l-ordered(A;x,y.↑R[x;y];L')
9. permutation(A;v;L')
10. L' = (filter(λy.R[y;u];L') @ filter(λy.(¬bR[y;u]);L')) ∈ (A List)
⊢ l-ordered(A;x,y.↑R[x;y];filter(λy.R[y;u];L') @ [u / filter(λy.(¬bR[y;u]);L')])
BY
{ (Repeat ((RW ListC 0 THEN Auto)) THEN Try ((BLemma `l-ordered-filter` THEN Auto))) }

1
1. A : Type
2. R : A ⟶ A ⟶ 𝔹
3. u : A
4. v : A List
5. Trans(A;x,y.↑R[x;y])
6. (∀x∈[u / v].(∀y∈[u / v].(¬↑R[x;y]) ⇒ (↑R[y;x])))
7. L' : A List
8. l-ordered(A;x,y.↑R[x;y];L')
9. permutation(A;v;L')
10. L' = (filter(λy.R[y;u];L') @ filter(λy.(¬bR[y;u]);L')) ∈ (A List)
11. l-ordered(A;x,y.↑R[x;y];filter(λy.R[y;u];L'))
12. l-ordered(A;x,y.↑R[x;y];filter(λy.(¬bR[y;u]);L'))
13. y : A
14. (y ∈ filter(λy.(¬bR[y;u]);L'))
⊢ ↑R[u;y]

2
1. A : Type
2. R : A ⟶ A ⟶ 𝔹
3. u : A
4. v : A List
5. Trans(A;x,y.↑R[x;y])
6. (∀x∈[u / v].(∀y∈[u / v].(¬↑R[x;y]) ⇒ (↑R[y;x])))
7. L' : A List
8. l-ordered(A;x,y.↑R[x;y];L')
9. permutation(A;v;L')
10. L' = (filter(λy.R[y;u];L') @ filter(λy.(¬bR[y;u]);L')) ∈ (A List)
11. l-ordered(A;x,y.↑R[x;y];filter(λy.R[y;u];L'))
12. l-ordered(A;x,y.↑R[x;y];[u / filter(λy.(¬bR[y;u]);L')])
13. x : A
14. y : A
15. (x ∈ filter(λy.R[y;u];L'))
16. (y ∈ [u / filter(λy.(¬bR[y;u]);L')])
⊢ ↑R[x;y]

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  R  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}
3.  u  :  A
4.  v  :  A  List
5.  Trans(A;x,y.\muparrow{}R[x;y])
6.  (\mforall{}x\mmember{}[u  /  v].(\mforall{}y\mmember{}[u  /  v].(\mneg{}\muparrow{}R[x;y])  {}\mRightarrow{}  (\muparrow{}R[y;x])))
7.  L'  :  A  List
8.  l-ordered(A;x,y.\muparrow{}R[x;y];L')
9.  permutation(A;v;L')
10.  L'  =  (filter(\mlambda{}y.R[y;u];L')  @  filter(\mlambda{}y.(\mneg{}\msubb{}R[y;u]);L'))
\mvdash{}  l-ordered(A;x,y.\muparrow{}R[x;y];filter(\mlambda{}y.R[y;u];L')  @  [u  /  filter(\mlambda{}y.(\mneg{}\msubb{}R[y;u]);L')])


By

---

Latex:
(Repeat  ((RW  ListC  0  THEN  Auto))  THEN  Try  ((BLemma  `l-ordered-filter`  THEN  Auto)))

---

Home Index