Nuprl Lemma : rec-bind-class_wf

[Info,A,B:Type]. ∀[X:A ─→ EClass(B)]. ∀[Y:A ─→ EClass(A)].
  rec-bind-class(X;Y) ∈ A ─→ EClass(B) supposing not-self-starting{i:l}(Info;A;Y)


Proof




Definitions occuring in Statement :  rec-bind-class: rec-bind-class(X;Y) not-self-starting: not-self-starting{i:l}(Info;A;Y) eclass: EClass(A[eo; e]) uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T function: x:A ─→ B[x] universe: Type
Lemmas :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf length_wf es-E_wf Id_wf es-loc_wf es-le-before_wf event-ordering+_wf event-ordering+_subtype decidable__le subtract_wf false_wf not-ge-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel nat_wf non_neg_length length_wf_nat void_wf not-self-starting_wf eclass_wf es-le-before_wf2 list-subtype-bag es-le_wf bag_wf bag-append_wf bag-combine-member-wf bag-combine_wf eo-forward-le-before list-subtype l_member_wf squash_wf true_wf list_wf iff_weakening_equal member_filter_2 subtype_rel_list es-ble_wf assert-es-ble member-es-le-before subtype_rel_sets eo-forward_wf member-eo-forward-E equal_wf sq_stable_from_decidable decidable__es-le eo-forward-le2 equal-eo-forward-E es-le-self and_wf member_wf classrel_wf es-le_weakening length-filter le_wf length-filter-decreases l_exists_iff set_wf not_wf assert_wf eo-forward-loc es-le-loc es-locl_transitivity2 es-locl_irreflexivity eo-forward-le decidable__lt filter_wf5 eo-forward-E-subtype member-es-le-before2 bag-member_wf

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:A  {}\mrightarrow{}  EClass(B)].  \mforall{}[Y:A  {}\mrightarrow{}  EClass(A)].
    rec-bind-class(X;Y)  \mmember{}  A  {}\mrightarrow{}  EClass(B)  supposing  not-self-starting\{i:l\}(Info;A;Y)



Date html generated: 2015_07_21-PM-03_13_10
Last ObjectModification: 2015_02_04-PM-06_23_33

Home Index