qex 原理（その２）

p2t では abs,max2,min2 も

defrule(powertk2, abs(aa), (aa^2)^(1/2))$
defrule(powertk3, max2(aa,bb), (aa+bb+abs(aa-bb))/2)$
defrule(powertk4, min2(aa,bb), (aa+bb-abs(aa-bb))/2)$

により，冪乗関数に変換して処理しています．流れを例示します．

次の式は恒真です．

(%i1) f:max2(min2(a,b),c)=min2(max2(a,c),max2(b,c));
Evaluation took 0.0000 seconds (0.0000 elapsed) using 560 bytes.
(%o1) max2(min2(a,b),c) = min2(max2(a,c),max2(b,c))

実際

(%i2) qex(f);
Evaluation took 1.9800 seconds (2.7400 elapsed) using 265.126 MB.
(%o2) true

となります．前回同様，量化の具合を見ると

(%i3) p2em(f);
Evaluation took 0.2200 seconds (0.2200 elapsed) using 22.855 MB.
(%o3) qe([[E,rt1],[E,rt2],[E,rt3],[E,rt4],[E,rt5]],
         (rt1 >= 0) %and (rt1^2 = (b-a)^2) %and (rt2 >= 0)
                    %and ((rt2+((-rt1)+b+a)/2+c)/2
                     = ((-rt5)+(rt4+c+b)/2+(rt3+c+a)/2)/2)
                    %and (rt2^2 = (c-((-rt1)+b+a)/2)^2) %and (rt3 >= 0)
                    %and (rt3^2 = (c-a)^2) %and (rt4 >= 0)
                    %and (rt4^2 = (c-b)^2) %and (rt5 >= 0)
                    %and (rt5^2 = ((rt4+c+b)/2-(rt3+c+a)/2)^2))

のように５変数です．

これに至る過程は，まず，powertk4 で，f における min2 を abs で

(%i4) applyb1(f,powertk4);
Evaluation took 0.0000 seconds (0.0000 elapsed) using 88.875 KB.
(%o4) max2(((-abs(b-a))+b+a)/2,c) = ((-abs(max2(b,c)-max2(a,c)))+max2(b,c)+max2(a,c))/2

powertk3 で max2 も abs で

(%i5) applyb1(f,powertk4,powertk3);
Evaluation took 0.0000 seconds (0.0100 elapsed) using 809.602 KB.
(%o5) (abs(c-((-abs(b-a))+b+a)/2)+c+((-abs(b-a))+b+a)/2)/2
  = ((-abs((abs(c-b)+c+b)/2-(abs(c-a)+c+a)/2))
  +(abs(c-b)+c+b)/2+(abs(c-a)+c+a)/2)/2

さらに，powertk2 で abs を sqrt で表し，前回述べた方法で束縛変数に置き換えています．

(%i6) applyb1(f,powertk4,powertk3,powertk2);
Evaluation took 0.0200 seconds (0.0100 elapsed) using 1.960 MB.
(%o6) (sqrt((c-((-sqrt((b-a)^2))+b+a)/2)^2)+c+((-sqrt((b-a)^2))+b+a)/2)/2
  = ((-sqrt(((sqrt((c-b)^2)+c+b)/2-(sqrt((c-a)^2)+c+a)/2)^2))
  +(sqrt((c-b)^2)+c+b)/2+(sqrt((c-a)^2)+c+a)/2)/2

なお，%o6 を見ると，sqrt の出現は８箇所ですが，sqrt((c-a)^2),sqrt((b-a)^2),sqrt((c-b)^2) は２箇所ずつあるので，５変数に納まっています．これが８変数だと

(%i7) p2em(f),p2etype:0;
Evaluation took 0.2800 seconds (0.2900 elapsed) using 30.215 MB.
(%o7) qe([[E,rt1],[E,rt2],[E,rt3],[E,rt4],[E,rt5],[E,rt6],[E,rt7],[E,rt8]],
         (rt1 >= 0) %and (rt1^2 = (b-a)^2) %and (rt2 >= 0)
                    %and (rt2^2 = (b-a)^2) %and (rt3 >= 0)
                    %and ((rt3+((-rt1)+b+a)/2+c)/2
                     = ((-rt8)+(rt5+c+b)/2+(rt4+c+a)/2)/2)
                    %and (rt3^2 = (c-((-rt2)+b+a)/2)^2) %and (rt4 >= 0)
                    %and (rt4^2 = (c-a)^2) %and (rt5 >= 0)
                    %and (rt5^2 = (c-b)^2) %and (rt6 >= 0)
                    %and (rt6^2 = (c-a)^2) %and (rt7 >= 0)
                    %and (rt7^2 = (c-b)^2) %and (rt8 >= 0)
                    %and (rt8^2 = ((rt7+c+b)/2-(rt6+c+a)/2)^2))

となり，これを評価するのは，．．．