(2steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc

At: permutable implies async

E:EventStruct, P:TraceProperty(E). R_permutation(E) preserves P asyncR(E) preserves P
By:
Unfolds [`trace_property`;`preserved_by`;`R_permutation`;`R_async`] 0
THEN
Reduce 0
THEN
Using [`x',x] BackThruSomeHyp
Generated subgoal:

11. 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[loc(E)(x) = loc(E)(y) & is-send(E)(x) & is-send(E)(y) is-send(E)(x) & is-send(E)(y)] y
x swap adjacent[True] y

About:
listimpliestrueall

(2steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc