---

Step * 1 of Lemma sublist-if-no_repeats


1. [A] : Type
2. R : A ⟶ A ⟶ 𝔹
3. u : A
4. v : A List
5. ∀bs:A List
     (StAntiSym(A;x,y.↑R[x;y])
     ⇒ Irrefl(A;x,y.↑R[x;y])
     ⇒ Trans(A;x,y.↑R[x;y])
     ⇒ no_repeats(A;v)
     ⇒ l-ordered(A;x,y.↑R[x;y];v)
     ⇒ l-ordered(A;x,y.↑R[x;y];bs)
     ⇒ (∀a∈v.(a ∈ bs))
     ⇒ v ⊆ bs)
6. bs : A List
7. StAntiSym(A;x,y.↑R[x;y])
8. Irrefl(A;x,y.↑R[x;y])
9. Trans(A;x,y.↑R[x;y])
10. no_repeats(A;v)
11. ¬(u ∈ v)
12. l-ordered(A;x,y.↑R[x;y];v)
13. ∀y:A. ((y ∈ v) ⇒ (↑R[u;y]))
14. l-ordered(A;x,y.↑R[x;y];bs)
15. (u ∈ bs)
16. (∀a∈v.(a ∈ bs))
17. bs = (filter(λy.R[y;u];bs) @ [u / filter(λy.R[u;y];bs)]) ∈ (A List)
18. u = u ∈ A
⊢ l-ordered(A;x,y.↑R[x;y];filter(λy.R[u;y];bs))
BY
{ ((HypSubst (-2) (-5) THENA Auto) THEN (RW ListC (-5) THEN Auto) THEN RW ListC (-6) THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  R  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}
3.  u  :  A
4.  v  :  A  List
5.  \mforall{}bs:A  List
          (StAntiSym(A;x,y.\muparrow{}R[x;y])
          {}\mRightarrow{}  Irrefl(A;x,y.\muparrow{}R[x;y])
          {}\mRightarrow{}  Trans(A;x,y.\muparrow{}R[x;y])
          {}\mRightarrow{}  no\_repeats(A;v)
          {}\mRightarrow{}  l-ordered(A;x,y.\muparrow{}R[x;y];v)
          {}\mRightarrow{}  l-ordered(A;x,y.\muparrow{}R[x;y];bs)
          {}\mRightarrow{}  (\mforall{}a\mmember{}v.(a  \mmember{}  bs))
          {}\mRightarrow{}  v  \msubseteq{}  bs)
6.  bs  :  A  List
7.  StAntiSym(A;x,y.\muparrow{}R[x;y])
8.  Irrefl(A;x,y.\muparrow{}R[x;y])
9.  Trans(A;x,y.\muparrow{}R[x;y])
10.  no\_repeats(A;v)
11.  \mneg{}(u  \mmember{}  v)
12.  l-ordered(A;x,y.\muparrow{}R[x;y];v)
13.  \mforall{}y:A.  ((y  \mmember{}  v)  {}\mRightarrow{}  (\muparrow{}R[u;y]))
14.  l-ordered(A;x,y.\muparrow{}R[x;y];bs)
15.  (u  \mmember{}  bs)
16.  (\mforall{}a\mmember{}v.(a  \mmember{}  bs))
17.  bs  =  (filter(\mlambda{}y.R[y;u];bs)  @  [u  /  filter(\mlambda{}y.R[u;y];bs)])
18.  u  =  u
\mvdash{}  l-ordered(A;x,y.\muparrow{}R[x;y];filter(\mlambda{}y.R[u;y];bs))


By

---

Latex:
((HypSubst  (-2)  (-5)  THENA  Auto)  THEN  (RW  ListC  (-5)  THEN  Auto)  THEN  RW  ListC  (-6)  THEN  Auto)

---

Home Index