docs: def _popup(self):
          """recursively find commutative binary operator
          among child formulas and pop up them at the same level"""
          res = ()
          for child in self.formulas:
              if type(child) == type(self):
                  superchilds = child.formulas
                  res += superchilds
              else:
                  res += (child, )
          return tuple(res)