---

Step * 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 ⟶ 𝔹
⊢ 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)
BY
{ ((InstHyp [⌜f⌝] (-2)⋅ THEN Auto')
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [1;1]
   THEN Thin (-1)
   THEN D -1
   THEN Reduce 0
   THEN AutoSplit
   THEN Auto
   THEN RWO "permutation-cons" 0
   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 ⟶ 𝔹
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))

---

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{}
\mvdash{}  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)


By

---

Latex:
((InstHyp  [\mkleeneopen{}f\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto')
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [1;1]
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Auto
  THEN  RWO  "permutation-cons"  0
  THEN  Auto)

---

Home Index