### Nuprl Lemma : equipollent-nat-list-as-product

`ℕ ~ k:ℕ × (ℕ^k)`

Proof

Definitions occuring in Statement :  power-type: `(T^k)` equipollent: `A ~ B` nat: `ℕ` product: `x:A × B[x]`
Definitions unfolded in proof :  exists: `∃x:A. B[x]` equipollent: `A ~ B` member: `t ∈ T` uall: `∀[x:A]. B[x]` nat: `ℕ` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` prop: `ℙ` subtype_rel: `A ⊆r B` power-type: `(T^k)` eq_int: `(i =z j)` bfalse: `ff` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` ge: `i ≥ j ` int_upper: `{i...}` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` so_lambda: `λ2x.t[x]` so_apply: `x[s]` pi1: `fst(t)` subtract: `n - m` inv_funs: `InvFuns(A;B;f;g)` tidentity: `Id{T}` identity: `Id` compose: `f o g` nequal: `a ≠ b ∈ T ` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  equipollent-nat-powered3 eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int false_wf le_wf it_wf subtype_rel_self equal-wf-base power-type_wf nat_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int int_upper_subtype_nat nat_properties nequal-le-implies zero-add coded-pair_wf subtract_wf int_upper_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_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_subtract_lemma int_term_value_var_lemma int_formula_prop_wf itermAdd_wf int_term_value_add_lemma biject_wf fun_with_inv_is_bij2 code-pair_wf exists_wf subtract-add-cancel inv_funs_wf add_nat_wf pi1_wf_top int_upper_wf set_subtype_base int_subtype_base add-associates add-swap add-commutes add-is-int-iff intformeq_wf int_formula_prop_eq_lemma decidable__equal_int add-subtract-cancel code-coded-pair assert_wf bnot_wf not_wf equal-wf-T-base bool_cases iff_transitivity iff_weakening_uiff assert_of_bnot equal-unit unit_wf2 nequal_wf coded-code-pair
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity productElimination thin dependent_pairFormation lambdaEquality isectElimination setElimination rename because_Cache hypothesis natural_numberEquality lambdaFormation unionElimination equalityElimination sqequalRule independent_isectElimination dependent_pairEquality dependent_set_memberEquality equalityTransitivity equalitySymmetry independent_pairFormation hypothesisEquality applyEquality intEquality baseClosed promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination voidElimination hypothesis_subsumption int_eqEquality isect_memberEquality voidEquality computeAll productEquality addEquality functionExtensionality functionEquality independent_pairEquality applyLambdaEquality pointwiseFunctionality baseApply closedConclusion hyp_replacement spreadEquality impliesFunctionality

Latex:
\mBbbN{}  \msim{}  k:\mBbbN{}  \mtimes{}  (\mBbbN{}\^{}k)

Date html generated: 2018_05_21-PM-08_14_47
Last ObjectModification: 2017_07_26-PM-05_49_30

Theory : general

Home Index