GenAutomata
Sections
NuprlLIB
Doc
Def
single-tag-decomposable(E)(L) ==
L = nil
|E| List
(
L_1,L_2:Trace(E). L = (L_1 @ L_2)
|E| List &
L_2 = nil
|E| List & (
x
L_1.(
y
L_2.
(x =msg=(E) y))) & (
m:Label. (
x
L_2.tag(E)(x) = m)))
is mentioned
In prior sections:
mb
hybrid
GenAutomata
Sections
NuprlLIB
Doc
L = nil 
|E| List 
(
L_1,L_2:Trace(E). L = (L_1 @ L_2) |E| List & L_2 = nil |E| List & (
xL_1.(yL_2.
(x =msg=(E) y))) & (m:Label. (xL_2.tag(E)(x) = m)))