Nuprl Lemma : imax_unfold

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


Proof




Definitions occuring in Statement :  imax: imax(a;b) le_int: i ≤j ifthenelse: if then else fi  uall: [x:A]. B[x] int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T imax: imax(a;b) has-value: (a)↓ uimplies: 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