---

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


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)
8. no_repeats(ℕn;[u / v2])
9. j : ℕ||v2|| + 1
10. v1 = [u / v2][j] ∈ ℕn
11. (j = ((||v2|| + 1) - 1) ∈ ℤ) ⇒ (v = b ∈ ℕn)
12. (¬(j = ((||v2|| + 1) - 1) ∈ ℤ)) ⇒ (v = [u / v2][j + 1] ∈ ℕn)
13. ¬(j = 0 ∈ ℤ)
⊢ 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
BY
{ TACTIC:((RWO "select_cons_tl" (-4) THENA Auto)
          THEN (RWO "no_repeats_cons" (-6) THENA Auto)
          THEN ThinTrivial
          THEN (SplitOnConclITE THENA Auto)) }

1
.....truecase..... 
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)
8. no_repeats(ℕn;v2) ∧ (¬(u ∈ v2))
9. j : ℕ||v2|| + 1
10. v1 = v2[j - 1] ∈ ℕn
11. (j = ((||v2|| + 1) - 1) ∈ ℤ) ⇒ (v = b ∈ ℕn)
12. (¬(j = ((||v2|| + 1) - 1) ∈ ℤ)) ⇒ (v = [u / v2][j + 1] ∈ ℕn)
13. ¬(j = 0 ∈ ℤ)
14. v1 = u ∈ ℤ
⊢ if null(v2) then b else hd(v2) fi  = v ∈ ℕn

2
.....falsecase..... 
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)
8. no_repeats(ℕn;v2) ∧ (¬(u ∈ v2))
9. j : ℕ||v2|| + 1
10. v1 = v2[j - 1] ∈ ℕn
11. (j = ((||v2|| + 1) - 1) ∈ ℤ) ⇒ (v = b ∈ ℕn)
12. (¬(j = ((||v2|| + 1) - 1) ∈ ℤ)) ⇒ (v = [u / v2][j + 1] ∈ ℕn)
13. ¬(j = 0 ∈ ℤ)
14. ¬(v1 = u ∈ ℤ)
⊢ 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  = v ∈ ℕn

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:((RWO  "select\_cons\_tl"  (-4)  THENA  Auto)
                THEN  (RWO  "no\_repeats\_cons"  (-6)  THENA  Auto)
                THEN  ThinTrivial
                THEN  (SplitOnConclITE  THENA  Auto))

---

Home Index