(70steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc
At:
P
causal
switchable0
2
1
1.
E:
EventStruct
2.
x:
|E| List
3.
y:
|E| List
4.
tr':|E| List. tr'
x
(
x
tr'.(
y
tr'.is-send(E)(y) & (y =msg=(E) x)))
5.
a:
|E|
6.
y = filter(
b.
(b =msg=(E) a);x)
7.
tr':
|E| List
8.
tr'
y
(
x
tr'.(
y
tr'.is-send(E)(y) & (y =msg=(E) x)))
By:
Assert (
tr:|E| List. tr
x & tr' = filter(
b.
(b =msg=(E) a);tr))
Generated subgoals:
1
tr:|E| List. tr
x & tr' = filter(
b.
(b =msg=(E) a);tr)
2
9.
tr:|E| List. tr
x & tr' = filter(
b.
(b =msg=(E) a);tr)
(
x
tr'.(
y
tr'.is-send(E)(y) & (y =msg=(E) x)))
About:
(70steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc