---

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

∀[t:Base]. ∀[n:ℕ].  Ax ∈ is-list-if-has-value-fun(t;n) supposing is-list-if-has-value-fun(t;n)
BY
{ (Auto
   THEN MoveToConcl 1
   THEN NatInd (-1)
   THEN Try (Complete ((RepUR ``is-list-if-has-value-fun`` 0 THEN Auto)))
   THEN Auto
   THEN RepUR ``is-list-if-has-value-fun`` 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN Fold `is-list-if-has-value-fun` 0
   THEN RepUR ``is-list-if-has-value-fun`` (-1)
   THEN (RWO "primrec-unroll" (-1) THENA Auto)
   THEN SplitOnHypITE -1 
   THEN Auto
   THEN Reduce (-3)
   THEN Fold `is-list-if-has-value-fun` (-3)
   THEN HVimplies2 0 [1]
   THEN ThinTrivial) }

1
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)

---

Latex:

---

Latex:
\mforall{}[t:Base].  \mforall{}[n:\mBbbN{}].    Ax  \mmember{}  is-list-if-has-value-fun(t;n)  supposing  is-list-if-has-value-fun(t;n)


By

---

Latex:
(Auto
  THEN  MoveToConcl  1
  THEN  NatInd  (-1)
  THEN  Try  (Complete  ((RepUR  ``is-list-if-has-value-fun``  0  THEN  Auto)))
  THEN  Auto
  THEN  RepUR  ``is-list-if-has-value-fun``  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  Fold  `is-list-if-has-value-fun`  0
  THEN  RepUR  ``is-list-if-has-value-fun``  (-1)
  THEN  (RWO  "primrec-unroll"  (-1)  THENA  Auto)
  THEN  SplitOnHypITE  -1 
  THEN  Auto
  THEN  Reduce  (-3)
  THEN  Fold  `is-list-if-has-value-fun`  (-3)
  THEN  HVimplies2  0  [1]
  THEN  ThinTrivial)

---

Home Index