Nuprl Lemma : fpf-join-ap

[A:Type]. ∀[B:A ─→ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a]]. ∀[x:A].
  f ⊕ g(x) if x ∈ dom(f) then f(x) else g(x) fi  ∈ B[x] supposing ↑x ∈ dom(f ⊕ g)


Proof




Definitions occuring in Statement :  fpf-join: f ⊕ g fpf-ap: f(x) fpf-dom: x ∈ dom(f) fpf: a:A fp-> B[a] deq: EqDecider(T) assert: b ifthenelse: if then else fi  uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] function: x:A ─→ B[x] universe: Type equal: t ∈ T
Lemmas :  fpf-ap_wf fpf-join_wf assert_wf fpf-dom_wf top_wf subtype-fpf2 subtype_top deq_wf
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f,g:a:A  fp->  B[a]].  \mforall{}[x:A].
    f  \moplus{}  g(x)  =  if  x  \mmember{}  dom(f)  then  f(x)  else  g(x)  fi    supposing  \muparrow{}x  \mmember{}  dom(f  \moplus{}  g)



Date html generated: 2015_07_17-AM-09_19_59
Last ObjectModification: 2015_01_28-AM-07_48_54

Home Index