### Nuprl Lemma : mccarthy91-eq-91

`∀x:ℤ. (mccarthy91(x) = if (x) < (102)  then 91  else (x - 10) ∈ ℤ)`

Proof

Definitions occuring in Statement :  mccarthy91: `mccarthy91(x)` all: `∀x:A. B[x]` less: `if (a) < (b)  then c  else d` subtract: `n - m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` top: `Top` less_than: `a < b` and: `P ∧ Q` less_than': `less_than'(a;b)` uall: `∀[x:A]. B[x]` true: `True` squash: `↓T` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ`
Lemmas referenced :  mccarthy91-sqeq top_wf less_than_wf subtract_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis hypothesisEquality natural_numberEquality lessCases independent_pairFormation isectElimination baseClosed equalityTransitivity equalitySymmetry imageMemberEquality isect_memberFormation axiomSqEquality because_Cache imageElimination productElimination independent_functionElimination intEquality

Latex:
\mforall{}x:\mBbbZ{}.  (mccarthy91(x)  =  if  (x)  <  (102)    then  91    else  (x  -  10))

Date html generated: 2019_06_20-PM-01_19_07
Last ObjectModification: 2018_08_20-PM-09_31_13

Theory : int_2

Home Index