1 | 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)))) |