### Nuprl Lemma : ipolynomial-term_wf

`∀[p:iMonomial() List]. (ipolynomial-term(p) ∈ int_term())`

Proof

Definitions occuring in Statement :  ipolynomial-term: `ipolynomial-term(p)` iMonomial: `iMonomial()` int_term: `int_term()` list: `T List` uall: `∀[x:A]. B[x]` member: `t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` ipolynomial-term: `ipolynomial-term(p)` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` ifthenelse: `if b then t else f fi ` bfalse: `ff` iff: `P `⇐⇒` Q` not: `¬A` prop: `ℙ` rev_implies: `P `` Q` false: `False` or: `P ∨ Q` nil: `[]` cons: `[a / b]` subtype_rel: `A ⊆r B` iMonomial: `iMonomial()` so_lambda: `λ2x.t[x]` so_apply: `x[s]` int_nzero: `ℤ-o` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]`
Lemmas referenced :  null_wf iMonomial_wf bool_wf uiff_transitivity equal-wf-T-base assert_wf list_wf eqtt_to_assert assert_of_null itermConstant_wf iff_transitivity bnot_wf not_wf iff_weakening_uiff eqff_to_assert assert_of_bnot list-cases it_wf unit_wf2 nil_wf equal_wf product_subtype_list list_accum_wf int_term_wf subtype_rel_list subtype_rel_product int_nzero_wf sorted_wf subtype_rel_self imonomial-term_wf itermAdd_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis hypothesisEquality lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry baseClosed independent_functionElimination because_Cache productElimination independent_isectElimination natural_numberEquality independent_pairFormation impliesFunctionality voidElimination dependent_functionElimination promote_hyp hypothesis_subsumption productEquality intEquality applyEquality lambdaEquality setEquality setElimination rename independent_pairEquality axiomEquality

Latex:
\mforall{}[p:iMonomial()  List].  (ipolynomial-term(p)  \mmember{}  int\_term())

Date html generated: 2017_04_14-AM-08_58_00
Last ObjectModification: 2017_02_27-PM-03_41_02

Theory : omega

Home Index