diff --git a/thun/TLA.pl b/thun/TLA.pl
index e15c1a8..048080f 100644
--- a/thun/TLA.pl
+++ b/thun/TLA.pl
@@ -36,6 +36,29 @@ next(PC, I) :- PC \= done, relly(PC, I, PCnext, Inext), next(PCnext, Inext).
 % Inext in 1..1001.
 
 
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 type_ok(Small, Big) :- Small in 0..3, Big in 0..5.
 
 
@@ -44,13 +67,11 @@ next_dh(Moves) :- next_dh(0, 0, Moves).
 next_dh(Small, Big, [[Move, Si, Bi]|Moves]) :-
     type_ok(Small, Big),
     die_hard(Move, Small, Big, Si, Bi),
-    (Bi = 4 -> Moves=[] ; next_dh(Si, Bi, Moves)).
+    (Bi = 4 -> Moves = [] ; next_dh(Si, Bi, Moves)).
 
 
-% die_hard(Small, Big, S, B).
-die_hard(fill_small, Small, Big, 3, Big) :- Small #\= 3.
-die_hard(  fill_big, Small, Big, Small, 5) :- Big #\= 5.
-
+die_hard( fill_small, Small, Big, 3, Big) :- Small #< 3.
+die_hard(   fill_big, Small, Big, Small, 5) :- Big #< 5.
 die_hard(empty_small, Small, Big, 0, Big) :- Small #> 0.
 die_hard(  empty_big, Small, Big, Small, 0) :- Big #> 0.
 
@@ -62,21 +83,56 @@ die_hard(big_to_small, Small, Big, S, B) :-
     Small #< 3, Big #> 0,
     big_to_small(Small, Big, S, B).
 
+
 big_to_small(Small, Big, S, 0) :-
     Small + Big #=< 3,
-    S is Small + Big.
+    S #= Small + Big.
 
 big_to_small(Small, Big, 3, B) :-
     Small + Big #> 3,
-    B is Big - (3 - Small).
+    B #= Big - (3 - Small).
+
 
 small_to_big(Small, Big, 0, B) :-
     Small + Big #=< 5,
-    B is Small + Big.
+    B #= Small + Big.
 
 small_to_big(Small, Big, S, 5) :-
     Small + Big #> 5,
-    S is Small - (5 - Big).
+    S #= Small - (5 - Big).
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 
 /*