Nuprl - Pf P_no_dup_send_enabled

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

At: P no dup send enabled

E:EventStruct. send-enabledR(E) preserves No-dup-deliver(E)

By: Auto

Generated subgoal:

1 1. E: EventStruct
send-enabledR(E) preserves No-dup-deliver(E)

About:

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