---

Step * of Lemma comb_for_itop_wf

λA,op,id,p,q,E,z. Π(op,id) p ≤ i < q. E[i] ∈ A:Type ⟶ op:(A ⟶ A ⟶ A) ⟶ id:A ⟶ p:ℤ ⟶ q:ℤ ⟶ E:({p..q-} ⟶ A) ⟶ (↓T\000Crue) ⟶ A
BY
{ ProveOpCombTyping `itop_wf` }

---

Latex:

---

Latex:
\mlambda{}A,op,id,p,q,E,z.  \mPi{}(op,id)  p  \mleq{}  i  <  q.  E[i]  \mmember{}  A:Type
{}\mrightarrow{}  op:(A  {}\mrightarrow{}  A  {}\mrightarrow{}  A)
{}\mrightarrow{}  id:A
{}\mrightarrow{}  p:\mBbbZ{}
{}\mrightarrow{}  q:\mBbbZ{}
{}\mrightarrow{}  E:(\{p..q\msupminus{}\}  {}\mrightarrow{}  A)
{}\mrightarrow{}  (\mdownarrow{}True)
{}\mrightarrow{}  A


By

---

Latex:
ProveOpCombTyping  `itop\_wf`

---

Home Index