public static Proposition copyProposition(Proposition self, KeyValueMap mapping) {
    { Proposition copy = ((Proposition)(mapping.lookup(self)));

      if (copy != null) {
        return (copy);
      }
      else if (self.kind == Logic.KWD_CONSTANT) {
        return (self);
      }
      copy = Logic.createProposition(Logic.SYM_STELLA_PREDICATE, self.arguments.length());
      copy.homeContext = ((Module)(Stella.$MODULE$.get()));
      copy.kind = self.kind;
      copy.operator = ((GeneralizedSymbol)(Logic.copyPropositionArgument(self.operator, mapping)));
      { Proposition object000 = copy;
        TruthValue value000 = ((TruthValue)(Stella_Object.accessInContext(self.truthValue, self.homeContext, false)));
        Stella_Object oldValue001 = object000.truthValue;
        Stella_Object newValue000 = Stella_Object.updateInContext(oldValue001, value000, object000.homeContext, false);

        if (!((oldValue001 != null) &&
            (oldValue001.primaryType() == Logic.SGT_STELLA_CS_VALUE))) {
          object000.truthValue = newValue000;
        }
      }
      if (((FloatWrapper)(KeyValueList.dynamicSlotValue(self.dynamicSlots, Logic.SYM_LOGIC_WEIGHT, Stella.NULL_FLOAT_WRAPPER))).wrapperValue != Stella.NULL_FLOAT) {
        KeyValueList.setDynamicSlotValue(copy.dynamicSlots, Logic.SYM_LOGIC_WEIGHT, FloatWrapper.wrapFloat(((FloatWrapper)(KeyValueList.dynamicSlotValue(self.dynamicSlots, Logic.SYM_LOGIC_WEIGHT, Stella.NULL_FLOAT_WRAPPER))).wrapperValue), Stella.NULL_FLOAT_WRAPPER);
      }
      if (BooleanWrapper.coerceWrappedBooleanToBoolean(self.variableTypeP())) {
        KeyValueList.setDynamicSlotValue(copy.dynamicSlots, Logic.SYM_LOGIC_VARIABLE_TYPEp, Stella.TRUE_WRAPPER, null);
      }
      if (((BooleanWrapper)(KeyValueList.dynamicSlotValue(self.dynamicSlots, Logic.SYM_LOGIC_DESCRIPTIVEp, Stella.FALSE_WRAPPER))).wrapperValue) {
        KeyValueList.setDynamicSlotValue(copy.dynamicSlots, Logic.SYM_LOGIC_DESCRIPTIVEp, Stella.TRUE_WRAPPER, Stella.FALSE_WRAPPER);
      }
      if (((BooleanWrapper)(KeyValueList.dynamicSlotValue(self.dynamicSlots, Logic.SYM_LOGIC_DONT_OPTIMIZEp, Stella.FALSE_WRAPPER))).wrapperValue) {
        KeyValueList.setDynamicSlotValue(copy.dynamicSlots, Logic.SYM_LOGIC_DONT_OPTIMIZEp, Stella.TRUE_WRAPPER, Stella.FALSE_WRAPPER);
      }
      if (((PropertyList)(KeyValueList.dynamicSlotValue(self.dynamicSlots, Logic.SYM_LOGIC_ANNOTATIONS, null))) != null) {
        KeyValueList.setDynamicSlotValue(copy.dynamicSlots, Logic.SYM_LOGIC_ANNOTATIONS, ((PropertyList)(KeyValueList.dynamicSlotValue(self.dynamicSlots, Logic.SYM_LOGIC_ANNOTATIONS, null))).copy(), null);
        Proposition.finalizePropositionAnnotations(copy);
      }
      mapping.insertAt(self, copy);
      { Keyword testValue000 = self.kind;

        if ((testValue000 == Logic.KWD_FORALL) ||
            (testValue000 == Logic.KWD_EXISTS)) {
          KeyValueList.setDynamicSlotValue(copy.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, Logic.copyVariablesVector(((Vector)(KeyValueList.dynamicSlotValue(self.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, null))), mapping), null);
        }
        else {
        }
      }
      { Stella_Object arg = null;
        Vector vector000 = self.arguments;
        int index000 = 0;
        int length000 = vector000.length();
        int i = Stella.NULL_INTEGER;
        int iter000 = 0;

        for (;index000 < length000; index000 = index000 + 1, iter000 = iter000 + 1) {
          arg = (vector000.theArray)[index000];
          i = iter000;
          (copy.arguments.theArray)[i] = (Logic.copyPropositionArgument(arg, mapping));
        }
      }
      return (copy);
    }
  }