%% The best constants/formulae which belongs to the unit square @var=2
%%
%% (1)  (u0,v0)=(0,0)  (1,v1) (u2,1)
%%
%% input formula QEPCAD
%% 
   (Ex1)(Ex2)[ L>1 /\ 0<=x1 /\ x1<=1 /\ 0<x2 /\ x2<=1 /\ 1+2 x1-x1 x2<=L(1-x1 x2) /\ 1+2 x2-x1 x2<=L(1-x1 x2) /\ 3-2 x1-2 x2+x1 x2<=L(1-x1 x2)].
%%
   (EL)(Ex1)(Ex2)[ L>1 /\ 5L^2-10L+1<0 /\ 0<=x1 /\ x1<=1 /\ 0<x2 /\ x2<=1 /\ 1+2 x1-x1 x2<=L(1-x1 x2) /\ 1+2 x2-x1 x2<=L(1-x1 x2) /\ 3-2 x1-2 x2+x1 x2<=L(1-x1 x2)].

%% input formula MMA
%%
   Exists[{x1,x2},L>1 \[And] (0<x1<=1) \[And] (0<x2<=1) \[And] 1+2 x1-x1 x2<=L(1-x1 x2) \[And] 1+2 x2-x1 x2<=L(1-x1 x2) \[And] 3-2 x1-2 x2+x1 x2<=L(1-x1 x2)]
%%
   Exists[{L,x1,x2},L>1 \[And] 5L^2-10L+1<0 \[And] (0<x1<=1) \[And] (0<x2<=1) \[And] 1+2 x1-x1 x2<=L(1-x1 x2) \[And] 1+2 x2-x1 x2<=L(1-x1 x2) \[And] 3-2 x1-2 x2+x1 x2<=L(1-x1 x2)]



%%
%% input formula for pari/gp
 
tst12([ex,ex],[l,x1,x2],(f1,f2,f3,f4,f5,f6,f7,f8)->(f1*f2*f3*f4*f5*f6*f7*f8),"l>1, 0<=x1, x1<=1, 0<=x2, x2<=1, (1+2*x1-x1*x2)<=l*(1-x1*x2), 1+2*x2-x1*x2<=l*(1-x1*x2), 3-2*x1-2*x2+x1*x2<=l*(1-x1*x2)",1) 


%% input formula INTLAB
%%
 
f02a=@(x) max(max(abs((-1-2*x(1,:)+x(1,:).*x(2,:))./(x(1,:).*x(2,:)-1)),(-1-2*x(2,:)+x(1,:).*x(2,:))./(x(1,:).*x(2,:)-1)),(-3+2*x(1,:)+2*x(2,:)-x(1,:).*x(2,:))./(x(1,:).*x(2,:)-1))

[mu,L,Ls]=verifyglobalmin(f02a,infsup(0,1)*ones(2,1))


%%OUTPUTS:

L - 1 > 0 /\ 5 L^2 - 10 L + 1 >= 0

Counts for Projection Phase:
----------------------------------------------------
Level                1         2         3     Total
----------------------------------------------------
Proj Poly           33        12         0        45
Proj Fact           18        11         5        34
----------------------------------------------------

Counts for Truth--Invariant CAD Construction Phase:
----------------------------------------------------
Level                1         2         3     Total
----------------------------------------------------
Stacks               1        21        85       107
..Rational           1        13        45        59
Cells               43       465       817      1325
Conversion           0         0        19        19
..Trivial            0         0        16        16
----------------------------------------------------


 *** using Lazard's method (MPP17).

parisize = 8000000, primelimit = 500000
tst12, 08/06/2021 17:43:16
? tst12([ex,ex],[l,x1,x2],(f1,f2,f3,f4,f5,f6,f7,f8)->(f1*f2*f3*f4*f5*f6*f7*f8),"l>1, 0<=x1, x1<=1, 0<=x2, x2<=1, (1+2*x1-x1*x2)<=l*(1-x1*x2), 1+2*x2-x1*x2<=l*(1-x1*x2), 3-2*x1-2*x2+x1*x2<=l*(1-x1*x2)",1) 
 *** using Lazard's method (MPP17).
[x2,5]
[x1,11]
[l,14]
proj = 117 ms.
21 279(4,33) 18(0,69) 
 *** combined adjacent 17 cells.
time = 106 ms.
%1 = [[[[p11, 2]~, +oo], [-oo, +oo], [-oo, +oo]]]
? pp
%2 = [[l - 1, l - 3, l - 2, l + 1, l^3 - 7*l^2 + 23*l - 25, l^2 - 5, l^3 - 7*l^2 + 7*l + 7, l^2 - 4*l - 1, l^3 + l^2 - l - 9, l^3 - 7*l^2 + 15*l - 1, 5*l^2 - 10*l + 1, l^3 + l^2 - 9*l - 1, l, l^3 + l^2 + 7*l - 1], [x1, x1 - 1, -l + (2*x1 + 1), l + (2*x1 - 3), (x1 - 1)*l + (x1 + 1), (x1 - 1)*l + (-x1 + 3), (x1^2 - 1)*l + (-x1^2 + 2*x1 + 1), (2*x1^2 - 2*x1 + 1)*l - 1, x1*l + (-x1 + 2), (x1^2 - 2*x1 + 2)*l + (-x1^2 + 4*x1 - 4), x1*l + (x1 - 2)], [x2, x2 - 1, (x2*x1 - 1)*l + ((-x2 + 2)*x1 + 1), (x2*x1 - 1)*l + (-x2*x1 + (2*x2 + 1)), (x2*x1 - 1)*l + ((x2 - 2)*x1 + (-2*x2 + 3))]]