Nuprl Lemma : int_formula_prop_eq_lemma

y,x,f:Top.  (int_formula_prop(f;x "=" y) int_term_value(f;x) int_term_value(f;y) ∈ ℤ)


Proof




Definitions occuring in Statement :  int_formula_prop: int_formula_prop(f;fmla) intformeq: left "=" right int_term_value: int_term_value(f;t) top: Top all: x:A. B[x] int: sqequal: t equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T int_formula_prop: int_formula_prop(f;fmla) intformeq: left "=" right int_formula_ind: int_formula_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\_formula\_prop(f;x  "="  y)  \msim{}  int\_term\_value(f;x)  =  int\_term\_value(f;y))



Date html generated: 2016_05_14-AM-07_07_40
Last ObjectModification: 2015_12_26-PM-01_08_33

Theory : omega


Home Index