---

Step * 1 1 1 of Lemma apply-nth_wf

.....subterm..... T:t
1:n
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)) ∈ primrec(n;T;λi,t. ((A (n - i)) ⟶ t)) ⟶ primrec(n - 1;T;λi,t. ((A (n - 1 - \000Ci)) ⟶ t))
BY
{ ((InstHyp [⌜λ2k.A[k + 1]⌝;⌜x⌝] 4⋅ THENA Auto) THEN InferEqualType THEN Auto) }

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))
10. 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) + 1] ⟶ t))
    ⟶ primrec(n - 1;T;λi,t. (A[(n - 1 - 1 - i) + 1] ⟶ t))
⊢ (primrec((n - 1) + 1;T;λi,t. (A[(((n - 1) + 1) - 1 - i) + 1] ⟶ t)) ⟶ primrec(n - 1;T;λi,t. (A[(n - 1 - 1 - i) + 1] ─\000C→ t)))
= (primrec(n;T;λi,t. ((A (n - i)) ⟶ t)) ⟶ primrec(n - 1;T;λi,t. ((A (n - 1 - i)) ⟶ t)))
∈ Type

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  T  :  Type
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}A:\mBbbN{}(n  -  1)  +  1  {}\mrightarrow{}  Type.  \mforall{}x:A[n  -  1].
          (primrec(n  -  1;\mlambda{}f.(f  x);\mlambda{}i,H,f.  (H  o  f))
            \mmember{}  primrec((n  -  1)  +  1;T;\mlambda{}i,t.  ((A  (((n  -  1)  +  1)  -  1  -  i))  {}\mrightarrow{}  t))  {}\mrightarrow{}  primrec(n  -  1;T;\mlambda{}i,t.  ((A\000C 
                                                                                                                                                                                              (n 
                                                                                                                                                                                              -  1 
                                                                                                                                                                                              -  1 
                                                                                                                                                                                              -  i))
                                                                                                                                                                                        {}\mrightarrow{}  t)))
5.  \mneg{}((n  +  1)  =  0)
6.  \mneg{}(n  =  0)
7.  A  :  \mBbbN{}n  +  1  {}\mrightarrow{}  Type
8.  x  :  A[n]
9.  f  :  (A  (n  -  n))  {}\mrightarrow{}  primrec(n;T;\mlambda{}i,t.  ((A  (n  -  i))  {}\mrightarrow{}  t))
\mvdash{}  primrec(n  -  1;\mlambda{}f.(f  x);\mlambda{}i,H,f.  (H  o  f))  \mmember{}  primrec(n;T;\mlambda{}i,t.  ((A  (n  -  i))  {}\mrightarrow{}  t))
    {}\mrightarrow{}  primrec(n  -  1;T;\mlambda{}i,t.  ((A  (n  -  1  -  i))  {}\mrightarrow{}  t))


By

---

Latex:
((InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}k.A[k  +  1]\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  4\mcdot{}  THENA  Auto)  THEN  InferEqualType  THEN  Auto)

---

Home Index