Nuprl 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]} })


Proof




Definitions occuring in Statement :  bm_T: bm_T(key;value;cnt;left;right) bm_E: bm_E() binary_map: binary_map(T;Key) uall: [x:A]. B[x] prop: guard: {T} so_apply: x[s1;s2] all: x:A. B[x] implies:  Q set: {x:A| B[x]}  function: x:A ─→ B[x] int: universe: Type
Lemmas :  binary_map-induction set_wf binary_map_wf all_wf bm_T_wf bm_E_wf
\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]\}  \})



Date html generated: 2015_07_17-AM-08_17_54
Last ObjectModification: 2015_01_27-PM-00_40_27

Home Index