collatz.elf

nat: type.
z: nat.
s: nat -> nat.

0 = z.
1 = s 0.
2 = s 1.
3 = s 2.
4 = s 3.
5 = s 4.
6 = s 5.
7 = s 6.
8 = s 7.
9 = s 8.
10 = s 9.

<: nat -> nat -> type. %infix none 1 <.
</0: X < s X.
</1: X < s Y
	<- X < Y.

!=: nat -> nat -> type. %infix none 1 !=.
!=/0: X != Y
	<- X < Y.
!=/1: X != Y
	<- Y < X.

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

mult: nat -> nat -> nat -> type.
mult/0: mult X 0 0.
mult/1: mult X (s 0) X.
mult/2: mult X (s Y) Z
	<- Y != 0
	<- sum Z1 X Z
	<- mult X Y Z1.

div: nat -> nat -> nat -> type.
div/0: div X 1 X.
div/1: div 0 X 0
	<- X != 0
	<- X != 1.
div/2: div X Y (s Z)
	<- Y != 0
	<- Y != 1
	<- sum X1 Y X
	<- div X1 Y Z.

bool: type.
true: bool.
false: bool.

not: bool -> bool -> type.
not/0: not true false.
not/1: not false true.

is_even: nat -> bool -> type.
is_even/0: is_even 0 true.
is_even/1: is_even (s X) Y
	<- not Y Z
	<- is_even X Z.

collatz: nat -> nat -> type.
collatz/0: collatz 1 0.
collatz/1: collatz X (s Y)
	<- X != 1
	<- is_even X true
	<- div X 2 Z
	<- collatz Z Y.
collatz/2: collatz X (s Y)
	<- X != 1
	<- is_even X false
	<- mult X 3 X1
	<- sum X1 1 Z
	<- collatz Z Y.

list: type.
*: list.
;: nat -> list -> list. %infix none 1 ;.

collatz_seq: nat -> list -> type.
collatz_seq/0: collatz_seq 1 (1 ; *).
collatz_seq/1: collatz_seq X (X ; Y)
	<- X != 1
	<- is_even X true
	<- div X 2 Z
	<- collatz_seq Z Y.
collatz_seq/1: collatz_seq X (X ; Y)
	<- X != 1
	<- is_even X false
	<- mult X 3 X1
	<- sum X1 1 Z
	<- collatz_seq Z Y.