for x, n, k being Nat holds DecSD2 (x,n,k) = DecSD (x,n,k)