### Nuprl Lemma : fpf-join-list-ap-disjoint

`∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ─→ Type]. ∀[L:a:A fp-> B[a] List]. ∀[x:A].`
`  (∀[f:a:A fp-> B[a]]. (⊕(L)(x) = f(x) ∈ B[x]) supposing ((↑x ∈ dom(f)) and (f ∈ L))) supposing `
`     ((∀f,g∈L.  ∀x:A. (¬((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))))) and `
`     (↑x ∈ dom(⊕(L))))`

Proof

Definitions occuring in Statement :  fpf-join-list: `⊕(L)` fpf-ap: `f(x)` fpf-dom: `x ∈ dom(f)` fpf: `a:A fp-> B[a]` deq: `EqDecider(T)` pairwise: `(∀x,y∈L.  P[x; y])` l_member: `(x ∈ l)` list: `T List` assert: `↑b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` not: `¬A` and: `P ∧ Q` function: `x:A ─→ B[x]` universe: `Type` equal: `s = t ∈ T`
Lemmas :  fpf-join-list-ap assert_wf fpf-dom_wf subtype-fpf2 top_wf subtype_top l_member_wf fpf_wf pairwise_wf2 all_wf not_wf fpf-join-list_wf subtype_rel_list list_wf equal_wf fpf-ap_wf decidable__lt deq_wf true_wf squash_wf assert_functionality_wrt_uiff length_wf lelt_wf le_weakening less_than_transitivity2 sq_stable__le less_than_wf le_wf select_wf
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[L:a:A  fp->  B[a]  List].  \mforall{}[x:A].
(\mforall{}[f:a:A  fp->  B[a]].  (\moplus{}(L)(x)  =  f(x))  supposing  ((\muparrow{}x  \mmember{}  dom(f))  and  (f  \mmember{}  L)))  supposing
((\mforall{}f,g\mmember{}L.    \mforall{}x:A.  (\mneg{}((\muparrow{}x  \mmember{}  dom(f))  \mwedge{}  (\muparrow{}x  \mmember{}  dom(g)))))  and
(\muparrow{}x  \mmember{}  dom(\moplus{}(L))))

Date html generated: 2015_07_17-AM-09_21_17
Last ObjectModification: 2015_07_16-AM-09_51_28

Home Index