---

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

.....truecase..... 
1. n : ℕ
2. x : ℕn
3. b : ℕn
4. u : ℕn
5. v : ℕn List
6. (¬(x ∈ v))
⇒ (rec-case(v) of [] => x | a::as => r.if (x =z a) then if null(as) then b else hd(as) fi  else r fi  = x ∈ ℕn)
7. ¬((x = u ∈ ℕn) ∨ (x ∈ v))
8. x = u ∈ ℤ
⊢ if null(v) then b else hd(v) fi  = x ∈ ℕn
BY
{ (D (-2) THEN Auto) }

---

Latex:

---

Latex:
.....truecase..... 
1.  n  :  \mBbbN{}
2.  x  :  \mBbbN{}n
3.  b  :  \mBbbN{}n
4.  u  :  \mBbbN{}n
5.  v  :  \mBbbN{}n  List
6.  (\mneg{}(x  \mmember{}  v))
{}\mRightarrow{}  (rec-case(v)  of
        []  =>  x
        a::as  =>
          r.if  (x  =\msubz{}  a)  then  if  null(as)  then  b  else  hd(as)  fi    else  r  fi 
      =  x)
7.  \mneg{}((x  =  u)  \mvee{}  (x  \mmember{}  v))
8.  x  =  u
\mvdash{}  if  null(v)  then  b  else  hd(v)  fi    =  x


By

---

Latex:
(D  (-2)  THEN  Auto)

---

Home Index