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

At: R delayable symmetric 1
1. E: EventStruct
2. a: |E|
3. b: |E|
4. (a =msg=(E) b)
5. is-send(E)(a) & is-send(E)(b) is-send(E)(a) & is-send(E)(b)

(b =msg=(E) a)
By:
ParallelOp -2
THEN
Inst Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) [E]
THEN
UseEquiv
Generated subgoals:

None

About:
assertapplyandor

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