from z3 import *
set_param(proof=True)
_p1=Int('_p1')
_p2=Int('_p2')
A=Int('A')
B=Int('B')
q=Int('q')
r=Int('r')
Y=Int('Y')
X=Int('X')
q1=Int('q1')
r1=Int('r1')
A1=Int('A1')
B1=Int('B1')
Y1=Int('Y1')
X1=Int('X1')
_N1=Function('_N1',IntSort(),IntSort())
A7=Function('A7',IntSort(),IntSort())
q7=Function('q7',IntSort(),IntSort())
B7=Function('B7',IntSort(),IntSort())
r7=Function('r7',IntSort(),IntSort())
_N2=Const('_N2',IntSort())
_k1=Const('_k1',IntSort())
_n2=Int('_n2')
_n1=Int('_n1')
power=Function('power',IntSort(),IntSort(),IntSort())
_s=Solver()
_s.add(ForAll([_p1],Implies(_p1>=0, power(0,_p1)==0)))
_s.add(ForAll([_p1,_p2],Implies(power(_p2,_p1)==0,_p2==0)))
_s.add(ForAll([_p1],Implies(_p1>0, power(_p1,0)==1)))
_s.add(ForAll([_p1,_p2],Implies(power(_p1,_p2)==1,Or(_p1==1,_p2==0))))
_s.add(ForAll([_p1,_p2],Implies(And(_p1>0,_p2>=0), power(_p1,_p2+1)==power(_p1,_p2)*_p1)))
_s.set("timeout",60000)
_s.add(Y1 == Y)
_s.add(X1 == X)
_s.add(A1 == A7(_N2))
_s.add(q1 == q7(_N2))
_s.add(r1 == r7(_N2))
_s.add(B1 == B7(_N2))
_s.add(ForAll([_n2],Implies(_n2>=0,r7((_n2))<power(2,(_N1((_n2))+1))*Y)))
_s.add(ForAll([_n1,_n2],Implies(And((_n1<_N1(_n2)),And(_n1>=0,_n2>=0)),power(2,(_n1+1))*Y<=r7((_n2)))))
_s.add(ForAll([_n2],Implies(_n2>=0,Or(_N1(_n2)==0,Y*power(2, _N1(_n2)) <= r7(_n2)))))
_s.add(ForAll([_n2],Implies(_n2>=0,A7(_n2 + 1) == power(2,_N1((_n2))))))
_s.add(ForAll([_n2],Implies(_n2>=0,q7(_n2 + 1) == power(2,_N1((_n2)))+q7((_n2)))))
_s.add(ForAll([_n2],Implies(_n2>=0,B7(_n2 + 1) == power(2,_N1((_n2)))*Y)))
_s.add(ForAll([_n2],Implies(_n2>=0,r7(_n2 + 1) == (-power(2,_N1((_n2))))*Y+r7((_n2)))))
_s.add(A7(0) == A)
_s.add(q7(0) == 0)
_s.add(B7(0) == B)
_s.add(r7(0) == X)
_s.add(r7(_N2) < Y)
_s.add(ForAll([_n2],Implies(And((_n2<_N2),_n2>=0),r7(_n2) >= Y)))
_s.add(Or(_N2==0,r7(_N2 - 1) >= Y))
_s.add(ForAll([_n2],_N1(_n2)>=0))
_s.add(_N2>=0)
_s.add(X>=0)
_s.add(Y>0)
_s.add(_k1>=0)
_s.add(Not(Implies(X==Y*q7(_k1) + r7(_k1),X==Y*(power(2,_N1((_k1)))+q7((_k1))) + ((-power(2,_N1((_k1))))*Y+r7((_k1))))))
if sat==_s.check():
	print "Counter Example"
	print _s.model()
elif unsat==_s.check():
	_s.check()
	if os.path.isfile('j2llogs.logs'):
		file = open('j2llogs.logs', 'a')
		file.write("\n**************\nProof Details\n**************\n"+str(_s.proof().children())+"\n")
		file.close()
	else:
		file = open('j2llogs.logs', 'w')
		file.write("\n**************\nProof Details\n**************\n"+str(_s.proof().children())+"\n")
		file.close()
	print "Successfully Proved"
else:
	print "Failed To Prove"