reg power2 lsd_2 "0*10*":
def adjacent "?lsd_2 ($power2(m) & $power2(n) & m=2*n) 
   | (m=1 & n=0)":
reg hmorph lsd_6 lsd_3 
   "([1,0]|[2,1]|[3,1]|[4,2]|[5,2])*[0,0]*":
reg validcode lsd_6 "(1|2|3|4|5)*0*":
reg prefix lsd_2 lsd_3 lsd_3 "(([0,0,0]|[0,1,0]|[0,2,0])*)|(([0,0,0]|[0,1,1]|[0,2,2])*)([1,0,0]|[1,1,1]|[1,2,2])([0,0,0]|[0,1,0]|[0,2,0])*":
def length "?lsd_2 El $hmorph(?lsd_6 c,?lsd_3 l) & 
   $normalize(?lsd_3 l,?lsd_2 n)":

def look1 "?lsd_2 Ep,q,l,g,h,r,s,x $validcode(?lsd_6 c) 
   & $adjacent(p,q) & $hmorph(?lsd_6 c,?lsd_3 l) & 
   $prefix(?lsd_2 p,?lsd_3 l,?lsd_3 g) & 
   $prefix(?lsd_2 q,?lsd_3 l,?lsd_3 h) & 
   $normalize(?lsd_3 g,?lsd_2 r) &
   $normalize(?lsd_3 h,?lsd_2 s) & n>=s & n<r & x+s=n &
   ((CODE[?lsd_2 p][?lsd_6 c]=@2 & T[x]=@1)
   |(CODE[?lsd_2 p][?lsd_6 c]=@3 & T[x]=@0)
   |(CODE[?lsd_2 p][?lsd_6 c]=@4 & x<p & T[x]=@1)
   |(CODE[?lsd_2 p][?lsd_6 c]=@4 & x>=p & T[x-p]=@1)
   |(CODE[?lsd_2 p][?lsd_6 c]=@5 & x<p & T[x]=@0)
   |(CODE[?lsd_2 p][?lsd_6 c]=@5 & x>=p & T[x-p]=@0))":
def look2 "?lsd_2 (~$validcode(?lsd_6 c)) |
   (El $length(?lsd_6 c,?lsd_2 l) & n>=l)":
combine LOOK look1=1 look2=2:

def hasover "?lsd_2 At (t<=n) => 
   LOOK[?lsd_6 c][i+t]=LOOK[?lsd_6 c][i+n+t]":
def ovlf "?lsd_2 $validcode(?lsd_6 c) & ~Ei,n,l 
   $length(?lsd_6 c,?lsd_2 l) & n>=1 & i+2*n<l & 
   $hasover(?lsd_6 c,?lsd_2 i,?lsd_2 n)":
reg good lsd_6 "(1|2|3|4|5)*":
def ovlfg "?lsd_6 $good(c) & $ovlf(c)":

reg good lsd_6 "(1|2|3|4|5)*":
def agrees "?lsd_2 At (t<b) => 
   LOOK[?lsd_6 c1][t]=LOOK[?lsd_6 c2][t]":
# inputs (b,c1,c2)
# does the word specified by c1 agree with that
# specified by c2 on positions 0 through b-1?

def ispref "?lsd_2 El1,l2 $length(?lsd_6 c1,?lsd_2 l1) & 
   $length(?lsd_6 c2,?lsd_2 l2) & l1<=l2 & 
   $agrees(l1,?lsd_6 c1, ?lsd_6 c2)":
# code c1, c2
# yes if word coded by c1 is a prefix of that coded by c2

def lexlt "?lsd_2 El1,l2,m,i $length(?lsd_6 c1,?lsd_2 l1) &
   $length(?lsd_6 c2,?lsd_2 l2) & $min(l1,l2,m) & i<m & 
   $agrees(i,?lsd_6 c1, ?lsd_6 c2) & 
   LOOK[?lsd_6 c1][?lsd_2 i]<LOOK[?lsd_6 c2][?lsd_2 i]":

def lexlte "?lsd_6 $ispref(c1,c2) | $lexlt(c1,c2)":

def lexleast "?lsd_2 $good(c1) & $validcode(?lsd_6 c1) & 
   $ovlf(?lsd_6 c1) & Ac2,l1,l2 ($validcode(?lsd_6 c2) &
   $ovlf(?lsd_6 c2) & $length(?lsd_6 c2,?lsd_2 l2) &
   $length(?lsd_6 c1,?lsd_2 l1) & l1<=l2) => $lexlte(c1,c2)":

reg prefixc lsd_6 lsd_6 "([1,1]|[2,2]|[3,3]|[4,4]|[5,5])*
([0,1]|[0,2]|[0,3]|[0,4]|[0,5])*[0,0]*":
reg lastnzcode lsd_6 lsd_2 "([1,0]|[2,0]|[3,0]|[4,0]|
   [5,0])*([1,1]|[2,1]|[3,1]|[4,1]|[5,1])[0,0]*":
def tmagree "?lsd_2 El $length(?lsd_6 c,?lsd_2 l) & 
   At (t>=n & t<l) => LOOK[?lsd_6 c][t] = T[t]":
def changebits "?lsd_2 $good(?lsd_6 c) & 
   El $length(?lsd_6 c,?lsd_6 l) & Az Ed,y 
   $prefixc(?lsd_6 c,?lsd_6 d) & $length(?lsd_6 d,?lsd_2 y)
   & y>=z & $tmagree(?lsd_6 d,?lsd_2 l) & $ovlf(?lsd_6 d)":

def avoid73 "?lsd_2 $validcode(?lsd_6 c) & ~Ei,n,l 
   $length(?lsd_6 c,?lsd_6 l) & n>=1 & i+(7*n)/3<l & 
   At (3*t<4*n) => LOOK[?lsd_6 c][i+t]=LOOK[?lsd_6 c][i+n+t]":
def avoid73g "?lsd_6 $good(c) & $avoid73(c)":

def has_square "?lsd_2 At (t<n) => 
   LOOK[?lsd_6 c][i+t]=LOOK[?lsd_6 c][i+t+n]":
eval squ "?lsd_2 Ac,l ($ovlf(?lsd_6 c) & 
   $length(?lsd_6 c,?lsd_2 l) & l>7) => Ei,n i+2*n<=l 
   & 6*n>=l & $has_square(?lsd_6 c,?lsd_2 i,?lsd_2 n)":

def squ3 "?lsd_2 Ei,n,l $ovlf(?lsd_6 c) & 
   $length(?lsd_6 c,?lsd_2 l) & i+2*n<=l & 6*n=l &
   $has_square(?lsd_6 c, ?lsd_2 i, ?lsd_2 n)":
def squ3b "?lsd_2 Ai,n,l ($ovlf(?lsd_6 c) & 
   $length(?lsd_6 c,?lsd_2 l) & i+2*n<=l & 
   $has_square(?lsd_6 c, ?lsd_2 i, ?lsd_2 n)) => 6*n<=l":
def squ4g "?lsd_6 $good(c) & $squ3(c) & $squ3b(c)":

eval squaresin "?lsd_2 Ac,l ($validcode(?lsd_6 c) &
   $length(?lsd_6 c,?lsd_2 l) & l>8) => Ei,n i+2*n<=l
   & 7*n>=l+2 & $has_square(?lsd_6 c,?lsd_2 i,?lsd_2 n)":

def squr3 "?lsd_2 Ei,n,l $validcode(?lsd_6 c) & 
   $length(?lsd_6 c,?lsd_2 l) & i+2*n<=l & 7*n=l+2 &
   $has_square(?lsd_6 c,?lsd_2 i,?lsd_2 n)":
def squr3b "?lsd_2 Ai,n,l ($validcode(?lsd_6 c) &
   $length(?lsd_6 c,?lsd_2 l) & i+2*n<=l & 
   $has_square(?lsd_6 c,?lsd_2 i,?lsd_2 n)) => 7*n<=l+2":
def squr4g "?lsd_6 $good(c) & $squr3(c) & $squr3b(c)":

eval fourthr "?lsd_2 Ei,n,l,c $validcode(?lsd_6 c) & 
   $length(?lsd_6 c,?lsd_6 l) & n>=1 & i+3*n<=l & At (t<3*n)
   => LOOK[?lsd_6 c][i+t]=LOOK[?lsd_6 c][i+n+t]":

eg lastnzcode lsd_6 lsd_2 "([1,0]|[2,0]|[3,0]|[4,0]|[5,0])*
   ([1,1]|[2,1]|[3,1]|[4,1]|[5,1])[0,0]*":
# last bit x with a nonzero code
# input is c,x
def maxexp "?lsd_2 Ex,l,i $lastnzcode(?lsd_6 c,?lsd_2 x) &
   $length(?lsd_6 c,?lsd_2 l) & i+2*x+2<=l+1 & At (t<3*x/2-1)
   => LOOK[?lsd_6 c][i+t]=LOOK[?lsd_6 c][i+t+x/2]":

def agrees "?lsd_2 At (t<b) => 
   LOOK[?lsd_6 c1][t]=LOOK[?lsd_6 c2][t]":
def prefixequal "?lsd_2 El,m 
   $length(?lsd_6 c1,?lsd_2 l) & 
   $length(?lsd_6 c2,?lsd_2 m) & l>=n & m>=n & 
   $agrees(?lsd_2 n,?lsd_6 c1, ?lsd_6 c2)":
def mincode "?lsd_2 El $ovlf(?lsd_6 c1) & 
   $length(?lsd_6 c1, ?lsd_2 l) & l>=n & 
   Ac2 ($prefixequal(?lsd_6 c1,?lsd_6 c2,?lsd_2 n) &
   $ovlf(?lsd_6 c2)) => (?lsd_6 c1<=c2)":
def minmat n "$mincode(?lsd_6 c,?lsd_2 n)":