---

Step * 2 1 1 1 of Lemma apply-cycle-member


1. n : ℕ
2. b : ℕn
3. v : ℕn
4. v1 : ℕn
⊢ no_repeats(ℕn;[])
⇒ (∃j:ℕ0. ((v1 = ⊥ ∈ ℕn) ∧ ((j = (-1) ∈ ℤ) ⇒ (v = b ∈ ℕn)) ∧ ((¬(j = (-1) ∈ ℤ)) ⇒ (v = ⊥ ∈ ℕn))))
⇒ (v1 = v ∈ ℕn)
BY
{ TACTIC:(Auto THEN ExRepD THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  b  :  \mBbbN{}n
3.  v  :  \mBbbN{}n
4.  v1  :  \mBbbN{}n
\mvdash{}  no\_repeats(\mBbbN{}n;[])
{}\mRightarrow{}  (\mexists{}j:\mBbbN{}0.  ((v1  =  \mbot{})  \mwedge{}  ((j  =  (-1))  {}\mRightarrow{}  (v  =  b))  \mwedge{}  ((\mneg{}(j  =  (-1)))  {}\mRightarrow{}  (v  =  \mbot{}))))
{}\mRightarrow{}  (v1  =  v)


By

---

Latex:
TACTIC:(Auto  THEN  ExRepD  THEN  Auto)

---

Home Index