reg power2 msd_2 "0*10*":
def same "At (t<n) => T[i+t]=T[j+t]":
def complementary "At (t<n) => T[i+t]!=T[j+t]":
eval lemma6_a_1 "Ai,x ($power2(x) & $same(0,i,x) & i<=x) => (i=0|i=x)":
eval lemma6_a_2 "Ai,x ($power2(x) & $complementary(0,i,x) & i<=x) =>
(i=0|i=x)":
eval lemma6_b_1 "Ai,x ($power2(x) & $same(5*x,5*x+i,x) & i<=x) =>
   (i=0|i=x)":
eval lemma6_b_2 "Ai,x ($power2(x) & $complementary(5*x,5*x+i,x) & i<=x) =>
   (i=0|2*i=x)":

def overlap_eq "n>k & n<=2*k & $same(0,n-k,2*k-n)":
def overlap_comp "n>k & n<=2*k & $complementary(0,n-k,2*k-n)":
eval lemma7_1a "Ak,n $overlap_eq(k,n) => 2*n>=3*k":
eval lemma7_1b "Ak,n  ($overlap_eq(k,n) & 2*n=3*k) => $power2(k)":
eval lemma7_2 "Ak,n $overlap_comp(k,n) => 2*n>=3*k":
eval lemma7_2b "Ak,n  ($overlap_comp(k,n) & 2*n=3*k) => $power2(k)":

reg twopower msd_2 msd_2 "[0,0]([1,0]|[0,0])*[1,1][0,0]*":
def tmper "p>0 & p<=n & Aj (j>=i & j+p<i+n) => T[j]=T[j+p]":
eval casea "Ai,n,p,x ($tmper(i,n,p) & $twopower(p,x)) => n<=p+3*x":

eval caseb_i "Ak,p,x ($tmper(0,k,p) & p<k & $twopower(p,x)) => k!=x":
eval caseb_ii "Ak,p,x ($tmper(0,k,p) & p<k & $twopower(p,x) & p=3*x) =>
   k<=5*x":
eval caseb_iii "Ak,p,x ($tmper(0,k,p) & p<k & $twopower(p,x) & p=5*x) =>
   k<=6*x":