mb
hybrid
Sections
GenAutomata
Doc
Rank
Theorem
Name
3
Thm*
E:EventStruct. asyncR(E) preserves No-dup-send(E)
[no_duplicate_send_async]
cites
0
Thm*
k:
, i,j:
k. Bij(
k;
k; (i, j))
[flip_bijection]
2
Thm*
L:T List, i,j:
||L||. ||swap(L;i;j)|| = ||L||
[swap_length]
mb
hybrid
Sections
GenAutomata
Doc