---

Step * of Lemma bag-function

∀[T,A:Type]. ∀[f:(T List) ⟶ bag(A)].
  f ∈ bag(T) ⟶ bag(A) supposing ∀as,bs:T List.  (f[as @ bs] = (f[as] + f[bs]) ∈ bag(A))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert ∀x:T. ∀xs:T List.  (f[[x / xs]] = (f[[x]] + f[xs]) ∈ bag(A)) BY
               ((RWO "-1<" 0 THEN Auto) THEN Reduce 0 THEN Auto))
   THEN (ExtWith [`L'] [(T List) ⟶ bag(A)]⋅ THENA Auto)
   THEN D -1
   THEN Auto
   THEN InstLemma `permutation-invariant2` [⌜T⌝;⌜λ2L1 L2.(f L1) = (f L2) ∈ bag(A)⌝]⋅
   THEN Auto
   THEN Try ((D 0 THEN Auto))
   THEN RWO "4 5" 0
   THEN Auto
   THEN Try ((BLemma `bag-append-comm` THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[f:(T  List)  {}\mrightarrow{}  bag(A)].
    f  \mmember{}  bag(T)  {}\mrightarrow{}  bag(A)  supposing  \mforall{}as,bs:T  List.    (f[as  @  bs]  =  (f[as]  +  f[bs]))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  \mforall{}x:T.  \mforall{}xs:T  List.    (f[[x  /  xs]]  =  (f[[x]]  +  f[xs]))  BY
                          ((RWO  "-1<"  0  THEN  Auto)  THEN  Reduce  0  THEN  Auto))
  THEN  (ExtWith  [`L']  [(T  List)  {}\mrightarrow{}  bag(A)]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Auto
  THEN  InstLemma  `permutation-invariant2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}L1  L2.(f  L1)  =  (f  L2)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((D  0  THEN  Auto))
  THEN  RWO  "4  5"  0
  THEN  Auto
  THEN  Try  ((BLemma  `bag-append-comm`  THEN  Auto)))

---

Home Index