Nuprl Lemma : test1

p:ℕ × ℕ. ∀bs:ℕ List.  (let x,y in y ∈ ℤ)


Proof




Definitions occuring in Statement :  list: List nat: all: x:A. B[x] member: t ∈ T spread: spread def product: x:A × B[x] add: m int:
Definitions unfolded in proof :  member: t ∈ T nat: uall: [x:A]. B[x] ge: i ≥  all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A top: Top and: P ∧ Q prop: subtype_rel: A ⊆B so_lambda: λ2y.t[x; y] so_apply: x[s1;s2]
Lemmas referenced :  spread_wf list_wf le_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermAdd_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut lemma_by_obid hypothesis dependent_set_memberEquality addEquality sqequalHypSubstitution setElimination thin rename hypothesisEquality isectElimination dependent_functionElimination natural_numberEquality unionElimination independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll because_Cache productEquality lambdaFormation applyEquality

Latex:
\mforall{}p:\mBbbN{}  \mtimes{}  \mBbbN{}.  \mforall{}bs:\mBbbN{}  List.    (let  x,y  =  p  in  x  +  y  \mmember{}  \mBbbZ{})



Date html generated: 2016_05_15-PM-07_46_04
Last ObjectModification: 2016_01_16-AM-09_34_02

Theory : general


Home Index