### Nuprl Lemma : qmul-elim

`∀[r,s:ℚ].`
`  (r * s ~ if isint(r)`
`  then if isint(s) then r * s else let i,j = s in <r * i, j> fi `
`  else let p,q = r `
`       in if isint(s) then <p * s, q> else let i,j = s in <p * i, q * j> fi `
`  fi )`

Proof

Definitions occuring in Statement :  qmul: `r * s` rationals: `ℚ` ifthenelse: `if b then t else f fi ` bfalse: `ff` btrue: `tt` uall: `∀[x:A]. B[x]` isint: isint def spread: spread def pair: `<a, b>` multiply: `n * m` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` qmul: `r * s` uimplies: `b supposing a` callbyvalueall: callbyvalueall has-value: `(a)↓` has-valueall: `has-valueall(a)`
Lemmas referenced :  valueall-type-has-valueall rationals_wf rationals-valueall-type evalall-reduce
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis independent_isectElimination hypothesisEquality callbyvalueReduce because_Cache sqequalAxiom isect_memberEquality

Latex:
\mforall{}[r,s:\mBbbQ{}].
(r  *  s  \msim{}  if  isint(r)
then  if  isint(s)  then  r  *  s  else  let  i,j  =  s  in  <r  *  i,  j>  fi
else  let  p,q  =  r
in  if  isint(s)  then  <p  *  s,  q>  else  let  i,j  =  s  in  <p  *  i,  q  *  j>  fi
fi  )

Date html generated: 2016_05_15-PM-10_39_44
Last ObjectModification: 2015_12_27-PM-07_58_56

Theory : rationals

Home Index