reg power2 msd_2 "0*10*": def same "At (t T[i+t]=T[j+t]": def complementary "At (t 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 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!=x": eval caseb_ii "Ak,p,x (\$tmper(0,k,p) & p k<=5*x": eval caseb_iii "Ak,p,x (\$tmper(0,k,p) & p k<=6*x":