Termination condition for max of array using divide and conuqer approach

Question

I want termination proof of divide and conquer approach to find max of array,I want equational proof in form of lemma.Below is my attempt.I have got accepted everything in dafny ,it is only pointing the termination proof as false.Below is the code-

method maxofarray(a:seq<int>) returns (max1:int)
requires |a|>=0 
ensures |a|==1==>max1==a[0]|||a|>1==>maxpred(max1,a[..|a|])
decreases |a[0..|a|/2]|
{
if (|a|==1)
{
max1:=a[0];
}
else
{
var middle:=|a|/2;
var m1:=maxofarray(a[0..middle]);
var m2:=maxofarray(a[middle..|a|]);
if (m1>=m2)
{
max1:=m1;
}
else
{
max1:=m2;
}
}
}
predicate maxpred(max1:int,a:seq<int>)
{
(|a|>1)==>max1==maxfunc(a)
}
function maxfunc(a:seq<int>):int
decreases |a|
{

if |a|==1 then a[0] else
 max2(
maxfunc(a[0..|a|/2]),
maxfunc(a[|a|/2..|a|])
)
}
function max2(a:int,b:int):int
requires a<b || a>b||a==b
{
if a>=b then a else b
}
I am getting the below error-

 Error: failure to decrease termination measure
Execution trace:
    (0,0): anon0
    (0,0): anon5_Else
C:\Users\Dell\Downloads\dafny\prog\recursion\intro\maxofarray.dfy(14,18): Error: failure to decrease termination measure
Execution trace:
    (0,0): anon0
    (0,0): anon5_Else
C:\Users\Dell\Downloads\dafny\prog\recursion\intro\maxofarray.dfy(35,0): Error: failure to decrease termination measure
Execution trace:

Answer 1

The problem got solved ,below is the fully verified code.

method maxofarray(a:seq<int>) returns (max1:int)
requires (|a|==1)|| (|a|>=2 && |a|>1  )
ensures (|a|==1==>max1==a[0])||(|a|>1==>|a|>=2 ==>maxpred(max1,a[..|a|]))
decreases |a|/2 
{
if (|a|==1)
{
max1:=a[0];

}
else
{
var m1:=maxofarray(a[0..|a|/2]);
var m2:=maxofarray(a[|a|/2..(|a|/2+|a|/2)]);
if (m1>=m2)
{
max1:=m1;
}
else
{
max1:=m2;
}
}
}
predicate maxpred(max1:int,a:seq<int>)
{
|a|>1 ==> |a|>=2==>max1==maxfunc(a)
}
function maxfunc(a:seq<int>):int
requires (|a|==1)|| (|a|>=2  )
decreases |a|/2 
{

if |a|==1 then a[0] else
 max2(
maxfunc(a[0..|a|/2]),
maxfunc(a[|a|/2..(|a|/2+|a|/2)])
)
}
function max2(a:int,b:int):int
requires a<b || a>b||a==b

{
if a>=b then a else b
}
method maxofarray(a:seq<int>) returns (max1:int)
requires (|a|==1)|| (|a|>=2 && |a|>1  )
ensures (|a|==1==>max1==a[0])||(|a|>1==>|a|>=2 ==>maxpred(max1,a[..|a|]))
decreases |a|/2 
{
if (|a|==1)
{
max1:=a[0];

}
else
{
var m1:=maxofarray(a[0..|a|/2]);
var m2:=maxofarray(a[|a|/2..(|a|/2+|a|/2)]);
if (m1>=m2)
{
max1:=m1;
}
else
{
max1:=m2;
}
}
}
predicate maxpred(max1:int,a:seq<int>)
{
|a|>1 ==> |a|>=2==>max1==maxfunc(a)
}
function maxfunc(a:seq<int>):int
requires (|a|==1)|| (|a|>=2  )
decreases |a|/2 
{

if |a|==1 then a[0] else
 max2(
maxfunc(a[0..|a|/2]),
maxfunc(a[|a|/2..(|a|/2+|a|/2)])
)
}
function max2(a:int,b:int):int
requires a<b || a>b||a==b

{
if a>=b then a else b
}
Dafny program verifier finished with 4 verified, 0 errors
Compiled assembly into maxofarray.dll