Step
*
of Lemma
natrec_wf
∀[T:ℕ ⟶ Type]. ∀[g:n:ℕ ⟶ (m:ℕn ⟶ T[m]) ⟶ T[n]]. (letrec f(n)=g[n;f] in f ∈ n:ℕ ⟶ T[n])
BY
{ (Unfold `natrec` 0 THEN Auto THEN Assert ⌜∀n:ℕ. (letrec f(n)=g[n;f] in f ∈ m:ℕn ⟶ T[m])⌝⋅) }
1
.....assertion.....
1. T : ℕ ⟶ Type
2. g : n:ℕ ⟶ (m:ℕn ⟶ T[m]) ⟶ T[n]
⊢ ∀n:ℕ. (letrec f(n)=g[n;f] in f ∈ m:ℕn ⟶ T[m])
2
1. T : ℕ ⟶ Type
2. g : n:ℕ ⟶ (m:ℕn ⟶ T[m]) ⟶ T[n]
3. ∀n:ℕ. (letrec f(n)=g[n;f] in f ∈ m:ℕn ⟶ T[m])
⊢ letrec f(n)=g[n;f] in
f ∈ n:ℕ ⟶ T[n]
Latex:
Latex:
\mforall{}[T:\mBbbN{} {}\mrightarrow{} Type]. \mforall{}[g:n:\mBbbN{} {}\mrightarrow{} (m:\mBbbN{}n {}\mrightarrow{} T[m]) {}\mrightarrow{} T[n]]. (letrec f(n)=g[n;f] in f \mmember{} n:\mBbbN{} {}\mrightarrow{} T[n])
By
Latex:
(Unfold `natrec` 0 THEN Auto THEN Assert \mkleeneopen{}\mforall{}n:\mBbbN{}. (letrec f(n)=g[n;f] in f \mmember{} m:\mBbbN{}n {}\mrightarrow{} T[m])\mkleeneclose{}\mcdot{})
Home
Index