Nuprl Lemma : binary_map_case-wf2

[X,T,Key:Type]. ∀[x:binary-map(T;Key)]. ∀[E:X]. ∀[F:key:Key
                                                     ─→ value:T
                                                     ─→ cnt:ℤ
                                                     ─→ left:binary-map(T;Key)
                                                     ─→ right:binary-map(T;Key)
                                                     ─→ X].
  (binary_map_case(x;E;key,value,cnt,left,right.F[key;value;cnt;left;right]) ∈ X)


Proof




Definitions occuring in Statement :  binary-map: binary-map(T;Key) binary_map_case: binary_map_case(m;E;key,value,cnt,left,right.F[key; value; cnt; left; right]) uall: [x:A]. B[x] so_apply: x[s1;s2;s3;s4;s5] member: t ∈ T function: x:A ─→ B[x] int: universe: Type
Lemmas :  binary_map-ext eq_atom_wf bool_wf eqtt_to_assert assert_of_eq_atom subtype_base_sq atom_subtype_base unit_wf2 unit_subtype_base it_wf eqff_to_assert equal_wf bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_atom bm_cnt_prop_T assert_wf bm_cnt_prop_wf binary-map_wf
\mforall{}[X,T,Key:Type].  \mforall{}[x:binary-map(T;Key)].  \mforall{}[E:X].  \mforall{}[F:key:Key
                                                                                                          {}\mrightarrow{}  value:T
                                                                                                          {}\mrightarrow{}  cnt:\mBbbZ{}
                                                                                                          {}\mrightarrow{}  left:binary-map(T;Key)
                                                                                                          {}\mrightarrow{}  right:binary-map(T;Key)
                                                                                                          {}\mrightarrow{}  X].
    (binary\_map\_case(x;E;key,value,cnt,left,right.F[key;value;cnt;left;right])  \mmember{}  X)



Date html generated: 2015_07_17-AM-08_18_39
Last ObjectModification: 2015_01_27-PM-00_40_13

Home Index