遅延リストやストリームといった仮想的に無限長とみなされるデータを扱う関数型プログラムの計算モデルとして，無限項書き換えシステムが提案されている．項書き換えシステムにおける停止性に対応する基本的な性質として，無限項書き換えシステムにおける強頭部正規化可能性があり，その証明法がZantema(2008)やEndrullisら(2009)によって報告されている．また，Endrullisら(2010)は無限項書き換えシステムの部分クラスであるストリーム項書き換えシステムを提案し，ある十分条件のもとでのストリームの生成性判定手続きを報告している．本論文では，強頭部正規化可能性および一般生成性に対する反証手続きを提案する．提案する手続きの基本的なアイデアは，有限表現をもつ無限項である正則項の反例を構成する点にある．反証手続きの正しさを示すとともに，手続きの実装を報告する．実験の結果，自動反証法が従来知られていない例について自動反証に成功することを確認した．