public static KeyValueMap yieldJustificationSubstitution(Justification justification, KeyValueMap substitution, Proposition argument) {
    { Proposition top = justification.proposition;
      Proposition proposition = ((argument == null) ? top : argument);

      { Stella_Object arg = null;
        Vector vector000 = proposition.arguments;
        int index000 = 0;
        int length000 = vector000.length();

        for (;index000 < length000; index000 = index000 + 1) {
          arg = (vector000.theArray)[index000];
          { Surrogate testValue000 = Stella_Object.safePrimaryType(arg);

            if (Surrogate.subtypeOfP(testValue000, Logic.SGT_LOGIC_PATTERN_VARIABLE)) {
              { PatternVariable arg000 = ((PatternVariable)(arg));

                if (PatternVariable.freeVariableP(arg000, top)) {
                  if (substitution == null) {
                    substitution = KeyValueMap.newKeyValueMap();
                  }
                  substitution.insertAt(arg000, Logic.justificationArgumentBoundTo(arg000, justification));
                }
              }
            }
            else if (Surrogate.subtypeOfP(testValue000, Logic.SGT_LOGIC_PROPOSITION)) {
              { Proposition arg000 = ((Proposition)(arg));

                substitution = Justification.yieldJustificationSubstitution(justification, substitution, arg000);
              }
            }
            else {
            }
          }
        }
      }
      return (substitution);
    }
  }