---

Step * 1 1 of Lemma permutation-rotate


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||))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN RepeatFor 2 ((SplitOnConclITE THENA Auto)) THEN Auto') }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  as  :  A  List
3.  bs  :  A  List
\mvdash{}  \mforall{}a1,a2:\mBbbN{}||as||  +  ||bs||.
        ((if  a1  <z  ||bs||  then  a1  +  ||as||  else  a1  -  ||bs||  fi 
        =  if  a2  <z  ||bs||  then  a2  +  ||as||  else  a2  -  ||bs||  fi  )
        {}\mRightarrow{}  (a1  =  a2))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  RepeatFor  2  ((SplitOnConclITE  THENA  Auto))  THEN  Auto')

---

Home Index