---

Step * of Lemma binary_map_ind_wf_simple

∀[T,Key,A:Type]. ∀[v:binary_map(T;Key)]. ∀[E:A]. ∀[T:key:Key
                                                     ─→ value:T
                                                     ─→ cnt:ℤ
                                                     ─→ left:binary_map(T;Key)
                                                     ─→ right:binary_map(T;Key)
                                                     ─→ A
                                                     ─→ A
                                                     ─→ A].
  (binary_map_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2]) ∈ A)
BY
{ ProveDatatypeIndWfSimple 2 `binary_map_ind_wf` }

---

Latex:


\mforall{}[T,Key,A:Type].  \mforall{}[v:binary\_map(T;Key)].  \mforall{}[E:A].  \mforall{}[T:key:Key
                                                                                                          {}\mrightarrow{}  value:T
                                                                                                          {}\mrightarrow{}  cnt:\mBbbZ{}
                                                                                                          {}\mrightarrow{}  left:binary\_map(T;Key)
                                                                                                          {}\mrightarrow{}  right:binary\_map(T;Key)
                                                                                                          {}\mrightarrow{}  A
                                                                                                          {}\mrightarrow{}  A
                                                                                                          {}\mrightarrow{}  A].
    (binary\_map\_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2])  \mmember{}  A)


By

ProveDatatypeIndWfSimple  2  `binary\_map\_ind\_wf`

---

Home Index