### Nuprl Lemma : fpf-join-ap-sq

`∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> Top]. ∀[g:Top]. ∀[x:A].  (f ⊕ g(x) ~ if x ∈ dom(f) then f(x) else g(x) fi )`

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)` ifthenelse: `if b then t else f fi ` uall: `∀[x:A]. B[x]` top: `Top` universe: `Type` sqequal: `s ~ t`
Definitions unfolded in proof :  fpf-ap: `f(x)` fpf-join: `f ⊕ g` pi2: `snd(t)` fpf-cap: `f(x)?z` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` ifthenelse: `if b then t else f fi ` bfalse: `ff` prop: `ℙ`
Lemmas referenced :  fpf-dom_wf bool_wf equal-wf-T-base assert_wf bnot_wf not_wf top_wf fpf_wf deq_wf eqtt_to_assert uiff_transitivity eqff_to_assert assert_of_bnot equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalRule cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality hypothesis because_Cache equalityTransitivity equalitySymmetry baseClosed lambdaEquality universeEquality isect_memberFormation sqequalAxiom isect_memberEquality lambdaFormation unionElimination equalityElimination productElimination independent_isectElimination independent_functionElimination dependent_functionElimination

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f:a:A  fp->  Top].  \mforall{}[g:Top].  \mforall{}[x:A].
(f  \moplus{}  g(x)  \msim{}  if  x  \mmember{}  dom(f)  then  f(x)  else  g(x)  fi  )

Date html generated: 2018_05_21-PM-09_21_50
Last ObjectModification: 2018_02_09-AM-10_18_30

Theory : finite!partial!functions

Home Index