Terminating Euclidean algorithm for a non-Noetherian Bézout domain

In this paper, we will define a Euclidean-like norm and a division algorithm for a non-Noetherian Bézout domain, k[y]+x⋅k(y)[x]k[y]+x⋅k(y)[x], where k   is a field. And we will show that the Euclidean algorithm for that domain always terminates. As its application, we will give an algorithm to find the normal form of any matrix in GL2(k[x,y])GL2(k[x,y]) over k, with respect to the amalgamated free product structure.