### Nuprl Lemma : norm-pair_wf

`∀[A:Type]. ∀[B:A ⟶ Type].`
`  (∀[Na:id-fun(A)]. ∀[Nb:⋂a:A. id-fun(B[a])].  (norm-pair(Na;Nb) ∈ id-fun(a:A × B[a]))) supposing `
`     ((∀a:A. value-type(B[a])) and `
`     value-type(A))`

Proof

Definitions occuring in Statement :  norm-pair: `norm-pair(Na;Nb)` id-fun: `id-fun(T)` value-type: `value-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` member: `t ∈ T` isect: `⋂x:A. B[x]` function: `x:A ⟶ B[x]` product: `x:A × B[x]` universe: `Type`
Definitions unfolded in proof :  guard: `{T}` and: `P ∧ Q` implies: `P `` Q` all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` so_apply: `x[s]` so_lambda: `λ2x.t[x]` prop: `ℙ` has-value: `(a)↓` norm-pair: `norm-pair(Na;Nb)` top: `Top` id-fun: `id-fun(T)` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  value-type_wf all_wf id-fun_wf and_wf subtype_rel-equal set_wf set-value-type equal_wf value-type-has-value top_wf
Rules used in proof :  universeEquality cumulativity because_Cache axiomEquality independent_functionElimination dependent_functionElimination productEquality applyLambdaEquality independent_pairFormation dependent_set_memberEquality dependent_pairEquality rename setElimination lambdaFormation functionEquality isectEquality equalitySymmetry equalityTransitivity applyEquality lambdaEquality independent_isectElimination hypothesisEquality setEquality isectElimination callbyvalueReduce productElimination thin hypothesis extract_by_obid voidEquality voidElimination isect_memberEquality functionExtensionality sqequalRule sqequalHypSubstitution cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
(\mforall{}[Na:id-fun(A)].  \mforall{}[Nb:\mcap{}a:A.  id-fun(B[a])].    (norm-pair(Na;Nb)  \mmember{}  id-fun(a:A  \mtimes{}  B[a])))  supposing
((\mforall{}a:A.  value-type(B[a]))  and
value-type(A))

Date html generated: 2018_07_25-PM-01_29_53
Last ObjectModification: 2018_07_14-PM-01_22_37

Theory : call!by!value_2

Home Index