theorem :: REVROT_1:7

canceled;