---

Step * of Lemma fset-to-list

∀[T:Type]
  ∀eq:EqDecider(T)
    ∀[R:T ⟶ T ⟶ ℙ]
      ((∀a,b:T.  Dec(R a b)) ⇒ Linorder(T;a,b.R a b) ⇒ (∀s:fset(T). ∃L:T List. ∀x:T. (x ∈ s ⇐⇒ (x ∈ L))))
BY
{ (Auto
   THEN (InstLemma `sorted-by-exists2` [⌜T⌝;⌜R⌝]⋅
         THENA (Auto THEN (InstLemma `deq_property` [⌜T⌝;⌜eq⌝]⋅ THENA Auto) THEN RWO  "-1" 0 THEN Auto)
         )
   THEN Skolemize (-1) `sort'
   THEN Auto) }

1
1. [T] : Type
2. eq : EqDecider(T)
3. [R] : T ⟶ T ⟶ ℙ
4. ∀a,b:T.  Dec(R a b)
5. Linorder(T;a,b.R a b)
6. s : fset(T)
7. ∀L:T List. ∃L':T List. (sorted-by(R;L') ∧ no_repeats(T;L') ∧ L ⊆ L' ∧ L' ⊆ L)
8. sort : L:(T List) ⟶ (T List)
9. ∀L:T List. (sorted-by(R;sort L) ∧ no_repeats(T;sort L) ∧ L ⊆ sort L ∧ sort L ⊆ L)
⊢ ∃L:T List. ∀x:T. (x ∈ s ⇐⇒ (x ∈ L))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T)
        \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}]
            ((\mforall{}a,b:T.    Dec(R  a  b))
            {}\mRightarrow{}  Linorder(T;a,b.R  a  b)
            {}\mRightarrow{}  (\mforall{}s:fset(T).  \mexists{}L:T  List.  \mforall{}x:T.  (x  \mmember{}  s  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `sorted-by-exists2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  (InstLemma  `deq\_property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  RWO    "-1"  0
                            THEN  Auto)
              )
  THEN  Skolemize  (-1)  `sort'
  THEN  Auto)

---

Home Index