[sv-ac] review 1734

I didn't see anything wrong but I think that some information is still 
missing.

At E.3.3.1 should add

* for neutral satisfaction

—For U = Q, w\models U iff w \models Q.
— For U = disable iff (b) Q, w\models U iff either
— w\models Q and no letter of w satisfies b, or
— Some letter of w satisfies b and w^{0.. i–1}\bot^\omega\models P for i 
the least index such that
w i\models b, 0 < i < |w| .

* for the \models^d relation , should add

Disabling of top-level properties is defined as follows:
— w\not\models^d Q.
— w\models^d Q disable iff (b) iff some letter of w satisfies b and both 
w^{0.. i–1}\top^\omega\not\models P and
w^{0..i–1}\bot^\omega\models P for i the least index such that 
w^i\models b, 0 < i < |w|.



* Vacuity,  should have a sub-section for T (Q is not there anyway) and 
put the disable iff there

* E.3.6.1 same as E.3.3.1

Doron

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.