(15steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc
At:
totalorder
switchable0
2
1
1.
E:
EventStruct
2.
f:
Label
(|E| List)
3.
g:
Label
(|E| List)
4.
p:Label. g(p)
f(p)
5.
p,q:Label. agree_on_common(|MS(E)|;map(msg(E);f(p));map(msg(E);f(q)))
6.
p:
Label
7.
q:
Label
agree_on_common(|MS(E)|;map(msg(E);g(p));map(msg(E);g(q)))
By:
InstHyp [p] 4
THEN
InstHyp [q] 4
THEN
Thin 4
THEN
InstHyp [p;q] 4
THEN
Thin 4
Generated subgoal:
1
4.
p:
Label
5.
q:
Label
6.
g(p)
f(p)
7.
g(q)
f(q)
8.
agree_on_common(|MS(E)|;map(msg(E);f(p));map(msg(E);f(q)))
agree_on_common(|MS(E)|;map(msg(E);g(p));map(msg(E);g(q)))
About:
(15steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc