---

Step * 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||
⊢ permutation(A;L;rev(L))
BY
{ (With ⌜λi.(||L|| - i + 1)⌝ (D 0)⋅ THEN 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||
⊢ Inj(ℕ||L||;ℕ||L||;λi.(||L|| - i + 1))

2
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))
⊢ rev(L) = (L o λi.(||L|| - i + 1)) ∈ (A List)

---

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||
\mvdash{}  permutation(A;L;rev(L))


By

---

Latex:
(With  \mkleeneopen{}\mlambda{}i.(||L||  -  i  +  1)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index