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

At: totalorder switchable0 2 3 1 1 1
1. E: EventStruct
2. f: Label(|E| List)
3. g: Label(|E| List)
4. h: Label(|E| List)
5. p,q:Label. (xf(p).(yg(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. (xf(p).(yg(q).(x =msg=(E) y)))
15. (xf(p).(yg(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. (xf(q).(yg(q@0).(x =msg=(E) y)))

(xmap(msg(E);f(q)).(x map(msg(E);g(p))))
By:
All (Unfold `l_all`)
THEN
Analyze 0
THEN
AllHyps (RWO "member_map")
THEN
ExRepD
THEN
InstHyp [q;p;y1;y] 5
THEN
Analyze -1
THEN
Unfold `event_msg_eq` 0
THEN
Reduce 0
THEN
SubstFor (msg(E)(y1)) 0
THEN
SubstFor (msg(E)(y)) 0
THEN
Inst Thm* M:MessageStruct. EquivRel(|M|)(_1 =(M) _2) [MS(E)]
THEN
UseEquiv
Generated subgoals:

None

About:
listassertapplyfunctionequalall

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