[sv-ac] afterthought

Hi Dmitry:

In my previous mail I said 

> The semantics we want is 
>   
>    w,{},L |== (logic v; (1, v=a) ##1 (logic v; (1, v = c) ##1 v == d) ##1 v == b)
> 
>    iff |w| = 4 and c[w^1] == d[w^2] and a[w^0] == b[w^3]

This was too strong -- I should have said

  The semantics we want has 
   
     w,{},L |== (logic v; (1, v=a) ##1 (logic v; (1, v = c) ##1 v == d) ##1 v == b)
 
     only if |w| = 4 and c[w^1] == d[w^2] and a[w^0] == b[w^3]

In fact, if we use 

   w,L,L' |== (t v; R) 
   iff there exists L" s.t. w,L\v,L" |== R
       and L' = L"\v U L[v], 

then I think we get 

     w,{},L |== (logic v; (1, v=a) ##1 (logic v; (1, v = c) ##1 v == d) ##1 v == b)
 
     iff L = {} and |w| = 4 and c[w^1] == d[w^2] and a[w^0] == b[w^3]
         
This makes sense to me.

J.H.

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