---

Step * 1 of Lemma rotate-injection


1. n : ℕ
2. a1 : ℕn
3. a2 : ℕn
4. if (a1 =z n - 1) then 0 else a1 + 1 fi  = if (a2 =z n - 1) then 0 else a2 + 1 fi  ∈ ℕn
⊢ a1 = a2 ∈ ℕn
BY
{ ((SplitOnHypITE -1  THENA Auto) THEN SplitOnHypITE -2  THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a1  :  \mBbbN{}n
3.  a2  :  \mBbbN{}n
4.  if  (a1  =\msubz{}  n  -  1)  then  0  else  a1  +  1  fi    =  if  (a2  =\msubz{}  n  -  1)  then  0  else  a2  +  1  fi 
\mvdash{}  a1  =  a2


By

---

Latex:
((SplitOnHypITE  -1    THENA  Auto)  THEN  SplitOnHypITE  -2    THEN  Auto)

---

Home Index