PrintForm
Definitions
mb
events
Sections
GenAutomata
Doc
At:
trace
projection
append
d:Decl, t1,t2:(
d) List, P:(Label
). t1 @ t2 | P ~ (t1 | P @ t2 | P)
By:
UnivCD
THEN
Unfold `trace_projection` 0
THEN
Easy
Generated subgoals:
None
About:
PrintForm
Definitions
mb
events
Sections
GenAutomata
Doc
d:Decl, t1,t2:(
d) List, P:(Label
). t1 @ t2 | P ~ (t1 | P @ t2 | P)
