14/02/11 20:00:03.23
論理式の構成列 n の最後の項が x とする
（無駄な項を省いて）構成列をツリー状に配置すれば
len(n’)≦len(x)^2 となるような構成列 n’がつくれる（理由は後述する）ことがわかるので
初めから len(n)≦len(x)^2 を満たす n を選んでおく
また、無駄を省いたことで、構成列 n には x の一部である論理式しか現れないとしてよい
n ＝ [P1]^m1×…×[Plen(n)]^mlen(n) ≦ [P1]^x×…×[Plen(n)]^x ≦ { [Plen(x)^2]^x }^len(x)^2 ＝ [Plen(x)^2]^xlen(x)^2
構成列をツリー状に配置すれば
len(n’)≦len(x)^2 となるような構成列 n’がつくれる理由：
構成列 n を元にして論理式 x を構成するツリーをつくる（ツリーの根に当たるのが x である）
このツリーには x の一部である論理式しか現れない
ツリーを遡るほど論理式は短くなるので、ツリーの高さは len(x) 以下
ツリーの葉（最も基本的な論理式）の個数も len(x) 以下
したがって、このツリーに現れる論理式の個数は len(x)×len(x) 以下である
逆にこのようなツリーを元にして x の構成列 n’がつくれる