---

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

.....falsecase..... 
1. n : ℕ
2. L : ℕn List
3. x : ℕn
4. ¬(x ∈ L)
5. ¬(L = [] ∈ (ℕn List))
⊢ rec-case(L) of [] => x | a::as => r.if (x =z a) then if null(as) then hd(L) else hd(as) fi  else r fi  = x ∈ ℕn
BY
{ (GenConcl ⌜hd(L) = b ∈ ℕn⌝⋅ THENA (Auto THEN DVar `L' THEN All Reduce THEN Auto THEN D -1 THEN Auto)) }

1
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

---

Latex:

---

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


By

---

Latex:
(GenConcl  \mkleeneopen{}hd(L)  =  b\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  DVar  `L'  THEN  All  Reduce  THEN  Auto  THEN  D  -1  THEN  Auto))

---

Home Index