rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> 
ext int by intro int
.
H >> int in 
by intro
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
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
.
H >> -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
.
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 
.