Nuprl - Pf no_duplicate_send

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

1. E: EventStruct
2. x: |E| List
3. y: |E| List

(asyncR(E) delayableR(E)) send-enabledR(E)^-1 = > (asyncR(E) delayableR(E)) send-enabledR(E)^-1

By: Unfolds [`rel_or`;`rel_inverse`;`rel_implies`] 0 THEN Reduce 0 THEN Repeat (ParallelOp -1) THEN Try (BackThru Thm* E:EventStruct, x,y:|E| List. (x asyncR(E) y) (y asyncR(E) x)) THEN Try (BackThru Thm* E:EventStruct, x,y:|E| List. (x delayableR(E) y) (y delayableR(E) x))

Generated subgoals:

None

About:

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