Axiomatization of Trace Semantics for Stochastic Nondeterministic Processes