Nuprl Lemma : apply-2-partial

∀[A,B,C:Type].
  (∀[f:Base]
     (∀[a:partial(A)]. ∀[b:partial(B)].  (f a b ∈ partial(C))) supposing 
        ((∀a:partial(A). ∀b:partial(B).  ((f a b)↓ ⇒ ((a)↓ ∧ (b)↓))) and 
        (∀a:partial(A). ∀b:partial(B).  (((¬is-exception(a)) ∧ (¬is-exception(b))) ⇒ (¬is-exception(f a b)))) and 
        (f ∈ A ⟶ B ⟶ C))) supposing 
     (value-type(C) and 
     (value-type(B) ∧ (B ⊆r Base)) and 
     (value-type(A) ∧ (A ⊆r Base)))


Proof



Definitions occuring in Statement :  partial: partial(T),  value-type: value-type(T),  has-value: (a)↓,  is-exception: is-exception(t),  uimplies: b supposing a,  subtype_rel: A ⊆r B,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  not: ¬A,  implies: P ⇒ Q,  and: P ∧ Q,  member: t ∈ T,  apply: f a,  function: x:A ⟶ B[x],  base: Base,  universe: Type
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  uimplies: b supposing a,  guard: {T},  member: t ∈ T,  and: P ∧ Q,  cand: A c∧ B,  subtype_rel: A ⊆r B,  all: ∀x:A. B[x],  implies: P ⇒ Q,  prop: ℙ,  not: ¬A,  false: False
Lemmas referenced :  partial-base,  subtype_rel_partial,  base_wf,  subtype_rel_transitivity,  partial_wf,  base-member-partial,  has-value_wf_base,  has-value_wf-partial,  not_wf,  is-exception_wf,  istype-universe,  value-type_wf,  subtype_rel_wf,  termination,  partial-not-exception
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  Error :isect_memberFormation_alt,  cut,  introduction,  extract_by_obid,  hypothesis,  sqequalHypSubstitution,  isectElimination,  thin,  hypothesisEquality,  independent_isectElimination,  productElimination,  because_Cache,  sqequalRule,  baseApply,  closedConclusion,  baseClosed,  applyEquality,  Error :universeIsType,  Error :functionIsType,  Error :productIsType,  Error :equalityIsType4,  Error :inhabitedIsType,  universeEquality,  axiomEquality,  equalityTransitivity,  equalitySymmetry,  dependent_functionElimination,  independent_functionElimination,  Error :lambdaFormation_alt,  Error :equalityIsType1,  independent_pairFormation,  voidElimination
Latex:
\mforall{}[A,B,C:Type].
    (\mforall{}[f:Base]
          (\mforall{}[a:partial(A)].  \mforall{}[b:partial(B)].    (f  a  b  \mmember{}  partial(C)))  supposing 
                ((\mforall{}a:partial(A).  \mforall{}b:partial(B).    ((f  a  b)\mdownarrow{}  {}\mRightarrow{}  ((a)\mdownarrow{}  \mwedge{}  (b)\mdownarrow{})))  and 
                (\mforall{}a:partial(A).  \mforall{}b:partial(B).
                      (((\mneg{}is-exception(a))  \mwedge{}  (\mneg{}is-exception(b)))  {}\mRightarrow{}  (\mneg{}is-exception(f  a  b))))  and 
                (f  \mmember{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C)))  supposing 
          (value-type(C)  and 
          (value-type(B)  \mwedge{}  (B  \msubseteq{}r  Base))  and 
          (value-type(A)  \mwedge{}  (A  \msubseteq{}r  Base)))


Date html generated: 2019_06_20-PM-00_34_15
Last ObjectModification: 2018_10_06-PM-05_10_42

Theory : partial_1


Home Index