#===================================================
#
#  Examples for RRC/PRF/RQE based geometrical inequality proving - gen file [1]
#   Each example is given with their inputs for
#   for easy copy/pasting (TempDecision: Infos are (will be) put to a different place)
#
#  Version 1.0 - 29/3/20
#===================================================

#===================================================

#1: IsoB1.1a (dervied from Bottema 1.1, b=c, wlog b=1)

#QEPCAD

[]
(m,a)
1
(Ea)[ m>0 /\ a>0 /\ 2-a>0 /\  (2+a)^2=m (1+2a)].

#MMA

Resolve[
Exists[a, m > 0 \[And] 0 < a < 2 \[And] (2 + a)^2 == m (1 + 2 a)], 
Reals]

#RRC

R:=PolynomialRing([a,m]):
IS:=[(2+a)^2-m*(1+2*a)],[],[m,a,2-a],[]:
rrc:=RealRootClassification(IS,1,1..k,R);

#PRF

IS:=[(2+a)^2-m*(1+2*a)=0, m>0,a>0,2-a>0],[a],[m]:
cc:=CellDecomposition(IS);

#2: IsoB1.1b (dervied from Bottema 1.1, b=c, wlog a=1)

#QEPCAD

[]
(m,b)
1
(Eb)[ m>0 /\ 2b>1 /\  (1+2b)^2=m (2b+b^2)].



#

#3: IsoB1.1d (derived from Bottema 1.1 GGBA/man generated problem)

#QEPCAD

#MMA

Resolve[
Exists[{v10, v11}, m > 0 \[And] v11 > 0 \[And] 
v10^2 - v11^2 + 1/4 == 0 \[And] (4 v11^2 + 4 v11 + 1)==m (v11^2 + 2 v11)],
m,Reals]


#4: TriB1.1a (dervied from Bottema 1.1, wlog c=1)

#QEPCAD

[]
(m,b,a)
1
(Eb)(Ea)[ m>0 /\ a+b-1>0 /\ a+1-b>0 /\ b+1-a>0 /\  (a+b+1)^2=m (a b+b+a)].


#MMA

Resolve[
Exists[{a,b}, m > 0 \[And] a+b>1 \[And] a+1-b>0 \[And] b+1-a>0 \[And]
(a+b+1)^2 == m (a b + b + a)], 
Reals]


#5 TriB1.1.d (derived from Bottema-1.1,a GGBA/man genrated problem, wlog c=1)

#MMA

Resolve[
Exists[{v5, v7, v8}, (m > 0) \[And] ((v7 + v8 + 1)^2 == 
     m*(v7*v8 + v8 + v7)) \[And] (v8 > 0) \[And] (v7 > 0) 
     \[And] (-v7^2 + v8^2 - 2*v5 + 1 == 0) \[And] v8^2 - v5^2 >= 0], Reals]



#QEPCAD

(m,v7,v8,v5)
1
(Ev7)(Ev8)(Ev5)[ m>0 /\ v7>0 /\ v8>0 /\ v8^2-v5^2>=0 /\ -v7^2+v8^2-2v5+1=0 /\ (v7+v8+1)^2=m(v7 v8+ v8+v7)].











#3: Bottema 1-3
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ m  (b+c-1) (1+c-b) (1+b-c)= 8 b c ].
finish

#4: Bottema 1-4
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ m b c=(b+1) (c+1) (b+c) ].
finish

#5: Bottema 1-5
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (1+b) (1+c) (b+c) = m (1^3+b^3+c^3) ].
assume[m>0].
finish

#6: Bottema 1-6
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (1 + b + c) (1^2 + b^2 + c^2) = m (1^3 + b^3 + c^3 + 3 b c) ].
assume[m>0].
finish

#7: Bottema 1-7
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (b + c - 1) + b^2 (1 + c - b) + c^2 (1 + b - c) = m 2 b c ].
assume[m>0].
finish

#8: Bottema 1-8
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ 8 (b c (b + c) + 1 c (1 + c) + 1 b (1 + b)) = m (b + c - 1) (1 + c - b) (1 + b - c) ].
assume[m>0].
finish

#9: Bottema 1-9
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ 1^3 (b + c - 1) + b^3 (1 + c - b) + c^3 (1 + b - c) = m b c (1 + b + c) ].
assume[m>0].
finish

#10: Bottema 1-11
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\  1^2 b (1-b)+b^2 c (b-c)+c^2 1 (c-1) = m].
finish

#11: Bottema 1-12
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (1+b+c)^3 (b+c-1) (1+c-b) (1+b-c)= 64 m (1 b c)^2].
assume[m>0].
finish

#12: Bottema 1-13-a1
(b,c,m,q)
3
(Eq)[q>0 /\ 2 q^2=(1-b)^2+(b-c)^2+(c-1)^2 /\ 1+b>c /\ 1+c>b /\ b+c>1 /\ m b c = 2 ((1/2)(1+b+c)-q) (1+b+c+q)^2].
assume[m>0].
proj-op(m,m,h)
finish

#13: Bottema 1-13-a2
(m,b,c)
1
(Eb)(Ec)[c - b - 1 < 0 /\ c - b + 1 > 0 /\ c + b - 1 > 0 /\ b c m + 2 c^3 - 3 b c^2 - 3 c^2 - 3 b^2 c - 15 b c - 3 c + 2 b^3 - 3 b^2 - 3 b + 2 < 0 /\ b^2 c^2 m^2 + 4 b c^4 m - 6 b^2 c^3 m - 6 b c^3 m - 6 b^3 c^2 m - 30 b^2 c^2 m - 6 b c^2 m + 4 b^4 c m - 6 b^3 c m - 6 b^2 c m + 4 b c m - 27 b^2 c^4 - 54 b c^4 - 27 c^4 + 54 b^3 c^3 + 108 b^2 c^3 + 108 b c^3 + 54 c^3 - 27 b^4 c^2 + 108 b^3 c^2 + 243 b^2 c^2 + 108 b c^2 - 27 c^2 - 54 b^4 c + 108 b^3 c + 108 b^2 c - 54 b c - 27 b^4 + 54 b^3 - 27 b^2 = 0].
assume[m>0].
finish

#14: Bottema 1-14
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\  m (1+b+c) b c = 2 (b^2 c^2+c^2+b^2)].
assume[m>0].
finish

#15: Bottema 1-15
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\  (1+b+c) ((1+c-b)(1+b-c)+(b+c-1)(1+b-c)+(b+c-1)(1+c-b)) = m (b+c-1) (1+b-c) (1+c-b)].
assume[m>0].
finish

#16: Bottema 1-16
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\  (c+1)(b+1)+b(b+c)(b+1)+c(b+c)(c+1) =m (b+c)(c+1)(b+1)].
assume[m>0].
finish

#17: Bottema 1-17
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (b+c+3)(b+1)(c+1)+(1+c+3b)(b+1)(b+c)+(1+b+3c)(c+1)(b+c)=2 m (b+c)(1+b)(1+c)].
assume[m>0].
finish

#18: Bottema 1-18
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (b-1)(c-1) + m b c=(c^2-c)+(b^2-b)].
assume[m>0].
finish

#19: Bottema 1-19
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\  (1^2+b^2+c^2) = m (1+b+c)^2].
assume[m>0].
finish

#20: Bottema 1-20-1
(b,x,y,z,u,c)
5
(Ec)[x>0 /\ y>0 /\ z>0 /\ u>0 /\ 2 x^2=1+b+c /\ 2 y^2=b+c-1 /\ 2 z^2=1+c-b /\ 2 u^2=1+b-c /\1+b>c /\ 1+c>b /\ b+c>1].
finish

#21: Bottema 1-20-2
(x,y,z,u,b)
4
(Eb)[x - 1 > 0 /\ y > 0 /\ y^2 - x^2 + 1 = 0 /\ z > 0 /\ z^2 - x^2 + b = 0 /\ u > 0 /\ u^2 + x^2 - b - 1 = 0].
finish

#22: Bottema 1-20-3
(m,x,y,z,u)
1
(Ex)(Ey)(Ez)(Eu)[ y+z+u = m x /\ x - 1 > 0 /\ y > 0 /\ y^2 - x^2 + 1 = 0 /\ z > 0 /\ u > 0 /\ u^2 + z^2 - 1 = 0].
finish

#23: Bottema 1-23
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (1+b+c)^3 = (m (b c (b+c)+c (c+1)+b (b+1))-3 b c)].
assume[m>0].
finish

#24: Bottema 1-24
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ 1+c>b /\ b+c>1 /\ (b+1)(c+1)=m b c+(b+b^2)+(c+c^2)].
assume[m>0].
finish