crossInst { \assumes ( ==> ( ( k <= - 1 | k >= i ) | c ) ) \find ( \forall v ; ( ( ( v <= - 1 | v >= j ) | b ) | a ) ==> ) \varcond \add ( sk = k & { \subst v ; sk } ( ( ( v <= - 1 | v >= j ) | b ) | a ) ==> ) \heuristics (loopInvariant ) };
cutUpperBound { \assumes ( \forall v ; ( ( ( v <= - 1 | v >= j ) | b ) | a ) ==> ) \find ( ==> ( ( k <= - 1 | k >= i ) | c ) ) \add ( ( k = i ) ==> ) ; \add ( ( k != i ) ==> ) \heuristics (loopInvariant ) };