Nuprl Lemma : rP_to_term-int_term_to_rP

[t:int_term()]. ∀[s:int_term() List].  (rP_to_term(s;int_term_to_rP(t)) [t s])


Proof




Definitions occuring in Statement :  rP_to_term: rP_to_term(stack;L) int_term_to_rP: int_term_to_rP(t) int_term: int_term() cons: [a b] list: List uall: [x:A]. B[x] sqequal: t
Definitions unfolded in proof :  and: P ∧ Q cand: c∧ B uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a iPolynomial: iPolynomial() so_lambda: λ2x.t[x] int_seg: {i..j-} sq_stable: SqStable(P) implies:  Q lelt: i ≤ j < k squash: T guard: {T} all: x:A. B[x] so_apply: x[s] iMonomial: iMonomial() prop: int_nzero: -o subtype_rel: A ⊆B int_term_to_rP: int_term_to_rP(t) itermConstant: "const" int_term_ind: int_term_ind append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) top: Top so_apply: x[s1;s2;s3] rP_to_term: rP_to_term(stack;L) cons: [a b] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] itermVar: vvar itermAdd: left (+) right itermSubtract: left (-) right itermMultiply: left (*) right itermMinus: "-"num list_ind: list_ind spreadn: spread3 nil: [] it:
Lemmas referenced :  int_term_subtype_base list_subtype_base iPolynomial_wf set_subtype_base list_wf iMonomial_wf all_wf int_seg_wf length_wf imonomial-less_wf select_wf sq_stable__le less_than_transitivity2 le_weakening2 product_subtype_base int_nzero_wf sorted_wf subtype_rel_self nequal_wf int_subtype_base int_term_wf int_term-induction sqequal-wf-base list_ind_cons_lemma list_ind_nil_lemma spread_cons_lemma eager-append-is-append int_term_to_rP_wf subtype_rel_list top_wf cons_wf nil_wf append_assoc append_wf eager-append_wf append_back_nil
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity introduction extract_by_obid hypothesis independent_pairFormation sqequalHypSubstitution isectElimination thin independent_isectElimination sqequalRule lambdaEquality natural_numberEquality hypothesisEquality because_Cache setElimination rename independent_functionElimination productElimination imageMemberEquality baseClosed imageElimination dependent_functionElimination setEquality intEquality lambdaFormation isect_memberFormation sqequalAxiom baseApply closedConclusion applyEquality isect_memberEquality voidElimination voidEquality

Latex:
\mforall{}[t:int\_term()].  \mforall{}[s:int\_term()  List].    (rP\_to\_term(s;int\_term\_to\_rP(t))  \msim{}  [t  /  s])



Date html generated: 2017_09_29-PM-05_55_05
Last ObjectModification: 2017_07_26-PM-01_43_01

Theory : omega


Home Index