---

Step * 1 2 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)
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]
BY
{ ((RW ListC (-1) THENA Auto)
   THEN D (-1)
   THEN (RW ListC (-2) THENA Auto)
   THEN RepD
   THEN Reduce (-2)
   THEN Auto
   THEN (RW ListC (-1) THENA Auto)
   THEN Reduce (-1)
   THEN RepD
   THEN (RW assert_pushdownC (-1) THENA Auto)
   THEN All(\i.xxxRepeat ((RWO "l_all_iff" i THENA Auto))xxx)⋅
   THEN FHyp 6 [-1]
   THEN Auto
   THEN (RW ListC 0 THENA Auto)
   THEN (OrRight THENA Auto)
   THEN (FLemma `member-permutation` [-10] THENA Auto)
   THEN RWO "-1" 0
   THEN Auto) }

---

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'))
11.  l-ordered(A;x,y.\muparrow{}R[x;y];filter(\mlambda{}y.R[y;u];L'))
12.  l-ordered(A;x,y.\muparrow{}R[x;y];[u  /  filter(\mlambda{}y.(\mneg{}\msubb{}R[y;u]);L')])
13.  x  :  A
14.  y  :  A
15.  (x  \mmember{}  filter(\mlambda{}y.R[y;u];L'))
16.  (y  \mmember{}  [u  /  filter(\mlambda{}y.(\mneg{}\msubb{}R[y;u]);L')])
\mvdash{}  \muparrow{}R[x;y]


By

---

Latex:
((RW  ListC  (-1)  THENA  Auto)
  THEN  D  (-1)
  THEN  (RW  ListC  (-2)  THENA  Auto)
  THEN  RepD
  THEN  Reduce  (-2)
  THEN  Auto
  THEN  (RW  ListC  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  RepD
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  All(\mbackslash{}i.xxxRepeat  ((RWO  "l\_all\_iff"  i  THENA  Auto))xxx)\mcdot{}
  THEN  FHyp  6  [-1]
  THEN  Auto
  THEN  (RW  ListC  0  THENA  Auto)
  THEN  (OrRight  THENA  Auto)
  THEN  (FLemma  `member-permutation`  [-10]  THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index