Nuprl Lemma : can-apply-compose

[A,B,C:Type]. ∀[g:A ⟶ (B Top)]. ∀[f:B ⟶ (C Top)]. ∀[x:A].
  {(↑can-apply(g;x)) ∧ (↑can-apply(f;do-apply(g;x)))} supposing ↑can-apply(f g;x)


Proof




Definitions occuring in Statement :  p-compose: g do-apply: do-apply(f;x) can-apply: can-apply(f;x) assert: b uimplies: supposing a uall: [x:A]. B[x] top: Top guard: {T} and: P ∧ Q function: x:A ⟶ B[x] union: left right universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a guard: {T} subtype_rel: A ⊆B all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q band: p ∧b q ifthenelse: if then else fi  assert: b cand: c∧ B true: True prop: bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) bnot: ¬bb false: False top: Top
Lemmas referenced :  can-apply-compose-sq can-apply_wf bool_wf eqtt_to_assert assert_wf do-apply_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot false_wf assert_witness subtype_rel_union top_wf p-compose_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin sqequalRule extract_by_obid sqequalHypSubstitution isectElimination because_Cache hypothesisEquality hypothesis cumulativity functionExtensionality applyEquality lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination natural_numberEquality independent_pairFormation dependent_pairFormation promote_hyp dependent_functionElimination instantiate independent_functionElimination voidElimination independent_pairEquality lambdaEquality isect_memberEquality voidEquality functionEquality unionEquality universeEquality

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[g:A  {}\mrightarrow{}  (B  +  Top)].  \mforall{}[f:B  {}\mrightarrow{}  (C  +  Top)].  \mforall{}[x:A].
    \{(\muparrow{}can-apply(g;x))  \mwedge{}  (\muparrow{}can-apply(f;do-apply(g;x)))\}  supposing  \muparrow{}can-apply(f  o  g;x)



Date html generated: 2017_10_01-AM-09_13_34
Last ObjectModification: 2017_07_26-PM-04_48_56

Theory : general


Home Index