### Nuprl Lemma : ring_term_polynomial

`∀r:CRng. ∀t:int_term().  ipolynomial-term(int_term_to_ipoly(t)) ≡ t`

Proof

Definitions occuring in Statement :  ringeq_int_terms: `t1 ≡ t2` crng: `CRng` int_term_to_ipoly: `int_term_to_ipoly(t)` ipolynomial-term: `ipolynomial-term(p)` int_term: `int_term()` all: `∀x:A. B[x]`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` iPolynomial: `iPolynomial()` crng: `CRng` so_apply: `x[s]` implies: `P `` Q` int_term_to_ipoly: `int_term_to_ipoly(t)` itermConstant: `"const"` int_term_ind: int_term_ind itermVar: `vvar` itermAdd: `left (+) right` prop: `ℙ` itermSubtract: `left (-) right` itermMultiply: `left (*) right` itermMinus: `"-"num` guard: `{T}` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` sq_type: `SQType(T)` false: `False` not: `¬A` ringeq_int_terms: `t1 ≡ t2` ring_term_value: `ring_term_value(f;t)` ipolynomial-term: `ipolynomial-term(p)` ifthenelse: `if b then t else f fi ` null: `null(as)` nil: `[]` it: `⋅` btrue: `tt` int-to-ring: `int-to-ring(r;n)` lt_int: `i <z j` bfalse: `ff` rng_nat_op: `n ⋅r e` mon_nat_op: `n ⋅ e` nat_op: `n x(op;id) e` itop: `Π(op,id) lb ≤ i < ub. E[i]` ycomb: `Y` grp_id: `e` pi1: `fst(t)` pi2: `snd(t)` add_grp_of_rng: `r↓+gp` rng_zero: `0` rng: `Rng` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` imonomial-term: `imonomial-term(m)` true: `True` and: `P ∧ Q` squash: `↓T` infix_ap: `x f y` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  int_term-induction ringeq_int_terms_wf ipolynomial-term_wf int_term_to_ipoly_wf iPolynomial_wf int_term_wf crng_wf decidable__equal_int subtype_base_sq int_subtype_base ring_term_value_wf itermConstant_wf rng_car_wf null_cons_lemma spread_cons_lemma list_accum_nil_lemma list_accum_cons_lemma ring_term_value_mul_lemma ring_term_value_const_lemma ring_term_value_var_lemma rng_times_wf rng_times_one equal_wf squash_wf true_wf int-to-ring-one subtype_rel_self iff_weakening_equal add-ipoly-ringeq add_ipoly_wf itermAdd_wf add-ipoly_wf1 uiff_transitivity add_ipoly-sq ringeq_int_terms_functionality ringeq_int_terms_weakening itermAdd_functionality_wrt_ringeq minus-poly-ringeq minus-poly_wf itermSubtract_wf itermMinus_wf ring_term_value_add_lemma ring_term_value_minus_lemma ring_term_value_sub_lemma rng_plus_wf rng_minus_wf ringeq_int_terms_transitivity itermMinus_functionality_wrt_ringeq mul-ipoly-ringeq mul_ipoly_wf itermMultiply_wf mul-ipoly_wf mul_poly-sq itermMultiply_functionality_wrt_ringeq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin sqequalRule lambdaEquality hypothesisEquality hypothesis applyEquality setElimination rename independent_functionElimination intEquality because_Cache dependent_functionElimination natural_numberEquality unionElimination instantiate cumulativity independent_isectElimination int_eqReduceFalseSq functionEquality isect_memberEquality voidElimination voidEquality productElimination imageElimination equalityTransitivity equalitySymmetry universeEquality imageMemberEquality baseClosed

Latex:
\mforall{}r:CRng.  \mforall{}t:int\_term().    ipolynomial-term(int\_term\_to\_ipoly(t))  \mequiv{}  t

Date html generated: 2018_05_21-PM-03_17_24
Last ObjectModification: 2018_05_19-AM-08_08_35

Theory : rings_1

Home Index