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
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
implies: P 
⇒ Q
, 
guard: {T}
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s1;s2]
, 
subtype_rel: A ⊆r B
, 
so_apply: x[s]
, 
prop: ℙ
, 
all: ∀x:A. B[x]
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]\}  \})
Date html generated:
2016_05_17-PM-01_37_42
Last ObjectModification:
2015_12_28-PM-08_11_23
Theory : binary-map
Home
Index