Nuprl Lemma : int_term_value_mul_lemma

y,x,f:Top.  (int_term_value(f;x "*" y) int_term_value(f;x) int_term_value(f;y))


Proof




Definitions occuring in Statement :  int_term_value: int_term_value(f;t) itermMultiply: left "*" right top: Top all: x:A. B[x] multiply: m sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T int_term_value: int_term_value(f;t) itermMultiply: left "*" right int_term_ind: int_term_ind
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule

Latex:
\mforall{}y,x,f:Top.    (int\_term\_value(f;x  "*"  y)  \msim{}  int\_term\_value(f;x)  *  int\_term\_value(f;y))



Date html generated: 2016_05_14-AM-06_59_28
Last ObjectModification: 2015_12_26-PM-01_12_58

Theory : omega


Home Index