---

Step * of Lemma bag-splits-permutation

∀T:Type. ∀L1,L2:T List.  (permutation(T;L1;L2) ⇒ permutation(bag(T) × bag(T);bag-splits(L1);bag-splits(L2)))
BY
{ (Auto
   THEN InstLemma `permutation-invariant2` [⌜T⌝;⌜λ2L1 L2.permutation(bag(T) × bag(T);bag-splits(L1);bag-splits(L2))⌝] ⋅
   THEN (Auto THEN Try ((BLemma `bag-splits-wf` THEN Auto)))
   THEN (Try ((BLemma `bag-splits-permutation1` THEN Auto))
         THEN Try ((D 0
                    THEN Auto
                    THEN Try ((BLemma `bag-splits-wf` THEN Auto))
                    THEN RelRST
                    THEN Auto
                    THEN BLemma `bag-splits-wf`
                    THEN Auto)⋅)
         )⋅) }

1
1. T : Type
2. L1 : T List
3. L2 : T List
4. permutation(T;L1;L2)
5. as : T List
6. a : T
⊢ permutation(bag(T) × bag(T);bag-splits([a / as]);bag-splits(as @ [a]))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}L1,L2:T  List.
    (permutation(T;L1;L2)  {}\mRightarrow{}  permutation(bag(T)  \mtimes{}  bag(T);bag-splits(L1);bag-splits(L2)))


By

---

Latex:
(Auto
  THEN  InstLemma  `permutation-invariant2`  [\mkleeneopen{}T\mkleeneclose{};
  \mkleeneopen{}\mlambda{}\msubtwo{}L1  L2.permutation(bag(T)  \mtimes{}  bag(T);bag-splits(L1);bag-splits(L2))\mkleeneclose{}]  \mcdot{}
  THEN  (Auto  THEN  Try  ((BLemma  `bag-splits-wf`  THEN  Auto)))
  THEN  (Try  ((BLemma  `bag-splits-permutation1`  THEN  Auto))
              THEN  Try  ((D  0
                                    THEN  Auto
                                    THEN  Try  ((BLemma  `bag-splits-wf`  THEN  Auto))
                                    THEN  RelRST
                                    THEN  Auto
                                    THEN  BLemma  `bag-splits-wf`
                                    THEN  Auto)\mcdot{})
              )\mcdot{})

---

Home Index