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

At: no duplicate send layer 1 1 1
1. E: EventStruct

send-enabledR(E)^-1 preserves No-dup-send(E)
By:
Inst Thm* E:EventStruct. safetyR(E) preserves No-dup-send(E) [E]
THEN
BackThruLemma' Thm* P:(TProp), R1,R2:(TTProp). (x,y:T. (x R1 y) (x R2 y)) R2 preserves P R1 preserves P
Generated subgoal:

12. x: |E| List
3. y: |E| List
4. x send-enabledR(E)^-1 y
x safetyR(E) y

About:
list

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