Nuprl Lemma : fpf-empty-join

[A:Type]. ∀[B:A ─→ Type]. ∀[f:a:A fp-> B[a]]. ∀[eq:EqDecider(A)].  (f ⊕ ⊗ f ∈ a:A fp-> B[a])


Proof




Definitions occuring in Statement :  fpf-join: f ⊕ g fpf-empty: fpf: a:A fp-> B[a] deq: EqDecider(T) uall: [x:A]. B[x] so_apply: x[s] function: x:A ─→ B[x] universe: Type equal: t ∈ T
Lemmas :  fpf_ap_pair_lemma filter_nil_lemma append_back_nil append-nil subtype_rel_list top_wf set_wf l_member_wf deq_wf fpf_wf deq-member_wf bool_wf equal-wf-T-base assert_wf bnot_wf not_wf iff_transitivity iff_weakening_uiff eqtt_to_assert assert-deq-member eqff_to_assert assert_of_bnot
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f:a:A  fp->  B[a]].  \mforall{}[eq:EqDecider(A)].    (f  \moplus{}  \motimes{}  =  f)



Date html generated: 2015_07_17-AM-09_19_07
Last ObjectModification: 2015_01_28-AM-07_50_32

Home Index