---

Step * 2 1 1 2 1 1 1 1 of Lemma permute-to-front-permutation


1. T : Type
2. L : T List
3. idxs : ℕ List
4. x : ℕ||L||
5. (x ∈ upto(||L||))
6. ↑int-list-member(x;idxs)
7. (x ∈ upto(||L||))
8. ↑¬bint-list-member(x;idxs)
⊢ False
BY
{ (RW assert_pushdownC (-1) THEN Auto THEN RW assert_pushdownC (-3) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  idxs  :  \mBbbN{}  List
4.  x  :  \mBbbN{}||L||
5.  (x  \mmember{}  upto(||L||))
6.  \muparrow{}int-list-member(x;idxs)
7.  (x  \mmember{}  upto(||L||))
8.  \muparrow{}\mneg{}\msubb{}int-list-member(x;idxs)
\mvdash{}  False


By

---

Latex:
(RW  assert\_pushdownC  (-1)  THEN  Auto  THEN  RW  assert\_pushdownC  (-3)  THEN  Auto)

---

Home Index