At: no duplicate send delayable E:EventStruct. delayableR(E) preserves No-dup-send(E) By: Auto
THEN
Unfolds [`preserved_by`;`R_delayable`;`R_async`] 0
THEN
Unfold `swap_adjacent` 0
THEN
Reduce 0
THEN
ExRepD
THEN
SubstFor y 0
THEN
Inst
Thm*L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||
[|E|;x;i;i+1]
THEN
All (h.(Unfold `no_duplicate_send` h) THEN (Reduce h))
THEN
RWO "swap_select" 0
THEN
GenConcl ((i, i+1) = f)
THEN
InstHyp [f(i@0);f(j)] 4
THEN
AssertBY Bij(||x||; ||x||; f)
((SubstFor f 0)
THEN
(BackThru
Thm*k:, i,j:k. Bij(k; k; (i, j))))
THEN
Analyze -1
THEN
Unfold `inject` -2
THEN
BackThru -2 Generated subgoals:
E:EventStruct. delayableR(E) preserves No-dup-send(E)
||L||. ||swap(L;i;j)|| = ||L|| 
[|E|;x;i;i+1]
h.(Unfold `no_duplicate_send` h) THEN (Reduce h))