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