---

Step * of Lemma list-partition-permutation

∀T:Type. ∀L:T List. ∀f:ℕ||L|| ⟶ 𝔹.  let as,bs = list-partition(f;L) in permutation(T;L;as @ bs)
BY
{ TACTIC:(InductionOnList
          THEN Unfold `list-partition` 0
          THEN Reduce 0
          THEN Try (Fold `list-partition` 0)
          THEN Auto
          THEN Try ((BLemma `permutation-nil` THEN Auto))) }

1
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 ⟶ 𝔹
⊢ let as,bs = let left,right = list-partition(f;v) 
              in if f ||v|| then <[u / left], right> else <left, [u / right]> fi  
  in permutation(T;[u / v];as @ bs)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}L:T  List.  \mforall{}f:\mBbbN{}||L||  {}\mrightarrow{}  \mBbbB{}.    let  as,bs  =  list-partition(f;L)  in  permutation(T;L;as  @  bs)


By

---

Latex:
TACTIC:(InductionOnList
                THEN  Unfold  `list-partition`  0
                THEN  Reduce  0
                THEN  Try  (Fold  `list-partition`  0)
                THEN  Auto
                THEN  Try  ((BLemma  `permutation-nil`  THEN  Auto)))

---

Home Index