---

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


1. n : ℕ
2. L : ℕn List
3. x : ℕn
4. ¬(x ∈ L)
5. b : ℕn
⊢ rec-case(L) of [] => x | a::as => r.if (x =z a) then if null(as) then b else hd(as) fi  else r fi  = x ∈ ℕn
BY
{ (ListInd 2 THEN Reduce 0 THEN Auto THEN (RWO "cons_member" (-1) THENA Auto) THEN SplitOnConclITE THEN Auto) }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  L  :  \mBbbN{}n  List
3.  x  :  \mBbbN{}n
4.  \mneg{}(x  \mmember{}  L)
5.  b  :  \mBbbN{}n
\mvdash{}  rec-case(L)  of
    []  =>  x
    a::as  =>
      r.if  (x  =\msubz{}  a)  then  if  null(as)  then  b  else  hd(as)  fi    else  r  fi 
=  x


By

---

Latex:
(ListInd  2
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "cons\_member"  (-1)  THENA  Auto)
  THEN  SplitOnConclITE
  THEN  Auto)

---

Home Index