### 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