---

Step * 1 2 1 of Lemma permutation-reverse


1. A : Type
2. L : A List
3. λi.(||L|| - i + 1) ∈ ℕ||L|| ⟶ ℕ||L||
4. ||rev(L)|| ~ ||L||
5. ||(L o λi.(||L|| - i + 1))|| ~ ||L||
6. Inj(ℕ||L||;ℕ||L||;λi.(||L|| - i + 1))
7. i : ℕ
8. i < ||rev(L)||
⊢ rev(L)[i] = (L o λi.(||L|| - i + 1))[i] ∈ A
BY
{ (DupHyp (-1) THEN (RWO "length-reverse" (-1) THENA Auto)) }

1
1. A : Type
2. L : A List
3. λi.(||L|| - i + 1) ∈ ℕ||L|| ⟶ ℕ||L||
4. ||rev(L)|| ~ ||L||
5. ||(L o λi.(||L|| - i + 1))|| ~ ||L||
6. Inj(ℕ||L||;ℕ||L||;λi.(||L|| - i + 1))
7. i : ℕ
8. i < ||rev(L)||
9. i < ||L||
⊢ rev(L)[i] = (L o λi.(||L|| - i + 1))[i] ∈ A

---

Latex:

---

Latex:

1.  A  :  Type
2.  L  :  A  List
3.  \mlambda{}i.(||L||  -  i  +  1)  \mmember{}  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L||
4.  ||rev(L)||  \msim{}  ||L||
5.  ||(L  o  \mlambda{}i.(||L||  -  i  +  1))||  \msim{}  ||L||
6.  Inj(\mBbbN{}||L||;\mBbbN{}||L||;\mlambda{}i.(||L||  -  i  +  1))
7.  i  :  \mBbbN{}
8.  i  <  ||rev(L)||
\mvdash{}  rev(L)[i]  =  (L  o  \mlambda{}i.(||L||  -  i  +  1))[i]


By

---

Latex:
(DupHyp  (-1)  THEN  (RWO  "length-reverse"  (-1)  THENA  Auto))

---

Home Index