public static Proposition consDbuildProposition(Cons tree) {
    { Proposition proposition = null;

      if (!Stella_Object.isaP(tree.value, Logic.SGT_STELLA_SYMBOL)) {
        System.err.print("Safety violation: INTERNAL ERROR: Illegal operator in proposition tree.");
      }
      { GeneralizedSymbol testValue000 = ((GeneralizedSymbol)(tree.value));

        if (testValue000 == Logic.SYM_STELLA_e) {
          proposition = Logic.buildEquivalenceProposition(tree);
        }
        else if ((testValue000 == Logic.SYM_STELLA_AND) ||
            ((testValue000 == Logic.SYM_STELLA_OR) ||
             (testValue000 == Logic.SYM_STELLA_NOT))) {
          proposition = Logic.buildAndOrNotProposition(tree);
        }
        else if (testValue000 == Logic.SYM_STELLA_ISA) {
          proposition = Logic.buildIsaProposition(tree);
        }
        else if (testValue000 == Logic.SYM_PL_KERNEL_KB_MEMBER_OF) {
          proposition = Logic.buildMemberOfProposition(tree);
        }
        else if ((testValue000 == Logic.SYM_LOGIC_IMPLIES) ||
            (testValue000 == Logic.SYM_PL_KERNEL_KB_SUBSET_OF)) {
          proposition = Logic.buildImpliesProposition(tree);
        }
        else if (testValue000 == Logic.SYM_STELLA_EXISTS) {
          proposition = Logic.buildExistsProposition(tree);
        }
        else if (testValue000 == Logic.SYM_STELLA_FORALL) {
          proposition = Logic.buildForallProposition(tree);
        }
        else if (testValue000 == Logic.SYM_LOGIC_FAIL) {
          proposition = Logic.buildFailProposition(tree);
        }
        else if (testValue000 == Logic.SYM_STELLA_COLLECT_INTO) {
          proposition = Logic.buildCollectIntoProposition(tree);
        }
        else if (testValue000 == Logic.SYM_LOGIC_ABOUT) {
          proposition = Logic.buildAnnotatedProposition(tree);
        }
        else {
          proposition = Logic.buildPredicateProposition(tree);
        }
      }
      if (proposition == null) {
        return (null);
      }
      if (Proposition.containsNestedArgumentP(proposition)) {
        proposition = Proposition.flattenNestedFunctionArguments(proposition);
      }
      return (proposition);
    }
  }