expected

gcd aa (aa + (S y)) (CmpLT y) = ?gcd_rhs_1
gcd bb bb CmpEQ = ?gcd_rhs_2
gcd (bb + (S x)) bb (CmpGT x) = ?gcd_rhs_3