Question

Tight satisfaction is denoted by . For unclocked sequences without local variables, tight satisfaction is

defined as follows. w, x, y, z denote finite words over Σ.

? w b iff |w| = 1 and w0 b .

? w ( R ) iff w R .

? w ( R1 ##1 R2 ) iff there exist x, y such that w = xy and x R1 and y R2 .

? w ( R1 ##0 R2 ) iff there exist x, y, z such that w = xyz and |y| = 1, and xy R1 and yz R2 .

? w ( R1 or R2 ) iff either w R1 or w R2 .

? w ( R1 intersect R2 ) iff both w R1 and w R2 .

? w first_match ( R ) iff both

— w R and

— if there exist x, y such that w = xy and x R, then y is empty.

? w R [*0] iff |w| = 0.

? w R [*1:$] iff there exist words w1, w2,..., wj ( j > 1) such that w = w1w2...wj and for every i such that

1 < i < j, wi R .

If S is a clocked sequence, then w S iff w S’, where S’ is the unclocked sequence that results from S by

applying the rewrite rules.

An unclocked sequence R is non-degenerate iff there exists a non-empty finite word w over Σ such that

w R. A clocked sequence S is non-degenerate iff the unclocked sequence S’ that results from S by applying

the rewrite rules is non-degenerate.