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
Lemmas :  l-ordered-cons l-ordered_wf gt_wf int-decr-map-inDom-prop1 int-decr-map-inDom-prop int-decr-map-find_wf not_wf assert_wf null_wf3 subtype_rel_set list_wf top_wf subtype_rel_list l_member_wf squash_wf l_all_wf2 equal-wf-base-T int_subtype_base cons_member le_weakening and_wf equal_wf pi1_wf_top subtype_rel_product le_wf le_weakening2 true_wf false_wf less_than_wf int-decr-map-inDom_wf cons_wf all_wf int-decr-map-type_wf
\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: 2015_07_17-AM-08_23_05
Last ObjectModification: 2015_04_02-PM-05_44_10

Home Index