1 | 1. E: TaggedEventStruct 2. m: Label tr_1,tr_2:|E| List. tr_1 = tr_2 ( < tr_1 > _m ((delayableR(E) asyncR(E))^*) < tr_2 > _m) |
2 | 1. E: TaggedEventStruct 2. m: Label 3. n: 4. 0 < n 5. tr_1,tr_2:|E| List. (tr_1 delayableR(E) asyncR(E)^n-1 tr_2) ( < tr_1 > _m ((delayableR(E) asyncR(E))^*) < tr_2 > _m) tr_1,tr_2:|E| List. (tr_1 if n=0 x,y. x = y |E| List else x,y. z:|E| List. (x (delayableR(E) asyncR(E)) z) & (z delayableR(E) asyncR(E)^n-1 y) fi tr_2) ( < tr_1 > _m ((delayableR(E) asyncR(E))^*) < tr_2 > _m) |
About: