Nuprl Lemma : fpf-union-compatible-self

[A,C:Type]. ∀[B:A ─→ Type].
  ∀eq:EqDecider(A). ∀f:x:A fp-> B[x] List. ∀R:(C List) ─→ C ─→ 𝔹.  fpf-union-compatible(A;C;x.B[x];eq;R;f;f) 
  supposing ∀a:A. (B[a] ⊆C)


Proof




Definitions occuring in Statement :  fpf-union-compatible: fpf-union-compatible(A;C;x.B[x];eq;R;f;g) fpf: a:A fp-> B[a] deq: EqDecider(T) list: List bool: 𝔹 uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] function: x:A ─→ B[x] universe: Type
Lemmas :  select_wf fpf-ap_wf sq_stable__le select_member lelt_wf length_wf l_member_wf or_wf list_wf subtype_rel_list not_wf assert_wf fpf-dom_wf subtype-fpf2 top_wf subtype_top bool_wf fpf_wf deq_wf all_wf subtype_rel_wf
\mforall{}[A,C:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}eq:EqDecider(A).  \mforall{}f:x:A  fp->  B[x]  List.  \mforall{}R:(C  List)  {}\mrightarrow{}  C  {}\mrightarrow{}  \mBbbB{}.
        fpf-union-compatible(A;C;x.B[x];eq;R;f;f) 
    supposing  \mforall{}a:A.  (B[a]  \msubseteq{}r  C)



Date html generated: 2015_07_17-AM-09_16_53
Last ObjectModification: 2015_01_28-AM-07_51_46

Home Index