     Next: LESS Up: The Rules Previous: VOID

# INT

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* formation . H >> ext int by intro int . H >> int in by intro

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* canonical . H >> int ext c by intro c . H >> c in int by intro

where c must be an integer constant.

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* noncanonical . H >> -t in int
* >> t in int . H >> int ext by intro op
* >> int ext m
* >> int ext n . H >> in int by intro
* >> m in int
* >> n in int

where op must be one of +,-,*,/, or mod. . H,x:int, >> T ext ind(x;y,z. ; ;y,z. ) by elim x new z[,y]
* y:int,y<0,z:T[y+1/x]

>> T[y/x] ext * >> T[0/x] ext * y:int,0<y,z:T[y-1/x]

>> T[y/x] ext The optional new name must be given if x occurs free in . . H >> ind(e;x,y. ; ;x,y. ) in * by intro [over z.T] [new u,v]
* >> e in int
* u:int,u<0,v: >> in * >> in * u:int,0<u,v: >> in  . H >> int_eq(a;b;t; ) in T by intro
* >> a in int
* >> b in int
* a=b in int >> t in T
* (a=b in int)->void >> in T . H >> less(a;b;t; ) in T by intro
* >> a in int
* >> b in int
* a<b >> t in T
* (a<b)->void >> in T

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* computation  . H >> ind(nt;x,y. ; ;x,y. ) = t in T by reduce 1 down
* >> [nt,(ind(nt+1;x,y. ; ;x,y. ))/x,y] = t in T
* >> nt<0  . H >> ind(zt;x,y./ ; ;x,y. ) = t in T by reduce 1 base
* >> = t in T
* >> zt = 0 in int  . H >> ind(nt;x,y. ; ;x,y. ) = t in T by reduce 1 up
* >> [nt,(ind(nt-1;x,y. ; ;x,y. ))/x,y] = t in T
* >> 0<nt  . H >> int_eq(a;a;t; ) = in T by reduce 1
* >> t= in T  . H >> int_eq(a;b;t; ) = in T by reduce 1
* >> = in T

where a and b are canonical int terms, and .  . H >> less(a;b;t; ) = in T by reduce 1
* >> t= in T

where a and b are canonical int terms such that a < b.  . H >> less(a;b;t; ) = in T by reduce 1
* >> = in T

where a and b are canonical int terms such that .     Next: LESS Up: The Rules Previous: VOID

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995