public static boolean justificationPropositionsEqlP(Proposition proposition1, Justification just1, Proposition proposition2, Justification just2) {
    if ((proposition1.operator == proposition2.operator) &&
        (proposition1.arguments.length() == proposition2.arguments.length())) {
      { Stella_Object arg1 = null;
        Vector vector000 = proposition1.arguments;
        int index000 = 0;
        int length000 = vector000.length();
        Stella_Object arg2 = null;
        Vector vector001 = proposition2.arguments;
        int index001 = 0;
        int length001 = vector001.length();

        for (;(index000 < length000) &&
                  (index001 < length001); index000 = index000 + 1, index001 = index001 + 1) {
          arg1 = (vector000.theArray)[index000];
          arg2 = (vector001.theArray)[index001];
          if ((!Stella_Object.eqlP(arg1, arg2)) ||
              Logic.variableP(arg1)) {
            { Surrogate testValue000 = Stella_Object.safePrimaryType(arg1);

              if (Surrogate.subtypeOfP(testValue000, Logic.SGT_LOGIC_PROPOSITION)) {
                { Proposition arg1000 = ((Proposition)(arg1));

                  if (!(Stella_Object.isaP(arg2, Logic.SGT_LOGIC_PROPOSITION) &&
                      Proposition.justificationPropositionsEqlP(arg1000, just1, ((Proposition)(arg2)), just2))) {
                    return (false);
                  }
                }
              }
              else if (Surrogate.subtypeOfP(testValue000, Logic.SGT_LOGIC_PATTERN_VARIABLE)) {
                { PatternVariable arg1000 = ((PatternVariable)(arg1));

                  if (Surrogate.subtypeOfP(Stella_Object.safePrimaryType(arg2), Logic.SGT_LOGIC_PATTERN_VARIABLE)) {
                    { PatternVariable arg2000 = ((PatternVariable)(arg2));

                      { Stella_Object value1 = Logic.justificationArgumentBoundTo(arg1000, just1);
                        Stella_Object value2 = Logic.justificationArgumentBoundTo(arg2000, just2);

                        if ((value1 == null) ||
                            ((value2 == null) ||
                             (!Stella_Object.eqlP(value1, value2)))) {
                          return (false);
                        }
                      }
                    }
                  }
                  else {
                    if (!Stella_Object.eqlP(Logic.justificationArgumentBoundTo(arg1000, just1), arg2)) {
                      return (false);
                    }
                  }
                }
              }
              else {
                if (Surrogate.subtypeOfP(Stella_Object.safePrimaryType(arg2), Logic.SGT_LOGIC_PATTERN_VARIABLE)) {
                  { PatternVariable arg2000 = ((PatternVariable)(arg2));

                    if (!Stella_Object.eqlP(Logic.justificationArgumentBoundTo(arg2000, just2), arg1)) {
                      return (false);
                    }
                  }
                }
                else {
                  return (false);
                }
              }
            }
          }
        }
      }
      return (true);
    }
    return (false);
  }