---

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


1. n : ℕ
2. L : ℕn List
3. x : ℕn
4. ¬(x ∈ L)
5. ¬(L = [] ∈ (ℕn List))
6. b : ℕn
7. hd(L) = 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
{ (Thin (-1) THEN Thin (-2)) }

1
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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  L  :  \mBbbN{}n  List
3.  x  :  \mBbbN{}n
4.  \mneg{}(x  \mmember{}  L)
5.  \mneg{}(L  =  [])
6.  b  :  \mBbbN{}n
7.  hd(L)  =  b
\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:
(Thin  (-1)  THEN  Thin  (-2))

---

Home Index