Nuprl Lemma : int-decr-map-inDom-prop1

`∀[Value:Type]`
`  ∀k:ℤ. ∀m:int-decr-map-type(Value).`
`    (¬↑null(m)) ∧ (<k, outl(int-decr-map-find(k;m))> ∈ m) supposing ↑int-decr-map-inDom(k;m)`

Proof

Definitions occuring in Statement :  int-decr-map-inDom: `int-decr-map-inDom(k;m)` int-decr-map-find: `int-decr-map-find(k;m)` int-decr-map-type: `int-decr-map-type(Value)` l_member: `(x ∈ l)` null: `null(as)` outl: `outl(x)` assert: `↑b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` not: `¬A` and: `P ∧ Q` pair: `<a, b>` product: `x:A × B[x]` int: `ℤ` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` prop: `ℙ`

Latex:
\mforall{}[Value:Type]
\mforall{}k:\mBbbZ{}.  \mforall{}m:int-decr-map-type(Value).
(\mneg{}\muparrow{}null(m))  \mwedge{}  (<k,  outl(int-decr-map-find(k;m))>  \mmember{}  m)  supposing  \muparrow{}int-decr-map-inDom(k;m)

Date html generated: 2016_05_17-PM-01_48_22
Last ObjectModification: 2015_12_28-PM-08_50_52

Theory : datatype-signatures

Home Index