Nuprl Lemma : int_term_to_ipoly-add

[a,b:Top].  (int_term_to_ipoly(a (+) b) add_ipoly(int_term_to_ipoly(a);int_term_to_ipoly(b)))


Proof




Definitions occuring in Statement :  int_term_to_ipoly: int_term_to_ipoly(t) add_ipoly: add_ipoly(p;q) itermAdd: left (+) right uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  int_term_to_ipoly: int_term_to_ipoly(t) itermAdd: left (+) right int_term_ind: int_term_ind uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut sqequalAxiom extract_by_obid hypothesis sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality because_Cache

Latex:
\mforall{}[a,b:Top].    (int\_term\_to\_ipoly(a  (+)  b)  \msim{}  add\_ipoly(int\_term\_to\_ipoly(a);int\_term\_to\_ipoly(b)))



Date html generated: 2017_09_29-PM-05_55_28
Last ObjectModification: 2017_05_10-PM-04_16_28

Theory : omega


Home Index