---

Step * 1 1 of Lemma apply-nth_wf


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))
BY
{ (MemCD THEN Try (Complete ((Auto THEN Auto')))) }

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

---

Latex:

---

Latex:

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))  o  f  \mmember{}  (A  (n  -  1  -  n  -  1))  {}\mrightarrow{}  primrec(n  -  1;T;\mlambda{}i,t.  ((A 
                                                                                                                                                                                  (n  -  1 
                                                                                                                                                                                  -  i))  {}\mrightarrow{}  t)\000C)


By

---

Latex:
(MemCD  THEN  Try  (Complete  ((Auto  THEN  Auto'))))

---

Home Index