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: P 
⇒ 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