### Nuprl Lemma : int_term_value_wf

`∀[f:ℤ ⟶ ℤ]. ∀[t:int_term()].  (int_term_value(f;t) ∈ ℤ)`

Proof

Definitions occuring in Statement :  int_term_value: `int_term_value(f;t)` int_term: `int_term()` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` int_term_value: `int_term_value(f;t)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` so_apply: `x[s1;s2;s3;s4]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]`
Lemmas referenced :  int_term_ind_wf_simple int_term_wf subtract_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality hypothesisEquality lambdaEquality applyEquality addEquality hypothesis multiplyEquality minusEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache functionEquality

Latex:
\mforall{}[f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[t:int\_term()].    (int\_term\_value(f;t)  \mmember{}  \mBbbZ{})

Date html generated: 2016_05_14-AM-06_59_23
Last ObjectModification: 2015_12_26-PM-01_13_02

Theory : omega

Home Index