Nuprl Lemma : code-seq-bijection

Bij(ℕ;k:ℕ × (ℕk ⟶ ℕ);λx.coded-seq(x))


Proof




Definitions occuring in Statement :  coded-seq: coded-seq(x) biject: Bij(A;B;f) int_seg: {i..j-} nat: lambda: λx.A[x] function: x:A ⟶ B[x] product: x:A × B[x] natural_number: $n
Definitions unfolded in proof :  biject: Bij(A;B;f) and: P ∧ Q inject: Inj(A;B;f) all: x:A. B[x] implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] nat: surject: Surj(A;B;f) squash: T label: ...$L... t guard: {T} ge: i ≥  decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top true: True subtype_rel: A ⊆B iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  equal_wf nat_wf int_seg_wf coded-seq_wf code-seq_wf squash_wf true_wf code-coded-seq nat_properties decidable__equal_int satisfiable-full-omega-tt intformand_wf intformnot_wf intformeq_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_wf decidable__le intformle_wf itermConstant_wf int_formula_prop_le_lemma int_term_value_constant_lemma le_wf iff_weakening_equal coded-code-seq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation lambdaFormation cut sqequalHypSubstitution sqequalRule hypothesis introduction extract_by_obid isectElimination thin productEquality functionEquality natural_numberEquality setElimination rename because_Cache dependent_functionElimination hypothesisEquality applyLambdaEquality productElimination functionExtensionality applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality unionElimination independent_isectElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll dependent_set_memberEquality imageMemberEquality baseClosed independent_functionElimination dependent_pairEquality

Latex:
Bij(\mBbbN{};k:\mBbbN{}  \mtimes{}  (\mBbbN{}k  {}\mrightarrow{}  \mBbbN{});\mlambda{}x.coded-seq(x))



Date html generated: 2019_06_20-PM-02_40_50
Last ObjectModification: 2019_06_12-PM-00_28_42

Theory : num_thy_1


Home Index