Nuprl Lemma : fpf-cap-compatible

[X:Type]. ∀[eq:EqDecider(X)]. ∀[f,g:x:X fp-> Type]. ∀[x:X].
  (f(x)?Void g(x)?Void ∈ Type) supposing (g(x)?Void and f(x)?Void and || g)


Definitions occuring in Statement :  fpf-compatible: || g fpf-cap: f(x)?z fpf: a:A fp-> B[a] deq: EqDecider(T) uimplies: supposing a uall: [x:A]. B[x] void: Void universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B all: x:A. B[x] top: Top fpf-compatible: || g implies:  Q and: P ∧ Q cand: c∧ B bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff fpf-cap: f(x)?z
Lemmas referenced :  fpf-compatible_wf fpf_wf deq_wf fpf-cap_wf fpf-dom_wf subtype-fpf2 top_wf bool_wf fpf-ap_wf equal-wf-T-base assert_wf bnot_wf not_wf eqtt_to_assert uiff_transitivity eqff_to_assert assert_of_bnot equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality axiomEquality hypothesis because_Cache equalityTransitivity equalitySymmetry instantiate extract_by_obid cumulativity lambdaEquality universeEquality voidEquality applyEquality independent_isectElimination lambdaFormation voidElimination dependent_functionElimination independent_functionElimination independent_pairFormation baseClosed unionElimination equalityElimination productElimination

\mforall{}[X:Type].  \mforall{}[eq:EqDecider(X)].  \mforall{}[f,g:x:X  fp->  Type].  \mforall{}[x:X].
    (f(x)?Void  =  g(x)?Void)  supposing  (g(x)?Void  and  f(x)?Void  and  f  ||  g)

Date html generated: 2018_05_21-PM-09_20_51
Last ObjectModification: 2018_02_09-AM-10_17_59

Theory : finite!partial!functions

Home Index