Step * 1 of Lemma bag-splits-permutation


1. Type
2. L1 List
3. L2 List
4. permutation(T;L1;L2)
5. as List
6. 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. Type
2. ∀b:T List. (bag-splits(b) ∈ (bag(T) × bag(T)) List)
3. L1 List
4. L2 List
5. permutation(T;L1;L2)
6. as List
7. 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