---

Step * of Lemma sublist-if-no_repeats

∀[A:Type]
  ∀R:A ⟶ A ⟶ 𝔹. ∀as,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;as)
    ⇒ l-ordered(A;x,y.↑R[x;y];as)
    ⇒ l-ordered(A;x,y.↑R[x;y];bs)
    ⇒ (∀a∈as.(a ∈ bs))
    ⇒ as ⊆ bs)
BY
{ (InductionOnList
   THEN RW ListC 0
   THEN Auto
   THEN (InstLemma `l-ordered-decomp2` [⌜A⌝;⌜R⌝;⌜u⌝;⌜bs⌝]⋅ THENA Auto)
   THEN (HypSubst (-1) 0 THENA Auto)
   THEN InstLemma `sublist_append` [⌜A⌝;⌜[]⌝;⌜[u / v]⌝;⌜filter(λy.R[y;u];bs)⌝;⌜[u / filter(λy.R[u;y];bs)]⌝]⋅
   THEN AllReduce
   THEN Auto
   THEN (BLemma `cons_sublist_cons` THENA Auto)
   THEN (OrLeft THEN Auto)
   THEN BackThruSomeHyp
   THEN Auto) }

1
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))

2
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
⊢ (∀a∈v.(a ∈ filter(λy.R[u;y];bs)))

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}as,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;as)
        {}\mRightarrow{}  l-ordered(A;x,y.\muparrow{}R[x;y];as)
        {}\mRightarrow{}  l-ordered(A;x,y.\muparrow{}R[x;y];bs)
        {}\mRightarrow{}  (\mforall{}a\mmember{}as.(a  \mmember{}  bs))
        {}\mRightarrow{}  as  \msubseteq{}  bs)


By

---

Latex:
(InductionOnList
  THEN  RW  ListC  0
  THEN  Auto
  THEN  (InstLemma  `l-ordered-decomp2`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (HypSubst  (-1)  0  THENA  Auto)
  THEN  InstLemma  `sublist\_append`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}[u  /  v]\mkleeneclose{};\mkleeneopen{}filter(\mlambda{}y.R[y;u];bs)\mkleeneclose{};\mkleeneopen{}[u  / 
                                                                                                                                                            filter(\mlambda{}y.R[u;y];bs)]\mkleeneclose{}
  ]\mcdot{}
  THEN  AllReduce
  THEN  Auto
  THEN  (BLemma  `cons\_sublist\_cons`  THENA  Auto)
  THEN  (OrLeft  THEN  Auto)
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index