---

Step * 1 of Lemma apply-nth_wf


1. T : Type
2. n : ℕ
3. A : ℕn + 1 ⟶ Type
4. x : A[n]
⊢ primrec(n;λf.(f x);λi,H,f. (H o f)) ∈ funtype(n + 1;A;T) ⟶ funtype(n;A;T)
BY
{ xxx(Unfold `funtype` 0
      THEN NatInd 2
      THEN (RWO "primrec-unroll" 0 THENA Auto)
      THEN RepeatFor 2 (OldAutoSplit)
      THEN RepeatFor 2 ((D 0 THENA Auto))
      THEN (MemCD THENA Auto')
      THEN Subst' (n + 1) - 1 ~ n -1
      THEN Try (Complete (Auto)))xxx }

1
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀A:ℕ(n - 1) + 1 ⟶ Type. ∀x:A[n - 1].
     (primrec(n - 1;λf.(f x);λi,H,f. (H o f)) ∈ primrec((n - 1) + 1;T;λi,t. ((A (((n - 1) + 1) - 1 - i)) ⟶ t))
      ⟶ primrec(n - 1;T;λi,t. ((A (n - 1 - 1 - i)) ⟶ t)))
5. ¬((n + 1) = 0 ∈ ℤ)
6. ¬(n = 0 ∈ ℤ)
7. A : ℕn + 1 ⟶ Type
8. x : A[n]
9. f : (A (n - n)) ⟶ primrec(n;T;λi,t. ((A (n - i)) ⟶ t))
⊢ primrec(n - 1;λf.(f x);λi,H,f. (H o f)) o f ∈ (A (n - 1 - n - 1)) ⟶ primrec(n - 1;T;λi,t. ((A (n - 1 - i)) ⟶ t))

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbN{}
3.  A  :  \mBbbN{}n  +  1  {}\mrightarrow{}  Type
4.  x  :  A[n]
\mvdash{}  primrec(n;\mlambda{}f.(f  x);\mlambda{}i,H,f.  (H  o  f))  \mmember{}  funtype(n  +  1;A;T)  {}\mrightarrow{}  funtype(n;A;T)


By

---

Latex:
xxx(Unfold  `funtype`  0
        THEN  NatInd  2
        THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
        THEN  RepeatFor  2  (OldAutoSplit)
        THEN  RepeatFor  2  ((D  0  THENA  Auto))
        THEN  (MemCD  THENA  Auto')
        THEN  Subst'  (n  +  1)  -  1  \msim{}  n  -1
        THEN  Try  (Complete  (Auto)))xxx

---

Home Index