public static void collectVisibleAntecedents(Justification self, List visibleantecedents) {
    { Cons antecedents = self.antecedents;

      { Justification antecedent = null;
        Cons iter000 = antecedents;

        for (;!(iter000 == Stella.NIL); iter000 = iter000.rest) {
          antecedent = ((Justification)(iter000.value));
          antecedent = Justification.visibleJustification(antecedent);
          { Keyword testValue000 = antecedent.inferenceRule;

            if (testValue000 == Logic.KWD_AND_INTRODUCTION) {
              if (((Keyword)(Logic.$EXPLANATION_STYLE$.get())) == Logic.KWD_BRIEF) {
                { Justification subantecedent = null;
                  Cons iter001 = Justification.visibleAntecedents(antecedent).theConsList;

                  for (;!(iter001 == Stella.NIL); iter001 = iter001.rest) {
                    subantecedent = ((Justification)(iter001.value));
                    visibleantecedents.push(subantecedent);
                  }
                }
              }
              else {
                visibleantecedents.push(antecedent);
              }
            }
            else if (testValue000 == Logic.KWD_PRIMITIVE_STRATEGY) {
              if (((PrimitiveStrategy)(antecedent)).strategy == Logic.KWD_EQUIVALENCE) {
                if (!(Proposition.auxiliaryEquivalencePropositionP(antecedent.proposition))) {
                  visibleantecedents.push(antecedent);
                }
              }
              else {
                visibleantecedents.push(antecedent);
              }
            }
            else {
              visibleantecedents.push(antecedent);
            }
          }
        }
      }
    }
  }