---

Step * 1 2 of Lemma permutation-rotate


1. A : Type
2. as : A List
3. bs : A List
⊢ (bs @ as) = mklist(||as @ bs||;λi.as @ bs[if i <z ||bs|| then i + ||as|| else i - ||bs|| fi ]) ∈ (A List)
BY
{ ((BLemma `list_extensionality` THEN Try (RWO "mklist_length" 0) THEN Try ((RWO "mklist_select" 0⋅ THEN Reduce 0)))
   THEN Auto
   THEN All (RWO "length-append")
   THEN Auto
   THEN Try ((SplitOnConclITE THEN Auto'))) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  as  :  A  List
3.  bs  :  A  List
\mvdash{}  (bs  @  as)  =  mklist(||as  @  bs||;\mlambda{}i.as  @  bs[if  i  <z  ||bs||  then  i  +  ||as||  else  i  -  ||bs||  fi  ])


By

---

Latex:
((BLemma  `list\_extensionality`
    THEN  Try  (RWO  "mklist\_length"  0)
    THEN  Try  ((RWO  "mklist\_select"  0\mcdot{}  THEN  Reduce  0)))
  THEN  Auto
  THEN  All  (RWO  "length-append")
  THEN  Auto
  THEN  Try  ((SplitOnConclITE  THEN  Auto')))

---

Home Index