Step
*
1
1
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))
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
BY
{ (xxx(RepeatFor 2 (EqCD) THEN Auto)xxx THEN RepUR ``so_apply`` 0 THEN RepeatFor 3 ((EqCD THEN Auto))) }
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))
10.  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)  +  1]  {}\mrightarrow{}  t))
        {}\mrightarrow{}  primrec(n  -  1;T;\mlambda{}i,t.  (A[(n  -  1  -  1  -  i)  +  1]  {}\mrightarrow{}  t))
\mvdash{}  (primrec((n  -  1)  +  1;T;\mlambda{}i,t.  (A[(((n  -  1)  +  1)  -  1  -  i)  +  1]  {}\mrightarrow{}  t))
{}\mrightarrow{}  primrec(n  -  1;T;\mlambda{}i,t.  (A[(n  -  1  -  1  -  i)  +  1]  {}\mrightarrow{}  t)))
=  (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:
(xxx(RepeatFor  2  (EqCD)  THEN  Auto)xxx  THEN  RepUR  ``so\_apply``  0  THEN  RepeatFor  3  ((EqCD  THEN  Auto)))
Home
Index