I have tried to understand the behaviour of dif/2 (which leads to a state diagram) but have a this little phenomenon:

Here is some code which has a dif/2 call in place of an implication premiss (ok, not really an implication rather than a control construct):

```
magic_of_dif(A,B,W) :-
A=f(_),
B=f(y),
% At this point, we cannot say for sure whether it will
% turn out that A==B or not. It could go either way.
(dif(A,B)
->
proceed_hoping_that_dif_will_turn_true(A,B,W)
;
try_again(A,B)).
try_again(A,B) :-
format("Trying again after dif(A,B) collapsed to 'false'\n",[]);
format("Post optimistic valus: A=~q, B=~q\n",[A,B]).
proceed_hoping_that_dif_will_turn_true(A,B,W) :-
format("Proceeding, hoping that dif/2 will turn true\n"),
format("Optimistic valus: A=~q, B=~q\n",[A,B]),
((W==make_equal)
->
(A=f(y),format("Never get here\n",[])) % dif(A,B) collapses to false
;
(A=f(x),format("inequality confirmed\n",[]))). % dif(A,B) confirmed to be true
```

The āhappy pathā of execution would be to confirm `dif(A,B)`

as true. āOptimistically continuingā when `dif(A,B)`

was the right choice:

```
?- magic_of_dif(A,B,_).
Proceeding, hoping that dif/2 will turn true
Optimistic valus: A=f(_13388), B=f(y)
inequality confirmed
A = f(x),
B = f(y).
```

On the other hand, calling `magic_of_dif/3`

with the instruction to make `A`

and `B`

equal (the case where optimism is not rewarded) reveals that the else branch of `->/2`

is not taken. Is this expected?

```
?- magic_of_dif(A,B,make_equal).
Proceeding, hoping that dif/2 will turn true
Optimistic valus: A=f(_12650), B=f(y)
false.
```

Maybe I have I have some wrong idea about the workings of `dif/2`

?