---

Step * 1 of Lemma has-value-mklist


1. n : Base
2. f : Base
3. (fix((λp,n. if (n) < (1)  then []  else ((p (n - 1)) @ [f (n - 1)]))) n)↓
⊢ n ∈ ℤ
BY
{ (Compactness (-1)
   THEN Unhide
   THEN Thin (-3)
   THEN MoveToConcl 1
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN (UnivCD THENA Auto)
   THEN BotDiv
   THEN (RWO "fun_exp_unroll_1" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN HasValueD (-1)) }

1
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 ∈ ℤ

---

Latex:

---

Latex:

1.  n  :  Base
2.  f  :  Base
3.  (fix((\mlambda{}p,n.  if  (n)  <  (1)    then  []    else  ((p  (n  -  1))  @  [f  (n  -  1)])))  n)\mdownarrow{}
\mvdash{}  n  \mmember{}  \mBbbZ{}


By

---

Latex:
(Compactness  (-1)
  THEN  Unhide
  THEN  Thin  (-3)
  THEN  MoveToConcl  1
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Strictness
  THEN  (UnivCD  THENA  Auto)
  THEN  BotDiv
  THEN  (RWO  "fun\_exp\_unroll\_1"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  HasValueD  (-1))

---

Home Index