Module 1-Inputs.Nonce_precondition