Nuprl Lemma : norm-union_wf

  (∀[Na:id-fun(A)]. ∀[Nb:id-fun(B)].  (norm-union(Na;Nb) ∈ id-fun(A B))) supposing (value-type(B) and value-type(A))


Definitions occuring in Statement :  norm-union: norm-union(Na;Nb) id-fun: id-fun(T) value-type: value-type(T) uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T union: left right universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a id-fun: id-fun(T) norm-union: norm-union(Na;Nb) so_lambda: λ2x.t[x] prop: so_apply: x[s] all: x:A. B[x] implies:  Q has-value: (a)↓
Lemmas referenced :  set_wf equal_wf value-type-has-value id-fun_wf value-type_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution functionExtensionality unionElimination thin sqequalRule applyEquality hypothesisEquality cumulativity extract_by_obid isectElimination lambdaEquality hypothesis lambdaFormation setElimination rename callbyvalueReduce independent_isectElimination inlEquality dependent_set_memberEquality equalityTransitivity equalitySymmetry unionEquality dependent_functionElimination independent_functionElimination inrEquality axiomEquality isect_memberEquality because_Cache universeEquality

    (\mforall{}[Na:id-fun(A)].  \mforall{}[Nb:id-fun(B)].    (norm-union(Na;Nb)  \mmember{}  id-fun(A  +  B)))  supposing 
          (value-type(B)  and 

Date html generated: 2017_04_14-AM-07_22_09
Last ObjectModification: 2017_02_27-PM-02_55_16

Theory : call!by!value_2

Home Index