public static String stringifiedKifOperator(Proposition self) {
    { GeneralizedSymbol operator = self.operator;

      if (operator == null) {
        return ("NULL");
      }
      { Surrogate testValue000 = Stella_Object.safePrimaryType(operator);

        if (Surrogate.subtypeOfSurrogateP(testValue000)) {
          { Surrogate operator000 = ((Surrogate)(operator));

            return (Logic.stringifiedSurrogate(operator000));
          }
        }
        else if (Surrogate.subtypeOfSymbolP(testValue000)) {
          { Symbol operator000 = ((Symbol)(operator));

            return (Logic.maybeDowncase(operator000.symbolName));
          }
        }
        else {
          { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

            stream000.nativeStream.print("`" + testValue000 + "' is not a valid case option");
            throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
          }
        }
      }
    }
  }