### 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 unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` int-decr-map-isEmpty: `int-decr-map-isEmpty(m)` int-decr-map-type: `int-decr-map-type(Value)` int-decr-map-empty: `int-decr-map-empty()` so_lambda: `λ2x y.t[x; y]` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` top: `Top` so_apply: `x[s1;s2]` gt: `i > j` prop: `ℙ` assert: `↑b` ifthenelse: `if b then t else f fi ` null: `null(as)` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` so_apply: `x[s1;s2;s3;s4]` strict4: `strict4(F)` implies: `P `` Q` has-value: `(a)↓` guard: `{T}` or: `P ∨ Q` squash: `↓T` nil: `[]` it: `⋅` btrue: `tt` true: `True` pi1: `fst(t)` sq_stable: `SqStable(P)`

Latex:
\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: 2016_05_17-PM-01_48_41
Last ObjectModification: 2016_01_18-PM-06_42_25

Theory : datatype-signatures

Home Index