Nuprl Lemma : coded-pair_wf

[n:ℕ]. (coded-pair(n) ∈ ℕ × ℕ)


Proof




Definitions occuring in Statement :  coded-pair: coded-pair(m) nat: uall: [x:A]. B[x] member: t ∈ T product: x:A × B[x]
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] subtype_rel: A ⊆B and: P ∧ Q squash: T prop: true: True guard: {T} iff: ⇐⇒ Q implies:  Q ge: i ≥  all: x:A. B[x] le: A ≤ B decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top less_than: a < b uiff: uiff(P;Q)
Lemmas referenced :  false_wf int_term_value_add_lemma int_formula_prop_less_lemma itermAdd_wf intformless_wf add-is-int-iff int_formula_prop_wf int_term_value_var_lemma int_term_value_subtract_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermSubtract_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties iff_weakening_equal triangular-num-add1 true_wf squash_wf less_than_wf tsqrt-property triangular-num_wf subtract_wf tsqrt_wf int-value-type le_wf set-value-type nat_wf value-type-has-value
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule callbyvalueReduce lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis independent_isectElimination intEquality lambdaEquality natural_numberEquality hypothesisEquality because_Cache setElimination rename applyEquality axiomEquality equalityTransitivity equalitySymmetry productElimination independent_pairFormation imageElimination imageMemberEquality baseClosed universeEquality independent_functionElimination promote_hyp independent_pairEquality dependent_set_memberEquality dependent_functionElimination unionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality computeAll pointwiseFunctionality baseApply closedConclusion

Latex:
\mforall{}[n:\mBbbN{}].  (coded-pair(n)  \mmember{}  \mBbbN{}  \mtimes{}  \mBbbN{})



Date html generated: 2019_06_20-PM-02_38_57
Last ObjectModification: 2019_06_12-PM-00_27_12

Theory : num_thy_1


Home Index