int 2 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Old and New versions of int_2 proofs exemplifying differences mentioned in int 2 differences.

OLDNEW
mul preserves leThm* a,b:, n:. ab  nanb
mul preserves ltThm* a,b:, n:. a<b  na<nb
mul cancel in leThm* a,b:, n:. nanb  ab
mul cancel in eqThm* a,b:, n:. na = nb  a = b
int entireThm* a,b:. ab = 0  a = 0  b = 0
int entire aThm* a,b:. a  0  b  0  ab  0
neg mul arg boundsThm* a,b:. ab<0  a<0 & b>0  a>0 & b<0
multiply nat wfThm* i,j:. ij  
absval negThm* i:{...0}. |i| = -i
absval zeroThm* i:. |i| = 0  i = 0
absval lboundThm* i:, n:. |i|>n  i<-n  i>n
absval eqThm* x,y:. |x| = |y|  x =  y
absval elimThm* P:(Prop). (x:. P(|x|))  (x:. P(x))
minus iminThm* a,b:. -imin(a;b) = imax(-a;-b)
imax assocThm* a,b,c:. imax(a;imax(b;c)) = imax(imax(a;b);c)
imin add rThm* a,b,c:. imin(a;b)+c = imin(a+c;b+c)
imin ubThm* a,b,c:. aimin(b;c)  ab & ac
ndiff ndiffThm* a,b:, c:. ((a -- b) -- c) = (a -- (b+c))
ndiff ndiff eq iminThm* a,b:. (a -- (a -- b)) = imin(a;b)
ndiff add eq imaxThm* a,b:. (a -- b)+b = imax(a;b)
rem to divThm* a:, n:. (a rem n) = a-(a  n)n
rem symThm* a:, b:. (a rem -b) = (a rem b)
rem antisymThm* a:, b:. ((-a) rem b) = -(a rem b)
div 2 to 1Thm* a:{...0}, b:. (a  b) = -((-a)  b)
div 3 to 1Thm* a:{...0}, b:{...-1}. (a  b) = ((-a)  (-b))
div 4 to 1Thm* a:, b:{...-1}. (a  b) = -(a  (-b))
rem 2 to 1Thm* a:{...0}, n:. (a rem n) = -((-a) rem n)
rem 3 to 1Thm* a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n)
rem 4 to 1Thm* a:, n:{...-1}. (a rem n) = (a rem -n)
rem bounds zThm* a:, b:. |a rem b|<|b|
div bounds 1Thm* a:, n:. 0(a  n)
div fun sat div nrelThm* a:, n:. Div(a;n;a  n)
div uniqueThm* a:, n:, p,q:. Div(a;n;p)  Div(a;n;q)  p = q
div lbound 1Thm* a:, n:, k:. k(a  n)  kna
rem fun sat rem nrelThm* a:, n:. Rem(a;n;a rem n)
div base caseThm* a:, n:. a<n  (a  n) = 0
div rec caseThm* a:, n:. an  (a  n) = ((a-n)  n)+1
rem base caseThm* a:, n:. a<n  (a rem n) = a
rem gen base caseThm* a:, n:. |a|<|n|  (a rem n) = a
rem rec caseThm* a:, n:. an  (a rem n) = ((a-n) rem n)
rem invariantThm* a,b:, n:. ((a+bn) rem n) = (a rem n)
rem additionThm* i,j:, n:. (((i rem n)+(j rem n)) rem n) = ((i+j) rem n)
rem rem to remThm* a:, n:. ((a rem n) rem n) = (a rem n)
rem eq args zThm* a:, b:. |a| = |b|  (a rem b) = 0
modulus wfThm* a:, n:. (a mod n)  
mod boundsThm* a:, n:. 0(a mod n) & (a mod n)<n
div floor mod sumThm* a:, n:. a = (a  n)n+(a mod n)
int upper well foundedThm* n:. WellFnd{i}({n...};x,y.x<y)
int lower well foundedThm* n:. WellFnd{i}({...n};x,y.x>y)
int seg well founded downThm* i:, j:{i...}. WellFnd{u}({i..j};x,y.x>y)
decidable ex int segThm* i,j:, F:({i..j}Prop). (k:{i..j}. Dec(F(k)))  Dec(k:{i..j}. F(k))
decidable all int segThm* i,j:, F:({i..j}Prop). (k:{i..j}. Dec(F(k)))  Dec(k:{i..j}. F(k))
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

int 2 Sections StandardLIB Doc