Question

w denotes a non-empty finite or infinite word over Σ, j denotes an integer such that 0 < j < |w|, and T(V) denotes

an instance of a clocked or unclocked sequence that is passed the local variables V as actual arguments.

? w j,L0,L1 T(V).ended iff there exist 0 < i < j and L such that both w i, j, {}, L T(V) and

L1 = L0 |D U LV , where D = dom(L0) – (dom(L) V).

? w j,L0,L1 @(c)(T(V).matched) iff there exists 0 < i < j such that w i,L0,L1

T(V).ended and

w i+1, j , {}, {} (!c [*0:$] ##1 c) .

? w j @(c)$stable(e) iff there exists 0 < i < j such that w

i, j , {}, {} (c ##1 c [->1]) and

e[w i] = e[w j].

? w j @(c)$rose(e) iff b[w j] = 1 and (if there exists 0 < i < j such that w i, j ,{}, {} (c ##1 c [->1])

then b[w i] 1), where b is the least-significant bit of e.

? w j @(c)$fell(e) iff b[w j] = 0 and (if there exists 0 < i < j such that w i, j ,{}, {} (c ##1 c [->1])

then b[w i] 0), where b is the least-significant bit of e.