---

Step * 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') @ [u / filter(λy.(¬bR[y;u]);L')])
⊢ permutation(A;[u / v];filter(λy.R[y;u];L') @ [u / filter(λy.(¬bR[y;u]);L')])
BY
{ ((BLemma `permutation-cons` THENA Auto)
   THEN InstConcl [⌜filter(λy.R[y;u];L')⌝;⌜filter(λy.(¬bR[y;u]);L')⌝]⋅
   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')  @  [u  /  filter(\mlambda{}y.(\mneg{}\msubb{}R[y;u]);L')])
\mvdash{}  permutation(A;[u  /  v];filter(\mlambda{}y.R[y;u];L')  @  [u  /  filter(\mlambda{}y.(\mneg{}\msubb{}R[y;u]);L')])


By

---

Latex:
((BLemma  `permutation-cons`  THENA  Auto)
  THEN  InstConcl  [\mkleeneopen{}filter(\mlambda{}y.R[y;u];L')\mkleeneclose{};\mkleeneopen{}filter(\mlambda{}y.(\mneg{}\msubb{}R[y;u]);L')\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index