Nuprl Lemma : p-conditional-domain

[A,B:Type].  ∀f,g:A ⟶ (B Top). ∀x:A.  (↑can-apply([f?g];x) ⇐⇒ (↑can-apply(f;x)) ∨ (↑can-apply(g;x)))


Proof




Definitions occuring in Statement :  p-conditional: [f?g] can-apply: can-apply(f;x) assert: b uall: [x:A]. B[x] top: Top all: x:A. B[x] iff: ⇐⇒ Q or: P ∨ Q function: x:A ⟶ B[x] union: left right universe: Type
Definitions unfolded in proof :  can-apply: can-apply(f;x) p-conditional: [f?g] uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T isl: isl(x) rev_implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) uimplies: supposing a ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False
Lemmas referenced :  istype-assert ifthenelse_wf btrue_wf bfalse_wf top_wf eqtt_to_assert eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot assert_witness istype-top bool_cases assert_of_bnot
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation_alt lambdaFormation_alt independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin applyEquality hypothesisEquality inhabitedIsType hypothesis unionElimination equalityIstype equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination unionEquality because_Cache equalityElimination productElimination independent_isectElimination dependent_pairFormation_alt promote_hyp instantiate cumulativity voidElimination unionIsType functionIsType inlFormation_alt inrFormation_alt

Latex:
\mforall{}[A,B:Type].
    \mforall{}f,g:A  {}\mrightarrow{}  (B  +  Top).  \mforall{}x:A.    (\muparrow{}can-apply([f?g];x)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}can-apply(f;x))  \mvee{}  (\muparrow{}can-apply(g;x)))



Date html generated: 2020_05_20-AM-08_06_11
Last ObjectModification: 2019_12_26-PM-04_07_22

Theory : general


Home Index