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.

odd: nat -> type.
odd/0: odd 1.
odd/1: odd (s (s X))
    <- odd X.

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

collatz: nat -> nat -> type.
collatz/0: collatz 1 0.
collatz/1: collatz X (s Y)
    <- sum X1 X1 X
    <- collatz X1 Y.
collatz/2: collatz X (s Y)
    <- odd X
    <- 1 < X
    <- sum X X X1
    <- sum X1 (s X) X2
    <- collatz X2 Y.