Nuprl Lemma : type-separation

x,y:Base.
  (((x)↓ ∨ is-exception(x))
   ((y)↓ ∨ is-exception(y))
   (∀n,m:ℤ. ∀T:Type.  ((x n ∈ T)  (y m ∈ T)  (x y ∈ T)))
   (x y ∈ Base))


Proof




Definitions occuring in Statement :  has-value: (a)↓ is-exception: is-exception(t) all: x:A. B[x] implies:  Q or: P ∨ Q int: base: Base universe: Type equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] so_lambda: λ2x.t[x] subtype_rel: A ⊆B so_apply: x[s] or: P ∨ Q exists: x:A. B[x] and: P ∧ Q cand: c∧ B true: True bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) uimplies: supposing a ifthenelse: if then else fi  decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) false: False not: ¬A top: Top bfalse: ff sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b squash: T iff: ⇐⇒ Q rev_implies:  Q label: ...$L... t has-value: (a)↓
Lemmas referenced :  all_wf equal-wf-base int_subtype_base or_wf has-value_wf_base is-exception_wf base_wf has-value-implies-dec-isint imax_wf less_than_wf ifthenelse_wf le_int_wf bool_wf eqtt_to_assert assert_of_le_int decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermVar_wf itermAdd_wf itermConstant_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot le_wf squash_wf true_wf add_functionality_wrt_eq imax_unfold iff_weakening_equal intformeq_wf int_formula_prop_eq_lemma subtype_rel_self not_wf exists_wf and_wf exception-not-value value-type-has-value int-value-type EquatePairs_wf EquatePairs-equality equal_functionality_wrt_subtype_rel2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination cumulativity intEquality sqequalRule lambdaEquality universeEquality functionEquality hypothesisEquality applyEquality because_Cache unionElimination dependent_functionElimination baseClosed independent_functionElimination dependent_pairFormation addEquality natural_numberEquality independent_pairFormation productEquality equalityTransitivity equalitySymmetry equalityElimination productElimination independent_isectElimination int_eqEquality isect_memberEquality voidElimination voidEquality computeAll promote_hyp imageElimination imageMemberEquality baseApply closedConclusion sqequalIntensionalEquality dependent_set_memberEquality applyLambdaEquality setElimination rename isintReduceTrue inrFormation inlFormation

Latex:
\mforall{}x,y:Base.
    (((x)\mdownarrow{}  \mvee{}  is-exception(x))
    {}\mRightarrow{}  ((y)\mdownarrow{}  \mvee{}  is-exception(y))
    {}\mRightarrow{}  (\mforall{}n,m:\mBbbZ{}.  \mforall{}T:Type.    ((x  =  n)  {}\mRightarrow{}  (y  =  m)  {}\mRightarrow{}  (x  =  y)))
    {}\mRightarrow{}  (x  =  y))



Date html generated: 2017_10_01-AM-09_07_46
Last ObjectModification: 2017_07_26-PM-04_46_49

Theory : general


Home Index