Nuprl - mb_hybrid Citations of layer

Def layerR(E) == ((asyncR(E)

delayableR(E))

send-enabledR(E))^*

is mentioned by

Thm* E:EventStruct. layerR(E)^-1 preserves No-dup-send(E) [no_duplicate_send_layer]

Def full_switch_inv(E;A;evt;tg;tr_u;tr_l) == tr_m:A List. (tr_l R(tg) tr_m) & (map(evt;tr_m) layerR(E) tr_u) & switch_inv( < A,evt,tg > (E))(tr_m) [full_switch_inv]

Try larger context: GenAutomata

mb hybrid Sections GenAutomata Doc

`Thm* E:EventStruct. layerR(E)^-1 preserves No-dup-send(E)`	[no_duplicate_send_layer]
`Def full_switch_inv(E;A;evt;tg;tr_u;tr_l) == tr_m:A List. (tr_l R(tg) tr_m) & (map(evt;tr_m) layerR(E) tr_u) & switch_inv( < A,evt,tg > (E))(tr_m)`	[full_switch_inv]