---

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


1. n : ℕ
2. L : ℕn List
3. no_repeats(ℕn;L)
4. i : ℕ||L||
5. ¬(L = [] ∈ (ℕn List))
6. b : ℕn
7. hd(L) = b ∈ ℕn
8. v : ℕn
9. v1 : ℕn
⊢ (∃j:ℕ||L||
    ((v1 = L[j] ∈ ℕn) ∧ ((j = (||L|| - 1) ∈ ℤ) ⇒ (v = b ∈ ℕn)) ∧ ((¬(j = (||L|| - 1) ∈ ℤ)) ⇒ (v = L[j + 1] ∈ ℕn))))
⇒ (rec-case(L) of [] => v1 | a::as => r.if (v1 =z a) then if null(as) then b else hd(as) fi  else r fi  = v ∈ ℕn)
BY
{ TACTIC:(Thin (-3) THEN (Thin 5 THEN Thin 4) THEN ListInd 2 THEN Reduce 0) }

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

2
1. n : ℕ
2. b : ℕn
3. v : ℕn
4. v1 : ℕn
5. u : ℕn
6. v2 : ℕn List
7. no_repeats(ℕn;v2)
⇒ (∃j:ℕ||v2||
     ((v1 = v2[j] ∈ ℕn)
     ∧ ((j = (||v2|| - 1) ∈ ℤ) ⇒ (v = b ∈ ℕn))
     ∧ ((¬(j = (||v2|| - 1) ∈ ℤ)) ⇒ (v = v2[j + 1] ∈ ℕn))))
⇒ (rec-case(v2) of [] => v1 | a::as => r.if (v1 =z a) then if null(as) then b else hd(as) fi  else r fi  = v ∈ ℕn)
⊢ no_repeats(ℕn;[u / v2])
⇒ (∃j:ℕ||v2|| + 1
     ((v1 = [u / v2][j] ∈ ℕn)
     ∧ ((j = ((||v2|| + 1) - 1) ∈ ℤ) ⇒ (v = b ∈ ℕn))
     ∧ ((¬(j = ((||v2|| + 1) - 1) ∈ ℤ)) ⇒ (v = [u / v2][j + 1] ∈ ℕn))))
⇒ (if (v1 =z u)
   then if null(v2) then b else hd(v2) fi 
   else rec-case(v2) of
        [] => v1
        h::t =>
         r.if (v1 =z h) then if null(t) then b else hd(t) fi  else r fi 
   fi 
   = v
   ∈ ℕn)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  L  :  \mBbbN{}n  List
3.  no\_repeats(\mBbbN{}n;L)
4.  i  :  \mBbbN{}||L||
5.  \mneg{}(L  =  [])
6.  b  :  \mBbbN{}n
7.  hd(L)  =  b
8.  v  :  \mBbbN{}n
9.  v1  :  \mBbbN{}n
\mvdash{}  (\mexists{}j:\mBbbN{}||L||
        ((v1  =  L[j])  \mwedge{}  ((j  =  (||L||  -  1))  {}\mRightarrow{}  (v  =  b))  \mwedge{}  ((\mneg{}(j  =  (||L||  -  1)))  {}\mRightarrow{}  (v  =  L[j  +  1]))))
{}\mRightarrow{}  (rec-case(L)  of
        []  =>  v1
        a::as  =>
          r.if  (v1  =\msubz{}  a)  then  if  null(as)  then  b  else  hd(as)  fi    else  r  fi 
      =  v)


By

---

Latex:
TACTIC:(Thin  (-3)  THEN  (Thin  5  THEN  Thin  4)  THEN  ListInd  2  THEN  Reduce  0)

---

Home Index