---

Step * of Lemma bag-count-map

∀[T1,T2:Type]. ∀[f:T1 ⟶ T2]. ∀[eq1:EqDecider(T1)]. ∀[eq2:EqDecider(T2)]. ∀[x:T2]. ∀[bs:bag(T1)]. ∀[g:T2 ⟶ T1].
  (#x in bag-map(f;bs)) ~ (#g x in bs) supposing (∀x:T2. ((f (g x)) = x ∈ T2)) ∧ (∀x:T1. ((g (f x)) = x ∈ T1))
BY
{ xxx(InstLemma `bag-count-ap-map` []
      THEN RepeatFor 5 (ParallelLast')
      THEN Auto
      THEN (InstHyp [⌜g x⌝;⌜bs⌝] (-6)⋅ THENM (RevHypSubst (-1) 0 THEN EqCD))
      THEN Auto
      THEN Try ((Symmetry THEN Complete (Auto))))xxx }

1
.....antecedent..... 
1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ T2
4. eq1 : EqDecider(T1)
5. eq2 : EqDecider(T2)
6. ∀[x:T1]. ∀[bs:bag(T1)].  (#f x in bag-map(f;bs)) ~ (#x in bs) supposing Inj(T1;T2;f)
7. x : T2
8. bs : bag(T1)
9. g : T2 ⟶ T1
10. ∀x:T2. ((f (g x)) = x ∈ T2)
11. ∀x:T1. ((g (f x)) = x ∈ T1)
⊢ Inj(T1;T2;f)

---

Latex:

---

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[f:T1  {}\mrightarrow{}  T2].  \mforall{}[eq1:EqDecider(T1)].  \mforall{}[eq2:EqDecider(T2)].  \mforall{}[x:T2].  \mforall{}[bs:bag(T1)].
\mforall{}[g:T2  {}\mrightarrow{}  T1].
    (\#x  in  bag-map(f;bs))  \msim{}  (\#g  x  in  bs)  supposing  (\mforall{}x:T2.  ((f  (g  x))  =  x))  \mwedge{}  (\mforall{}x:T1.  ((g  (f  x))  =  x))


By

---

Latex:
xxx(InstLemma  `bag-count-ap-map`  []
        THEN  RepeatFor  5  (ParallelLast')
        THEN  Auto
        THEN  (InstHyp  [\mkleeneopen{}g  x\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]  (-6)\mcdot{}  THENM  (RevHypSubst  (-1)  0  THEN  EqCD))
        THEN  Auto
        THEN  Try  ((Symmetry  THEN  Complete  (Auto))))xxx

---

Home Index