%Commands for section 1

def a260317 "?msd_fib Aa,b (a<b & $upper(a) & $upper(b)) => a+b!=n":

eval test "?msd_fib An ($a260317(n) & $a260317(n+1)) => n<14":

def marker2 "?msd_fib $a260317(n) & $a260317(n+2) & n>13":

def gapmark2 "?msd_fib En (t>0) & $marker2(n) & $marker2(n+t) & (As (s<t & s>0) => ˜$marker2(n+s))":

eval test "?msd_fib An $gapmark2(n) <=> (n>4 & $isfib(n))":

def triplegap "?msd_fib En (t>0) & (u>0) & (v>0) & $marker2(n) & $marker2(n+t) & $marker2(n+t+u) & $marker2(n+t+u+v) & (Aw (w>0) & (w<t+u+v) & (w!=t&w!=t+u) => ˜$marker2(n+w))":

eval test "?msd_fib At,u,v $triplegap(t,u,v) <=> ( $isfib(t) & $isfib(u) & $isfib(v) & $isfib(t+v) & (t<=u) & (u<=v) & (t>4) )":

eval test "?msd_fib Ak,m,n ( m>14 & k>m+2 & n>k ) (& $marker2(m) & $marker2(n) & (Ap((p<n) & (p>m)) => ˜$marker2(p))) => ($a260317(k) <=> $a260317(n+m+2-k) )":

eval test "?msd_fib A n (n>=14 & $marker2(n)) => $a260317(n+5)":

eval test "?msd_fib A m,n (n>m & $marker2(m) & $marker2(n) & (Ap ((p<n) & (p>m)) => ˜$marker2(p))) => (Ak k>m+2 & k<n => ($a260317(k)<=> $a260317(n-m+k)))":

reg isoddfib msd_fib "0*10(00)*":

eval test "?msd_fib A m,n (n>m & $marker2(m) & $marker2(n) & $isoddfib(n-m) & (Ap ((p<n) & (p>m)) => ˜$marker2(p))) => (Ak k>m+2 & k<=n => ($a260317(k)<=> $a260317(n-m+k)))":

reg isevenfib msd_fib "0*1(00)*":

eval test "?msd_fib A m,n (n>m & $marker2(m) & $marker2(n) & ˜$marker2(2*n-m) & $isevenfib(n-m) & (Ap ((p<n) & (p>m)) => ˜$marker2(p))) => ˜$a260317(2*n-m)":

%Commands section 3

def antifib "Ek n=2*k+1 & x=3+10*k | Ek n=2*k+2 & PD[k]=@1 & x=9+10*k | Ek n=2*k+2 & PD[k]=@0 & x=8+10*k":

def nonafib "Ek n=4*k & y=5*k | Ek n=4*k+1 & y=5*k+1 | Ek n=4*k+2 & y=5*k+2 | Ek n=4*k+3 & PD[k]=@1 & y=5*k+4 | Ek n=4*k+3 & PD[k]=@0 & y=5*k+3":

eval zaslavsky1 "An,x,y,z ((n>0) & $nonafib(2*n-1,x) & $nonafib(2*n,y) & $antifib(n,z)) => x+y=z":

eval zaslavsky2 "Ei,j,n (n>0) & $nonafib(i,n) & $antifib(j,n)":

eval zaslavsky3 "An (n>0) => (Ej $nonafib(j,n) | $antifib(j,n))":

def seqa "?lsd_3 s=(10*n-6-xkimber[n-1])/3":

def seqb "?lsd_3 s=(10*n-2-ykimber[n-1])/3":

def seqc "?lsd_3 s=(10*n+1-zkimber[n-1])/3":

def seqd "?lsd_3 s=(10*n-3-wkimber[n-1])":

eval test1 "?lsd_3 An,s,t,u,v ($seqa(n,s) & $seqb(n,t) & $seqc(n,u) & $seqa(n+1,v)) => ((s<t)&(t<u)&(u<v))":

eval test2 "?lsd_3 As (s>0) => Em ($seqa(m,s)|$seqb(m,s)|$seqc(m,s)|$seqd(m,s))":

eval test3 "?lsd_3 Em,n,s $seqd(n,s) & ($seqa(m,s) | $seqb(m,s) | $seqc(m,s))":

eval test4 "?lsd_3 An,s,t,u,v ($seqa(n,s) & $seqb(n,t) & $seqc(n,u) & $seqd(n,v)) => v=s+t+u":

eval kimconj "?lsd_3 An,r,s,t,u ($seqa(n,r) & $seqa(n+1,s) & $seqa(n+3,t) & $seqa(n+4,u)) => r+u=s+t":

def seq4A "?lsd_2 s=(17*n-11-xxkimber[n-1])/4":

def seq4B "?lsd_2 s=(17*n-7-yykimber[n-1])/4":

def seq4C "?lsd_2 s=(17*n-3-zzkimber[n-1])/4":

def seq4D "?lsd_2 s=(17*n+1-vvkimber[n-1])/4":

def seq4E "?lsd_2 s=(17*n-5-wwkimber[n-1])":

eval test1 "?lsd_2 An,s,t,u,v,w ($seq4A(n,s) & $seq4B(n,t)& $seq4C(n,u) & $seq4D(n,v) & $seq4A(n+1,w)) => ((s<t)&(t<u)&(u<v)&(v<w))":

eval test2 "?lsd_2 As (s>0) => Em ($seq4A(m,s) | $seq4B(m,s) | $seq4C(m,s) |$seq4D(m,s) | $seq4E(m,s))":