Nuprl Lemma : code-coded-pair

n:ℕ(let a,b coded-pair(n) in code-pair(a;b) n ∈ ℤ)


Proof




Definitions occuring in Statement :  code-pair: code-pair(a;b) coded-pair: coded-pair(m) nat: all: x:A. B[x] spread: spread def int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] code-pair: code-pair(a;b) coded-pair: coded-pair(m) member: t ∈ T uall: [x:A]. B[x] implies:  Q has-value: (a)↓ uimplies: supposing a nat: so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B prop: top: Top guard: {T} ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A and: P ∧ Q subtract: m
Lemmas referenced :  tsqrt_wf nat_wf value-type-has-value set-value-type le_wf int-value-type subtract_wf triangular-num_wf equal_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_wf itermMultiply_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_term_value_mul_lemma int_formula_prop_wf minus-add minus-minus add-associates minus-one-mul add-swap add-commutes add-mul-special zero-mul zero-add add-zero
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis callbyvalueReduce independent_isectElimination intEquality lambdaEquality natural_numberEquality because_Cache equalityTransitivity equalitySymmetry setElimination rename applyEquality dependent_functionElimination independent_functionElimination isect_memberEquality voidElimination voidEquality dependent_set_memberEquality addEquality multiplyEquality minusEquality applyLambdaEquality unionElimination dependent_pairFormation int_eqEquality independent_pairFormation computeAll

Latex:
\mforall{}n:\mBbbN{}.  (let  a,b  =  coded-pair(n)  in  code-pair(a;b)  =  n)



Date html generated: 2019_06_20-PM-02_39_22
Last ObjectModification: 2019_06_12-PM-00_27_32

Theory : num_thy_1


Home Index