Nuprl Lemma : coded-code-pair

[a,b:ℕ].  (coded-pair(code-pair(a;b)) = <a, b> ∈ (ℕ × ℕ))


Proof




Definitions occuring in Statement :  code-pair: code-pair(a;b) coded-pair: coded-pair(m) nat: uall: [x:A]. B[x] pair: <a, b> product: x:A × B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T coded-pair: coded-pair(m) has-value: (a)↓ uimplies: supposing a nat: so_lambda: λ2x.t[x] so_apply: x[s] code-pair: code-pair(a;b) ge: i ≥  all: x:A. B[x] decidable: Dec(P) or: P ∨ Q 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 guard: {T} uiff: uiff(P;Q) sq_type: SQType(T) cand: c∧ B squash: T le: A ≤ B true: True iff: ⇐⇒ Q rev_implies:  Q subtract: m
Lemmas referenced :  value-type-has-value nat_wf set-value-type le_wf int-value-type code-pair_wf tsqrt_wf triangular-num_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_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_formula_prop_wf add_nat_wf add-is-int-iff intformeq_wf int_formula_prop_eq_lemma false_wf equal_wf subtract_wf subtype_base_sq set_subtype_base int_subtype_base tsqrt-unique decidable__equal_int less_than_wf squash_wf true_wf triangular-num-add1 iff_weakening_equal decidable__lt intformless_wf int_formula_prop_less_lemma add-associates minus-one-mul add-swap minus-one-mul-top add-commutes add-mul-special zero-mul add-zero minus-add minus-minus zero-add
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule callbyvalueReduce extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis independent_isectElimination intEquality lambdaEquality natural_numberEquality hypothesisEquality dependent_set_memberEquality addEquality setElimination rename because_Cache dependent_functionElimination unionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll applyEquality lambdaFormation equalityTransitivity equalitySymmetry applyLambdaEquality pointwiseFunctionality promote_hyp baseApply closedConclusion baseClosed productElimination independent_functionElimination axiomEquality instantiate cumulativity imageElimination imageMemberEquality universeEquality independent_pairEquality minusEquality

Latex:
\mforall{}[a,b:\mBbbN{}].    (coded-pair(code-pair(a;b))  =  <a,  b>)



Date html generated: 2019_06_20-PM-02_39_14
Last ObjectModification: 2019_06_12-PM-00_27_27

Theory : num_thy_1


Home Index