Termination condition for max of array using divide and conuqer approach

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
Execution trace:
(0,0): anon0
(0,0): anon5_Else
Execution trace:

• We are not a coding site. I don't think asking us to provide proofs of correctness for a bunch of code is on-topic here. Any community votes? (We're looking to build up an archive of knowledge that will be useful to others in the future. It seems hard to see how this question will be useful to anyone else unless they are trying to do exactly the same thing with exactly the same code.)
– D.W.
Commented Mar 8, 2022 at 21:19
– D.W.
Commented Mar 8, 2022 at 21:19

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