---

Step * 1 of Lemma bag-splits-permutation


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]))
BY
{ ((InstLemma `bag-splits_wf_list` [⌜T⌝]⋅ THENA Auto) THEN PromoteHyp (-1) 2) }

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  L1  :  T  List
3.  L2  :  T  List
4.  permutation(T;L1;L2)
5.  as  :  T  List
6.  a  :  T
\mvdash{}  permutation(bag(T)  \mtimes{}  bag(T);bag-splits([a  /  as]);bag-splits(as  @  [a]))


By

---

Latex:
((InstLemma  `bag-splits\_wf\_list`  [\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  PromoteHyp  (-1)  2)

---

Home Index