### Nuprl Lemma : pcs-to-integer-problem_wf

`∀[X:polynomial-constraints()]`
`  (pcs-to-integer-problem(X) ∈ ⋃n:ℕ.({L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List × ({L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List)))`

Proof

Definitions occuring in Statement :  pcs-to-integer-problem: `pcs-to-integer-problem(X)` polynomial-constraints: `polynomial-constraints()` length: `||as||` list: `T List` nat: `ℕ` tunion: `⋃x:A.B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` set: `{x:A| B[x]} ` product: `x:A × B[x]` add: `n + m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` pcs-to-integer-problem: `pcs-to-integer-problem(X)` all: `∀x:A. B[x]` implies: `P `` Q` polynomial-constraints: `polynomial-constraints()` has-value: `(a)↓` uimplies: `b supposing a` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` tunion: `⋃x:A.B[x]` nat: `ℕ` subtract: `n - m` top: `Top` sq_type: `SQType(T)` guard: `{T}` pi2: `snd(t)` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` or: `P ∨ Q` iPolynomial: `iPolynomial()` iMonomial: `iMonomial()` pi1: `fst(t)` pcs-mon-vars: `pcs-mon-vars(X)` not: `¬A` false: `False` cons: `[a / b]` exists: `∃x:A. B[x]` decidable: `Dec(P)` ge: `i ≥ j `
Lemmas referenced :  reverse_wf list_wf pcs-mon-vars_wf value-type-has-value list-value-type eager-map_wf iPolynomial_wf equal-wf-base set-value-type linearization_wf evalall-reduce list-valueall-type set-valueall-type int-valueall-type subtype_base_sq nat_wf set_subtype_base le_wf int_subtype_base add-associates add-swap length_wf add-commutes zero-add length_wf_nat equal-wf-base-T equal_wf polynomial-constraints_wf list_subtype_base member-reverse nil_wf member-pcs-mon-vars or_wf l_exists_wf l_member_wf pi1_wf iMonomial_wf pi2_wf list-cases length_of_nil_lemma null_nil_lemma btrue_wf member-implies-null-eq-bfalse btrue_neq_bfalse product_subtype_list length_of_cons_lemma subtract_wf non_neg_length nat_properties decidable__le
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin intEquality hypothesis hypothesisEquality lambdaFormation productElimination sqequalRule callbyvalueReduce independent_isectElimination setEquality because_Cache lambdaEquality baseApply closedConclusion baseClosed applyEquality imageMemberEquality dependent_pairEquality independent_pairEquality instantiate cumulativity natural_numberEquality isect_memberEquality voidElimination voidEquality dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination productEquality addEquality setElimination rename axiomEquality inlFormation unionElimination promote_hyp hypothesis_subsumption dependent_set_memberEquality dependent_pairFormation sqequalIntensionalEquality

Latex:
\mforall{}[X:polynomial-constraints()]
(pcs-to-integer-problem(X)  \mmember{}  \mcup{}n:\mBbbN{}.(\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List
\mtimes{}  (\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List)))

Date html generated: 2017_04_14-AM-09_04_40
Last ObjectModification: 2017_02_27-PM-03_44_14

Theory : omega

Home Index