Nuprl Lemma : ndiff_id_r

[a:ℕ]. ((a -- 0) a ∈ ℤ)


Proof




Definitions occuring in Statement :  ndiff: -- b nat: uall: [x:A]. B[x] natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  ndiff: -- b imax: imax(a;b) uall: [x:A]. B[x] has-value: (a)↓ member: t ∈ T uimplies: supposing a nat: all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top prop: bfalse: ff sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b
Lemmas referenced :  value-type-has-value int-value-type subtract_wf le_int_wf bool_wf eqtt_to_assert assert_of_le_int nat_properties decidable__equal_int satisfiable-full-omega-tt intformand_wf intformnot_wf intformeq_wf itermConstant_wf itermVar_wf intformle_wf itermSubtract_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_term_value_subtract_lemma int_formula_prop_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot le_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation cut callbyvalueReduce introduction extract_by_obid sqequalHypSubstitution isectElimination thin intEquality independent_isectElimination hypothesis setElimination rename hypothesisEquality natural_numberEquality because_Cache lambdaFormation unionElimination equalityElimination productElimination dependent_functionElimination dependent_pairFormation lambdaEquality int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll equalityTransitivity equalitySymmetry promote_hyp instantiate cumulativity independent_functionElimination

Latex:
\mforall{}[a:\mBbbN{}].  ((a  --  0)  =  a)



Date html generated: 2017_04_14-AM-09_14_50
Last ObjectModification: 2017_02_27-PM-03_52_47

Theory : int_2


Home Index