### Nuprl Lemma : fpf-all-join-decl

`∀[A:Type]`
`  ∀eq:EqDecider(A)`
`    ∀[P:x:A ─→ Type ─→ ℙ]`
`      ∀f,g:x:A fp-> Type.`
`        (∀y∈dom(f). w=f(y) ``  P[y;w] `` ∀y∈dom(g). w=g(y) ``  P[y;w] `` ∀y∈dom(f ⊕ g). w=f ⊕ g(y) ``  P[y;w])`

Proof

Definitions occuring in Statement :  fpf-all: `∀x∈dom(f). v=f(x) ``  P[x; v]` fpf-join: `f ⊕ g` fpf: `a:A fp-> B[a]` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ─→ B[x]` universe: `Type`
Lemmas :  fpf-join-dom2 fpf-join-ap-sq assert_wf fpf-dom_wf fpf-join_wf top_wf subtype-fpf2 subtype_top fpf-all_wf fpf_wf deq_wf bool_wf equal-wf-T-base bnot_wf not_wf eqtt_to_assert uiff_transitivity eqff_to_assert assert_of_bnot
\mforall{}[A:Type]
\mforall{}eq:EqDecider(A)
\mforall{}[P:x:A  {}\mrightarrow{}  Type  {}\mrightarrow{}  \mBbbP{}]
\mforall{}f,g:x:A  fp->  Type.
(\mforall{}y\mmember{}dom(f).  w=f(y)  {}\mRightarrow{}    P[y;w]
{}\mRightarrow{}  \mforall{}y\mmember{}dom(g).  w=g(y)  {}\mRightarrow{}    P[y;w]
{}\mRightarrow{}  \mforall{}y\mmember{}dom(f  \moplus{}  g).  w=f  \moplus{}  g(y)  {}\mRightarrow{}    P[y;w])

Date html generated: 2015_07_17-AM-11_14_00
Last ObjectModification: 2015_01_28-AM-07_41_57

Home Index