---

Step * of Lemma bag-count_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  ((#x in bs) ∈ ℕ)
BY
{ xxx((UnivCD THENA Auto)
      THEN (BagD (-1) THENA Auto)
      THEN Unfold `bag-count` 0
      THEN ((InstLemma `permutation-invariant` [⌜T⌝;⌜λ2L.count(eq x;L) = count(eq x;bs) ∈ ℕ⌝]⋅
            THENM (InstHyp [⌜as⌝;⌜bs⌝]  (-1) ⋅ THEN Auto)
            )
            THENA (Auto THEN RevHypSubst' (-1) 0)
            ))xxx }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. as : T List
5. bs : T List
6. permutation(T;as;bs)
7. a1 : T List
8. a : T
9. count(eq x;[a / a1]) = count(eq x;bs) ∈ ℕ
⊢ count(eq x;a1 @ [a]) = count(eq x;[a / a1]) ∈ ℕ

2
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. as : T List
5. bs : T List
6. permutation(T;as;bs)
7. a1 : T List
8. a1@0 : T
9. a2 : T
10. count(eq x;[a1@0; [a2 / a1]]) = count(eq x;bs) ∈ ℕ
⊢ count(eq x;[a2; [a1@0 / a1]]) = count(eq x;[a1@0; [a2 / a1]]) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[bs:bag(T)].    ((\#x  in  bs)  \mmember{}  \mBbbN{})


By

---

Latex:
xxx((UnivCD  THENA  Auto)
        THEN  (BagD  (-1)  THENA  Auto)
        THEN  Unfold  `bag-count`  0
        THEN  ((InstLemma  `permutation-invariant`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}L.count(eq  x;L)  =  count(eq  x;bs)\mkleeneclose{}]\mcdot{}
                    THENM  (InstHyp  [\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]    (-1)  \mcdot{}  THEN  Auto)
                    )
                    THENA  (Auto  THEN  RevHypSubst'  (-1)  0)
                    ))xxx

---

Home Index