Q with no negatives

q.elf

int: type.
z: int.
s: int -> int.

0 = z.
1 = s 0.
2 = s 1.
3 = s 2.
4 = s 3.
5 = s 4.

<: int -> int -> type. %infix none 1 <.
ord/0: X < s X.
ord/1: X < (s Y)
	<- X < Y.

<>: int -> int -> type. %infix none 1 <>.
dis/0: X <> Y
	<- X < Y.
dis/1: X <> Y
	<- Y < X.

sum: int -> int -> int -> type.
sum/0: sum X z X.
sum/1: sum X (s Y) (s Z)
	<- sum X Y Z.

sub: int -> int -> int -> type.
sub/0: sub X z X.
sub/1: sub (s X) (s Y) Z
	<- sub X Y Z.

mult: int -> int -> int -> type.
mult/0: mult X z z.
mult/1: mult X (s Y) Z
	<- sum Z1 X Z
	<- mult X Y Z1.

float: type.
q: int -> int -> float.

qsum: float -> float -> float -> type.
qsum/0: qsum (q N1 D) (q N2 D) (q NR D)
	<- D <> 0
	<- sum N1 N2 NR.
qsum/1: qsum (q N1 D1) (q N2 D2) (q NR DR)
	<- D1 <> 0
	<- D2 <> 0
	<- D1 <> D2
	<- mult D1 D2 DR
	<- mult N1 D2 S1
	<- mult N2 D1 S2
	<- sum S1 S2 NR.

qmult: float -> float -> float -> type.
qmult/0: qmult (q N1 D1) (q N2 D2) (q NR DR)
	<- D1 <> 0
	<- D2 <> 0
	<- mult N1 N2 NR
	<- mult D1 D2 DR.

qdiv: float -> float -> float -> type.
qdiv/0: qdiv (q N1 D1) (q N2 D2) (q NR DR)
	<- D1 <> 0
	<- D2 <> 0
	<- qmult (q N1 D1) (q D2 N2) (q NR DR).