### Nuprl Lemma : imax_unfold

`∀[a,b:ℤ].  (imax(a;b) = if a ≤z b then b else a fi  ∈ ℤ)`

Proof

Definitions occuring in Statement :  imax: `imax(a;b)` le_int: `i ≤z j` ifthenelse: `if b then t else f fi ` uall: `∀[x:A]. B[x]` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` imax: `imax(a;b)` has-value: `(a)↓` uimplies: `b supposing a`
Lemmas referenced :  value-type-has-value int-value-type ifthenelse_wf le_int_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule callbyvalueReduce lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality independent_isectElimination hypothesis hypothesisEquality because_Cache isect_memberEquality axiomEquality

Latex:
\mforall{}[a,b:\mBbbZ{}].    (imax(a;b)  =  if  a  \mleq{}z  b  then  b  else  a  fi  )

Date html generated: 2016_05_13-PM-04_01_47
Last ObjectModification: 2015_12_26-AM-10_49_11

Theory : bool_1

Home Index