Time 
Nick 
Message 
09:11 

kowey joined #darcstheory 
15:58 

kowey joined #darcstheory 
17:28 

arjanb joined #darcstheory 
19:45 
arjanb 
Igloo: theory.pdf on the camp website seems to be 2 months out of date 
19:47 
Igloo 
Thanks for the prod, updated 
19:47 
Igloo 
And I've made a Makefile target to make updating easier, so hopefully I'll do more of it :) 
20:24 
arjanb 
nice progress 
20:24 
Igloo 
Thanks! 
20:25 
arjanb 
for lemma 9.2 what about: minimal context of P is the common subset of N(Rs) for all Rs in QsP <*> RsP'Ts 
20:27 
Igloo 
What we need to prove is that is if As P Bs <>* Cs P' Ds 
20:28 
Igloo 
Then we can commute out anything in As but not Cs, and viceversa 
20:29 
Igloo 
Or to put it another way, if As B Cs P Ds <>* Es P' Fs where B \notin Es 
20:29 
Igloo 
Then <B, Cs P> <> <Cs' P'', B'> 
20:30 
Igloo 
Which I think you can prove by considering the rightmost B, and using the previous lemma for each patch in Cs P. Does that sound good? 
20:31 
arjanb 
yeah 
20:32 
arjanb 
or it's just a matter of enumerating the ways of how B could have ended up in that place 
20:33 
Igloo 
I need to talk to gal_bolle about whether he can make coq happy with this approach 
21:06 
Heffalump 
gal_bolle is coq'ing stuff? 
21:09 
Igloo 
Yup 
21:29 

kowey joined #darcstheory 