(2steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc

At: permutable implies delayable 1
1. E: EventStruct
2. P: (|E| List)Prop
3. x,y:|E| List. P(x) (x swap adjacent[True] y) P(y)
4. x: |E| List
5. y: |E| List
6. P(x)
7. x swap adjacent[(x =msg=(E) y) & is-send(E)(x) & is-send(E)(y) is-send(E)(x) & is-send(E)(y)] y

x swap adjacent[True] y
By:
All (h.(Unfold `swap_adjacent` h) THEN (Reduce h))
THEN
ParallelOp -1
Generated subgoals:

None

About:
listassertapplyfunctionpropimpliesandortrueall

(2steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc