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

At: no duplicate send layer 1 1 1 1 1
1. E: EventStruct
2. x: |E| List
3. y: |E| List
4. x@0: |E|
5. is-send(E)(x@0)
6. x = (y @ [x@0])

y y @ [x@0]
By:
BackThru Thm* l1,l2,l3:T List. l1 l2 l1 l2 @ l3
THEN
Easy
Generated subgoals:

None

About:
listconsnilassertapplyequal

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