formalizing-rtdeques