---

Step * of Lemma bag-to-list_wf

∀[T:Type]
  ∀[b:bag(T)]. ∀[cmp:comparison({x:T| x ↓∈ b} )].
    bag-to-list(cmp;b) ∈ T List supposing ∀x,y:{x:T| x ↓∈ b} .  (((cmp x y) = 0 ∈ ℤ) ⇒ (x = y ∈ T)) 
  supposing valueall-type(T)
BY
{ (Auto
   THEN D 3
   THEN (FLemma  `member-permutation` [-3] THENA Auto)
   THEN (InstLemma `bag-member-iff-sq-list-member` [⌜T⌝;⌜b⌝]⋅ THENA Auto)
   THEN (Assert {x:T| x ↓∈ b}  ≡ {x:T| (x ∈ b)}  BY
               (RepeatFor 2 ((D 0 THENA Auto))
                THEN (D -1 THEN Auto)
                THEN (FHyp (-3) [-1] THENA Auto)
                THEN D -1
                THEN Auto⋅))
   THEN (Assert Linorder({x:T| (x ∈ b)} ;a,b.0 ≤ (cmp a b)) BY
               (RepeatFor 2 ((D 0 THEN Auto))
                THEN BLemma `comparison-antisym`
                THEN Auto
                THEN D -3
                THEN EqTypeCD
                THEN Auto))
   THEN Thin (-5)
   THEN PromoteHyp (-1) (-4)) }

1
1. T : Type
2. valueall-type(T)
3. b : Base
4. b1 : Base
5. b = b1 ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
6. b ∈ T List
7. b1 ∈ T List
8. permutation(T;b;b1)
9. cmp : comparison({x:T| x ↓∈ b} )
10. Linorder({x:T| (x ∈ b)} ;a,b.0 ≤ (cmp a b))
11. ∀a:T. ((a ∈ b) ⇐⇒ (a ∈ b1))
12. ∀x:T. uiff(x ↓∈ b;↓(x ∈ b))
13. {x:T| x ↓∈ b}  ≡ {x:T| (x ∈ b)} 
⊢ bag-to-list(cmp;b) = bag-to-list(cmp;b1) ∈ (T List)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[b:bag(T)].  \mforall{}[cmp:comparison(\{x:T|  x  \mdownarrow{}\mmember{}  b\}  )].
        bag-to-list(cmp;b)  \mmember{}  T  List  supposing  \mforall{}x,y:\{x:T|  x  \mdownarrow{}\mmember{}  b\}  .    (((cmp  x  y)  =  0)  {}\mRightarrow{}  (x  =  y)) 
    supposing  valueall-type(T)


By

---

Latex:
(Auto
  THEN  D  3
  THEN  (FLemma    `member-permutation`  [-3]  THENA  Auto)
  THEN  (InstLemma  `bag-member-iff-sq-list-member`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \{x:T|  x  \mdownarrow{}\mmember{}  b\}    \mequiv{}  \{x:T|  (x  \mmember{}  b)\}    BY
                          (RepeatFor  2  ((D  0  THENA  Auto))
                            THEN  (D  -1  THEN  Auto)
                            THEN  (FHyp  (-3)  [-1]  THENA  Auto)
                            THEN  D  -1
                            THEN  Auto\mcdot{}))
  THEN  (Assert  Linorder(\{x:T|  (x  \mmember{}  b)\}  ;a,b.0  \mleq{}  (cmp  a  b))  BY
                          (RepeatFor  2  ((D  0  THEN  Auto))
                            THEN  BLemma  `comparison-antisym`
                            THEN  Auto
                            THEN  D  -3
                            THEN  EqTypeCD
                            THEN  Auto))
  THEN  Thin  (-5)
  THEN  PromoteHyp  (-1)  (-4))

---

Home Index