Step
*
2
1
1
1
1
of Lemma
Cn-comb_wf
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀m:ℕ. ∀A:ℕm ⟶ Type.
(n - 1 < m
⇒ (primrec(n - 1;λf.f;λi,F,f,x. (F (C-comb() f x))) ∈ funtype(m;A;T) ⟶ funtype(m;λk.if k <z n - 1 then A (k + 1)
if (k =z n - 1) then A 0
else A k
fi ;T)))
5. m : ℕ
6. A : ℕm ⟶ Type
7. n < m
8. 1 ≤ n
9. f : funtype(m;A;T)
10. x : A 1
11. C-comb() ∈ funtype(m;A;T) ⟶ funtype(m;λk.if (k =z 0) then A 1
if (k =z 1) then A 0
else A k
fi ;T)
12. v : funtype(m;λk.if (k =z 0) then A 1
if (k =z 1) then A 0
else A k
fi ;T)
13. (C-comb() f) = v ∈ funtype(m;λk.if (k =z 0) then A 1 if (k =z 1) then A 0 else A k fi ;T)
14. primrec(n - 1;λf.f;λi,F,f,x. (F (C-comb() f x))) ∈ funtype(m - 1;λk.if (k =z 0) then A 0 else A (k + 1) fi ;T)
⟶ funtype(m - 1;λk.if k <z n - 1 then (λk.if (k =z 0) then A 0 else A (k + 1) fi ) (k + 1)
if (k =z n - 1) then (λk.if (k =z 0) then A 0 else A (k + 1) fi ) 0
else (λk.if (k =z 0) then A 0 else A (k + 1) fi ) k
fi ;T)
⊢ primrec(n - 1;λf.f;λi,F,f,x. (F (C-comb() f x))) (v x) ∈ funtype(m - 1;λk.if k <z n - 1 then A (k + 2)
if (k =z n - 1) then A 0
else A (k + 1)
fi ;T)
BY
{ TACTIC:(Reduce (-1) THEN GenConclAtAddr [2;1]) }
1
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀m:ℕ. ∀A:ℕm ⟶ Type.
(n - 1 < m
⇒ (primrec(n - 1;λf.f;λi,F,f,x. (F (C-comb() f x))) ∈ funtype(m;A;T) ⟶ funtype(m;λk.if k <z n - 1 then A (k + 1)
if (k =z n - 1) then A 0
else A k
fi ;T)))
5. m : ℕ
6. A : ℕm ⟶ Type
7. n < m
8. 1 ≤ n
9. f : funtype(m;A;T)
10. x : A 1
11. C-comb() ∈ funtype(m;A;T) ⟶ funtype(m;λk.if (k =z 0) then A 1
if (k =z 1) then A 0
else A k
fi ;T)
12. v : funtype(m;λk.if (k =z 0) then A 1
if (k =z 1) then A 0
else A k
fi ;T)
13. (C-comb() f) = v ∈ funtype(m;λk.if (k =z 0) then A 1 if (k =z 1) then A 0 else A k fi ;T)
14. primrec(n - 1;λf.f;λi,F,f,x. (F (C-comb() f x))) ∈ funtype(m - 1;λk.if (k =z 0) then A 0 else A (k + 1) fi ;T)
⟶ funtype(m - 1;λk.if k <z n - 1 then if (k + 1 =z 0) then A 0 else A ((k + 1) + 1) fi
if (k =z n - 1) then A 0
if (k =z 0) then A 0
else A (k + 1)
fi ;T)
15. v1 : funtype(m - 1;λk.if (k =z 0) then A 0 else A (k + 1) fi ;T) ⟶ funtype(m - 1;λk.if k <z n - 1
then if (k + 1 =z 0)
then A 0
else A ((k + 1) + 1)
fi
if (k =z n - 1) then A 0
if (k =z 0) then A 0
else A (k + 1)
fi ;T)
16. primrec(n - 1;λf.f;λi,F,f,x. (F (C-comb() f x)))
= v1
∈ (funtype(m - 1;λk.if (k =z 0) then A 0 else A (k + 1) fi ;T) ⟶ funtype(m - 1;λk.if k <z n - 1
then if (k + 1 =z 0)
then A 0
else A ((k + 1) + 1)
fi
if (k =z n - 1) then A 0
if (k =z 0) then A 0
else A (k + 1)
fi ;T))
⊢ v1 (v x) ∈ funtype(m - 1;λk.if k <z n - 1 then A (k + 2)
if (k =z n - 1) then A 0
else A (k + 1)
fi ;T)
Latex:
Latex:
1. T : Type
2. n : \mBbbZ{}
3. 0 < n
4. \mforall{}m:\mBbbN{}. \mforall{}A:\mBbbN{}m {}\mrightarrow{} Type.
(n - 1 < m
{}\mRightarrow{} (primrec(n - 1;\mlambda{}f.f;\mlambda{}i,F,f,x. (F (C-comb() f x))) \mmember{} funtype(m;A;T) {}\mrightarrow{} funtype(m;\mlambda{}k.if k <z n\000C - 1
then A (k + 1)
if (k =\msubz{} n - 1)
then A 0
else A k
fi ;T)))
5. m : \mBbbN{}
6. A : \mBbbN{}m {}\mrightarrow{} Type
7. n < m
8. 1 \mleq{} n
9. f : funtype(m;A;T)
10. x : A 1
11. C-comb() \mmember{} funtype(m;A;T) {}\mrightarrow{} funtype(m;\mlambda{}k.if (k =\msubz{} 0) then A 1
if (k =\msubz{} 1) then A 0
else A k
fi ;T)
12. v : funtype(m;\mlambda{}k.if (k =\msubz{} 0) then A 1
if (k =\msubz{} 1) then A 0
else A k
fi ;T)
13. (C-comb() f) = v
14. primrec(n - 1;\mlambda{}f.f;\mlambda{}i,F,f,x. (F (C-comb() f x))) \mmember{} funtype(m - 1;\mlambda{}k.if (k =\msubz{} 0)
then A 0
else A (k + 1)
fi ;T)
{}\mrightarrow{} funtype(m - 1;\mlambda{}k.if k <z n - 1 then (\mlambda{}k.if (k =\msubz{} 0) then A 0 else A (k + 1) fi ) (k + 1)
if (k =\msubz{} n - 1) then (\mlambda{}k.if (k =\msubz{} 0) then A 0 else A (k + 1) fi ) 0
else (\mlambda{}k.if (k =\msubz{} 0) then A 0 else A (k + 1) fi ) k
fi ;T)
\mvdash{} primrec(n - 1;\mlambda{}f.f;\mlambda{}i,F,f,x. (F (C-comb() f x))) (v x) \mmember{} funtype(m - 1;\mlambda{}k.if k <z n - 1 then A (k \000C+ 2)
if (k =\msubz{} n - 1) then A 0
else A (k + 1)
fi ;T)
By
Latex:
TACTIC:(Reduce (-1) THEN GenConclAtAddr [2;1])
Home
Index