Re: How to extend a patch theory to fully commute

On Thu, 2 Jul 2020 at 08:57, Ben Franksen <[email protected]> wrote:
> > Definition: Let A=(a, b, (Qi), (nj), X, Y) be an patch sequence address
> > of length n (i.e. (nj) has n names in it). The /separation/ of A is a
> > sequence of n extended patches. Patch j in the sequence is the minimal
> > form of (a, b, (Qi), nj, X U {before}, Y U {after}), where {before} is
> > the set of names that came before j in the sequence and {after} is the
> > names that came after.
>
> Could explicitly state which sequence you refer to in the last sentence?
> I.e. do you mean (Qi) or (nj) here? The wording ("set of names")
> suggests that you refer to (nj). It would also be better if you would
> not use j for both the generic index and the particular index here. Here
> is a reformulation that is clearer IMO:

Yes, the names in the sequence (nj).

> Definition: Let A=(a, b, (Qi), (nj), X, Y) be a patch sequence address,
> where j ranges from 1 to l (i.e. (nj) has l names in it). The
> /separation/ of A is a sequence of l extended patches, such that patch k
> in the sequence is the minimal form of (a, b, (Qi), nk, Xk, Yk), where
> Xk = X U {nj|j<k} and Yk = Y U {nj|j>k}.

Thanks, that's better. I put in your definition (but wrote [nk]
instead of nk) and also updated the proof of Proposition 3 to match
(and add a bit more explanation):
https://hub.darcs.net/falsifian/misc-pub/patch/17b04398d42f5c8ebf8f3aff79201cc766261503