---

Step * of Lemma permutation-reverse

∀[A:Type]. ∀L:A List. permutation(A;L;rev(L))
BY
{ (Auto
   THEN (Assert λi.(||L|| - i + 1) ∈ ℕ||L|| ⟶ ℕ||L|| BY
               Auto')
   THEN (InstLemma `length-reverse` [⌜L⌝]⋅ THENA Auto)
   THEN (InstLemma `permute_list_length` [⌜A⌝;⌜L⌝;⌜λi.(||L|| - i + 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||
⊢ permutation(A;L;rev(L))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}L:A  List.  permutation(A;L;rev(L))


By

---

Latex:
(Auto
  THEN  (Assert  \mlambda{}i.(||L||  -  i  +  1)  \mmember{}  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L||  BY
                          Auto')
  THEN  (InstLemma  `length-reverse`  [\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `permute\_list\_length`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}\mlambda{}i.(||L||  -  i  +  1)\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index