datatype Node = startFlow25 | end0 | A2 | startFlow69 | end1 | agateFlow70 | agateFlow74 | TG | EC | TG_T | startFlow36 | end2 | TG_G | EC_C | EC_E | startFlow59 | end3 | agateFlow60 | agateFlow64
datatype Msg = init | done

channel Flow25 , Flow28 , Flow69 , Flow74 , Flow70 , Flow71 , Flow72 , Flow73 , Flow36 , Flow37 , Flow38 , Flow60 , Flow61 , Flow62 , Flow63 , Flow59 , Flow64
channel starts : Node
channel fin , aborts : { 0, 1, 2, 3 }
channel finish , cancel , delayed , interrupted : Signal


APool(startFlow25) = { fin.0, Flow25 }
APool(end0) = { fin.0, Flow28 }
APool(A2) = { fin.0, Flow25, Flow28, Flow69, Flow74, fin.1, Flow70, Flow71, Flow72, Flow73, Flow36, Flow37, starts.TG_T, Flow38, fin.2, starts.TG_G, Flow60, Flow61, starts.EC_C, Flow62, Flow63, starts.EC_E, Flow59, Flow64, fin.3 }
AA2(startFlow69) = { fin.1, Flow69 }
AA2(end1) = { fin.1, Flow74 }
AA2(agateFlow70) = { fin.1, Flow69, Flow70, Flow71 }
AA2(agateFlow74) = { fin.1, Flow72, Flow73, Flow74 }
AA2(TG) = { fin.1, Flow71, Flow73, Flow36, Flow37, starts.TG_T, Flow38, fin.2, starts.TG_G }
AA2(EC) = { fin.1, Flow70, Flow72, Flow60, Flow61, starts.EC_C, Flow62, Flow63, starts.EC_E, Flow59, Flow64, fin.3 }
ATG(TG_T) = { fin.2, Flow36, Flow37, starts.TG_T }
ATG(startFlow36) = { fin.2, Flow36 }
ATG(end2) = { fin.2, Flow38 }
ATG(TG_G) = { fin.2, Flow37, Flow38, starts.TG_G }
AEC(EC_C) = { fin.3, Flow60, Flow61, starts.EC_C }
AEC(EC_E) = { fin.3, Flow62, Flow63, starts.EC_E }
AEC(startFlow59) = { fin.3, Flow59 }
AEC(end3) = { fin.3, Flow64 }
AEC(agateFlow60) = { fin.3, Flow59, Flow60, Flow62 }
AEC(agateFlow64) = { fin.3, Flow61, Flow63, Flow64 }
Signal = { Flow25, Flow28, Flow69, Flow70, Flow74, Flow73, Flow37, Flow36, Flow38, Flow72, Flow61, Flow63, Flow59, Flow60, Flow64, fin.0, fin.1, fin.2, fin.3 }

PPool(startFlow25) = ( Flow25 -> ( SKIP ) ) ; ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
PPool(A2) = ( ( ( Flow25 -> ( SKIP ) ) ; ( ( LA2 ) ; ( Flow28 -> ( SKIP ) ) ) ) ; ( PPool(A2) ) ) [] ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
PPool(end0) = ( Flow28 -> ( SKIP ) ) ; ( fin.0 -> ( SKIP ) )
PA2(startFlow69) = ( Flow69 -> ( SKIP ) ) ; ( [] i:{ 1 } @ ( fin.i -> ( SKIP ) ) )
PA2(agateFlow70) = ( ( ( Flow69 -> ( SKIP ) ) ; ( ( Flow70 -> ( SKIP ) ) ||| ( Flow71 -> ( SKIP ) ) ) ) ; ( PA2(agateFlow70) ) ) [] ( [] i:{ 1 } @ ( fin.i -> ( SKIP ) ) )
PA2(agateFlow74) = ( ( ( ( Flow72 -> ( SKIP ) ) ||| ( Flow73 -> ( SKIP ) ) ) ; ( Flow74 -> ( SKIP ) ) ) ; ( PA2(agateFlow74) ) ) [] ( [] i:{ 1 } @ ( fin.i -> ( SKIP ) ) )
PA2(TG) = ( ( ( Flow71 -> ( SKIP ) ) ; ( ( LTG ) ; ( Flow73 -> ( SKIP ) ) ) ) ; ( PA2(TG) ) ) [] ( [] i:{ 1 } @ ( fin.i -> ( SKIP ) ) )
PA2(EC) = ( ( ( Flow70 -> ( SKIP ) ) ; ( ( LEC ) ; ( Flow72 -> ( SKIP ) ) ) ) ; ( PA2(EC) ) ) [] ( [] i:{ 1 } @ ( fin.i -> ( SKIP ) ) )
PA2(end1) = ( Flow74 -> ( SKIP ) ) ; ( fin.1 -> ( SKIP ) )
PTG(TG_T) = ( ( ( Flow36 -> ( SKIP ) ) ; ( ( SKIP ) ; ( ( starts.TG_T -> ( SKIP ) ) ; ( ( ( SKIP ) ; ( ( SKIP ) ; ( SKIP ) ) ) ; ( Flow37 -> ( SKIP ) ) ) ) ) ) ; ( PTG(TG_T) ) ) [] ( [] i:{ 2 } @ ( fin.i -> ( SKIP ) ) )
PTG(startFlow36) = ( Flow36 -> ( SKIP ) ) ; ( [] i:{ 2 } @ ( fin.i -> ( SKIP ) ) )
PTG(TG_G) = ( ( ( Flow37 -> ( SKIP ) ) ; ( ( SKIP ) ; ( ( starts.TG_G -> ( SKIP ) ) ; ( ( ( SKIP ) ; ( ( SKIP ) ; ( SKIP ) ) ) ; ( Flow38 -> ( SKIP ) ) ) ) ) ) ; ( PTG(TG_G) ) ) [] ( [] i:{ 2 } @ ( fin.i -> ( SKIP ) ) )
PTG(end2) = ( Flow38 -> ( SKIP ) ) ; ( fin.2 -> ( SKIP ) )
LTG = || iTG:{ TG_T, startFlow36, end2, TG_G } @ [ ATG(iTG) ] ( PTG(iTG) )
PEC(EC_C) = ( ( ( Flow60 -> ( SKIP ) ) ; ( ( SKIP ) ; ( ( starts.EC_C -> ( SKIP ) ) ; ( ( ( SKIP ) ; ( ( SKIP ) ; ( SKIP ) ) ) ; ( Flow61 -> ( SKIP ) ) ) ) ) ) ; ( PEC(EC_C) ) ) [] ( [] i:{ 3 } @ ( fin.i -> ( SKIP ) ) )
PEC(EC_E) = ( ( ( Flow62 -> ( SKIP ) ) ; ( ( SKIP ) ; ( ( starts.EC_E -> ( SKIP ) ) ; ( ( ( SKIP ) ; ( ( SKIP ) ; ( SKIP ) ) ) ; ( Flow63 -> ( SKIP ) ) ) ) ) ) ; ( PEC(EC_E) ) ) [] ( [] i:{ 3 } @ ( fin.i -> ( SKIP ) ) )
PEC(startFlow59) = ( Flow59 -> ( SKIP ) ) ; ( [] i:{ 3 } @ ( fin.i -> ( SKIP ) ) )
PEC(agateFlow60) = ( ( ( Flow59 -> ( SKIP ) ) ; ( ( Flow60 -> ( SKIP ) ) ||| ( Flow62 -> ( SKIP ) ) ) ) ; ( PEC(agateFlow60) ) ) [] ( [] i:{ 3 } @ ( fin.i -> ( SKIP ) ) )
PEC(agateFlow64) = ( ( ( ( Flow61 -> ( SKIP ) ) ||| ( Flow63 -> ( SKIP ) ) ) ; ( Flow64 -> ( SKIP ) ) ) ; ( PEC(agateFlow64) ) ) [] ( [] i:{ 3 } @ ( fin.i -> ( SKIP ) ) )
PEC(end3) = ( Flow64 -> ( SKIP ) ) ; ( fin.3 -> ( SKIP ) )
LEC = || iEC:{ EC_C, EC_E, startFlow59, end3, agateFlow60, agateFlow64 } @ [ AEC(iEC) ] ( PEC(iEC) )
LA2 = || iA2:{ startFlow69, end1, agateFlow70, agateFlow74, TG, EC } @ [ AA2(iA2) ] ( PA2(iA2) )
LPool = || iPool:{ startFlow25, end0, A2 } @ [ APool(iPool) ] ( PPool(iPool) )
DFPool = ( |~| i:{ starts.TG_T, starts.TG_G, starts.EC_C, starts.EC_E, fin.1, fin.2, fin.3 } @ ( i -> ( DFPool ) ) ) |~| ( |~| i:{ fin.0 } @ ( i -> ( SKIP ) ) )
UPool = ( LPool ) \ ( { Flow25, Flow28, Flow69, Flow74, Flow70, Flow71, Flow72, Flow73, Flow36, Flow37, Flow38, Flow60, Flow61, Flow62, Flow63, Flow59, Flow64 } )

CPool =
let
	Internal = { finish.Flow28, cancel.Flow28, finish.Flow73, cancel.Flow73, delayed.Flow37, finish.Flow37, cancel.Flow37, delayed.Flow38, finish.Flow38, cancel.Flow38, finish.Flow72, cancel.Flow72, delayed.Flow61, finish.Flow61, cancel.Flow61, delayed.Flow63, finish.Flow63, cancel.Flow63 }
	ses = { fin.0 }
	run(S) = ( [] i:S @ ( i -> ( run(S) ) ) ) [] ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
	CPool1 = Flow25 -> ( Flow69 -> ( Flow70 -> ( Flow71 -> ( Flow59 -> ( Flow36 -> ( Flow60 -> ( Flow62 -> ( ( ( ( ( ( starts.TG_T -> ( Flow37 -> ( SKIP ) ) ) ; ( finish.Flow37 -> ( SKIP ) ) ) |~| ( delayed.Flow37 -> ( SKIP ) ) ) /\ ( cancel.Flow37 -> ( SKIP ) ) ) ; ( run({ finish.Flow37, delayed.Flow37, cancel.Flow37 }) ) ) [| union(ses,{ finish.Flow37, delayed.Flow37, cancel.Flow37 }) |] ( ( delayed.Flow37 -> ( ( ( ( ( starts.TG_T -> ( Flow37 -> ( SKIP ) ) ) ; ( finish.Flow37 -> ( SKIP ) ) ) /\ ( cancel.Flow37 -> ( SKIP ) ) ) ; ( run({ finish.Flow37, cancel.Flow37 }) ) ) [| union(ses,{ finish.Flow37, cancel.Flow37 }) |] ( finish.Flow37 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) |~| ( delayed.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, delayed.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, delayed.Flow38, cancel.Flow38 }) |] ( ( delayed.Flow38 -> ( ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) |~| ( delayed.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, delayed.Flow61, cancel.Flow61, finish.Flow38, delayed.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow61, delayed.Flow61, cancel.Flow61, finish.Flow38, delayed.Flow38, cancel.Flow38 }) |] ( ( ( delayed.Flow61 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) |~| ( delayed.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61, finish.Flow38, delayed.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61, finish.Flow38, delayed.Flow38, cancel.Flow38 }) |] ( ( ( delayed.Flow63 -> ( ( ( delayed.Flow61 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) |] ( ( delayed.Flow63 -> ( ( finish.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow38 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow63 -> ( ( finish.Flow38 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow61 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( delayed.Flow61 -> ( ( ( delayed.Flow63 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, cancel.Flow38 }) |] ( ( delayed.Flow63 -> ( ( finish.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow38 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( finish.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) |] ( ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) |] ( ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow38 -> ( ( ( delayed.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow63 -> ( ( finish.Flow38 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( finish.Flow38 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) |] ( ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) |] ( ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( ( delayed.Flow61 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) |] ( ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow38 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) |] ( ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow38 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( ( delayed.Flow63 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow38 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow38 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( ( delayed.Flow63 -> ( ( delayed.Flow61 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) |] ( ( ( delayed.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow38 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) |~| ( delayed.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, delayed.Flow38, cancel.Flow38, finish.Flow61, delayed.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, delayed.Flow38, cancel.Flow38, finish.Flow61, delayed.Flow61, cancel.Flow61 }) |] ( ( ( delayed.Flow63 -> ( ( ( delayed.Flow38 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow63 -> ( ( finish.Flow38 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) |] ( ( delayed.Flow63 -> ( ( finish.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow61 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( delayed.Flow38 -> ( ( ( delayed.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow63 -> ( ( finish.Flow38 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( finish.Flow38 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) |] ( ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) |] ( ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( ( delayed.Flow63 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, cancel.Flow38 }) |] ( ( delayed.Flow63 -> ( ( finish.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow38 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( finish.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) |] ( ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) |] ( ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( ( delayed.Flow38 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow61, cancel.Flow61 }) |] ( ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow38, cancel.Flow38 }) |] ( ( finish.Flow61 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow38 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( ( delayed.Flow63 -> ( ( delayed.Flow61 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow61 -> ( Flow73 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( delayed.Flow63 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow38 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow38 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) |~| ( delayed.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, delayed.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, delayed.Flow38, cancel.Flow38 }) |] ( ( ( delayed.Flow63 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, cancel.Flow38 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow38 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow38 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) |~| ( delayed.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, delayed.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, delayed.Flow38, cancel.Flow38 }) |] ( ( ( delayed.Flow63 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow38, cancel.Flow38 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow38 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow38 -> ( Flow64 -> ( Flow72 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow63 -> ( Flow73 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( Flow64 -> ( ( Flow73 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) [] ( Flow72 -> ( Flow73 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( Flow73 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow61 -> ( Flow73 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) |] ( ( ( delayed.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, delayed.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, delayed.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) |] ( ( ( delayed.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow37 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) |~| ( delayed.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, delayed.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, delayed.Flow38, cancel.Flow38 }) |] ( ( delayed.Flow38 -> ( ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) |~| ( delayed.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, delayed.Flow61, cancel.Flow61, finish.Flow38, delayed.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow61, delayed.Flow61, cancel.Flow61, finish.Flow38, delayed.Flow38, cancel.Flow38 }) |] ( ( ( delayed.Flow61 -> ( ( delayed.Flow38 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow61, delayed.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow61, delayed.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) |] ( ( ( delayed.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow61 -> ( Flow73 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) |] ( ( ( delayed.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) |] ( ( ( delayed.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow38 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow38, cancel.Flow38, finish.Flow61, delayed.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38, finish.Flow61, delayed.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) |] ( ( ( delayed.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow38 -> ( ( delayed.Flow61 -> ( Flow73 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) |] ( ( ( delayed.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow38 -> ( ( ( ( ( starts.TG_G -> ( Flow38 -> ( SKIP ) ) ) ; ( finish.Flow38 -> ( SKIP ) ) ) /\ ( cancel.Flow38 -> ( SKIP ) ) ) ; ( run({ finish.Flow38, cancel.Flow38 }) ) ) [| union(ses,{ finish.Flow38, cancel.Flow38 }) |] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( ( delayed.Flow61 -> ( Flow73 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) |] ( ( ( delayed.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow38 -> ( Flow73 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, delayed.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, delayed.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) |~| ( delayed.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, delayed.Flow61, cancel.Flow61 }) |] ( ( ( delayed.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ||| ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63, finish.Flow61, cancel.Flow61 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) [] ( delayed.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ||| ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ) ; ( run({ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61, finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( finish.Flow61 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) [] ( ( finish.Flow63 -> ( ( delayed.Flow61 -> ( ( ( ( ( starts.EC_C -> ( Flow61 -> ( SKIP ) ) ) ; ( finish.Flow61 -> ( SKIP ) ) ) /\ ( cancel.Flow61 -> ( SKIP ) ) ) ; ( run({ finish.Flow61, cancel.Flow61 }) ) ) [| union(ses,{ finish.Flow61, cancel.Flow61 }) |] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) [] ( finish.Flow61 -> ( ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) |~| ( delayed.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, delayed.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, delayed.Flow63, cancel.Flow63 }) |] ( ( delayed.Flow63 -> ( ( ( ( ( starts.EC_E -> ( Flow63 -> ( SKIP ) ) ) ; ( finish.Flow63 -> ( SKIP ) ) ) /\ ( cancel.Flow63 -> ( SKIP ) ) ) ; ( run({ finish.Flow63, cancel.Flow63 }) ) ) [| union(ses,{ finish.Flow63, cancel.Flow63 }) |] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow63 -> ( Flow64 -> ( Flow72 -> ( Flow74 -> ( Flow28 -> ( fin.0 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
within
	( CPool1 ) \ ( Internal )


TPool =
let
	TPool1 = ( LPool ) [| { Flow25, Flow28, fin.0, Flow69, Flow74, Flow70, Flow71, Flow72, Flow73, Flow36, Flow37, starts.TG_T, Flow38, starts.TG_G, Flow60, Flow61, starts.EC_C, Flow62, Flow63, starts.EC_E, Flow59, Flow64 } |] ( CPool )
within
	( TPool1 ) \ ( { Flow25, Flow28, Flow69, Flow74, Flow70, Flow71, Flow72, Flow73, Flow36, Flow37, Flow38, Flow60, Flow61, Flow62, Flow63, Flow59, Flow64 } )


--assert DFPool [F= UPool
--assert DFPool [F= TPool

-- not <starts.EC_C,starts.TG_G,starts.EC_E>
X = starts.TG_G -> X |~| starts.EC_E -> X |~| starts.EC_C -> Y |~| fin.0 -> SKIP
Y = starts.EC_E -> X |~| starts.EC_C -> Y 

assert X [F= TPool \ {starts.TG_T,fin.1,fin.2,fin.3}