(join (-> A 3 B, -> B 2 C)
,
exists (X) join (-> A X, <- X B) // B before A one hill
,
->X<- A * B // B before A, several hills
,
=>X<= A B // up, over and down: class graph: special kind of meta graph 
,
seq A (B, C)
,
// reachability formula "from A to B", B concrete
exists (R1) join ( =>X<= A edge e R1, =>X<= R1 B)
)
equations (
-> A B = =>X<= A B // if B is concrete
,
seq A (Q, C) = join( -> A Q, ->X<- Q C)
)