Balanced rectangles Walnut code

reg shift {0,1} {0,1} "([0,0]|[0,1][1,1]*[1,0])*":
def phin "?msd_fib (n=0 & y=0) | Ez $shift(n-1,z) & y=z+1":
def alpha "?msd_fib (n=0&z=0) | (n>0 & Ex $phin(n,x) & z+1+x=2*n)":
def diff "?msd_fib Ea,b,c,d $alpha(i,a) & $alpha(i+m,b) & $alpha(i+n,c) 
   & $alpha(i+m+n,d) & z+b+c=a+d+1":
def bal "?msd_fib ~Ei,j i>0 & i<j & (($diff(i,m,n,2) 
   & (Ak (i<k & k<j) => $diff(k,m,n,1)) & $diff(j,m,n,2)) |
   ($diff(i,m,n,0) & (Ak (i<k & k<j) => $diff(k,m,n,1)) & $diff(j,m,n,0)))":

reg isfib msd_fib "0*10*":
def max "?msd_fib (z=m|z=n) & z>=m & z>=n":
eval anselmo "?msd_fib Am,n,z ($max(m,n,z) & $isfib(z)) => $bal(m,n)":

reg adjfib msd_fib msd_fib "[0,0]*[0,1][1,0][0,0]*":
eval claim_a "?msd_fib Au,v,x,i,ip,j ($adjfib(u,v) & x=u+v & i>v & ip>v 
   & i<x & ip<x & j>=v-u) => ($bal(i,j) <=> $bal(ip,j))":
eval claim_b "?msd_fib Au,v,x,i,j ($adjfib(u,v) & x=u+v & i>=1 & i<u & j>=1) 
   => ($bal(v+i,j) <=> $bal(x-i,j))":
eval density "?msd_fib Am,x,y,n ($adjfib(x,y) & x<m & m<=y) 
   => Ej j>=1 & j<=y & $bal(m,n+j)":
eval density2 "?msd_fib Am,x,y ($adjfib(x,y) & x<m & m<=y) 
   => (En Aj (j>=1 & j<y) => ~$bal(m,n+j))":

def balp "?msd_fib $bal(m,n) & m<=n":

reg case_a msd_fib msd_fib "([0,0]|[0,1])*|([0,0]|[0,1])*([1,0]|[1,1])":
reg case_b msd_fib msd_fib 
"([0,0]|[0,1])*[0,1][0,0]([0,0][0,0])*[1,0]([0,0]|[0,1])*":
reg case_c msd_fib msd_fib "([0,0]|[0,1])*[1,1]([0,0]|[0,1])*":
reg case_d msd_fib msd_fib 
"([0,0]|[0,1])*[0,1]([0,0][0,0])*[1,1]([0,0]|[1,0])*":
reg case_e msd_fib msd_fib "([0,0]|[0,1])*([0,0]|[1,0])*":
eval test "?msd_fib Am,n (m<=n) => 
   (($case_a(m,n)|$case_b(m,n)|$case_c(m,n)|$case_d(m,n)|$case_e(m,n)) 
   <=> $bal(m,n))":

reg fib6 msd_fib "0*1(000000)*0000":
def cnt6a t "?msd_fib $fib6(t) & Ex,y $adjfib(t,x) & $adjfib(x,y) & 
   F[(y-1)/4+j+k]=@1 & j<t/2 & k<t/2":
def cnt6b t "?msd_fib $fib6(t) & Eu $adjfib(u,t) & 
   F[(u-1)/4+j+k]=@1 & j<t/2 & k<t/2":
def numfib "?msd_fib Ey $adjfib(x,y) & i<=y & $isfib(i)":
def numfib6 t "?msd_fib $fib6(t) & $numfib(i,t)":

reg shift {0,1} {0,1} "([0,0]|[0,1][1,1]*[1,0])*":

def triba "?msd_trib (s=0&n=0) | Ex $shift(n-1,x) & s=x+1":
def tribb "?msd_trib (s=0&n=0) | Ex,y $shift(n-1,x) &
   $shift(x,y) & s=y+2":
def tribc "?msd_trib (s=0&n=0) | Ex,y,z $shift(n-1,x) &
   $shift(x,y) & $shift(y,z) & s=z+4":
def tribd "?msd_trib Et,u $triba(s,t) & $triba(s+1,u) & t<=n & n<u":
def tribe "?msd_trib Et,u $tribb(s,t) & $tribb(s+1,u) & t<=n & n<u":
def tribf "?msd_trib Et,u $tribc(s,t) & $tribc(s+1,u) & t<=n & n<u":

def num0 "?msd_trib Ex,y $tribd(i,x) & $tribd(i+n,y) & z+x=y":
def num1 "?msd_trib Ex,y $tribe(i,x) & $tribe(i+n,y) & z+x=y":
def num2 "?msd_trib Ex,y $tribf(i,x) & $tribf(i+n,y) & z+x=y":

def row2_0 "?msd_trib Ex,y $num0(i,n,x) & $num0(i+1,n,y) & z=x+y":
def row2_1 "?msd_trib Ex,y $num1(i,n,x) & $num1(i+1,n,y) & z=x+y":
def row2_2 "?msd_trib Ex,y $num2(i,n,x) & $num2(i+1,n,y) & z=x+y":

def chk2_0 "?msd_trib Ai,j,y,z ($row2_0(i,n,y) & $row2_0(j,n,z) & y<=z) 
   => (z<=y+2)":
def chk2_1 "?msd_trib Ai,j,y,z ($row2_1(i,n,y) & $row2_1(j,n,z) & y<=z) 
   => (z<=y+2)":
def chk2_2 "?msd_trib Ai,j,y,z ($row2_2(i,n,y) & $row2_2(j,n,z) & y<=z) 
   => (z<=y+2)":

def bal2 "?msd_trib $chk2_0(n) & $chk2_1(n) & $chk2_2(n)":

morphism map2 "0->0 1->0 2->2":
image TR2 map2 TR:
def trib2eqfac "?msd_trib Au,v (u>=i & u<i+n & u+j=v+i) =>
TR2[u]=TR2[v]":
eval cb2 "?msd_trib Ap Ei,j $trib2eqfac(i,j,p) & TR2[i+p]=@0 &
TR2[i+p+1]=@0 & TR2[i+p+2]=@0 & TR2[i+p+3]=@0 & TR2[i+p+4]=@0 &
TR2[j+p]=@0 & TR2[j+p+1]=@0 & TR2[j+p+2]=@2 & TR2[j+p+3]=@0 &
TR2[j+p+4]=@0": 

def n2even "?msd_neg_2 Ek n=2*k":
def n2odd "?msd_neg_2 Ek n=2*k+1":
def prefsum "?msd_neg_2 (s=n/2 & $n2even(n)) | (s=n/2+TM2[n-1] & $n2odd(n))":
def factorsum "?msd_neg_2 Eu,v $prefsum(i,u) & $prefsum(i+n,v) & s+u=v":
def m_even_n_even "?msd_neg_2 Ea,b $factorsum(i/2,m/2,a) &
$factorsum((i+n)/2,m/2,b) & s=2*(b-a)":
def m_even_n_odd "?msd_neg_2 Ea,b $m_even_n_even(i,m,n-1,a) &
$factorsum(i+n-1,m,b) & s=a+2*b-m":
def m_odd_n_even "?msd_neg_2 Ea,b $m_even_n_even(i,m-1,n,a) &
$factorsum(i+m-1,n,b) & s=a+2*b-n":
def m_odd_n_odd "?msd_neg_2 Ea,b $m_odd_n_even(i,m,n-1,a) &
$factorsum(i+n-1,m,b) & s=a+2*b-m":
def tmt "?msd_neg_2 i>=0 & m>=0 & n>=0 &
(($n2even(m) & $n2even(n) & $m_even_n_even(i,m,n,s)) |
($n2even(m) & $n2odd(n) & $m_even_n_odd(i,m,n,s)) |
($n2odd(m) & $n2even(n) & $m_odd_n_even(i,m,n,s)) |
($n2odd(m) & $n2odd(n) & $m_odd_n_odd(i,m,n,s)))":
def maxval "?msd_neg_2 (Ei $tmt(i,m,n,x)) & Ai,s $tmt(i,m,n,s) => s<=x":
def tmbal "Ex,y,b $twonegtwo((?msd_neg_2 x),m) & $twonegtwo((?msd_neg_2 y),n) &
$twonegtwo((?msd_neg_2 b),z) & $maxval(?msd_neg_2 x,y,b)":
def aut0 "$tmbal(m,n,0)":
def aut1 "$tmbal(m,n,1)":
def aut2 "$tmbal(m,n,2)":
def aut3 "$tmbal(m,n,3)":
def aut4 "$tmbal(m,n,4)":
combine TMB aut0=0 aut1=1 aut2=2 aut3=3 aut4=4:

def even "Ek n=2*k":
def odd "Ek n=2*k+1":
eval bal3 "Am,n (m>=3 & n>=3) => (($odd(m) & $odd(n)) <=> TMB[m][n]=@3)":

