; Hacker's Delight, page 52, theorem 
1 var 8 a
2 var 8 b
3 var 8 x
4 slte 1 1 2
5 slte 1 1 3
6 slte 1 3 2
7 and 1 5 6

8 sub 8 3 1
9 sub 8 2 1
10 ulte 1 8 9

11 eq 1 7 10
12 implies 1 4 11
13 root 1 -12