Nuprl Lemma : int_term_value_subtract_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) itermSubtract: left "-" right top: Top all: x:A. B[x] subtract: m sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T int_term_value: int_term_value(f;t) itermSubtract: 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_31
Last ObjectModification: 2015_12_26-PM-01_12_54

Theory : omega


Home Index