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

Proof

Definitions occuring in Statement :  qadd: `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` add: `n + m` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` qadd: `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  *  j)  +  i,  j>  fi
else  let  p,q  =  r
in  if  isint(s)  then  <p  +  (s  *  q),  q>  else  let  i,j  =  s  in  <(p  *  j)  +  (i  *  q),  q  *  j>  fi
fi  )

Date html generated: 2016_05_15-PM-10_39_42
Last ObjectModification: 2015_12_27-PM-07_58_53

Theory : rationals

Home Index