---

Step * of Lemma binary_map_ind_wf

∀[T,Key,A:Type]. ∀[R:A ─→ binary_map(T;Key) ─→ ℙ]. ∀[v:binary_map(T;Key)]. ∀[E:{x:A| R[x;bm_E()]} ].
∀[T:key:Key
    ─→ value:T
    ─→ cnt:ℤ
    ─→ left:binary_map(T;Key)
    ─→ right:binary_map(T;Key)
    ─→ {x:A| R[x;left]} 
    ─→ {x:A| R[x;right]} 
    ─→ {x:A| R[x;bm_T(key;value;cnt;left;right)]} ].
  (binary_map_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2]) ∈ {x:A| R[x;v]} )
BY
{ ProveDatatypeIndWf TERMOF{binary_map-definition:o, 1:l, i:l}⋅ }

---

Latex:


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


By

ProveDatatypeIndWf  TERMOF\{binary\_map-definition:o,  1:l,  i:l\}\mcdot{}

---

Home Index