Nuprl - Pf P_no_dup_composable

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

At: P no dup composable

E:EventStruct. (ternary) composableR(E) preserves No-dup-deliver(E)

By: Auto

Generated subgoal:

1 1. E: EventStruct
(ternary) composableR(E) preserves No-dup-deliver(E)

About:

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