Step
*
of Lemma
rec-comb_wf2
∀[Info:Type]. ∀[n,m:ℕ]. ∀[A:{m..n-} ─→ Type]. ∀[X:i:{m..n-} ─→ EClass(A i)]. ∀[T:Type]. ∀[f:Id
─→ (i:{m..n-} ─→ bag(A i))
─→ bag(T)
─→ bag(T)].
∀[init:Id ─→ bag(T)].
(rec-comb(X;f;init) ∈ EClass(T))
BY
{ (BasicUniformUnivCD Auto THEN All (Unfold `eclass`) THEN Unhide) }
1
1. Info : Type
2. n : ℕ
3. m : ℕ
4. A : {m..n-} ─→ Type
5. X : i:{m..n-} ─→ es:EO+(Info) ─→ e:E ─→ bag(A i)
6. T : Type
7. f : Id ─→ (i:{m..n-} ─→ bag(A i)) ─→ bag(T) ─→ bag(T)
8. init : Id ─→ bag(T)
⊢ rec-comb(X;f;init) ∈ es:EO+(Info) ─→ e:E ─→ bag(T)
Latex:
Latex:
\mforall{}[Info:Type]. \mforall{}[n,m:\mBbbN{}]. \mforall{}[A:\{m..n\msupminus{}\} {}\mrightarrow{} Type]. \mforall{}[X:i:\{m..n\msupminus{}\} {}\mrightarrow{} EClass(A i)]. \mforall{}[T:Type].
\mforall{}[f:Id {}\mrightarrow{} (i:\{m..n\msupminus{}\} {}\mrightarrow{} bag(A i)) {}\mrightarrow{} bag(T) {}\mrightarrow{} bag(T)]. \mforall{}[init:Id {}\mrightarrow{} bag(T)].
(rec-comb(X;f;init) \mmember{} EClass(T))
By
Latex:
(BasicUniformUnivCD Auto THEN All (Unfold `eclass`) THEN Unhide)
Home
Index