Nuprl Lemma : fpf-sub-val3

[A:Type]. ∀[B,C:A ⟶ Type].
  ∀eq:EqDecider(A). ∀f:a:A fp-> B[a]. ∀g:a:A fp-> C[a]. ∀x:A.
    ∀[P:a:A ⟶ B[a] ⟶ ℙ]. ∀[Q:a:A ⟶ C[a] ⟶ ℙ].
      ((∀x:A. ((C[x] ⊆B[x]) c∧ (P[x;g(x)]  Q[x;g(x)])) supposing ((↑x ∈ dom(f)) and (↑x ∈ dom(g))))
       {z != f(x) ==> P[y;z]  != g(x) ==> Q[y;z] supposing g ⊆ f})


Definitions occuring in Statement :  fpf-sub: f ⊆ g fpf-val: != f(x) ==> P[a; z] fpf-ap: f(x) fpf-dom: x ∈ dom(f) fpf: a:A fp-> B[a] deq: EqDecider(T) assert: b uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] cand: c∧ B prop: guard: {T} so_apply: x[s1;s2] so_apply: x[s] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  fpf-val: != f(x) ==> P[a; z] fpf-sub: f ⊆ g guard: {T} uall: [x:A]. B[x] all: x:A. B[x] implies:  Q uimplies: supposing a member: t ∈ T cand: c∧ B subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] top: Top prop: so_apply: x[s1;s2]
Lemmas referenced :  assert_witness fpf-dom_wf subtype-fpf2 top_wf assert_wf fpf-ap_wf all_wf equal_wf isect_wf subtype_rel_wf fpf_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation lambdaFormation cut introduction sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality productElimination independent_pairEquality extract_by_obid isectElimination cumulativity applyEquality functionExtensionality hypothesis independent_isectElimination isect_memberEquality voidElimination voidEquality because_Cache independent_functionElimination axiomEquality rename functionEquality productEquality universeEquality hyp_replacement equalitySymmetry applyLambdaEquality

\mforall{}[A:Type].  \mforall{}[B,C:A  {}\mrightarrow{}  Type].
    \mforall{}eq:EqDecider(A).  \mforall{}f:a:A  fp->  B[a].  \mforall{}g:a:A  fp->  C[a].  \mforall{}x:A.
        \mforall{}[P:a:A  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q:a:A  {}\mrightarrow{}  C[a]  {}\mrightarrow{}  \mBbbP{}].
                    ((C[x]  \msubseteq{}r  B[x])  c\mwedge{}  (P[x;g(x)]  {}\mRightarrow{}  Q[x;g(x)]))  supposing  ((\muparrow{}x  \mmember{}  dom(f))  and  (\muparrow{}x  \mmember{}  dom(g))))
            {}\mRightarrow{}  \{z  !=  f(x)  ==>  P[y;z]  {}\mRightarrow{}  z  !=  g(x)  ==>  Q[y;z]  supposing  g  \msubseteq{}  f\})

Date html generated: 2018_05_21-PM-09_24_11
Last ObjectModification: 2018_02_09-AM-10_19_33

Theory : finite!partial!functions

Home Index