(9steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: no duplicate send layer 1 1 1 1
1. E: EventStruct
2. x: |E| List
3. y: |E| List
4. x send-enabledR(E)^-1 y

x safetyR(E) y
By:
All (Unfolds [`rel_inverse`;`R_send_enabled`;`R_safety`])
THEN
All Reduce
THEN
ExRepD
THEN
SubstFor x 0
Generated subgoal:

14. x@0: |E|
5. is-send(E)(x@0)
6. x = (y @ [x@0])
y y @ [x@0]

About:
listconsnil

(9steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc