---

Step * 1 1 of Lemma has-value-mklist


1. f : Base
2. j : ℤ
3. 0 < j
4. ∀n:Base. ((λp,n. if (n) < (1)  then []  else ((p (n - 1)) @ [f (n - 1)])^j - 1 ⊥ n)↓ ⇒ (n ∈ ℤ))
5. n : Base
6. (if (n) < (1)
       then []
       else ((λp,n. if (n) < (1)  then []  else ((p (n - 1)) @ [f (n - 1)])^j - 1 ⊥ (n - 1)) @ [f (n - 1)]))↓
7. n ∈ ℤ
8. 1 ∈ ℤ
⊢ n ∈ ℤ
BY
{ Auto }

---

Latex:

---

Latex:

1.  f  :  Base
2.  j  :  \mBbbZ{}
3.  0  <  j
4.  \mforall{}n:Base.  ((\mlambda{}p,n.  if  (n)  <  (1)    then  []    else  ((p  (n  -  1))  @  [f  (n  -  1)])\^{}j  -  1  \mbot{}  n)\mdownarrow{}  {}\mRightarrow{}  (n  \mmember{}  \mBbbZ{}))
5.  n  :  Base
6.  (if  (n)  <  (1)
              then  []
              else  ((\mlambda{}p,n.  if  (n)  <  (1)    then  []    else  ((p  (n  -  1))  @  [f  (n  -  1)])\^{}j  -  1  \mbot{}  (n  -  1))
                        @  [f  (n  -  1)]))\mdownarrow{}
7.  n  \mmember{}  \mBbbZ{}
8.  1  \mmember{}  \mBbbZ{}
\mvdash{}  n  \mmember{}  \mBbbZ{}


By

---

Latex:
Auto

---

Home Index