module Godel2 where{
import Data.Bits;

bitLength'::Integer->Integer;
shift'::Integer->Integer->Integer;
clearBit'::Integer->Integer->Integer;

diag::Integer->Integer;
num::Integer->Integer;
getint::Integer->(Integer,Integer);
varb::Integer->Integer;
unop::Integer->Integer->Integer;
binop::Integer->Integer->Integer->Integer;
sgetvar::Integer->(Integer,Integer);
sterm :: Integer -> (Integer,Integer);
swff :: Integer -> (Integer,Integer);
ax1::Integer->Integer->Integer;
ax2::Integer->Integer->Integer->Integer;
ax3::Integer->Integer->Integer;
ax4::Integer->Integer->Integer->Integer;
ax5::Integer->Integer->Integer->Integer;
ind::Integer->Integer->Integer;
gen::Integer->Integer->Integer;
mP::Integer->Integer->Integer;
subst::Integer->Integer->Integer->Integer;
proof::Integer->Integer;
proof1 :: Integer->[Integer]->[Integer];
lproof::Integer->[Integer]->(Integer,Integer);
glin::[Integer]->Integer->(Integer,Integer);
falll::Integer->Integer->Integer;
getintp::(Integer,Integer) -> (Integer,Integer);
impp::Integer->Integer->Integer;
nott::Integer->Integer;
inlist::Integer->[Integer]->Integer;
sterm1::Integer->Integer->Integer->[Integer]->(Integer,Integer);
swff1::Integer->Integer->Integer->[Integer]->(Integer,Integer);
last'::[Integer]->Integer;
proofafter::Integer->Integer->Integer;
proofsearch::Integer->Integer;


shift' n k=if (k==0) then n else 2*(shift' n k-1);
bitLength' n = if (n==0) then 0 else 1+(bitLength'(n `div` 2));
clearBit' n k =let {sk=shift' 1 k }in if ((n `div` sk)`mod` 2 ==0) then n else n-sk;
num n = if (n<3) then case n of {
  0->1;
  1->11;
  2->91;}
else let { n1=(num (n `div` 3))*16384+14031} in
 case (n `mod` 3) of {
  0->n1;
  1->n1*512+93;
  2->n1*4096+733;};

getint n= getintp (0,n);

varb n= if n==0 then 7 else 4*varb((n-1) `div` 3)+( (n-1) `mod` 3);

unop op t1= if op<4 then t1*4+op else t1*8+2*op-7;

binop op t1 t2=let {n2=toInteger (bitLength' t1) - 1} in unop op (t2*(shift 1 (fromInteger n2))+(clearBit t1 (fromInteger n2)));

inlist n list=if length list==0 then 0
else if n==list!!0 then 1
else inlist n (tail list);

tbok::Integer->[Integer]->Integer;
tbok t bound = if t==0 then 0 
else if t `mod` 2==0 then 
 let {(v1,t2)=getint (t `div` 2)} in 
   if inlist v1 bound==1 then 0 else t2
else let { ta=t `div` 8;tb= t `mod` 8 }in
  if (tb==1) then ta
  else let {tc=tbok ta bound} in
     if (tb==3) then tc else tbok tc bound;
    
sterm1 n v t bound =
if n `mod` 2==0 then let {(x,n2)=getint (n `div` 2)} in
    if  x==v then 
      if t==0 then (0,0)
      else if tbok t bound==0 then (0,0)
      else  (t,n2)
    else (2*varb(x),n2)
  else let { nn=n `div` 8;na=n `mod` 8; }in
   if na==1 then (9,nn)
   else let {(s1,n1) = sterm1 nn v t bound;} in
   if s1==0 then (0,0) else
   if na==3 then (unop 5 s1,  n1)
   else let {(s2,n2) = sterm1 n1 v t bound} in
   if s2==0 then (0,0) else
   if na==5 then (binop 6 s1 s2, n2) else (binop 7 s1 s2, n2);

swff1 n v t bound = if n==0 then (0,0)
else let {na= n `div` 4} in 
case (n `mod` 4) of {
  0 -> let {(s1, n1) = sterm1 na  v t bound ;(s2, n2) = sterm1 n1  v t bound } in (binop 0 s1 s2, n2);
  1 ->let {(s1,n1) = swff1 (n `div` 4) v t bound}in (unop 1 s1, n1);
  2 -> let {(s1, n1) = swff1 na v t bound; (s2,n2) = swff1 n1 v t bound;} in (binop 2 s1 s2, n2);
  3 ->let {(x, n1) = getint na;
       (s2,n2) =if (x==v)then swff n1 else swff1 n1 v t (if t==0 then bound else x:bound);} 
       in (binop 3 (2*varb x) s2, n2);};

impp wf1 wf2 = binop 2 wf1 wf2;
nott wf1= unop 1 wf1;
falll v wf= binop 3 (varb v) wf;
subst wf v t=let {(wft,r)=swff1 wf v t []} in wft;
ax1 wf1 wf2= impp wf1 (impp wf2 wf1);
ax2 wf1 wf2 wf3=
  impp (impp wf1 (impp wf2 wf3 )) (impp (impp wf1 wf2) (impp wf1 wf3));
ax3 wf1 wf2 =impp (impp (nott wf2) (nott wf1))(impp (impp (nott wf2) wf1) wf2);
ax4 v t wf = impp (falll v wf) (subst wf v t);
ax5 v wf1 wf2=impp (falll v (impp wf1 wf2))(impp wf1 (falll v wf2));
ind v wf=impp (subst wf v 9) (impp (falll v (impp wf (subst wf v (unop 5 (varb v))))) (falll v wf)) ;
gen v wf=falll v wf;

last' list=list!!(length list);


sterm n = if n `mod` 2==0 then sgetvar (n `div` 2)
  else let { nn=n `div` 8;(s1,n1) = sterm nn;(s2,n2) = sterm n1 }in
   case  n `mod` 8 of {
    1 -> (9,nn);
    3 -> (unop 5 s1,  n1);
    5 -> (binop 6 s1 s2, n2);
    7 -> (binop 7 s1 s2, n2);};



swff n = let {na= n `div` 4} in case (n `mod` 4) of {
  0 -> let {(s1, n1) = sterm na;(s2, n2) = sterm n1} in (binop 0 s1 s2, n2);
  1 ->let {(s1,n1) = swff (n `div` 4) }in (unop 1 s1, n1);
  2 -> let {(s1, n1) = swff na; (s2,n2) = swff n1;} in (binop 2 s1 s2, n2);
  3 ->let {(s1, n1) = getint na;(s2,n2) = swff n1;} in (binop 3 (varb s1) s2, n2);};
 
glin lins n=if n `mod` 2 ==0 then
  let {(i1, n2)=getint (n `div` 2);len=length lins} in
  if  i1<=toInteger len then (lins!!(len - (fromInteger i1)), n2) else (0,0)
else let {
 iax=case (n `mod` 32) of{
 3->126178700386;
 5->473746530;
 7->14737;
 9->476254002;
 11->29140;
 13->1907082196;
 15->6620;
 17->15866905564;
 _->0;}} 
 in ( iax,n `div`  32) ;
 

mP wf1 wf2 =if (wf2 `mod` 4)==2 then (let{( s1,wf3)=swff (wf2 `div` 4)} in if s1==wf1 then wf3 else 0) else 0;

lproof n lines=let{na=n `div` 4;nb=na `div` 4} in
case n `mod` 4 of {
1->  let{(wf1, n1) = swff nb;(wf2, n2) = swff n1;} in case na `mod` 4 of {
    0->(ax1 wf1 wf2, n2);
    1->let{(wf3, n3) = swff n2 ;}in (ax2 wf1 wf2 wf3, n3) ;
    _->(ax3 wf1 wf2, n2);};
2-> let {(v, n1) = getint nb;} in case na `mod`  4 of {
    0->let {( t, n2) = sterm n1;(wf2, n3) = swff n2;} in (ax4 v t wf2, n3);
    1->let{(wf1, n2) = swff1 v 0 n1 [];( wf2, n3) = swff n2 } in (ax5 v wf1 wf2, n3);
    _->let{(wf1, n2) = swff n1;} in (ind v wf1, n2);};
_-> case na `mod` 4 of {
    0->let{(wf1, n1) = glin lines nb;(wf2, n2) = glin lines n1;} in (mP wf1 wf2, n2);
    _->let {(v, n1) = getint nb;(wf1, n2) = glin lines n1 ;} in (gen v wf1, n2) ;};};

proof1 n lines = if n==0 then lines 
else let {(n1, n2)=lproof n lines }in 
if (n1==0)then (0:[]) else(proof1 n2 (n1:lines));

getintp n =let {(sofar,i1)=n}
  in case  i1 `mod` 4 of {
  3 -> (sofar,i1 `div` 4) ;
  _ -> getintp (sofar*3+(i1 `mod` 4)+1, i1 `div` 4);};
  
sgetvar n=let {(n1,n2)=getint n }in (2*(varb n1), n2);  


proof n =(proof1 n [])!!0 ;

diag n=nott (falll 2 (impp (binop 0 (varb 2) (num n)) (nott n)));

proofafter n m=
  if (n==proof m)then 1 
  else if (nott n==proof m) then 0
  else proofafter n m+1;
  		
proofsearch n =proofafter n 0;
}