Step
*
2
2
1
1
1
of Lemma
uncurry_wf
.....equality.....
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀[A:ℕn - 1 ⟶ Type]. ∀[f:funtype(n - 1;A;T)]. (uncurry(n - 1;f) ∈ (i:ℕn - 1 ⟶ A[i]) ⟶ T)
5. ¬(n = 0 ∈ ℤ)
6. A : ℕn ⟶ Type
7. f : (A 0) ⟶ primrec(n - 1;T;λi,t. ((A (n - 1 - i)) ⟶ t))
8. a : i:ℕn ⟶ A[i]
9. uncurry(n - 1;f (a 0)) ∈ (i:ℕn - 1 ⟶ λi.(A (i + 1))[i]) ⟶ T
⊢ primrec(n - 1;f;λi,z. (z (a i))) (a (n - 1)) ~ uncurry(n - 1;f (a 0)) (λi.(a (i + 1)))
BY
{ xxx(Unfold `uncurry` 0 THEN Reduce 0)xxx }
1
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀[A:ℕn - 1 ⟶ Type]. ∀[f:funtype(n - 1;A;T)]. (uncurry(n - 1;f) ∈ (i:ℕn - 1 ⟶ A[i]) ⟶ T)
5. ¬(n = 0 ∈ ℤ)
6. A : ℕn ⟶ Type
7. f : (A 0) ⟶ primrec(n - 1;T;λi,t. ((A (n - 1 - i)) ⟶ t))
8. a : i:ℕn ⟶ A[i]
9. uncurry(n - 1;f (a 0)) ∈ (i:ℕn - 1 ⟶ λi.(A (i + 1))[i]) ⟶ T
⊢ primrec(n - 1;f;λi,z. (z (a i))) (a (n - 1)) ~ primrec(n - 1;f (a 0);λi,z. (z (a (i + 1))))
Latex:
Latex:
.....equality.....
1. T : Type
2. n : \mBbbZ{}
3. 0 < n
4. \mforall{}[A:\mBbbN{}n - 1 {}\mrightarrow{} Type]. \mforall{}[f:funtype(n - 1;A;T)]. (uncurry(n - 1;f) \mmember{} (i:\mBbbN{}n - 1 {}\mrightarrow{} A[i]) {}\mrightarrow{} T)
5. \mneg{}(n = 0)
6. A : \mBbbN{}n {}\mrightarrow{} Type
7. f : (A 0) {}\mrightarrow{} primrec(n - 1;T;\mlambda{}i,t. ((A (n - 1 - i)) {}\mrightarrow{} t))
8. a : i:\mBbbN{}n {}\mrightarrow{} A[i]
9. uncurry(n - 1;f (a 0)) \mmember{} (i:\mBbbN{}n - 1 {}\mrightarrow{} \mlambda{}i.(A (i + 1))[i]) {}\mrightarrow{} T
\mvdash{} primrec(n - 1;f;\mlambda{}i,z. (z (a i))) (a (n - 1)) \msim{} uncurry(n - 1;f (a 0)) (\mlambda{}i.(a (i + 1)))
By
Latex:
xxx(Unfold `uncurry` 0 THEN Reduce 0)xxx
Home
Index