---

Step * of Lemma permutation-rotate

∀[A:Type]. ∀as,bs:A List.  permutation(A;as @ bs;bs @ as)
BY
{ ((Unfold `permutation` 0 THEN Auto)
   THEN (RWO "length-append" 0 THENA Auto)
   THEN (InstConcl [⌜λi.if i <z ||bs|| then i + ||as|| else i - ||bs|| fi ⌝]⋅ THENA Auto)) }

1
1. [A] : Type
2. as : A List
3. bs : A List
⊢ Inj(ℕ||as|| + ||bs||;ℕ||as|| + ||bs||;λi.if i <z ||bs|| then i + ||as|| else i - ||bs|| fi )
∧ ((bs @ as) = (as @ bs o λi.if i <z ||bs|| then i + ||as|| else i - ||bs|| fi ) ∈ (A List))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}as,bs:A  List.    permutation(A;as  @  bs;bs  @  as)


By

---

Latex:
((Unfold  `permutation`  0  THEN  Auto)
  THEN  (RWO  "length-append"  0  THENA  Auto)
  THEN  (InstConcl  [\mkleeneopen{}\mlambda{}i.if  i  <z  ||bs||  then  i  +  ||as||  else  i  -  ||bs||  fi  \mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index