Time 
Nick 
Message 
15:40 

thorkilnaur joined #darcstheory 
19:22 

arjanb joined #darcstheory 
21:00 
* Heffalump 
thinks he has identified 26 distinct ways of commuting two move patches 
21:01 
arjanb 
how do you know you haven't missed any? 
21:01 
Heffalump 
I don't 
21:02 
Heffalump 
Once I've finished with the details of them I'll think about how to gain confidence that I haven't.. 
21:02 
Heffalump 
But also some cases may be subjective 
21:04 
arjanb 
i hope some of them can be collapsed in a more general ones, because 26 is too much for intuition 
21:05 
Heffalump 
well, do you agree there are two cases for hunkhunk commute? 
21:05 
arjanb 
yes 
21:05 
Heffalump 
ok, so for movemove commute I've so far identified (2^2+1)^2+1 cases 
21:06 
Heffalump 
the 2 is exactly the same as for hunkhunk commute, i.e. before and after cases 
21:06 
Heffalump 
but then you have to consider both the source and the destination of each move, so it gets squared twice 
21:06 
Heffalump 
and there's also an "inside" case where one move is nested inside the other 
21:06 
Heffalump 
and that pops up in a few places 
21:08 
arjanb 
i see 
21:08 
Heffalump 
I'm working it out programmatically, so hopefully someone else can look at it all themselves without too much pain. 
21:08 
arjanb 
so using a theorem prover will be a must to get it right.. 
21:09 
Heffalump 
I think so, yes. 
21:09 
Heffalump 
but I'm not sure how you formulate a completeness property with a theorem prover 
21:09 
* Igloo 
wants something like Hoare triples for Haskell 