### Nuprl Lemma : fpf-compatible-join-iff

`∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ─→ Type]. ∀[f,g,h:a:A fp-> B[a]].`
`  uiff(h || f ⊕ g;h || f ∧ h || g) supposing f || g`

Proof

Definitions occuring in Statement :  fpf-join: `f ⊕ g` fpf-compatible: `f || g` fpf: `a:A fp-> B[a]` deq: `EqDecider(T)` uiff: `uiff(P;Q)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` and: `P ∧ Q` function: `x:A ─→ B[x]` universe: `Type`
Lemmas :  assert_wf fpf-dom_wf subtype-fpf2 top_wf subtype_top fpf-compatible_wf fpf-join_wf fpf-compatible-join fpf_wf deq_wf fpf-join-dom fpf-join-ap-left iff_weakening_equal fpf-join-ap bool_cases subtype_base_sq bool_wf bool_subtype_base eqtt_to_assert eqff_to_assert assert_of_bnot
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f,g,h:a:A  fp->  B[a]].
uiff(h  ||  f  \moplus{}  g;h  ||  f  \mwedge{}  h  ||  g)  supposing  f  ||  g

Date html generated: 2015_07_17-AM-11_12_13
Last ObjectModification: 2015_02_04-PM-05_06_51

Home Index