(|fir_filter5| (|ax1_TCC1| "" (SUBTYPE-TCC) NIL)
 (|ax1_TCC2| "" (SUBTYPE-TCC) NIL) (|ax2_TCC1| "" (SUBTYPE-TCC) NIL)
 (|ax2_TCC2| "" (SUBTYPE-TCC) NIL) (|ax3_TCC1| "" (SUBTYPE-TCC) NIL)
 (|ax3_TCC2| "" (SUBTYPE-TCC) NIL) (|ax3_TCC3| "" (SUBTYPE-TCC) NIL)
 (|ax4_TCC1| "" (SUBTYPE-TCC) NIL) (|ax4_TCC2| "" (SUBTYPE-TCC) NIL)
 (|fir_filter_char_TCC1| "" (SUBTYPE-TCC) NIL)
 (|fir_filter_char_TCC2| "" (SUBTYPE-TCC) NIL)
 (|fir_filter_char_TCC3| "" (SUBTYPE-TCC) NIL)
 (|fir_filter_char| "" (SKOSIMP)
  (("" (AUTO-REWRITE-THEORIES "sum[1, 5]" "fir_filter5")
    (("" (ASSERT) NIL))))))