---

Step * 1 1 of Lemma list-partition-permutation


1. T : Type
2. u : T
3. v : T List
4. ∀f:ℕ||v|| ⟶ 𝔹. let as,bs = list-partition(f;v) in permutation(T;v;as @ bs)
5. f : ℕ||v|| + 1 ⟶ 𝔹
6. v2 : T List
7. v3 : T List
8. ↑(f ||v||)
9. permutation(T;v;v2 @ v3)
⊢ ∃as,bs:T List. (([u / (v2 @ v3)] = (as @ [u / bs]) ∈ (T List)) ∧ permutation(T;v;as @ bs))
BY
{ (InstConcl [⌜[]⌝;⌜v2 @ v3⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}f:\mBbbN{}||v||  {}\mrightarrow{}  \mBbbB{}.  let  as,bs  =  list-partition(f;v)  in  permutation(T;v;as  @  bs)
5.  f  :  \mBbbN{}||v||  +  1  {}\mrightarrow{}  \mBbbB{}
6.  v2  :  T  List
7.  v3  :  T  List
8.  \muparrow{}(f  ||v||)
9.  permutation(T;v;v2  @  v3)
\mvdash{}  \mexists{}as,bs:T  List.  (([u  /  (v2  @  v3)]  =  (as  @  [u  /  bs]))  \mwedge{}  permutation(T;v;as  @  bs))


By

---

Latex:
(InstConcl  [\mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}v2  @  v3\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index