Nuprl Lemma : int-decr-map-isEmpty-assert
∀[Value:Type]. ∀[m:int-decr-map-type(Value)].
uiff(↑int-decr-map-isEmpty(m);m = int-decr-map-empty() ∈ int-decr-map-type(Value))
Proof
Definitions occuring in Statement :
int-decr-map-isEmpty: int-decr-map-isEmpty(m),
int-decr-map-empty: int-decr-map-empty(),
int-decr-map-type: int-decr-map-type(Value),
assert: ↑b,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
universe: Type,
equal: s = t ∈ T
Definitions :
assert: ↑b,
ifthenelse: if b then t else f fi ,
int-decr-map-isEmpty: int-decr-map-isEmpty(m),
null: null(as),
int-decr-map-empty: int-decr-map-empty(),
nil: [],
it: ⋅,
btrue: tt,
true: True,
member: t ∈ T
Lemmas :
assert_of_null,
l-ordered_wf,
gt_wf,
assert_wf,
int-decr-map-isEmpty_wf,
assert_witness,
equal-wf-T-base,
int-decr-map-type_wf,
squash_wf,
sq_stable__l-ordered,
sq_stable__less_than,
member-less_than
\mforall{}[Value:Type]. \mforall{}[m:int-decr-map-type(Value)].
uiff(\muparrow{}int-decr-map-isEmpty(m);m = int-decr-map-empty())
Date html generated:
2015_07_17-AM-08_23_14
Last ObjectModification:
2015_04_02-PM-05_44_18
Home
Index