Nuprl Lemma : apply-2-partial

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


Definitions occuring in Statement :  partial: partial(T) value-type: value-type(T) has-value: (a)↓ is-exception: is-exception(t) uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] all: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q member: t ∈ T apply: a function: x:A ⟶ B[x] base: Base universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a guard: {T} member: t ∈ T and: P ∧ Q cand: c∧ B subtype_rel: A ⊆B all: x:A. B[x] implies:  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

          (\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