Nuprl Lemma : int-decr-map-empty-prop
∀[Value:Type]. ∀[k:ℤ].  (¬↑int-decr-map-inDom(k;int-decr-map-empty()))
Proof
Definitions occuring in Statement : 
int-decr-map-empty: int-decr-map-empty()
, 
int-decr-map-inDom: int-decr-map-inDom(k;m)
, 
assert: ↑b
, 
uall: ∀[x:A]. B[x]
, 
not: ¬A
, 
int: ℤ
, 
universe: Type
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
not: ¬A
, 
implies: P 
⇒ Q
, 
false: False
, 
int-decr-map-empty: int-decr-map-empty()
, 
int-decr-map-inDom: int-decr-map-inDom(k;m)
, 
int-decr-map-find: int-decr-map-find(k;m)
, 
find-combine: find-combine(cmp;l)
, 
list_ind: list_ind, 
nil: []
, 
it: ⋅
, 
isl: isl(x)
, 
assert: ↑b
, 
ifthenelse: if b then t else f fi 
, 
bfalse: ff
, 
prop: ℙ
Latex:
\mforall{}[Value:Type].  \mforall{}[k:\mBbbZ{}].    (\mneg{}\muparrow{}int-decr-map-inDom(k;int-decr-map-empty()))
Date html generated:
2016_05_17-PM-01_48_35
Last ObjectModification:
2015_12_28-PM-08_50_38
Theory : datatype-signatures
Home
Index