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

[Value:Type]. ∀[k:ℤ]. ∀[u:ℤ × Value]. ∀[v:int-decr-map-type(Value)].
  (k ≤ (fst(u))) supposing ((↑int-decr-map-inDom(k;[u v])) and (∀y:ℤ × Value. ((y ∈ v)  ((fst(u)) > (fst(y))))))


Definitions occuring in Statement :  int-decr-map-inDom: int-decr-map-inDom(k;m) int-decr-map-type: int-decr-map-type(Value) l_member: (x ∈ l) cons: [a b] assert: b uimplies: supposing a uall: [x:A]. B[x] pi1: fst(t) gt: i > j le: A ≤ B all: x:A. B[x] implies:  Q product: x:A × B[x] int: universe: Type
Definitions unfolded in proof :  int-decr-map-type: int-decr-map-type(Value) member: t ∈ T uall: [x:A]. B[x] all: x:A. B[x] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q cand: c∧ B subtype_rel: A ⊆B gt: i > j prop: uimplies: supposing a guard: {T} so_lambda: λ2x.t[x] pi1: fst(t) so_apply: x[s] top: Top isl: isl(x) outl: outl(x) assert: b ifthenelse: if then else fi  btrue: tt or: P ∨ Q decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A bfalse: ff le: A ≤ B

\mforall{}[Value:Type].  \mforall{}[k:\mBbbZ{}].  \mforall{}[u:\mBbbZ{}  \mtimes{}  Value].  \mforall{}[v:int-decr-map-type(Value)].
    (k  \mleq{}  (fst(u)))  supposing 
          ((\muparrow{}int-decr-map-inDom(k;[u  /  v]))  and 
          (\mforall{}y:\mBbbZ{}  \mtimes{}  Value.  ((y  \mmember{}  v)  {}\mRightarrow{}  ((fst(u))  >  (fst(y))))))

Date html generated: 2016_05_17-PM-01_48_28
Last ObjectModification: 2016_01_17-AM-11_37_11

Theory : datatype-signatures

Home Index