(15steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc
At:
totalorder
switchable0
2
3
1
1.
E:
EventStruct
2.
f:
Label
(|E| List)
3.
g:
Label
(|E| List)
4.
h:
Label
(|E| List)
5.
p,q:Label. (
x
f(p).(
y
g(q).
(x =msg=(E) y)))
6.
p:Label. h(p) = ((f(p)) @ (g(p)))
7.
p,q:Label. agree_on_common(|MS(E)|;map(msg(E);f(p));map(msg(E);f(q)))
8.
p,q:Label. agree_on_common(|MS(E)|;map(msg(E);g(p));map(msg(E);g(q)))
9.
p:
Label
10.
q:
Label
11.
q:Label. agree_on_common(|MS(E)|;map(msg(E);g(p));map(msg(E);g(q)))
12.
q:Label. agree_on_common(|MS(E)|;map(msg(E);f(p));map(msg(E);f(q)))
13.
h(p) = ((f(p)) @ (g(p)))
14.
q:Label. (
x
f(p).(
y
g(q).
(x =msg=(E) y)))
15.
(
x
f(p).(
y
g(q).
(x =msg=(E) y)))
16.
agree_on_common(|MS(E)|;map(msg(E);f(p));map(msg(E);f(q)))
17.
agree_on_common(|MS(E)|;map(msg(E);g(p));map(msg(E);g(q)))
18.
q@0:Label. agree_on_common(|MS(E)|;map(msg(E);g(q));map(msg(E);g(q@0)))
19.
q@0:Label. agree_on_common(|MS(E)|;map(msg(E);f(q));map(msg(E);f(q@0)))
20.
h(q) = ((f(q)) @ (g(q)))
21.
q@0:Label. (
x
f(q).(
y
g(q@0).
(x =msg=(E) y)))
agree_on_common(|MS(E)|;map(msg(E);(f(p)) @ (g(p)));map(msg(E);(f(q)) @ (g(q))))
By:
RW MapAppendC 0
Generated subgoal:
1
agree_on_common(|MS(E)|;map(msg(E);f(p)) @ map(msg(E);g(p));map(msg(E);f(q)) @ map(msg(E);g(q)))
About:
(15steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc