<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span>> I am concerned with the condition of the closedness that \mathcal{L}(s)<br>
> # T..  Due to this restriction I believe the closure is in general not<br>
> minimal w.r.t. the closedness.<br>
<br>
</span>Oh, right, we also added this well-formedness condition here because we<br>
are lazy. However, considering T to be fixed, this condition is<br>
monotone, i.e., if it rules out a set then it also rules out all larger<br>
sets. How should this violate minimality?</blockquote></div><div class="gmail_extra"><br></div>Consider an STS consisting of two nodes s1, s2 and an edge s1 -> s2, with L(s1)={T} and L(s2)={}.  Then closure({s1},{T}) = {s1,s2}.  But ({s1},{T}), which is less than (closure({s1},{T}),{T}), is also closed.  Which implies that a closure may not be minimal w.r.t. the closedness.</div><div class="gmail_extra"><br></div><div class="gmail_extra">I started to understand why you called it "closure", and yet I want to know the exact meaning of the word in this context.  This is partly because when reading the POPL 2015 paper I couldn't understand the STS construction..<br clear="all"><div><br></div>-- <br><div data-smartmail="gmail_signature"><div dir="ltr"><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank">Jeehoon Kang (Ph.D. student)</a><div><a href="http://sf.snu.ac.kr" target="_blank">Software Foundations Laboratory</a><div><a href="http://www.snu.ac.kr" target="_blank">Seoul National University</a></div></div></div></div>
</div></div>