---

Step * 1 of Lemma is-list-if-has-value-fun-ax-mem


1. n : ℤ
2. n ≠ 0
3. 0 < n
4. ∀t:Base. (is-list-if-has-value-fun(t;n - 1) ⇒ (Ax ∈ is-list-if-has-value-fun(t;n - 1)))
5. t : Base
6. ¬(n = 0 ∈ ℤ)
7. (t)↓
8. ∀a,b:Base.  (if t is a pair then a otherwise b ~ b)
9. ↑isaxiom(t)
⊢ Ax ∈ ↑isaxiom(t)
BY
{ xxx((FLemma `isaxiom-implies` [-1] THENA Auto) THEN HypSubst'  (-1) 0 THEN Reduce 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  n  \mneq{}  0
3.  0  <  n
4.  \mforall{}t:Base.  (is-list-if-has-value-fun(t;n  -  1)  {}\mRightarrow{}  (Ax  \mmember{}  is-list-if-has-value-fun(t;n  -  1)))
5.  t  :  Base
6.  \mneg{}(n  =  0)
7.  (t)\mdownarrow{}
8.  \mforall{}a,b:Base.    (if  t  is  a  pair  then  a  otherwise  b  \msim{}  b)
9.  \muparrow{}isaxiom(t)
\mvdash{}  Ax  \mmember{}  \muparrow{}isaxiom(t)


By

---

Latex:
xxx((FLemma  `isaxiom-implies`  [-1]  THENA  Auto)  THEN  HypSubst'    (-1)  0  THEN  Reduce  0  THEN  Auto)xxx

---

Home Index