---

Step * 1 of Lemma permutation-rotate


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))
BY
{ (RepUR ``inject permute_list`` 0  THEN D 0) }

1
1. [A] : Type
2. as : A List
3. bs : A List
⊢ ∀a1,a2:ℕ||as|| + ||bs||.
    ((if a1 <z ||bs|| then a1 + ||as|| else a1 - ||bs|| fi 
    = if a2 <z ||bs|| then a2 + ||as|| else a2 - ||bs|| fi 
    ∈ ℕ||as|| + ||bs||)
    ⇒ (a1 = a2 ∈ ℕ||as|| + ||bs||))

2
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)

---

Latex:

---

Latex:

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


By

---

Latex:
(RepUR  ``inject  permute\_list``  0    THEN  D  0)

---

Home Index