---

Step * of Lemma binary_map-definition

∀[T,Key,A:Type]. ∀[R:A ─→ binary_map(T;Key) ─→ ℙ].
  ({x:A| R[x;bm_E()]} 
  ⇒ (∀key:Key. ∀value:T. ∀cnt:ℤ. ∀left,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)]} ))
  ⇒ {∀v:binary_map(T;Key). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `binary_map-induction` }

---

Latex:


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


By

ProveDatatypeDefinition  `binary\_map-induction`

---

Home Index