Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq)

is mentioned by

Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(State(ds)ma-valtype(da; k)ds(x)?Void). Thm* ma-single-effect(ds; da; k; x; f)  MsgA	[ma-single-effect_wf]
Thm* ds,ds':ltg:Id fp-> Type. ds  ds'  State(ds')  State(ds)	[ma-state-subtype2]
Thm* ds,ds':ltg:Id fp-> Type. ds  ds'  (State(ds') r State(ds))	[ma-state-subtype]
Def @i (with ds: ds init: init action a:T precondition a(v) is P s v)(j) Def == if eqof(IdDeq)(j,i) Def == if (with ds: ds Def == if (init: init Def == if action a:T Def == if aprecondition a(v) is Def == if aP) Def == else  fi	[d-single-pre-init]
Def @i (with ds: ds action a:T precondition a(v) is P s v)(j) Def == if eqof(IdDeq)(j,i) (with ds: ds action a:T precondition a(v) is P s v) Def == else  fi	[d-single-pre]
Def d-single-sends(i; ds; da; k; l; f)(j) Def == if eqof(IdDeq)(j,i) ma-single-sends(ds; da; k; l; f) else  fi	[d-single-sends]
Def d-single-effect(i; ds; da; k; x; f)(j) Def == if eqof(IdDeq)(j,i) ma-single-effect(ds; da; k; x; f) else  fi	[d-single-effect]
Def @i: only L sends on (l with tg)(j) Def == if eqof(IdDeq)(j,i) only L sends on (l with tg) else  fi	[d-single-sframe]
Def @i: only L affects x : t(j) Def == if eqof(IdDeq)(j,i) only members of L affect x :t else  fi	[d-single-frame]
Def @i: x:T initially x = v(j) Def == if eqof(IdDeq)(j,i) x : T initially x = v else  fi	[d-single-init]

In prior sections: mb event system 2 mb event system 3 mb event system 4

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html