top_sequences : THEORY BEGIN IMPORTING convergence_ops, convergence_sequences END top_sequences