Nuprl Lemma : can-apply-p-co-restrict

[A,B:Type]. ∀[f:A ⟶ (B Top)]. ∀[P:A ⟶ ℙ]. ∀[p:∀x:A. Dec(P[x])]. ∀[x:A].
  uiff(↑can-apply(p-co-restrict(f;p);x);(↑can-apply(f;x)) ∧ P[x]))


Proof




Definitions occuring in Statement :  p-co-restrict: p-co-restrict(f;p) can-apply: can-apply(f;x) assert: b decidable: Dec(P) uiff: uiff(P;Q) uall: [x:A]. B[x] top: Top prop: so_apply: x[s] all: x:A. B[x] not: ¬A and: P ∧ Q function: x:A ⟶ B[x] union: left right universe: Type
Definitions unfolded in proof :  p-co-restrict: p-co-restrict(f;p) uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] squash: T prop: true: True guard: {T} not: ¬A implies:  Q false: False all: x:A. B[x] top: Top rev_uimplies: rev_uimplies(P;Q) iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  can-apply-compose-iff iff_weakening_uiff decidable_wf all_wf p-co-restrict_wf uiff_wf p-compose_wf not_wf and_wf subtype_rel_union subtype_rel_dep_function assert_wf assert_witness can-apply-p-co-filter do-apply-p-co-filter top_wf true_wf squash_wf p-co-filter_wf do-apply_wf can-apply_wf assert_functionality_wrt_uiff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin lemma_by_obid isectElimination hypothesisEquality applyEquality because_Cache hypothesis sqequalRule lambdaEquality independent_isectElimination imageElimination equalityTransitivity equalitySymmetry functionEquality unionEquality natural_numberEquality imageMemberEquality baseClosed lambdaFormation independent_functionElimination voidElimination independent_pairEquality dependent_functionElimination productEquality cumulativity isect_memberEquality voidEquality universeEquality addLevel

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  (B  +  Top)].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[p:\mforall{}x:A.  Dec(P[x])].  \mforall{}[x:A].
    uiff(\muparrow{}can-apply(p-co-restrict(f;p);x);(\muparrow{}can-apply(f;x))  \mwedge{}  (\mneg{}P[x]))



Date html generated: 2016_05_15-PM-03_31_29
Last ObjectModification: 2016_01_16-AM-10_49_04

Theory : general


Home Index