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

.`
H >> int in
by intro
`

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

.`
H >> c in int by intro
`

wherecmust be an integer constant.

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

* >>

.`
H >> int ext by intro op `

* >> int ext m

* >> int ext n

`
.
H >> in int by intro `

* >> m in int

* >> n in int

whereopmust be one of+,-,*,/, ormod.

.`
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 optionalnew name must be given ifxoccurs 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`

.`
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

whereaandbare canonicalint terms, and .

.`
H >> less(a;b;t;) = in T by reduce 1 `

* >> t= in T

whereaandbare canonicalint terms such thata < b.

.`
H >> less(a;b;t;) = in T by reduce 1 `

* >> = in T

whereaandbare canonicalint terms such that .

`
`

Thu Sep 14 08:45:18 EDT 1995