### Nuprl Lemma : qeq-elim

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

Proof

Definitions occuring in Statement :  rationals: `ℚ` qeq: `qeq(r;s)` ifthenelse: `if b then t else f fi ` eq_int: `(i =z j)` bfalse: `ff` btrue: `tt` uall: `∀[x:A]. B[x]` isint: isint def spread: spread def multiply: `n * m` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` qeq: `qeq(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{}].
(qeq(r;s)  \msim{}  if  isint(r)
then  if  isint(s)  then  (r  =\msubz{}  s)  else  let  i,j  =  s  in  (r  *  j  =\msubz{}  i)  fi
else  let  p,q  =  r
in  if  isint(s)  then  (p  =\msubz{}  s  *  q)  else  let  i,j  =  s  in  (p  *  j  =\msubz{}  i  *  q)  fi
fi  )

Date html generated: 2016_05_15-PM-10_39_48
Last ObjectModification: 2015_12_27-PM-07_58_48

Theory : rationals

Home Index