def even "?msd_fib Ek n=2*k":
eval check_fn1 "?msd_fib Ax,y Ez $m(x,y,z)": 
eval check_fn2 "?msd_fib Ax,y,z1,z2 ($m(x,y,z1) & $m(x,y,z2)) => z1=z2":
eval sada_c1 "?msd_fib An $m(0,n,n)":
def p "?msd_fib $m(n-1,z,n)":
eval case_a "?msd_fib An,i,j,x ($p(n,i) & j<i & $m(n-1,j,x)) => $m(n,j,x)":
eval case_b "?msd_fib An,x,y ($p(n,x) & $m(n,x+n,y)) => y=n":
eval case_c "?msd_fib An,x,y,j ($m(n-1,j+1,x) & $p(n,y) & y<=j & j<y+n)
   => $m(n,j,x)":
eval case_d "?msd_fib An,j,x,z ($m(n-1,j,x) & $p(n,z) & j>n+z) => $m(n,j,x)":
eval return "?msd_fib An Em Ax (x>=m) => $m(x,n,n)":
def leaves "?msd_fib (Ai i<z => $m(i,n,n)) & ~$m(z,n,n)":
eval leaves_thm "?msd_fib An,z $leaves(n,z) => $noverphi(n+1,z)":
def returns "?msd_fib (Aj (j>=z) => $m(j,n,n)) & ~$m(z-1,n,n)": 
eval returns_thm "?msd_fib An,z $returns(n,z) => $phin(n+1,z+1)":
def p "?msd_fib $m(n-1,z,n)":
eval p_check "?msd_fib An,z $p(n,z) => $noverphi(n+1,z)":
def sad "?msd_fib Ex $p(n,x) & $m(n-1,x+1,z)":
eval thma "?msd_fib An (Ek $phi2n(k,n+1)) <=> $sad(n,n+1)":
eval thmb "?msd_fib An (n>0) => 
   ((~Ek $phi2n(k,n+1)) <=> (Ex $sad(n,x) & $noverphi(n+1,x)))":
eval no3 "?msd_fib ~Ei,j,k,n i<j & j<k & $sad(i,n) & $sad(j,n) & $sad(k,n)":
eval twice "?msd_fib An (Ei,j i<j & $sad(i,n) & $sad(j,n)) <=> 
   (Ek k>=1 & $phi2n(k,n))":
def t "?msd_fib Ex $p(n,x) & $m(n-1,n+x,z)":
eval test_t "?msd_fib An,x,y ($t(n,x) & $phin(n+1,y)) => x+1=y":
def d "?msd_fib $m(n,n,z)":
def dlgn "?msd_fib Ex $d(n,x) & x>=n":
eval dltn "?msd_fib An,x,y (~$dlgn(n) & $d(n,x) & $phin(2*n+3,y)) 
   => x+y=4*n+4":
eval dgn "?msd_fib An,x,y (n>=1 & $dlgn(n) & $d(n,x) & $phin(2*n,y)) 
   => x+2*n=y+1":
def dp "?msd_fib $m(n-1,n,z)":
def dpg "?msd_fib Ez $dp(n,z) & z>=n":
eval dpgn "?msd_fib An,x,y (n>=1 & $dpg(n) & $dp(n,x) & $phin(4*n,y))
   => x=((y+1)-4*n)/2":
eval dpltn "?msd_fib An,x,y (n>=1 & ~$dpg(n) & $dp(n,x) & $phin(2*n,y))
   => x+1+y=4*n":
def b "?msd_fib (~$m(n,z+1,z+1)) & At (t<=z) => $m(n,t,t)":
def c "?msd_fib (~$m(n,z-1,z-1)) & At (t>=z) => $m(n,t,t)":
eval test_perm1 "?msd_fib An,x,y,i (n>=1 & $b(n,x) & $c(n,y) & i>x & i<y) =>
   Ej j>x & j<y & $m(n,i,j)":
eval no_fixed_point "?msd_fib ~En,x,y,i n>=1 & $b(n,x) & $c(n,y) & i>x
   & i<y & $m(n,i,i)":
eval decreasing "?msd_fib Ai,n,x,y (i<n & $m(i,n-i,x) &
   $m(i+1,n-(i+1),y)) => x>=y":
def occurs_twice "?msd_fib Ei,j i<j & j<=n & $m(i,n-i,x) & $m(j,n-j,x)":
eval never2 "?msd_fib An ~Ex,y x!=y & $occurs_twice(n,x) & $occurs_twice(n,y)":
eval has1 "?msd_fib An (n>=2) => Ex $occurs_twice(n,x)":
def r "?msd_fib (n=0&z=0)|(n=1&z=1)|(n>1 & $occurs_twice(n,z))":
def h "?msd_fib (n<=1&i=0) | (n>=2 & Ex $occurs_twice(n,x) & $m(i,n-i,x) & 
   Aj (j<i) => ~$m(j,n-j,x))":
def hp "?msd_fib (n<=1&i=0) | (n>=2 & Ex $occurs_twice(n,x) & $m(i,n-i,x) &
   Aj (j>i & j<=n) => ~$m(j,n-j,x))":
eval check_decreasing1 "?msd_fib An,i,x,y,z (n>=2 & $h(x,n) &
   i<=x-2 & $m(i,n-i,y) & $m(i+1,n-(i+1),z)) => y=z+1":
eval check_decreasing2 "?msd_fib An,i,x,y,z (n>=2 & $hp(x,n) &
   i>x & i<n & $m(i,n-i,y) & $m(i+1,n-(i+1),z)) => y=z+1":
def prop "?msd_fib $r(n-(k+1),k) & ~Ei,j i<j & j<n & $r(i,k) & $r(j,k)":
def part1 "?msd_fib $prop(k,n) & Aj (j<k) => ~$prop(j,n)":
eval test1 "?msd_fib Ak,n (n>=1 & k>=1 & $part1(k,n)) => $r(n,k)":
def occurs "?msd_fib Ei i<n & $r(i,z)":
def mex "?msd_fib (~$occurs(n,z)) & At (t<z) => $occurs(n,t)":
eval test2 "?msd_fib An (~Ek $part1(k,n)) => Es $mex(n,s) & $r(n,s)":
eval h_formula "?msd_fib An,z $h(z,n) <=> Ex $phin(n+3,x) & z+x=2*n+4":
eval hp_formula "?msd_fib An,z $hp(z,n) <=> Ex $noverphi(n+2,x) & z+1=x":