---

Step * 1 1 1 of Lemma taba_wf


1. A : Type
2. B : Type
3. init : B
4. F : A ⟶ A ⟶ B ⟶ B
5. xs : A List
⊢ ∀ys:A List. ((0 ≤ ||ys||) ⇒ (<init, ys> ∈ {p:B × (A List)| (0 + ||snd(p)||) = ||ys|| ∈ ℤ} ))
BY
{ Auto }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  init  :  B
4.  F  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B
5.  xs  :  A  List
\mvdash{}  \mforall{}ys:A  List.  ((0  \mleq{}  ||ys||)  {}\mRightarrow{}  (<init,  ys>  \mmember{}  \{p:B  \mtimes{}  (A  List)|  (0  +  ||snd(p)||)  =  ||ys||\}  ))


By

---

Latex:
Auto

---

Home Index