from z3 import *
set_param(proof=True)
_p1=Int('_p1')
_p2=Int('_p2')
q=Int('q')
p=Int('p')
r=Int('r')
Y=Int('Y')
X=Int('X')
ds=Int('ds')
q1=Int('q1')
p1=Int('p1')
r1=Int('r1')
ds1=Int('ds1')
Y1=Int('Y1')
X1=Int('X1')
_N1=Const('_N1',IntSort())
q7=Function('q7',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(q1 == q7(_N2))
_s.add(p1 == power(2,(_N1-_N2)))
_s.add(r1 == r7(_N2))
_s.add(ds1 == power(2,(_N1-_N2))*Y)
_s.add(X<power(2,_N1)*Y)
_s.add(ForAll([_n1],Implies(And((_n1<_N1),_n1>=0),X>=power(2,_n1)*Y)))
_s.add(Or(_N1==0,X >= Y*power(2, _N1 - 1)))
_s.add(ForAll([_n2],Implies(_n2>=0,q7(_n2 + 1) == If(power(2,(_N1-_n2-1))*Y<=r7((_n2)),power(2,(_N1-_n2-1))+q7((_n2)),q7(_n2)))))
_s.add(ForAll([_n2],Implies(_n2>=0,r7(_n2 + 1) == If(power(2,(_N1-_n2-1))*Y<=r7((_n2)),(-power(2,(_N1-_n2-1)))*Y+r7((_n2)),r7(_n2)))))
_s.add(q7(0) == 0)
_s.add(r7(0) == X)
_s.add((power(2,(_N1-_N2))==1))
_s.add(ForAll([_n2],Implies(And((_n2<_N2),_n2>=0),(power(2,(_N1-_n2))!=1))))
_s.add(Or(_N2==0,(power(2, _N1 - _N2 + 1)!=1)))
_s.add(_N1>=0)
_s.add(_N2>=0)
_s.add(X>=0)
_s.add(Y>0)
_s.add(Not(r7(0) >= 0))
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"
