# restart; read `d:/Ake/tf/ToadsAndFrogs.txt`;

with(numtheory):
with(combinat):

print(`Welcome to ToadsAndFrogs, a Maple package written by`):
print(`Thotsaporn (Aek) Thanatipanonda with minimal guidance`):
print(`by Doron Zeilberger. First Version: August 21, 2007 `):
print():
print(`It accompanies the article: `):
print(` A  Symbolic Finite-State Approach for Automated Proving of`):
print(`Theorems in Combinatorial Game Theory `):
print(` by Thotsaporn (Aek) Thanatipanonda and Doron Zeilberger`):
print(`available from both authors' websites`):
print(` http://www.math.rutgers.edu/~[thot, zeilberg] `):
print():
print(`Warning: L, R, B, F, T, pass, fail, a`):
print(` are global variables, do not use them`):
print(`for anything else `):


Help := proc()

if args = NULL then
print(`The main functions are`):
print(` ToFr, Conj, Type1, MainConj, SVG, Rec, Prove .`);
print(`To see a list of all procedures, type Help1(); `):
print():
print(` For help with a function, type: `):
print(` Help(FunctionName); `):
print(`For example, with help with ToFr, type: Help(ToFr); `):

elif args = ToFr then


print(`The input is a list consisting of the letters T,F,B `);
print(`[Warining: These are global variables, do not use them for`):
print(` other things ] ` ):
print(`T is short for Toad, F is short for Frog, and B is short for Blank`):
print(`The output is  the numerical value of the game,`);
print(`in the sense of Berlekemp, Conway and Guy's Winning Ways `);
print(`For example, try: `):
print(` ToFr([T,T,B,F,T,F]);  `);
print(``);
print(``);

elif args = Conj then

print(` Conj(X,Ini,SymbolList);'`);
print(`Inputs: X is a list of list of lists of values of games `);
print(`Ini, the initial values for the parameters, and SymbolList is`):
print(`the list of symbols (parameters) that the positions are `):
print(` parametrized by`):
print(``):
print(`Output: A conjetured closed-form, if found, `):
print(` followed by the domain,or FAIL. ` );
print(`For example, Try: `):
print():
print(` XX:=[seq([seq(ToFr([T$a,B,T$b,B,T,F]),a=2..5)],b=1..3)]; ` );
print(` Conj(XX,[2,1],[a,b]); `);

elif args = Type1 then

print(`Type1(A,Ini,Let)`);
print(`Inputs: Same as in Conj`);
print(`Output: the list of conjetures for all the values of A`);
print(``);
print(`Try: `):
print(` XX:=[seq([seq(ToFr([T$A[1],B,T$A[2],B,F]),A[1]=0..4)],A[2]=0..4)]; `);
print(`Type1(XX,[0,0],[a[1],a[2]]); `);
print(` SimpT1 (%,a) ; `):
print(`[to simplify it ] `):
print(``);

elif args = MainConj then

print(`MainConj(b,f,A) `);
print(`Input: number of Blank b, number of Frogs f`);
print(` , variable a`);
print(`Output: the list of all the conjectures of class Abf`);
print(``);
print(`Try: MainConj(2,1,A) ; `);
print(``);

elif args = SVG then

print(`  SVG(G)`);
print(` Input: Game G (could be symbolic or numeric)`);
print(` Output: the value of the game after simplification. `);
print(``);
print(` For example, try: `):
print(` assume(a>=2): `);
print(` SVG([{[a+4]},{}]); `);
print(``);

elif args = Rec then

print(`Rec(A,a): `);
print(`Input: the position A and symbol a`);
print(`Output: the recurrence from this position in term of a`);
print(``);
print(`Try:  Rec([B,B,F],a); `);

elif args = Prove then

print(` Prove(b, f, a)`);
print(`Input: number of Blank b, number of Frogs f`);
print(` , variable a`);
print(`Output: program will print the conjecture and`);
print(` the proof of all the value of the game in class Abf`);
print(``);
print(`Try:  Prove(2,1,a); `);

fi:
end:


Help1 := proc()

print(`Here is the list of all the procedures for ToFr: `);
print(` (Part1) `);
print(``);
print(`ValGame(G) , SumGame(G,H)`);
print(`VG(G),ByPass(G),BP(G,a,n),Dom(x,N)`);
print(`SN(a,b), subSN(x,y)`);
print(`GEZ(G,H), LW(G), IsLW(G)`);
print(`SetSum(x,H), Su(G,H)`);
print(`Form(G), Minus(G), Plus(G,a)`);
print(``);
print(`ValGame(G), SumGame(G,H), VG(G)`);
print(`and GEZ(G,H) are quite useful procedures`);
print(``):

print(`Here is the list of all the procedures used in Conj: `);
print(` (Part2) `);
print(``);
print(`Conj(A,C,Let),MakeConj(ListGame,D,C,Let)`);
print(`RearrangeAA(AA,n),CheckRestrictCon(G)`);
print(`IsSameShape(G,H), FindSameShape(G,SetGame)`);
print(`GuessLi(L,D,C,Let),MakeEq(L,D,C,b), fmod(k,n)`);
print(``);

print(`Here is the list of all the procedures used in Type1: `);
print(` (Part3) `);
print(``);
print(`Type1(A,C,Let)), AddDom(S,n,l)`);
print(`SimpT1(AA,a), SimpT1Ea(Eq1,EQ2,a), DomCondition(D1,D2) `);
print(``);

print(`Here is the list of all the procedures used in MainConj: `);
print(` (Part4) `);
print(``);
print(` MainConj(b, f, a), Input(Y)`);
print(` MakePos(k, AA, n, a) ,CallToFr(AA, n)`) :
print(``);
print(`Note:`);
print(`1) We should have a function to check whether the domain`):
print(` includes everything.`);
print(``);

print(`Here is the list of all the procedures used in SVG: `);
print(` (Part 5): `);
print(` Symbolic Value of the Game!! `);
print(``);
print(` SVG(G), SValGame(G)` );
print(` SByPass(G), SDom(x,N) `);
print(` SGEZ(G,H), SLW(G), SIsLW(G)`);
print(` SSetSum(x,H), SSu(G,H)`);
print(` SSarmRR(G,H), SSN(L,R), SNextDay(n)`);
print(` SFindNum(A), SsubSN(x,y)`);
print(` SForm(G), SMinus(G), SPlus(G,x)`);
print(``);

print(`Here is the list of all the procedures used in Rec: `);
print(`(Part 6)`);
print(``);
print(`Rec(A,a), BRec(A,i,a), FRec(A,i,a)`);
print(`Put(LL1,LL2), SW(A,i), LastFrog(A)`);
print(``);

print(`Here is the list of all the procedures used in Prove: `);
print(`(Part 7) `);
print(`that prove the conjectures of the class of ToFr `);
print(``);
print(`Prove(b, f, a, C), ProveEach(rec, value, R, a, AllC)`);
print(`SplitConj(rec, dom , a, AllC) , GroupSide(LL)`);
print(`Induction(G, H, R, C, a)`);
print(`PrintConj(AC, a, f) , PrintRec(rec, AllC, f) `);
print(``);

end:


############################################################
# Part1) ToFr
############################################################

## ValGame
## Input: game G (don't need to be in the simplest form)
## Output: the value of the game G in the simplest form

ValGame := proc(G) local i:

if nops(G) = 1 then
      return G;
else
      return( VG([{seq(ValGame(G[1][i]),i=1..nops(G[1]))},
	          {seq(ValGame(G[2][i]),i=1..nops(G[2]))}]));
fi:
end:

## SumGame
## Input: game G,H (dont need to be in the simplest form)
## Output: the value of the sum, G+H, in the simplest form

SumGame := proc(G,H) local A,B,i;

A := ValGame(G);
B := ValGame(H);

if nops(A) = 1 then
   return Plus(B,A[1]);
elif nops(B) = 1 then
   return Plus(A,B[1]);
else
   return VG([ {seq(SumGame(A[1][i],B),i=1..nops(A[1])),
              seq(SumGame(A,B[1][i]),i=1..nops(B[1]))},
			  {seq(SumGame(A[2][i],B),i=1..nops(A[2])),
              seq(SumGame(A,B[2][i]),i=1..nops(B[2]))} ]);
fi:
end:

##############################################################
VG := proc(G) option remember;

local temp,l,m:

m := NULL;
l := G;

while l <> m do

m := l;

temp := ByPass(m);

if nops(temp) = 1 then
   l := temp;
else
   l := [Dom(temp[1],L),Dom(temp[2],R)];
fi:
od:

if nops(m) = 1 then
   return(m);
else
   return(SN(m[1],m[2]));
fi:
end:

######################################################
ByPass := proc(G)

local L,R;

if nops(G) = 1 then
	return(G);
fi:

L := BP(G,G[1],1);
R := BP(G,G[2],2);
return([L,R]);
end:

BP := proc(G,a,n)  local flag,i,j,S;

S := G[n];
for i from 1 to nops(a) do

   if nops(a[i]) = 2 then
      flag := 0;
      j:=1;
       while flag = 0 and j <= nops(a[i][(n mod 2) +1]) do
          if (n=1 and GEZ(G,Minus(a[i][2][j]))) or
             (n=2 and GEZ(a[i][1][j],Minus(G))) then
 S := (S minus {a[i]}) union Form(a[i][(n mod 2) +1][j])[n];
             flag := 1;
          fi:
          j := j+1;
       od:
   fi:
od:
return(S);
end:

Dom := proc(x,N) option remember;

local i,j,S,CS;

if member(nops(x) ,{0,1}) then return(x);  fi:

S := [op(x)];
CS:= x;

for i from 1 to nops(S)-1 do
   for j from i+1 to nops(S) do

      if GEZ(S[i],Minus(S[j])) then
         if N = L then
            CS := CS minus {S[j]};
         else
            CS := CS minus {S[i]};
         fi:
      elif GEZ(S[j],Minus(S[i])) then
         if N = L then
            CS := CS minus {S[i]};
         else
            CS := CS minus {S[j]};
         fi:
      fi:
   od
od:
return(CS);

end:
#######################################################
SN := proc(a,b) option remember;

if ((nops(a) = 1 and nops(a[1])=1 ) or a = {})
   and ((nops(b) = 1 and nops(b[1])=1 ) or b = {})
   then
  if a = {} and b = {} then
    return([0]);

  elif b = {} then
    if a[1][1] < 0 then
       return([0]);
    elif type(a[1][1],integer) then
       return([a[1][1]+1]):
    else
       return([ceil(a[1][1])]):
    fi:

  elif a = {} then
    if b[1][1] > 0 then
       return([0]);
    elif type(b[1][1],integer) then
       return([b[1][1]-1]):
    else
       return([floor(b[1][1])]):
    fi:

  elif a[1][1] = b[1][1] then return([a,b]);
  elif a[1][1] > b[1][1] then return([a,b]):
  elif a[1][1] < 0 and b[1][1] > 0 then return([0]):
  elif a[1][1] >= 0 and b[1][1] >= 0 then

		return(subSN(a[1][1],b[1][1])):

	elif a[1][1] <= 0 and b[1][1] <= 0 then
		return(-subSN(-b[1][1],-a[1][1])):
	else
		ERROR();
	fi:
else
  return([a,b]);
fi:
end:

subSN := proc(x,y)  local a,pow,r:
r := 1;
pow := 1;

while true do
  a := floor(x*pow)/pow;
  if a + r < y then
     return([a+r]):
  fi:
  r := r/2;
  pow := 2*pow;
od:
end:
############################################################

## Sum game of G,H : Right moves first and left wins
## Input: games G and H
## Output: true if G+H >= 0, false otherwise.

GEZ := proc(G,H) local i,RRR;
RRR := SetSum(Form(G)[2],H) union SetSum(Form(H)[2],G);

for i from 1 to nops(RRR) do
   if LW(RRR[i]) = false then
        return(false);
   fi:
od:

return(true);
end:

LW := proc(G)  local i;

if nops(G) = 1 then
    if G[1] > 0 then
		return(true);
    else
		return(false);
    fi:
fi:

for i from 1 to nops(G[1]) do
    if IsLW(G[1][i]) then
       return(true);
    fi:
od:
return(false);
end:

#Right turn to play
IsLW := proc(G) local i;

if nops(G) = 1 then
    if G[1] >= 0 then
		return(true);
    else
		return(false);
    fi:
fi:

for i from 1 to nops(G[2]) do
    if LW(G[2][i]) = false then
       return(false);
    fi:
od:

return(true);
end:

############################################################

## SetSum
## Input: a set of games x and game H
## (both in the simplest form)
## Output: the sum of these 2 elements.

SetSum := proc(x,H) option remeber; local i,S:
S := {};
for i from 1 to nops(x) do

   if nops(x[i])=1 then
      S := S union {Plus(H,x[i][1])};
   elif nops(H)=1 then
      S := S union {Plus(x[i],H[1])};
   else
      S := S union {Su(x[i],H)};
   fi:

od:

return(S);
end:

Su := proc(G,H)
    return([SetSum(G[1],H) union SetSum(H[1],G),
            SetSum(G[2],H) union SetSum(H[2],G)]);
end:
###########################################################

Form := proc(G) option remember; local b,n;

if nops(G) = 2 then return(G);
else
   n := G[1];

   # n must be of type rational.

   if type(n,integer) then
       if   n = 0  then return([{},{}]);
       elif n > 0  then return([{[n-1]},{}]);
       elif n < 0  then return([{},{[n+1]}]);
       fi:
   else
       b := convert(n,fraction);
       return([{[b-(1/denom(b))]},{[b+(1/denom(b))]}]);
   fi:
fi:
end:

Minus := proc(G) local i;

if nops(G) = 1 then return([-G[1]]);
else return( [{seq(Minus(G[2][i]),i=1..nops(G[2]))},
              {seq(Minus(G[1][i]),i=1..nops(G[1]))}]);
fi:
end:

Plus := proc(G,a)   local i:
if nops(G) = 1 then
   return([G[1]+a]);
else
   return([{seq(Plus(G[1][i],a),i=1..nops(G[1]))},
           {seq(Plus(G[2][i],a),i=1..nops(G[2]))}]);
fi:
end:
############################################################

ToFr := proc(A) option remember;  local i,L,R:
if not type(A,list) then
 ERROR(`Bad input`):
fi:

if convert(A,set) minus {B,F,T}<>{} then
 ERROR(`Bad input`):
fi:

L:={};
R:={};

for i from 1 to nops(A)-1 do
   if A[i] = T and A[i+1] = B then
      L := {op(L),ToFr([op(1..i-1,A),B,T,op(i+2..nops(A),A)])};
   elif i <= nops(A)-2 and A[i] = T and A[i+1] = F and A[i+2] = B then
      L := {op(L),ToFr([op(1..i-1,A),B,F,T,op(i+3..nops(A),A)])};
   fi:
od:

for i from 2 to nops(A) do
   if A[i-1] = B and A[i] = F then
      R := {op(R),ToFr([op(1..i-2,A),F,B,op(i+1..nops(A),A)])};
   elif i >= 3 and A[i-2] = B and A[i-1] = T and A[i] = F then
      R := {op(R),ToFr([op(1..i-3,A),F,T,B,op(i+1..nops(A),A)])};
   fi:
od:

return(VG([L,R]));
end:

############################################################
#Part 2) Conj
############################################################

Conj := proc(AA,C,Let) local i, temp, ListGame, Dimension, Dom;

temp := RearrangeAA(AA,nops(C));

ListGame := temp[1];
Dimension := temp[2];

CheckRestrictCon(ListGame[1]);

Dom := [];

for i from 1 to nops(Dimension) do
	if Dimension[i] = 1 then
		Dom := [op(Dom), Let[i] = C[i]];
	else
		Dom := [op(Dom), C[i] <= Let[i]];
	fi:
od:

temp := MakeConj(ListGame,Dimension,C,Let);

if temp = FAIL then
	return FAIL
else
	return [temp,{Dom}];
fi:
end:

## MakeConj:
## Input: ListGame,Dimension,C,Let
## Output: [Conjecture, list of domain] or FAIL

MakeConj := proc(ListGame,Dimension,C,Let)

local h, i, j, G, temp, listG, ret, tempI;

G := ListGame[1];

#initial condition

tempI := {seq(nops(ListGame[i]),i=1..nops(ListGame))};

if  tempI = {1} then

	temp := [seq(op(ListGame[i]),i=1..nops(ListGame))];
	return( GuessLi(temp,Dimension,C,Let) );

elif member(1,tempI) then
	return(FAIL);

elif {nops(G[1])} <> {seq(nops(ListGame[j][1]), j =1..nops(ListGame))}  
     or {nops(G[2])} <>  {seq(nops(ListGame[j][2]), j =1..nops(ListGame))} then
	return(FAIL);
fi:

ret := [{},{}];

for h from 1 to 2 do
	for i from 1 to nops(G[h]) do
		listG := [G[h][i]];
		for j from 2 to nops(ListGame) do

			temp := FindSameShape(G[h][i], ListGame[j][h]);
				if temp = FAIL then 
					return(FAIL);
				fi:

			listG := [op(listG),temp];
		od:

		temp := MakeConj(listG,Dimension,C,Let);

		if temp = FAIL then
			return(FAIL);
		else
			ret[h] := {op(ret[h]), temp};
		fi:
	od:
od:

return(ret);
end:

#####################################################
## RearrangeAA:
## Input: list of list of ... of
## list of games AA that has dimension n
## Output: [ListGame, Dimension]

RearrangeAA := proc(AA,n) local ret,i ;

if n = 1 then
    ret := [AA, [nops(AA)]];
else
	ret := [[seq( op(RearrangeAA(AA[i],n-1)[1]), i=1..nops(AA))]
			,[op(RearrangeAA(AA[1],n-1)[2]),nops(AA)]];
fi:

return(ret);
end:

CheckRestrictCon := proc(G)  local i, temp, j;

if nops(G) = 1 then
   return():
fi:

temp := {seq(seq(
IsSameShape(G[1][i],G[1][j]),j=i+1..nops(G[1])),i=1..nops(G[1]))}
  union {seq(seq(
IsSameShape(G[2][i],G[2][j]),j=i+1..nops(G[2])),i=1..nops(G[2]))};

if member(true,temp) then
print(` I have not included the case `);
print(`where 2 options have the same shape ` );
	ERROR();
fi:

seq( CheckRestrictCon(G[1][i]), i =1..nops(G[1]));
seq( CheckRestrictCon(G[2][i]), i =1..nops(G[2]));

end:
#####################################################
## IsSameShape:
## Input:  games G and H
## Output: true if G and H has the same
## shape, false otherwise.

IsSameShape := proc(G,H) local h,i,K,temp;

if nops(G) = 1 or nops(H) = 1 then
	if nops(G) = nops(H) then
		return(true);
	else
		return(false);
	fi:
fi:

K := H;

for h from 1 to 2 do
	for i from 1 to nops(G[h]) do
		temp := FindSameShape(G[h][i], K[h]);
		if temp = FAIL then
			return(false);
		else
			K[h] := K[h] minus {temp};
		fi:
	od:
od:

if K <> [{},{}] then
	return(false);
else
	return(true);
fi:
end:

## FindSameShape:
## Input:  games G and SetGame
## Output: game in SetGame that has
## the same shape as G or FAIL otherwise.

FindSameShape := proc(G,SetGame) local i;

i := 1;

while i <= nops(SetGame) do

	if	IsSameShape(G,SetGame[i]) then
		return(SetGame[i]);
	fi:
	i := i+1;
od:

return(FAIL);
end:

##########################################################
## GuessLi:
## Input the list of numbers L, Dimension
## and the starting values C of each variable a
## Output : the conj that we want

GuessLi := proc(L, Dimension, C, Let)

local i,P,var,eq,b;

P := add(b[i]*Let[i],i=1..nops(C))+b[nops(C)+1];

#subs value of Let when Dimension = 1
for i from 1 to nops(Dimension) do
	if Dimension[i] = 1 then
	    P := subs(Let[i] = C[i],P);
	fi:
od:

var:={seq(b[i],i=0..nops(C)+1)}:

eq:= MakeEq(L,Dimension,C,b):

var:=solve(eq,var):

if var=NULL then
	return(FAIL):
fi:

[subs(var,P)];
end:

## MakeEq:
## Input the list of list L of numbers
## ,and the starting values C of
## each variable a, position P and variable a
## Output : the set of equations with variable a

MakeEq := proc(L,Dimension,C,b) local i,n,mult,j;

n := nops(C);
mult := [0$n];

for i from 1 to n do
	mult[i] := mul(Dimension[j],j=1..i);
od:

{seq( b[1]*(fmod(i, mult[1])+C[1]-1)
	+ add(b[j]*( ceil(fmod(i, mult[j])/mult[j-1]) +C[j] -1 )
	,j=2..n) + b[n+1] = L[i], i = 1..nops(L))};

end:

fmod := proc(k, n)
	if `mod`(k, n) = 0 then
		return n;
	else
		return `mod`(k, n) ;
	fi;
end:

###################################################
# Part 3) Type1
####################################################

## Type1 :
## Input: the list A of the value of the game and
## the value that each variable starts
## (First one is the most inside one) and
## the letters L that you want to use.
## Output: [[conj that we want, domain],[...]].

Type1:= proc(A,C,Let) local ret, NewC, temp ;

if C = [] then
    return( [[A,[[]]]]);

elif Conj(A,C,Let) = FAIL then
    temp := Type1(A[1], [op(1..nops(C)-1,C)],[op(1..nops(Let)-1,Let)]);
    ret := AddDom(temp,C[nops(C)],Let[nops(Let)]);

    if nops(A) = 1 then
       return(ret);
    else
       NewC := [op(1..nops(C)-1,C), C[nops(C)]+1];
       return( [op(ret), op(Type1([op(2..nops(A),A)], NewC,Let))]);
    fi:
else
   return([Conj(A,C,Let)]);
fi:

end:

## AddDom :
## Input: the big output [[VG,{domain}],[...]] S,
## number n, letter l
## Output: [[VG, [new domain]],[...]]

AddDom := proc(S,n,l) local i, temp, ret,j;

ret := S;
for i from 1 to nops(ret) do

	temp := {seq([op(S[i][2][j]), l=n], j = 1..nops(S[i][2]))};
    ret[i][2] := temp;

od:

return(ret);
end:

#############################################################
## The below is complete independent of the above

## SimpT1 :
## Input: the list of conjectures :
## [value of the game, [domain]] and vairables.
## Output: The new simplify list of conjectures!
## Note: SimpT1 only works when the input
## come from the conjecture of type 1

SimpT1 := proc(AA ,a) local i, n, ret, temp;

ret := [AA[1]];

for i from 2 to nops(AA) do

	n := nops(ret);
	temp := SimpT1Ea(ret[n], AA[i], a);

	if  temp = FAIL then
		ret := [op(ret), AA[i]];
	else
		ret := SimpT1([op(1..n-1,ret), temp], a);
	fi:
od:

return(ret);
end:

## SimpT1Ea :
## Input: EQ1,EQ2, Let
## Output: The new simplify list of conjectures or FAIL
## if can not simplify or if more than one codition already!

SimpT1Ea := proc(EQ1, EQ2, a)

local temp, VG1,VG2,D1,D2, var,i ;

if nops(EQ1[2]) <> 1 or nops(EQ2[2]) <> 1 then
   #print("I have not included the case yet when many domains yet");
   return FAIL:
fi:

VG1 := EQ1[1];
VG2 := EQ2[1];
D1  := EQ1[2][1];
D2  := EQ2[2][1];

temp := DomCondition(D1, D2);

if temp[1] = pass then

	if (temp[2] = 1 or nops(temp[3]) > 1) and
		SValGame(subs(D1[temp[2]],VG2)) = VG1 then

		return([VG2, temp[3]]):

	elif  temp[2] > 1 and nops(temp[3]) = 1 then

		var := temp[3][1];
		seq(assume(var[i]), i = 1..temp[2]-1);

			if SValGame(subs(D1[temp[2]],VG2)) = VG1 then
				a := 'a';
				return([VG2, temp[3]]):
			fi:
		a := 'a';
	fi:
fi:

return(FAIL):

end:

##########################################################################

DomCondition := proc(D1, D2) local i, j,  NewDom;

# Alredy assume good inputs which means nops(D1)= nops(D2)
# and D1 <> D2

for i from nops(D1) by -1 to 1 while D1[i] = D2[i] do
od:

if type( D1[i] ,`=`) and type( D2[i] ,`<=`)  then

	if ({seq(evalb(D1[j]=D2[j]), j=1..i-1)} = {true} or i = 1)
		and rhs(D1[i]) + 1 = lhs(D2[i]) then
		NewDom := {[op(1..i-1,D1), rhs(D1[i]) <= lhs(D1[i]),
					op(i+1..nops(D1),D1)]}
	else
		NewDom := {D1,D2};
	fi:

	return [pass,i, NewDom];
else
	return [fail,0,0];
fi:

end:

#########################################################
# Part4) MainConj
#########################################################

## MainConj :
## Input: the number B and F respectively
## Output: Conjecture for everything in the given class.

MainConj := proc(b, f, a) option remember;

local A,Y,XX,i,ret;

A := [B$b,F$f];
Y := permute(A);
ret := [];

if f = 1 then
	for i from 1 to nops(Y) do

		XX  := Input(Y[i], a);
		ret :=
[op(ret),[Y[i],SimpT1(Type1(XX[1],XX[2],XX[3]),a)]];
	od:

else
	print(` Program can't Conjecture F =`, f, `yet`);
	ERROR();
fi:

return(ret);
end:

## Input :
## Input: an order position P with B and F
## , symbol for conjecture a.
## Output: Give the input (value of the games) for
##         other procedures to find conjectures.

Input := proc(P, a) local i, n, pos;

#locate last frog:
for i from nops(P) by -1 to 1 while P[i] <> F do
od:

n := i;

pos := [seq(op([T$a[i],P[i]]), i = 1..n),seq(P[i],i=n+1..nops(P))];

return( [ CallToFr(MakePos(1,pos,n,a),n) , [0$n] , [seq(a[i],i=1..n)] ] );

end:

## MakePos :
## Input:  level of recursive, postion,
## last frog, symbol a
## Output: seq of ToFr.

MakePos := proc(k, pos ,n,a) local i;

if k = n then
    return( [seq( eval(subs(a[k] = i, pos)),i=0..4)] );
else
    return( MakePos(k+1, [seq(eval(subs(a[k] = i, pos)), i=0..4)], n, a));
fi:
end:

## CallToFr 
## Input: list of position and level of recursive
## Output: the value of the game for each position.

CallToFr := proc(AA,n) local i;

if n = 1 then
   return( [seq(ToFr(AA[i]),i=1..nops(AA))]);
else
   return([seq(CallToFr(AA[i],n-1),i=1..nops(AA))]);
fi:

end:

#############################################################
# Part5) SVG
#############################################################

#****************************************************************
## assume the coeff. of variables and variables itsself are integers.
## assume variables in the condition in the form a[i]>= c (constant c).
#****************************************************************

## SValGame
## Input: game G (dont need to be in the simplest form)
## Output: the value of the game G in the simplest form

SValGame := proc(G) local i:

if nops(G) = 1 then
      return G;
else
      return( SVG([{seq(SValGame(G[1][i]),i=1..nops(G[1]))},
	          {seq(SValGame(G[2][i]),i=1..nops(G[2]))}]));
fi:
end:
######################################################

SVG := proc(G)  local temp, old, new:

old := NULL;
new := G;

while old <> new do
	old := new;
	if nops(old) <> 1 then

		
		temp := [SDom(old[1],L),SDom(old[2],R)];
		new := SByPass([temp[1],temp[2]]);

  #    temp := SByPass([old[1],old[2]]);
  #    new := [SDom(temp[1],L),SDom(temp[2],R)];
  fi:
od:

if nops(new) =  1 then
   return(new);
else
   return(SSN(new[1],new[2]));
fi:

end:

########################################################
SByPass := proc(G) local A,B,i,j,L,R;

A := G[1];
B := G[2];
L := G[1];
R := G[2];

for i from 1 to nops(B) do

   if nops(B[i]) = 2 then
      for j from 1 to nops(B[i][1]) do
          if SGEZ(B[i][1][j],SMinus(G)) then
             R := (R minus {B[i]}) union SForm(B[i][1][j])[2];
          fi:
       od:
   fi:
od:

for i from 1 to nops(A) do

   if nops(A[i]) = 2 then
     for j from 1 to nops(A[i][2]) do
        if SGEZ(G,SMinus(A[i][2][j])) then
           L := (L minus {A[i]}) union SForm(A[i][2][j])[1];
        fi:
     od:
   fi:
od:

return([L,R]);
end:

SDom := proc(x,N) local i,j,S,CS;

if member(nops(x) ,{0,1}) then return(x);  fi:

S := [op(x)];
CS:= x;

for i from 1 to nops(S)-1 do
   for j from i+1 to nops(S) do

      if SGEZ(S[i],SMinus(S[j])) then
         if N = L then
            CS := CS minus {S[j]};
         else
            CS := CS minus {S[i]};
         fi:
      elif SGEZ(S[j],SMinus(S[i])) then
         if N = L then
            CS := CS minus {S[i]};
         else
            CS := CS minus {S[j]};
         fi:
      fi:
   od
od:
return(CS);

end:
########################################################

## Sum game of G,H : Right moves first and left wins
## Input : G,H
## Output: true if G+H >=0. false otherwise

SGEZ := proc(G,H) local i,RRR;

RRR := SSarmRR(G,H);

for i from 1 to nops(RRR) do
   if SLW(RRR[i]) = false then
        return(false);
   fi:
od:

return(true);
end:

SLW := proc(G) local i;

if nops(G) = 1 then
    return(is(G[1] > 0));
fi:

for i from 1 to nops(G[1]) do
    if SIsLW(G[1][i]) then
       return(true);
    fi:
od:
return(false);
end:

SIsLW := proc(G) local i;

if nops(G) = 1 then
    return(is(G[1]>=0));
fi:

for i from 1 to nops(G[2]) do
    if SLW(G[2][i]) = false then
       return(false);
    fi:
od:

return(true);
end:
#############################################################

SSetSum := proc(x,H) local i,S:

S := {};
for i from 1 to nops(x) do

   if nops(x[i])=1 then
      S := S union {SPlus(H,x[i][1])};
   elif nops(H)=1 then
      S := S union {SPlus(x[i],H[1])};
   else
      S := S union {SSu(x[i],H)}
   fi:

od:

return(S);
end:

SSu := proc(G,H) ;

return([SSetSum(G[1],H) union SSetSum(H[1],G),
        SSetSum(G[2],H) union SSetSum(H[2],G)]);
end:

SSarmRR := proc(G,H)

if nops(G) = 1 and nops(H) = 1 then
	return( SForm([G[1]+H[1]])[2] );
elif nops(H) = 1 then
	return(SPlus(G,H[1])[2]);
elif nops(G) = 1 then
	return(SPlus(H,G[1])[2]);
else
	return(SSetSum(G[2],H) union SSetSum(H[2],G));
fi:

end:

###################################################

SSN := proc(L,R) local L1,R1,numL,numR;

if not(((nops(L) = 1 and nops(L[1])=1 ) or L = {})
   and ((nops(R) = 1 and nops(R[1])=1 ) or R = {})) then
   return([L,R]);
fi:

if L = {} and R = {} then
    return([0]);
elif R = {} then
    return(SNextDay(L[1][1]));
elif L = {} then
    return(SMinus(SNextDay(-R[1][1])));
fi:

L1 := L[1][1];
R1 := R[1][1];

numL := SFindNum(L1);
numR := SFindNum(R1);

if is(L1 - R1 >= 0) then
    return([L,R]);
elif is(L1 < 0) and is(R1 > 0) then
    return([0]):

elif is(R1 - L1 > 1) then
    if type(numL,integer) and is(L1 >= -1) then
        return([L1+1]):
	elif type(numL,integer) and L1+2 = R1 then
		return [L1+1];
    elif type(numR,integer) and is(R1 <= 1) then
        return([R1-1]):
    elif type(numL,rational) and is(L1 >= -1) then
        return([L1-numL+ceil(numL)]);
    elif type(numR,rational) and is(R1 <= 1) then
        return([R1-numR+floor(numR)]);
    else
#print(`No case in SSN, but that is ok!: R1>L1`,[L,R],about(a));
        return([L,R]);
    fi:
elif is(0 < R1-L1 ) and is(R1 - L1 <= 1) then
    return([L1-numL+SsubSN(numL,numR)]);

else
#print(`No case in SSN, but that is ok!`,[L,R],about(a));
    return([L,R]);
fi:
end:

SNextDay := proc(n) local num;

num := SFindNum(n);

if is(n < 0) then
    return([0]);
elif is(n >= -1) and type(num,integer) then
    return([n+1]):
elif is(n > -1) then
    return([n-num+ceil(num)]):
else
    return([{[n]},{}]);
fi:

end:

SFindNum := proc(A) local i,S;

if  type(A,symbol) or type(A,`*`) or type(A,`indexed`) then
   return(0);
elif  type(A,rational) then
   return(A);
elif type(A,`+`) then
  S:= [op(A)];
  for i from 1 to nops(S) do
    if type(S[i],rational) then
      return(S[i]);
    fi:
  od:
  return(0);
else
   ERROR();
fi:

end:

SsubSN := proc(x,y) local aa,pow,r:
r := 1;
pow := 1;

while true do
  aa := floor(x*pow)/pow;
  if aa + r < y then
     return(aa+r):
  fi:
  r := r/2;
  pow := 2*pow;
od:
end:
##################################################

SForm := proc(G)  local r,n,num;

if nops(G) = 2 then return(G); fi:

n := G[1];

num := SFindNum(n);

if is(n = 0) then
   return([{},{}]);
elif is(n>=0) and type(num,integer) then
   return([{[n-1]},{}]);
elif is(n<=0) and type(num,integer) then
   return([{},{[n+1]}]);
elif (is(n>0) or is(n<0)) and type(num,rational) then
   r := convert(num,fraction);
   return([{[n-(1/denom(r))]},{[n+(1/denom(r))]}]);
else
   print(`No case in SForm, I am in trouble!!`,G);
   ERROR():
fi:

end:

SMinus := proc(G) local i;

if nops(G) = 1 then return([-G[1]]);
else return( [{seq(SMinus(G[2][i]),i=1..nops(G[2]))},
              {seq(SMinus(G[1][i]),i=1..nops(G[1]))}]);
fi:
end:

SPlus := proc(G,aa)  local i;
if nops(G) = 1 then
   return([G[1]+aa]);
else
   return([{seq(SPlus(G[1][i],aa),i=1..nops(G[1]))},
           {seq(SPlus(G[2][i],aa),i=1..nops(G[2]))}]);
fi:
end:

##################################################
# Part6) Rec
##################################################

## Rec:
## Input: the list A and letter a
## Output: list of [L,R,d] in every position
## L is left option, R is right option and d is domain.

Rec := proc(A,a) option remember:

local i, ret;

if {seq(A[i],i=1..nops(A))} <> {B,F} then
	ERROR();
fi:

i := 1;
ret := [];

while i <= LastFrog(A) do

	if A[i] = B then
		  ret := Put(ret, BRec(A,i,a));
	else
		  ret := Put(ret, FRec(A,i,a));
	fi:

	# A[i+1] will be taken cared by FRec above already.
	if A[i] = F and i < nops(A) and A[i+1] = B then
		  i := i+2;
	else
		  i := i+1;
	fi:
od:

return(ret);
end:

#####################################################

## BRec :
## Input : Position A,
## the position in A we consider i, variable a
## Output : the recurrence of A at position i

BRec  := proc(A,i,a) local n,L,R,d,j :

n := LastFrog(A):
L := [[A,[seq(a[j],j=1..i-1),a[i]-1,a[i+1]+1,seq(a[j],j=i+2..n)]]];
R := [];
d := [0 <= a[i]];
return([[L,R,d]]);
end:

## FRec :
## Input : Position A,
## the position in A we consider i, variable a
## Output : the recurrence of A at position i

FRec := proc(A,i,a) local n,L,R,d,ret0,ret1,j:

n := LastFrog(A):

##position i (For Right move)

if i >= 2 and A[i-1] = B then
	if i < n then
		R := [[Sw(A,i-1),[seq(a[j],j=1..n)]]];
	else
		R := [[Sw(A,i-1),[seq(a[j],j=1..n-1)],
a[i]*(nops(A)-n+1)]];
	fi:

	d := [0 <= a[i], a[i] <= 1 ];
	ret0 := [[[],R,d],[[],[],[2 <= a[i]]]];

else
	ret0 := [[[],[],[0 <= a[i]]]];
fi:

##position i+1 (For Left move)

if i < n and A[i+1] = B then
	L :=
[[Sw(A,i),[seq(a[j],j=1..i-1),a[i]-1,0,a[i+2]+1,seq(a[j],j=i+3..n)]]];
	d := [a[i+1] = 0];
	ret1 := [[L,[],d]];
	L :=
[[A,[seq(a[j],j=1..i),a[i+1]-1,a[i+2]+1,seq(a[j],j=i+3..n)]]];
	d := [1 <= a[i+1]];
	ret1 := [op(ret1),[L,[],d]];

elif i=n and n < nops(A) and A[i+1] = B then
	L := [[Sw(A,i),[seq(a[j],j=1..i-1),a[i]-1,0], nops(A)-n-1]];
	d := [a[i+1] = 0];
	ret1 := [[L,[],d]];

else
	ret1 := [];
fi:

return(Put(ret0,ret1)):
end:

##########################################################

## Put:
## Input the list c1 and c2
## Output: list of [L,R,d] in every
## position after merge the 2 lists

Put:=proc(c1,c2) local i, j, temp, ret;

if c1 = [] then
  return(c2):
elif c2 = [] then
  return(c1):
fi:

ret := []:

for i from 1 to nops(c1) do
	for j from 1 to nops(c2) do

        temp := [[op(c1[i][1]),op(c2[j][1])],[op(c1[i][2]),op(c2[j][2])]
	        ,[op(c1[i][3]),op(c2[j][3])]]:
        ret := [op(ret),temp];
	od:
od:

return(ret);
end:

##Sw : swap the element of A[i] and A[i+1];
Sw := proc(A,i)
  return( [op(1..i-1,A),A[i+1],A[i],op(i+2..nops(A),A)]);
end:

## LastFrog :
## Input : position P
## Output : the position of last frog in A;
LastFrog := proc(P) local i;

for i from nops(P) by -1 to 1 while P[i] <> F do
od:
return(i);

end:

####################################################################
# Part 7) Prove
####################################################################

## AllC := all conjectures
## For each conjecture :
## Step1: split to smaller recurrence
## (the only time using recurrence)
## send to ProveEach here
## Step2: split to smaller conjecture : SplitConj
## Stpe3: induction step -> Check with SVG : Induction

## Prove
## Input: number of blank nb, number of F nf, variable a,
## conjectures C (only needed when f > 1)
## (since program cannot find conjecture for f>1 yet)
## Output: NULL but print the values of
## the game in the class with proof.

Prove := proc(nb,nf,a,C)

local i, j, k, l, f, AllC, pos,
CON, value, D , Recurs, inter, rec;

if nargs = 4 then
	AllC := C(a);
else
	AllC := MainConj(nb, nf, a);
fi:

print(`##Conjectures##`);
PrintConj(AllC, a, f);

print(``);
print(`Now we will prove by applying `);
print(`induction to each of the above`);
print(`conjectures one by one.`);
print(``);
print(`If everythings are true, we get the proofs.`);

print(``);
print(`###############`);
print(`##Begin to prove##`);
print(`###############`);

for i from 1 to nops(AllC) do
# for each position Ex:[B,F,F]

	pos := AllC[i][1];

	print(``);
	print(`##########`);
	print(`#`, f[i] ,`#`);
	print(`##########`);

	CON := AllC[i][2];
	Recurs := Rec(pos,a);

	for j from 1 to nops(CON) do
# for each conjecture Ex: [2a]

		value := CON[j][1];
		D	  := CON[j][2];

		for k from 1 to nops(D) do
# each domain of the above conjecture

			for l from 1 to nops(Recurs) do
# split D into smaller recurrence

				inter := solve( {op(D[k])} union
{op(Recurs[l][3])});

				if  inter <> NULL then

					rec :=
[Recurs[l][1],Recurs[l][2],inter]:

	ProveEach(rec, value,
	PrintRec(rec, AllC, f), pos, a, AllC);

				fi:
			od:
		od:
	od:
od:

print(``);
print(`###The conjectures is proved###`)
end:

## ProveEach
## Input:  the reucurrence [L,R,D] rec,
## conj of the game value,
## symbol of recurrence,  position pos, 
## variable a, all conjectures AllC
## Output: NULL but spilt conj and
## call the induction to print out
## the proof.

ProveEach := proc(rec, value, R, pos, a, AllC)

local i, j, left, right, inter;

# Now I split the recurrence into each
# smaller conjecture
# so that I can do induction.

left  := SplitConj(rec[1], rec[3], a, AllC);
right := SplitConj(rec[2], rec[3], a, AllC);

for i from 1 to nops(left) do
	for j from 1 to nops(right) do

		inter := solve( left[i][2] union right[j][2]);

		if inter <> NULL then
			Induction( [ left[i][1], right[j][1]],
value, R, inter, pos, a) ;
		fi:
	od:
od:

end:

######################################################
## SplitConj
## Input : recurrence rec, domain dom,
## variable a, all conjectures AllC
## Output: list of [{option},domain]

SplitConj := proc(rec, dom , a, AllC)

local i, j, j1, k, AC, temp, inter;

if rec = [] then
   return([[{},dom]]);
fi:

temp := [[]$nops(rec)];

for i from 1 to nops(rec) do

	# find the same pos in AllC
	for j from 1 to nops(AllC) while rec[i][1] <> AllC[j][1] do
	od:

	AC :=  [op(AllC[j][2]),
seq([{},[[a[k]=-1]]], k=1..nops(rec[i][2]))];

	#change domain of conj (AC) according to the recurrence
	for j from 1 to nops(AC) do

		AC[j] :=
subs({seq(a[j1] = rec[i][2][j1],j1=1..nops(rec[i][2]))},
					AC[j]);

# intersect dom of conjecture with the given domain.
# And make list out of it.

		for k from 1 to nops(AC[j][2]) do

			inter := solve( {op(AC[j][2][k])} union dom);
			#the part above makes program slow down a lot.

			if inter <> NULL then
				
				if AC[j][1] = {} then
					temp[i] :=
[op(temp[i]),[AC[j][1],inter]];

				elif nops(rec[i]) = 2 then
					temp[i] :=
[op(temp[i]),[{AC[j][1]},inter]];

				else
					temp[i] :=
[op(temp[i]),[{Plus(AC[j][1],rec[i][3] )},inter]];
				fi:
			fi:
		od:
	od:
od:

GroupSide(temp);
end:

GroupSide := proc(LL) local i, j, A, B, new, inter;

if nops(LL) = 1 then
	return(LL[1]);
fi:

A := LL[1];
B := LL[2];
new := [];

for i from 1 to nops(A) do
	for j from 1 to nops(B) do

		inter := solve (A[i][2] union B[j][2]);
		if  inter <> NULL then
			new := [op(new),[A[i][1] union B[j][1], inter]];
		fi:
	od:
od:

GroupSide( [new, op(3..nops(LL), LL)]);

end:

###################################################################

## Induction
## Input: games G and H, recurrence R
## domain C, position pos, symbol a
## Output: NULL but will print out the
## proof that game G and H are
## actually the same under the domain C

Induction := proc(G, H, R, C, pos, a)

local i, b, sta, solu, sta1,
solu1, NewC, NewR, NewRR:

# assign the new name to local variable
sta  := G;
solu := H;
NewC := C;
NewR := R;

# assign the value to the variable
for i from 1 to nops(NewC) do

	if type(NewC[i],`=`) then
		sta  := subs(NewC[i], sta);
		solu := subs(NewC[i], solu);
		NewR := subs(NewC[i], NewR);
	fi:
od:

# NewRR for print out the recurrence only
NewRR := [{},NewR[2]];

# check whether any recurrence is -1 of the left
# if yes  then get rid of it
for i from 1 to nops(NewR[1]) do
	if not(type(NewR[1][i],`+`)) then
		if not(member(-1,{op(NewR[1][i])})) then
			NewRR[1] := NewRR[1] union {NewR[1][i]};
		fi:
	elif not(member(-1,{op(op(NewR[1][i])[1])})) then

		NewRR[1] := NewRR[1] union {NewR[1][i]};
	fi:
od:

print(``);
print(`For the domain` ,
NewC minus {a[LastFrog(pos)+1]=0});
print(`The value of the game = ` , NewRR);
print(` = `, sta );

# change the name of variable before send it to SVG
# the thing is if not then the program not working
# very well
sta  := subs({seq(a[i]=b[i], i =1..nops(C))}, sta);
solu := subs({seq(a[i]=b[i], i =1..nops(C))}, solu);
NewC := subs({seq(a[i]=b[i], i =1..nops(C))}, NewC);

assume(op(NewC));

sta1 := SValGame(sta);
solu1 := SValGame(solu);

b := 'b';

#print more calculation
if sta1 <> sta then
	print( ` = ` ,
	subs({seq( b[i]=a[i], i =1..nops(C))}, sta1));
fi:

# really check if the conjecture and the one
# from induction is the same.
if evalb(sta1 = solu1) = false then
	print(" something is wrong in induction",sta1,solu1);
	ERROR();
fi:

end:

################################################################################

# PrintConj
# Input:  conjectures AC, variable name a,
# function name f
# Output: NULL   but print the conjectures
# out in a nice format

PrintConj := proc(AC, a, f)

local i, j, k, l, temp, DD, dom, value, newB;

for i from 1 to nops(AC) do

	temp := [seq( op([T$a[j],AC[i][1][j]]),
		j=1..LastFrog(AC[i][1])),
		seq(AC[i][1][j],j =
		LastFrog(AC[i][1])+1..nops(AC[i][1]))];

	print(``);
	print(`#############################`);
	print(`Let`, f[i], `be the value of `, temp);
	print(`#############################`);


	for j from 1 to nops(AC[i][2]) do

		
		DD    := AC[i][2][j][2];

		for k from 1 to nops(DD) do
			value := AC[i][2][j][1];
			dom := DD[k];

			newB := {};

			for l from 1 to nops(dom) do
				if not(type(dom[l],`=`)) then
					newB := newB union {dom[l]};
				else
					value := subs(dom[l],value);
				fi:
			od:

print(f[i](seq( rhs(dom[l]), l = 1..nops(dom)))
= value, op(newB));

		od:
	od:
od:

end:

# PrintRec
# Input:  the recurrence with domain rec,
# all conjectures AllC, name of function f
# Output: return the game in rec in
# the function format.

PrintRec := proc( rec, AC, f)

local hola, i, j, k, L, G;

G  := [rec[1], rec[2]];
L := [[],[]];

for i from 1 to nops(rec[3]) do
	if type(rec[3][i],`=`) then
		G  := subs(rec[3][i], G);
	fi:
od:

for hola from 1 to 2 do
	for i from 1 to nops(G[hola]) do
		for j from 1 to nops(AC) do
			if AC[j][1] = G[hola][i][1]
			and not(member(-1,{op(G[hola][i][2])})) then
				if nops(G[hola][i]) = 2 then
		L[hola] := [op(L[hola]), f[j](op(G[hola][i][2]))];

				else
		L[hola] := [op(L[hola]),

f[j](op(G[hola][i][2]))+[G[hola][i][3]]];
				fi:
			fi:
		od:
	od:
od:

return([{op(L[1])},{op(L[2])}]);

end:

##############################################

#############################################
# Conjectures done by hand for A12, A22 and A32
#############################################

A12 := proc(a)

[

 [[B, F, F], [
 [[-2], {[a[1] = 0, a[2] = 0, a[3] = 0]}]
,[[-1], {[a[1] = 0, a[2] = 0, 1 <= a[3]]}]
,[[{[0]}, {[-1/2]}],
{[a[1] = 1, a[2] = 0, a[3] = 0]}]
,[[{[0]}, {[0]}],
{[a[1] = 1, a[2] = 0, 1 <= a[3]]}]
,[[{[{[a[1]-2]}, {[{[0]},{[a[3]]}]}]}, {[0]}],
{[2 <= a[1], a[2] = 0, 0 <= a[3]]}]
,[[{[a[1]-1]}, {[{[0]},{[a[3]]}]}],
{[0 <= a[1], a[2] = 1, 0 <= a[3]]}]
,[[a[1]], {[0 <= a[1], 2 <= a[2], 0 <= a[3]]}]
]]

,[[F, B,F], [
 [[-1], {[a[1] = 0, a[2] = 0, a[3] = 0]}]
,[[-1/2], {[a[1] = 1, a[2] = 0, a[3] = 0]}]
,[[{[{[{[a[1]-3]}, {[1/2]}]}, {[0]}]}, {[0]}],
{[2 <= a[1], a[2] = 0, a[3] = 0]}]
,[[{[{[-2+a[2]]}, {[1]}]}, {[0]}],
{[0 <= a[1], 1 <= a[2], a[3] = 0]}]
,[[{[-1+a[2]]}, {[1]}],
{[0 <= a[1], 0 <= a[2], a[3] = 1]}]
,[[a[2]],
{[0 <= a[1], 0 <= a[2], 2 <= a[3]]}]
]]

,[[F, F,B], [
 [[0], {[0 <= a[1], 0 <= a[2]]}]
 ]]    
 
 ];

end:

A22 := proc(a)

[

[[B, B, F, F], [
 
[[-4], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[-1], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[{[0]}, {[0]}], {[a[1] = 2, a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[{[a[1]-5/2]}, {[0]}], 
{[3 <= a[1], a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[-3/2], {[a[1] = 0, a[2] = 1, a[3] = 0, a[4] = 0]}]
,[[0], {[a[1] = 1, a[2] = 1, a[3] = 0, a[4] = 0]}]
,[[{[1]}, {[{[1/2]}, {[0]}]}], 
{[a[1] = 2, a[2] = 1, a[3] = 0, a[4] = 0]}]
,[[a[1]-3/2], {[3 <= a[1], a[2] = 1, a[3] = 0, a[4] = 0]}]
,[[{[{[0]}, {[{[0]}, {[0]}]}]}, {[-1/4]}], 
{[a[1] = 0, a[2] = 2, a[3] = 0, a[4] = 0]}]
,[[{[1/2]}, {[1/2]}], 
{[a[1] = 1, a[2] = 2, a[3] = 0, a[4] = 0]}]
,[[a[1]-1], {[2 <= a[1], a[2] = 2, a[3] = 0, a[4] = 0]}]
,[[{[a[1]]}, {[a[1]]}], 
{[0 <= a[1], 3 <= a[2], a[3] = 0, a[4] = 0]}]
,[[-2], {[a[1] = 0, a[2] = 0, a[3] = 1, a[4] = 0]}]
,[[{[0]}, {[0]}], {[a[1] = 1, a[2] = 0, a[3] = 1, a[4] = 0]}]
,[[1], {[a[1] = 2, a[2] = 0, a[3] = 1, a[4] = 0]}]
,[[1], {[a[1] = 3, a[2] = 0, a[3] = 1, a[4] = 0]}]
,[[{[{[a[1]-2]}, {[a[1]-2]}]}, {[{[1]}, {[1]}]}], 
{[4 <= a[1], a[2] = 0, a[3] = 1, a[4] = 0]}]
,[[{[0]}, {[{[0]}, {[0]}]}], 
{[a[1] = 0, a[2] = 1, a[3] = 1, a[4] = 0]}]
,[[{[2]}, {[{[1/2]}, {[1/2]}]}], 
{[a[1] = 1, a[2] = 1, a[3] = 1, a[4] = 0]}]
,[[{[2*a[1]]}, {[{[{[a[1]-1]}, {[a[1]-1]}]}, {[{[1]}, {[1]}]}]}], 
{[2 <= a[1], a[2] = 1, a[3] = 1, a[4] = 0]}]
,[[{[2*a[1]+a[2]-1]}, {[{[a[1]]}, {[a[1]]}]}], 
{[0 <= a[1], 2 <= a[2], a[3] = 1, a[4] = 0]}]
,[[2*a[1]+a[2]], 
{[0 <= a[1], 0 <= a[2], 2 <= a[3], 0 <= a[4] ]}]
,[[-3], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 1]}]
,[[{[a[1]-2]}, {[1]}], {[1 <= a[1], a[2] = 0, a[3] = 0, a[4] = 1]}]
,[[-1/2], {[a[1] = 0, a[2] = 1, a[3] = 0, a[4] = 1]}]
,[[{[a[1]-1/2]}, {[{[a[1]-1]}, {[1]}]}], 
{[1 <= a[1], a[2] = 1, a[3] = 0, a[4] = 1]}]
,[[{[{[2*a[1]]}, {[{[a[1]]}, {[{[a[1]]}, {[2]}]}]}]}, {[a[1]]}], 
{[0 <= a[1], a[2] = 2, a[3] = 0, a[4] = 1]}]
,[[{[{[2*a[1]+a[2]-2]}, {[a[1]+1/2]}]}, {[a[1]]}], 
{[0 <= a[1], 3 <= a[2], a[3] = 0, a[4] = 1]}]
,[[-1], {[a[1] = 0, a[2] = 0, a[3] = 1, a[4] = 1]}]
,[[a[1]-1/2], {[1 <= a[1], a[2] = 0, a[3] = 1, a[4] = 1]}]
,[[{[2*a[1]]}, {[{[a[1]]}, {[{[a[1]]}, {[2]}]}]}], 
{[0 <= a[1], a[2] = 1, a[3] = 1, a[4] = 1]}]
,[[{[2*a[1]+a[2]-1]}, {[a[1]+1/2]}], 
{[0 <= a[1], 2 <= a[2], a[3] = 1, a[4] = 1]}]
,[[2*a[1]+a[2]], 
{[0 <= a[1], 0 <= a[2], 2 <= a[3], 0 <= a[4]]}]
,[[-2], {[ a[1] = 0, a[2] = 0, a[3] = 0, 2 <= a[4]]}]
,[[a[1]-1], {[ 1 <= a[1], a[2] = 0,a[3] = 0, 2 <= a[4]]}]
,[[-1/2], {[ a[1] = 0, a[2] = 1,a[3] = 0, 2 <= a[4]]}]
,[[{[a[1]]}, {[a[1]]}], {[ 1 <= a[1], a[2] = 1,a[3] = 0, 2 <= a[4]]}]
,[[{[{[-2+2*a[1]+a[2]]}, {[1+a[1]]}]}, {[a[1]]}], 
{[ 0 <= a[1], 2 <= a[2],a[3] = 0, 2 <= a[4]]}]
,[[-1], {[a[1] = 0, a[2] = 0,a[3] = 1, 2 <= a[4]]}]
,[[a[1]], {[ 1 <= a[1], a[2] = 0, a[3] = 1, 2 <= a[4]]}]
,[[{[-1+2*a[1]+a[2]]}, {[1+a[1]]}], 
{[ 0 <= a[1], 1 <= a[2], a[3] = 1, 2 <= a[4]]}]

 ]]    

,[[B, F, B, F], [
 
[[-3], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[-3/2], {[a[1] = 0, a[2] = 0, a[3] = 1, a[4] = 0]}]
,[[{[{[a[3]-3]}, {[0]}]}, {[-1]}], 
{[a[1] = 0, a[2] = 0, 2 <= a[3], a[4] = 0]}]
,[[-2], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 1]}]
,[[{[a[3]-2]}, {[0]}], 
{[a[1] = 0, a[2] = 0, 1 <= a[3], a[4] = 1]}]
,[[a[3]-1], {[a[1] = 0, a[2] = 0, 0 <= a[3], 2 <= a[4]]}]
,[[{[-1]}, {[-1]}],
{[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[0], {[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[-1], {[a[1] = 0, a[2] = 1, a[3] = 0, a[4] = 0]}]
,[[{[0]}, {[0]}], 
{[a[1] = 1, a[2] = 1, a[3] = 0, a[4] = 0]}]
,[[{[a[1]-3/2]}, {[0]}], 
{[2 <= a[1], a[2] = 1, a[3] = 0, a[4] = 0]}]
,[[-1/4], {[a[1] = 0, a[2] = 2, a[3] = 0, a[4] = 0]}]
,[[a[1]-1/2], {[1 <= a[1], a[2] = 2, a[3] = 0, a[4] = 0]}]
,[[{[{[{[2*a[1]]}, {[{[a[1]]}, {[{[a[1]]}, {[2]}]}]}]}, {[a[1]]}]}, {[a[1]]}], 
{[0 <= a[1], a[2] = 3, a[3] = 0, a[4] = 0]}]
,[[{[{[{[2*a[1]+a[2]-3]}, {[a[1]+1/2]}]}, {[a[1]]}]}, {[a[1]]}],
{[0 <= a[1], 4 <= a[2], a[3] = 0, a[4] = 0]}]
,[[0], {[a[1] = 1, a[2] = 0, a[3] = 1, a[4] = 0]}]
,[[{[1]}, {[{[1/2]}, {[0]}]}], 
{[a[1] = 2, a[2] = 0, a[3] = 1, a[4] = 0]}]
,[[{[1]}, {[1]}], {[3 <= a[1], a[2] = 0, a[3] = 1, a[4] = 0]}]
,[[{[{[a[1]+a[3]-5/2]}, {[{[{[a[1]-1]}, {[2]}]}, {[1]}]}]}, 
{[{[{[a[1]-2]}, {[1]}]}, {[0]}]}], 
{[1 <= a[1], a[2] = 0, 2 <= a[3], a[4] = 0]}]
,[[{[0]}, {[0]}], 
{[a[1] = 0, a[2] = 1, a[3] = 1, a[4] = 0]}]
,[[{[1/2]}, {[1/2]}], 
{[a[1] = 1, a[2] = 1, a[3] = 1, a[4] = 0]}]
,[[{[{[a[1]-1]}, {[a[1]-1]}]}, {[{[1]}, {[1]}]}], 
{[2 <= a[1], a[2] = 1, a[3] = 1, a[4] = 0]}]
,[[{[{[a[1]+a[3]-2]}, {[{[a[1]]}, {[2]}]}]}, {[{[a[1]-1]}, {[1]}],[2]}], 
{[0 <= a[1], a[2] = 1, 2 <= a[3], a[4] = 0]}]
,[[{[{[a[1]-2+a[3]]}, {[a[1]+1]}]}, {[a[1]]}], 
{[0 <= a[1], 2 <= a[2], 1 <= a[3], a[4] = 0]}]
,[[{[0]}, {[0]}], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 1]}]
,[[1], {[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 1]}]
,[[{[a[1]-3/2+a[3]]}, {[{[{[a[1]-1]}, {[2]}]}, {[1]}]}], 
{[1 <= a[1], a[2] = 0, 1 <= a[3], a[4] = 1]}]
,[[{[a[1]-1]}, {[1]}], {[0 <= a[1], a[2] = 1, a[3] = 0, a[4] = 1]}]
,[[{[a[1]+a[3]-1]}, {[{[a[1]]}, {[2]}]}], 
{[0 <= a[1], a[2] = 1, 1 <= a[3], a[4] = 1]}]
,[[{[a[1]-1+a[3]]}, {[a[1]+1]}], 
{[0 <= a[1], 2 <= a[2], 0 <= a[3], a[4] = 1]}]
,[[a[3]-1], {[ a[1] = 0, a[2] = 0, 0 <= a[3], 2 <= a[4]]}]
,[[a[1]-1/2+a[3]], {[1 <= a[1], a[2] = 0, 0 <= a[3], 2 <= a[4]]}]
,[[a[1]+a[3]], {[ 0 <= a[1], 1 <= a[2], 0 <= a[3], 2 <= a[4]]}]

 ]]    

,[[F, B, B, F], [
 
[[-2], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[-1], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[{[0]}, {[0]}], 
{[a[1] = 2, a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[{[1/2]}, {[0]}], 
{[a[1] = 3, a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[{[{[1]}, {[1]}]}, {[0]}], 
{[4 <= a[1], a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[-1+a[2]], 
{[0 <= a[1], 1 <= a[2], a[3] = 0, a[4] = 0]}]
,[[-1/2], {[a[1] = 0, a[2] = 0, a[3] = 1, a[4] = 0]}]
,[[{[0]}, {[0]}], 
{[a[1] = 1, a[2] = 0, a[3] = 1, a[4] = 0]}]
,[[{[{[{[a[1]-2]}, {[2]}]}, {[1]}]}, {[0]}], 
{[2 <= a[1], a[2] = 0, a[3] = 1, a[4] = 0]}]
,[[{[a[2]]}, {[a[2]]}], 
{[0 <= a[1], 1 <= a[2], a[3] = 1, a[4] = 0]}]
,[[{[{[a[1]+2*a[2]+a[3]-2]}, {[1+a[2]]}]}, {[a[2]]}], 
{[0 <= a[1], 0 <= a[2], 2 <= a[3], a[4] = 0]}]
,[[-1], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 1]}]
,[[0], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 1]}]
,[[{[{[a[1]-2]}, {[2]}]}, {[1]}], 
{[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 1]}]
,[[a[2]], {[0 <= a[1], 1 <= a[2], a[3] = 0, a[4] = 1]}]
,[[{[a[1]+2*a[2]+a[3]-1]}, {[1+a[2]]}], 
{[0 <= a[1], 0 <= a[2], 1 <= a[3], a[4] = 1]}]
,[[a[1]+2*a[2]+a[3]], 
{[0 <= a[1], 0 <= a[2], 0 <= a[3], 2 <= a[4]]}]

]]    
 
,[[B, F, F, B], [

[[-2], {[a[1] = 0, a[2] = 0, a[3] = 0]}]
,[[{[0]}, {[-1/2]}], 
{[a[1] = 1, a[2] = 0, a[3] = 0]}]
,[[{[{[a[1]-2]}, {[1/2]}]}, 
{[{[{[{[a[1]-3]}, {[1]}]}, {[0]}]}, {[0]}]}],
{[2 <= a[1], a[2] = 0, a[3] = 0]}]
,[[-1], {[a[1] = 0, a[2] = 0, 1 <= a[3]]}]
,[[{[{[a[1]-2]}, {[1]}]}, {[0]}], 
{[1 <= a[1], a[2] = 0, 1 <= a[3]]}]
,[[{[a[1]-1]}, {[1/2]}], 
{[0 <= a[1], a[2] = 1, a[3] = 0]}]
,[[{[a[1]-1]}, {[1]}], 
{[0 <= a[1], a[2] = 1, 1 <= a[3]]}]
,[[a[1]], {[0 <= a[1], 2 <= a[2], 0 <= a[3]]}]

]]

,[[F, B, F, B], [

[[-1], {[a[1] = 0, a[2] = 0, a[3] = 0]}]
,[[-1/2], {[a[1] = 1, a[2] = 0, a[3] = 0]}]
,[[{[{[{[a[1]-3]}, {[1]}]}, {[0]}]}, {[0]}], 
{[2 <= a[1], a[2] = 0, a[3] = 0]}]
,[[-1/2+a[2]], {[0 <= a[1], 1 <= a[2], a[3] = 0]}]
,[[a[2]], {[0 <= a[1], 0 <= a[2], 1 <= a[3]]}]

]]

,[[F, F, B, B], [

[[a[2]], {[0 <= a[1], 0 <= a[2]]}]

]]  
 
];

end:


A32 := proc(a)

[

[[B, B, B, F, F], [
 
[[-6], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[-2]}, {[-2]}], 
{[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[a[1]-2]}, {[a[1]-2]}],
{[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[-2], {[a[1] = 0, a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[a[1]-1], 
{[1 <= a[1], a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[2*a[1]-1]}, {[a[1]]}], 
{[0 <= a[1], a[2] = 2, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[2*a[1]+a[2]-5/2]}, {[a[1]]}], 
{[0 <= a[1], 3 <= a[2], a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[-3], {[a[1] = 0, a[2] = 0, a[3] = 1, a[4] = 0, a[5] = 0]}]
,[[{[2*a[1]-3]}, {[a[1]-1]}], 
{[1 <= a[1], a[2] = 0, a[3] = 1, a[4] = 0, a[5] = 0]}]
,[[2*a[1]-1], 
{[0 <= a[1], a[2] = 1, a[3] = 1, a[4] = 0, a[5] = 0]}]
,[[2*a[1]+a[2]-3/2], 
{[0 <= a[1], 2 <= a[2], a[3] = 1, a[4] = 0, a[5] = 0]}]
,[[{[-1]}, {[-1]}], 
{[a[1] = 0, a[2] = 0, a[3] = 2, a[4] = 0, a[5] = 0]}]
,[[{[1]}, {[1]}], 
{[a[1] = 1, a[2] = 0, a[3] = 2, a[4] = 0, a[5] = 0]}]
,[[2*a[1]-3/2], 
{[2 <= a[1], a[2] = 0, a[3] = 2, a[4] = 0, a[5] = 0]}]
,[[{[1/2]}, {[1/2]}], 
{[a[1] = 0, a[2] = 1, a[3] = 2, a[4] = 0, a[5] = 0]}]
,[[2*a[1]+a[2]-1], 
{[0 <= a[1], 2 <= a[2], a[3] = 2, a[4] = 0, a[5] = 0], 
[1 <= a[1], a[2] = 1, a[3] = 2, a[4] = 0, a[5] = 0]}]
,[[{[2*a[1]+a[2]]}, {[2*a[1]+a[2]]}], 
{[0 <= a[1], 0 <= a[2], 3 <= a[3], a[4] = 0, a[5] = 0]}]
,[[-4], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[-1], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[a[1]-1], 
{[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[-1]}, {[-1]}], 
{[a[1] = 0, a[2] = 1, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[1]}, {[1]}], 
{[a[1] = 1, a[2] = 1, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[{[{[2*a[1]-2]}, {[2*a[1]-2]}]}, {[a[1]+1/2]}]}, {[a[1]]}], 
{[2 <= a[1], a[2] = 1, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[1/2]}, {[1/2]}], 
{[a[1] = 0, a[2] = 2, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[{[2*a[1]+a[2]-2]}, {[2*a[1]+a[2]-2]}]}, 
{[{[a[1]+1]}, {[a[1]+1]}]}], 
{[1 <= a[1], a[2] = 2, a[3] = 0, a[4] = 1, a[5] = 0], 
[0 <= a[1], 3 <= a[2], a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[0]}, {[{[-1]}, {[-1]}]}], 
{[a[1] = 0, a[2] = 0, a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[{[3]}, {[{[1]}, {[1]}]}], 
{[a[1] = 1, a[2] = 0, a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[{[3*a[1]]}, {[{[{[{[2*a[1]-2]}, 
{[2*a[1]-2]}]}, {[a[1]+1/2]}]}, {[a[1]]}]}], 
{[2 <= a[1], a[2] = 0, a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[{[2]}, {[{[1/2]}, {[1/2]}]}], 
{[a[1] = 0, a[2] = 1, a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[{[3*a[1]+2*a[2]]}, {[{[{[2*a[1]+a[2]-1]}, 
{[2*a[1]+a[2]-1]}]}, {[{[a[1]+1]}, {[a[1]+1]}]}]}], 
{[1 <= a[1], a[2] = 1, a[3] = 1, a[4] = 1, a[5] = 0],
[0 <= a[1], 2 <= a[2], a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[{[3*a[1]+2*a[2]+a[3]-1]}, 
{[{[2*a[1]+a[2]]}, {[2*a[1]+a[2]]}]}], 
{[0 <= a[1], 0 <= a[2], 2 <= a[3], a[4] = 1, a[5] = 0]}]
,[[3*a[1]+2*a[2]+a[3]], 
{[0 <= a[1], 0 <= a[2], 0 <= a[3], 2 <= a[4], a[5] = 0]}]
,[[-5], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[-1]}, {[-1]}], 
{[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[1]}, {[1]}], 
{[a[1] = 2, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[{[{[2*a[1]-4]}, {[2*a[1]-4]}]}, {[a[1]-1/2]}]}, {[a[1]-1]}], 
{[3 <= a[1], a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[-1], {[a[1] = 0, a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[1], {[a[1] = 1, a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[{[2*a[1]-2]}, {[2*a[1]-2]}]}, {[a[1]+1/2]}], 
{[2 <= a[1], a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[2*a[1]+a[2]-2]}, {[a[1]+1]}], 
{[0 <= a[1], 2 <= a[2], a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[-3/2], {[a[1] = 0, a[2] = 0, a[3] = 1, a[4] = 0, a[5] = 1]}]
,[[1/2], {[a[1] = 1, a[2] = 0, a[3] = 1, a[4] = 0, a[5] = 1]}]
,[[{[2*a[1]-2]}, {[2*a[1]-2]}], 
{[2 <= a[1], a[2] = 0, a[3] = 1, a[4] = 0, a[5] = 1]}]
,[[2*a[1]], {[0 <= a[1], a[2] = 1, a[3] = 1, a[4] = 0, a[5] = 1]}]
,[[{[{[2*a[1]+a[2]-1]}, {[{[2*a[1]+a[2]-1]}, {[a[1]+2]}]}]}, 
{[{[2*a[1]+a[2]-1]}, {[a[1]+1]}]}], 
{[0 <= a[1], 2 <= a[2], a[3] = 1, a[4] = 0, a[5] = 1]}]
,[[{[2*a[1]]}, {[2*a[1]]}], 
{[0 <= a[1], a[2] = 0, a[3] = 2, a[4] = 0, a[5] = 1]}]
,[[{[{[3*a[1]+2*a[2]]}, {[{[2*a[1]+a[2]]}, {[{[2*a[1]+a[2]]}, 
{[a[1]+2]}]}]}]}, {[2*a[1]+a[2]]}], 
{[0 <= a[1], 1 <= a[2], a[3] = 2, a[4] = 0, a[5] = 1]}]
,[[{[{[3*a[1]+2*a[2]+a[3]-2]}, {[2*a[1]+a[2]+1/2]}]}, {[2*a[1]+a[2]]}], 
{[0 <= a[1], 0 <= a[2], 3 <= a[3], a[4] = 0, a[5] = 1]}]
,[[2*a[1]-2], {[0 <= a[1], a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 1]}]
,[[{[2*a[1]]}, {[2*a[1]]}], 
{[0 <= a[1], a[2] = 1, a[3] = 0, a[4] = 1, a[5] = 1]}]
,[[{[2*a[1]+a[2]-1]}, {[{[{[2*a[1]+a[2]-1]}, 
{[{[2*a[1]+a[2]-1]}, {[a[1]+2]}]}], [{[2*a[1]+a[2]-1]}, 
{[2*a[1]+a[2]-1]}]}, {[{[{[2*a[1]+a[2]-1]}, {[a[1]+2]}]}, 
{[a[1]+1]}], [{[2*a[1]+a[2]-1]}, {[a[1]+1]}]}]}], 
{[0 <= a[1], 2 <= a[2], a[3] = 0, a[4] = 1, a[5] = 1]}]
,[[{[0]}, {[{[0]}, {[0]}]}], 
{[a[1] = 0, a[2] = 0, a[3] = 1, a[4] = 1, a[5] = 1]}]
,[[{[3*a[1]]}, {[{[2*a[1]]}, {[a[1]+1]}]}], 
{[1 <= a[1], a[2] = 0, a[3] = 1, a[4] = 1, a[5] = 1]}]
,[[{[3*a[1]+2*a[2]]}, {[{[2*a[1]+a[2]]}, 
{[{[2*a[1]+a[2]]}, {[a[1]+2]}]}]}],
{[0 <= a[1], 1 <= a[2], a[3] = 1, a[4] = 1, a[5] = 1]}]
,[[{[3*a[1]+2*a[2]+a[3]-1]}, {[2*a[1]+a[2]+1/2]}], 
{[0 <= a[1], 0 <= a[2], 2 <= a[3], a[4] = 1, a[5] = 1]}]
,[[3*a[1]+2*a[2]+a[3]], 
{[0 <= a[1], 0 <= a[2], 0 <= a[3], 2 <= a[4], a[5] = 1]}]
,[[-3], {[ a[1] = 0, a[2] = 0, a[3] = 0,a[4] = 0, 2 <= a[5]]}]
,[[{[-2+2*a[1]]}, {[-2+2*a[1]]}], 
{[ 1 <= a[1], a[2] = 0, a[3] = 0,a[4] = 0, 2 <= a[5]]}]
,[[-1+2*a[1]+a[2]], 
{[ 0 <= a[1], 1 <= a[2], a[3] = 0,a[4] = 0, 2 <= a[5]]}]
,[[-1+2*a[1]], 
{[ 0 <= a[1], a[2] = 0, a[3] = 1,a[4] = 0, 2 <= a[5]]}]
,[[{[2*a[1]+a[2]]}, {[2*a[1]+a[2]]}],
{[ 0 <= a[1], 1 <= a[2], a[3] = 1,a[4] = 0, 2 <= a[5]]}]
,[[{[{[-2+3*a[1]+2*a[2]+a[3]]}, {[1+2*a[1]+a[2]]}]}, {[2*a[1]+a[2]]}], 
{[ 0 <= a[1], 0 <= a[2], 2 <= a[3],a[4] = 0, 2 <= a[5]]}]
,[[-2], {[ a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 1, 2 <= a[5]]}]
,[[{[-1+2*a[1]]}, {[-1+2*a[1]]}], 
{[ 1 <= a[1], a[2] = 0, a[3] = 0, a[4] = 1, 2 <= a[5]]}]
,[[2*a[1]+a[2]], {[ 0 <= a[1], 1 <= a[2], a[3] = 0, a[4] = 1, 2 <= a[5]]}]
,[[{[-1+3*a[1]+2*a[2]+a[3]]}, {[1+2*a[1]+a[2]]}], 
{[ 0 <= a[1], 0 <= a[2], 1 <= a[3],a[4] = 1, 2 <= a[5]]}]
,[[3*a[1]+2*a[2]+a[3]], 
{[ 0 <= a[1], 0 <= a[2], 0 <= a[3], 2 <= a[4], 2 <= a[5]]}]


]] 

,[[B, B, F, B, F], [
 
[[-5], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[-3], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[{[a[4]-4]}, {[-1]}]}, {[-2]}], 
{[a[1] = 0, a[2] = 0, a[3] = 0, 2 <= a[4], a[5] = 0]}]
,[[-2], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[a[1]-2], {[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[-2]}, {[-2]}], {[a[1] = 0, a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[a[1]-1]}, {[a[1]-1]}], 
{[1 <= a[1], a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[-1/2]}, {[-1/2]}], 
{[a[1] = 0, a[2] = 2, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[a[1]], {[0 <= a[1], 3 <= a[2], a[3] = 0, a[4] = 0, a[5] = 0], 
[1 <= a[1], a[2] = 2, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[-2], {[a[1] = 0, a[2] = 0, a[3] = 1, a[4] = 0, a[5] = 0]}]
,[[a[1]-1], {[1 <= a[1], a[2] = 0, a[3] = 1, a[4] = 0, a[5] = 0]}]
,[[{[2*a[1]-1]}, {[a[1]]}], 
{[0 <= a[1], a[2] = 1, a[3] = 1, a[4] = 0, a[5] = 0]}]
,[[{[2*a[1]+a[2]-3/2]}, {[a[1]]}],
{[0 <= a[1], 2 <= a[2], a[3] = 1, a[4] = 0, a[5] = 0]}]
,[[2*a[1]-1], {[0 <= a[1], a[2] = 0, a[3] = 2, a[4] = 0, a[5] = 0]}]
,[[2*a[1]+a[2]-1/2], {[0 <= a[1], 1 <= a[2], a[3] = 2, a[4] = 0, a[5] = 0]}]
,[[{[{[2*a[1]]}, {[2*a[1]]}]}, {[2*a[1]]}],
{[0 <= a[1], a[2] = 0, a[3] = 3, a[4] = 0, a[5] = 0]}]
,[[{[{[{[3*a[1]+2*a[2]]}, {[{[2*a[1]+a[2]]}, 
{[{[2*a[1]+a[2]]}, {[a[1]+2]}]}]}]}, {[2*a[1]+a[2]]}]}, {[2*a[1]+a[2]]}], 
{[0 <= a[1], 1 <= a[2], a[3] = 3, a[4] = 0, a[5] = 0]}]
,[[{[{[{[3*a[1]+2*a[2]+a[3]-3]}, {[2*a[1]+a[2]+1/2]}]},
{[2*a[1]+a[2]]}]}, {[2*a[1]+a[2]]}], 
{[0 <= a[1], 0 <= a[2], 4 <= a[3], a[4] = 0, a[5] = 0]}]
,[[-1/2], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[a[1]-1]}, {[a[1]-1]}], 
{[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[{[2*a[1]+a[4]-4]}, {[a[1]]}]}, {[a[1]-1]}], 
{[1 <= a[1], a[2] = 0, a[3] = 0, 2 <= a[4], a[5] = 0]}]
,[[-1], {[a[1] = 0, a[2] = 1, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[{[{[-2+a[4]]}, {[-2+a[4]]}]}, {[1/2]}]}, {[-1/2]}], 
{[a[1] = 0, a[2] = 1, a[3] = 0, 2 <= a[4], a[5] = 0]}]
,[[a[1]], {[1 <= a[1], a[2] = 1, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[{[{[2*a[1]+a[4]-2]}, {[2*a[1]+a[4]-2]}]}, 
{[{[a[1]+1]}, {[a[1]+1]}]}]}, {[{[a[1]]}, {[a[1]]}]}], 
{[1 <= a[1], a[2] = 1, a[3] = 0, 2 <= a[4], a[5] = 0]}]
,[[1/2], {[a[1] = 0, a[2] = 2, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[a[1]+1]}, {[a[1]+1]}], 
{[1 <= a[1], a[2] = 2, a[3] = 0, a[4] = 1, a[5] = 0], 
[0 <= a[1], 3 <= a[2], a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[{[{[2*a[1]+a[2]-1]}, {[2*a[1]+a[2]-1]}],
[{[2*a[1]+a[2]-1]}, {[{[2*a[1]+a[2]-1]}, {[a[1]+2]}]}]}, 
{[{[{[2*a[1]+a[2]-1]}, {[a[1]+2]}]}, {[a[1]+1]}], 
[{[2*a[1]+a[2]-1]}, {[a[1]+1]}]}]}, {[{[{[2*a[1]+a[2]-2]}, 
{[a[1]+1]}]}, {[a[1]]}]}], 
{[0 <= a[1], 2 <= a[2], a[3] = 0, a[4] = 2, a[5] = 0]}]
,[[{[{[{[2*a[1]+a[2]+a[4]-3]}, {[2*a[1]+a[2]+a[4]-3]}]}, 
{[{[{[2*a[1]+a[2]-1]}, {[a[1]+2]}]}, {[a[1]+1]}]}]}, 
{[{[{[2*a[1]+a[2]-2]}, {[a[1]+1]}]}, {[a[1]]}]}], 
{[0 <= a[1], 2 <= a[2], a[3] = 0, 3 <= a[4], a[5] = 0]}]
,[[{[-1]}, {[-1]}],
{[a[1] = 0, a[2] = 0, a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[{[1]}, {[1]}], 
{[a[1] = 1, a[2] = 0, a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[{[{[{[2*a[1]-2]}, {[2*a[1]-2]}]}, {[1/2+a[1]]}]}, {[a[1]]}], 
{[2 <= a[1], a[2] = 0, a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[{[1/2]}, {[1/2]}], 
{[a[1] = 0, a[2] = 1, a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[{[{[2*a[1]+a[2]-1]}, {[2*a[1]+a[2]-1]}]}, {[{[a[1]+1]}, {[a[1]+1]}]}], 
{[1 <= a[1], a[2] = 1, a[3] = 1, a[4] = 1, a[5] = 0], 
[0 <= a[1], 2 <= a[2], a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[{[{[a[4]-2]}, {[0]}]}, {[-1]}], 
{[a[1] = 0, a[2] = 0, a[3] = 1, 2 <= a[4], a[5] = 0]}]
,[[{[{[2*a[1]+a[4]-2]}, {[a[1]+1]}]}, {[a[1]]}], 
{[1 <= a[1], a[2] = 0, a[3] = 1, 2 <= a[4], a[5] = 0]}]
,[[{[{[2*a[1]+a[2]+a[4]-2]}, {[{[2*a[1]+a[2]]}, {[a[1]+2]}]}]}, 
{[a[1]+2], [{[2*a[1]+a[2]-1]}, {[a[1]+1]}]}], 
{[0 <= a[1], 1 <= a[2], a[3] = 1, 2 <= a[4], a[5] = 0]}]
,[[{[2*a[1]+a[2]]}, {[2*a[1]+a[2]]}], 
{[0 <= a[1], 0 <= a[2], 2 <= a[3], a[4] = 1, a[5] = 0]}]
,[[{[{[2*a[1]+a[2]-2+a[4]]}, 
{[2*a[1]+a[2]+1]}]}, {[2*a[1]+a[2]]}], 
{[0 <= a[1], 0 <= a[2], 2 <= a[3], 2 <= a[4], a[5] = 0]}]
,[[-4], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[a[4]-3]}, {[-1]}], 
{[a[1] = 0, a[2] = 0, a[3] = 0, 1 <= a[4], a[5] = 1]}]
,[[-1], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[a[1]-1], {[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[-1]}, {[-1]}], 
{[a[1] = 0, a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[1]}, {[1]}], 
{[a[1] = 1, a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[{[{[2*a[1]-2]}, {[2*a[1]-2]}]}, {[a[1]+1/2]}]}, {[a[1]]}], 
{[2 <= a[1], a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[1/2]}, {[1/2]}], 
{[a[1] = 0, a[2] = 2, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[a[1]+1], {[1 <= a[1], a[2] = 2, a[3] = 0, a[4] = 0, a[5] = 1], 
[0 <= a[1], 3 <= a[2], a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[-1], {[a[1] = 0, a[2] = 0, a[3] = 1, a[4] = 0, a[5] = 1]}]
,[[1], {[a[1] = 1, a[2] = 0, a[3] = 1, a[4] = 0, a[5] = 1]}]
,[[{[{[2*a[1]-2]}, {[2*a[1]-2]}]}, {[a[1]+1/2]}],
{[2 <= a[1], a[2] = 0, a[3] = 1, a[4] = 0, a[5] = 1]}]
,[[{[2*a[1]+a[2]-1]}, {[a[1]+1]}], 
{[0 <= a[1], 1 <= a[2], a[3] = 1, a[4] = 0, a[5] = 1]}]
,[[2*a[1]+a[2]], 
{[0 <= a[1], 0 <= a[2], 2 <= a[3], a[4] = 0, a[5] = 1]}]
,[[{[2*a[1]+a[4]-3]}, {[a[1]]}], 
{[1 <= a[1], a[2] = 0, a[3] = 0, 1 <= a[4], a[5] = 1]}]
,[[{[{[a[4]-1]}, {[a[4]-1]}]}, {[1/2]}], 
{[a[1] = 0, a[2] = 1, a[3] = 0, 1 <= a[4], a[5] = 1]}]
,[[{[{[2*a[1]-1+a[4]]}, {[2*a[1]-1+a[4]]}]}, 
{[{[a[1]+1]}, {[a[1]+1]}]}], 
{[1 <= a[1], a[2] = 1, a[3] = 0, 1 <= a[4], a[5] = 1]}]
,[[{[{[2*a[1]+a[2]-1]}, {[2*a[1]+a[2]-1]}], 
[{[2*a[1]+a[2]-1]}, {[{[2*a[1]+a[2]-1]}, 
{[a[1]+2]}]}]}, {[{[{[2*a[1]+a[2]-1]}, 
{[a[1]+2]}]}, {[a[1]+1]}], [{[2*a[1]+a[2]-1]}, {[a[1]+1]}]}], 
{[0 <= a[1], 2 <= a[2], a[3] = 0, a[4] = 1, a[5] = 1]}]
,[[{[{[2*a[1]+a[2]+a[4]-2]}, {[2*a[1]+a[2]+a[4]-2]}]}, 
{[{[{[2*a[1]+a[2]-1]}, {[a[1]+2]}]}, {[a[1]+1]}]}],
{[0 <= a[1], 2 <= a[2], a[3] = 0, 2 <= a[4], a[5] = 1]}]
,[[{[a[4]-1]}, {[0]}], 
{[a[1] = 0, a[2] = 0, a[3] = 1,1 <= a[4], a[5] = 1]}]
,[[{[a[4]+2*a[1]-1]}, {[a[1]+1]}], 
{[ 1 <= a[1], a[2] = 0, a[3] = 1,1 <= a[4], a[5] = 1]}]
,[[{[a[4]+2*a[1]+a[2]-1]}, {[{[2*a[1]+a[2]]}, {[a[1]+2]}]}], 
{[ 0 <= a[1], 1 <= a[2], a[3] = 1,1 <= a[4], a[5] = 1]}]
,[[{[a[4]+2*a[1]+a[2]-1]}, {[2*a[1]+a[2]+1]}], 
{[0 <= a[1], 0 <= a[2], 2 <= a[3], 1 <= a[4], a[5] = 1]}]
,[[2*a[1]+a[4]-2], 
{[0 <= a[1], a[2] = 0, a[3] = 0, 0 <= a[4], 2 <= a[5]]}]
,[[{[a[4]+2*a[1]+a[2]-1]}, {[a[4]+2*a[1]+a[2]-1]}], 
{[ 0 <= a[1], 1 <= a[2], a[3] = 0, 0 <= a[4], 2 <= a[5]]}]
,[[a[4]+2*a[1]+a[2]], 
{[ 0 <= a[1], 0 <= a[2], 1 <= a[3], 0 <= a[4], 2 <= a[5]]}]

]] 

,[[B, F, B, B, F], [

[[-4], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[a[3]-2], {[a[1] = 0, a[2] = 0, 1 <= a[3], a[4] = 0, a[5] = 0]}]
,[[-2], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[a[3]-1]}, {[a[3]-1]}], 
{[a[1] = 0, a[2] = 0, 1 <= a[3], a[4] = 1, a[5] = 0]}]
,[[{[{[2*a[3]+a[4]-3]}, {[a[3]]}]}, {[a[3]-1]}], 
{[a[1] = 0, a[2] = 0, 0 <= a[3], 2 <= a[4], a[5] = 0]}]
,[[-1], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[a[1]-2]}, {[{[a[1]-2]}, {[3]}]}], 
{[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[-2], {[a[1] = 0, a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[a[1]-1], {[1 <= a[1], a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[-1/2], {[a[1] = 0, a[2] = 2, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[a[1]]}, {[a[1]]}], 
{[1 <= a[1], a[2] = 2, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[1/2]}, {[0]}], 
{[a[1] = 0, a[2] = 3, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[{[a[1]+1]}, {[a[1]+1]}]}, {[a[1]]}], 
{[0 <= a[1], 4 <= a[2], a[3] = 0, a[4] = 0, a[5] = 0], 
[1 <= a[1], a[2] = 3, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[a[1]+a[3]-3/2], {[1 <= a[1], a[2] = 0, 1 <= a[3], a[4] = 0, a[5] = 0]}]
,[[{[0]}, {[0]}], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[3/2]}, {[3/2]}], {[a[1] = 2, a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[5/2]}, {[5/2]}], {[a[1] = 3, a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[27/8], {[a[1] = 4, a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[a[1]-1]}, {[{[a[1]-1]}, {[5]}]}], 
{[5 <= a[1], a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[a[1]+a[3]-1/2]}, {[a[1]+a[3]-1/2]}], 
{[1 <= a[1], a[2] = 0, 1 <= a[3], a[4] = 1, a[5] = 0]}]
,[[{[5/4]}, {[1/2]}], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 2, a[5] = 0]}]
,[[{[{[3]}, {[5/2]}]}, {[3/2]}], 
{[a[1] = 2, a[2] = 0, a[3] = 0, a[4] = 2, a[5] = 0]}]
,[[{[{[5]}, {[7/2]}]}, {[5/2]}], 
{[a[1] = 3, a[2] = 0, a[3] = 0, a[4] = 2, a[5] = 0]}]
,[[{[{[7]}, {[9/2]}]}, {[7/2]}], 
{[a[1] = 4, a[2] = 0, a[3] = 0, a[4] = 2, a[5] = 0]}]
,[[{[{[9]}, {[11/2]}]}, {[9/2]}],
{[a[1] = 5, a[2] = 0, a[3] = 0, a[4] = 2, a[5] = 0]}]
,[[{[{[11]}, {[{[6]}, {[6]}]}]}, {[11/2]}],
{[a[1] = 6, a[2] = 0, a[3] = 0, a[4] = 2, a[5] = 0]}]
,[[{[a[1]]}, {[a[1]-1/2]}], 
{[7 <= a[1], a[2] = 0, a[3] = 0, a[4] = 2, a[5] = 0]}]
,[[{[{[2*a[1]+2*a[3]-1]}, {[a[1]+a[3]+1/2]}]}, {[a[1]+a[3]-1/2]}], 
{[1 <= a[1], a[2] = 0, 1 <= a[3], a[4] = 2, a[5] = 0]}]
,[[{[{[2*a[1]+2*a[3]+a[4]-3]}, {[a[1]+a[3]+1/2]}]}, {[a[1]+a[3]-1/2]}], 
{[1 <= a[1], a[2] = 0, 0 <= a[3], 3 <= a[4], a[5] = 0]}]
,[[a[1]+a[3]-1], {[0 <= a[1], 1 <= a[2], 1 <= a[3], a[4] = 0, a[5] = 0]}]
,[[-1/2], {[a[1] = 0, a[2] = 1, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[a[1]]}, {[a[1]]}], 
{[1 <= a[1], a[2] = 1, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[1/2]}, {[0]}], 
{[a[1] = 0, a[2] = 2, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[{[a[1]+1]}, {[a[1]+1]}]}, {[a[1]]}],
{[1 <= a[1], a[2] = 2, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[{[{[{[2*a[1]+a[2]-2]}, {[2*a[1]+a[2]-2]}], 
[{[2*a[1]+a[2]-2]}, {[{[2*a[1]+a[2]-2]}, {[a[1]+2]}]}]}, 
{[{[2*a[1]+a[2]-2]}, {[a[1]+1]}], [{[{[2*a[1]+a[2]-2]}, 
{[a[1]+2]}]}, {[a[1]+1]}]}]}, {[a[1]+1]}]}, {[a[1]]}], 
{[0 <= a[1], 3 <= a[2], a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[a[1]+a[3]]}, {[a[1]+a[3]]}], 
{[0 <= a[1], 1 <= a[2], 1 <= a[3], a[4] = 1, a[5] = 0]}]
,[[{[{[2*a[1]+a[2]+2*a[3]+a[4]-3]}, {[a[1]+1+a[3]]}]}, {[a[1]+a[3]]}], 
{[0 <= a[1], 1 <= a[2], 0 <= a[3], 2 <= a[4], a[5] = 0]}]
,[[-3], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[a[3]-1], {[a[1] = 0, a[2] = 0, 1 <= a[3], a[4] = 0, a[5] = 1]}]
,[[{[2*a[3]+a[4]-2]}, {[a[3]]}], 
{[a[1] = 0, a[2] = 0, 0 <= a[3], 1 <= a[4], a[5] = 1]}]
,[[0], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[a[1]-1]}, {[{[a[1]-1]}, {[4]}]}], 
{[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[-1], {[a[1] = 0, a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[a[1]], {[1 <= a[1], a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[1/2], {[a[1] = 0, a[2] = 2, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[a[1]+1]}, {[a[1]+1]}], 
{[1 <= a[1], a[2] = 2, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[{[{[2*a[1]+a[2]-2]}, {[2*a[1]+a[2]-2]}], [{[2*a[1]+a[2]-2]}, 
{[{[2*a[1]+a[2]-2]}, {[a[1]+2]}]}]}, {[{[{[2*a[1]+a[2]-2]}, {[a[1]+2]}]}, 
{[a[1]+1]}], [{[2*a[1]+a[2]-2]}, {[a[1]+1]}]}]}, {[a[1]+1]}], 
{[0 <= a[1], 3 <= a[2], a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[a[1]+a[3]-1/2], 
{[1 <= a[1], a[2] = 0, 1 <= a[3], a[4] = 0, a[5] = 1]}]
,[[5/4], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 1]}]
,[[{[3]}, {[5/2]}], 
{[a[1] = 2, a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 1]}]
,[[{[5]}, {[7/2]}], 
{[a[1] = 3, a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 1]}]
,[[{[7]}, {[9/2]}], 
{[a[1] = 4, a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 1]}]
,[[{[2*a[1]-1]}, {[{[a[1]]}, {[6]}]}], 
{[5 <= a[1], a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 1]}]
,[[{[2*a[1]+2*a[3]-1]}, {[a[1]+a[3]+1/2]}], 
{[1 <= a[1], a[2] = 0, 1 <= a[3], a[4] = 1, a[5] = 1]}]
,[[{[2*a[1]+2*a[3]+a[4]-2]}, {[a[1]+a[3]+1/2]}], 
{[1 <= a[1], a[2] = 0, 0 <= a[3], 2 <= a[4], a[5] = 1]}]
,[[a[1]+a[3]], 
{[0 <= a[1], 1 <= a[2], 1 <= a[3], a[4] = 0, a[5] = 1]}]
,[[{[2*a[1]+a[2]+2*a[3]+a[4]-2]}, {[a[1]+1+a[3]]}],
{[0 <= a[1], 1 <= a[2], 0 <= a[3], 1 <= a[4], a[5] = 1]}]
,[[2*a[1]+a[2]+2*a[3]+a[4]-1], 
{[0 <= a[1], 0 <= a[2], 0 <= a[3], 0 <= a[4], 2 <= a[5]]}]

]] 

,[[F, B, B, B, F], [
 
[[-3], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[-1]}, {[-1]}], 
{[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[a[1]-1], {[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[a[1]]}, {[a[1]]}], 
{[0 <= a[1], a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[2*a[2]-2]}, {[2*a[2]-2]}], 
{[a[1] = 0, 2 <= a[2], a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[2*a[2]-1]}, {[2*a[2]-1]}], 
{[a[1] = 1, 2 <= a[2], a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[2*a[2]]}, {[2*a[2]]}], 
{[a[1] = 2, 2 <= a[2], a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[{[2*a[2]+1/2]}, {[2*a[2]+1/2]}], 
{[a[1] = 3, 2 <= a[2], a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[a[1]+2*a[2]-3], 
{[4 <= a[1], 2 <= a[2], a[3] = 0, a[4] = 0, a[5] = 0]}]
,[[2*a[2]+a[3]-1], 
{[a[1] = 0, 0 <= a[2], 1 <= a[3], a[4] = 0, a[5] = 0]}]
,[[2*a[2]+a[3]], 
{[a[1] = 1, 0 <= a[2], 1 <= a[3], a[4] = 0, a[5] = 0]}]
,[[2*a[2]+a[3]+1], 
{[a[1] = 2, 0 <= a[2], 1 <= a[3], a[4] = 0, a[5] = 0]}]
,[[3], {[a[1] = 3, a[2] = 0, a[3] = 1, a[4] = 0, a[5] = 0]}]
,[[2*a[2]+5/2], 
{[a[1] = 3, 1 <= a[2], a[3] = 1, a[4] = 0, a[5] = 0]}]
,[[2*a[2]+a[3]+2], 
{[a[1] = 3, 0 <= a[2], 2 <= a[3], a[4] = 0, a[5] = 0]}]
,[[a[1]], {[4 <= a[1], a[2] = 0, a[3] = 1, a[4] = 0, a[5] = 0]}]
,[[{[a[1]+2*a[2]-1]}, {[a[1]+2*a[2]-1]}], 
{[4 <= a[1], 1 <= a[2], a[3] = 1, a[4] = 0, a[5] = 0]}]
,[[a[1]+2*a[2]+a[3]-1],
{[4 <= a[1], 0 <= a[2], 2 <= a[3], a[4] = 0, a[5] = 0]}]
,[[-1], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[0], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[a[1]]}, {[a[1]]}], 
{[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[a[1]+2*a[2]-1],
{[0 <= a[1], 1 <= a[2], a[3] = 0, a[4] = 1, a[5] = 0]}]
,[[{[2*a[2]+1]}, {[2*a[2]+1]}], 
{[a[1] = 0, 0 <= a[2], a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[{[2*a[2]+2]}, {[2*a[2]+2]}], 
{[a[1] = 1, 0 <= a[2], a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[{[2*a[2]+3]}, {[2*a[2]+3]}], 
{[a[1] = 2, 0 <= a[2], a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[{[4]}, {[4]}], 
{[a[1] = 3, a[2] = 0, a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[2*a[2]+15/4], 
{[a[1] = 3, 1 <= a[2], a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[{[a[1]+1]}, {[a[1]+1]}], 
{[4 <= a[1], a[2] = 0, a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[a[1]+2*a[2]], 
{[4 <= a[1], 1 <= a[2], a[3] = 1, a[4] = 1, a[5] = 0]}]
,[[{[a[1]+2*a[2]+a[3]]}, {[a[1]+2*a[2]+a[3]]}], 
{[0 <= a[1], 0 <= a[2], 2 <= a[3], a[4] = 1, a[5] = 0]}]
,[[{[{[3*a[2]+2*a[3]]}, {[2*a[2]+a[3]+1]}]}, {[2*a[2]+a[3]]}], 
{[a[1] = 0, 0 <= a[2], 0 <= a[3], a[4] = 2, a[5] = 0]}]
,[[{[{[3*a[2]+2*a[3]+2]}, {[2*a[2]+a[3]+2]}]}, {[2*a[2]+a[3]+1]}], 
{[a[1] = 1, 0 <= a[2], 0 <= a[3], a[4] = 2, a[5] = 0]}]
,[[{[{[3*a[2]+2*a[3]+4]}, {[2*a[2]+a[3]+3]}]}, {[2*a[2]+a[3]+2]}], 
{[a[1] = 2, 0 <= a[2], 0 <= a[3], a[4] = 2, a[5] = 0]}]
,[[{[{[6]}, {[4]}]}, {[3]}], 
{[a[1] = 3, a[2] = 0, a[3] = 0, a[4] = 2, a[5] = 0]}]
,[[{[{[3*a[2]+6]}, {[2*a[2]+7/2]}]}, {[2*a[2]+3]}], 
{[a[1] = 3, 1 <= a[2], a[3] = 0, a[4] = 2, a[5] = 0]}]
,[[{[{[3*a[2]+2*a[3]+6]}, {[2*a[2]+a[3]+4]}]}, {[2*a[2]+a[3]+3]}], 
{[a[1] = 3, 0 <= a[2], 1 <= a[3], a[4] = 2, a[5] = 0]}]
,[[{[{[2*a[1]]}, {[a[1]+1]}]}, {[a[1]]}], 
{[4 <= a[1], a[2] = 0, a[3] = 0, a[4] = 2, a[5] = 0]}]
,[[{[a[1]+2*a[2]]}, {[a[1]+2*a[2]]}], 
{[4 <= a[1], 1 <= a[2], a[3] = 0, a[4] = 2, a[5] = 0]}]
,[[{[{[2*a[1]+3*a[2]+2*a[3]]}, {[a[1]+2*a[2]+a[3]+1]}]}, {[a[1]+2*a[2]+a[3]]}], 
{[4 <= a[1], 0 <= a[2], 1 <= a[3], a[4] = 2, a[5] = 0]}]
,[[{[{[2*a[1]+3*a[2]+2*a[3]+a[4]-2]}, {[a[1]+2*a[2]+a[3]+1]}]}, {[a[1]+2*a[2]+a[3]]}], 
{[0 <= a[1], 0 <= a[2], 0 <= a[3], 3 <= a[4], a[5] = 0]}]
,[[-2], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[0]}, {[0]}], 
{[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[a[1]], 
{[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[a[1]+1]}, {[a[1]+1]}], 
{[0 <= a[1], a[2] = 1, a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[2*a[2]-1]}, {[2*a[2]-1]}], 
{[a[1] = 0, 2 <= a[2], a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[2*a[2]]}, {[2*a[2]]}], 
{[a[1] = 1, 2 <= a[2], a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[2*a[2]+1]}, {[2*a[2]+1]}], 
{[a[1] = 2, 2 <= a[2], a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[{[2*a[2]+3/2]}, {[2*a[2]+3/2]}], 
{[a[1] = 3, 2 <= a[2], a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[a[1]+2*a[2]-2], 
{[4 <= a[1], 2 <= a[2], a[3] = 0, a[4] = 0, a[5] = 1]}]
,[[2*a[2]+a[3]], 
{[a[1] = 0, 0 <= a[2], 1 <= a[3], a[4] = 0, a[5] = 1]}]
,[[2*a[2]+a[3]+1], 
{[a[1] = 1, 0 <= a[2], 1 <= a[3], a[4] = 0, a[5] = 1]}]
,[[2*a[2]+a[3]+2], 
{[a[1] = 2, 0 <= a[2], 1 <= a[3], a[4] = 0, a[5] = 1]}]
,[[4], {[a[1] = 3, a[2] = 0, a[3] = 1, a[4] = 0, a[5] = 1]}]
,[[2*a[2]+7/2], 
{[a[1] = 3, 1 <= a[2], a[3] = 1, a[4] = 0, a[5] = 1]}]
,[[2*a[2]+a[3]+3], 
{[a[1] = 3, 0 <= a[2], 2 <= a[3], a[4] = 0, a[5] = 1]}]
,[[a[1]+1], 
{[4 <= a[1], a[2] = 0, a[3] = 1, a[4] = 0, a[5] = 1]}]
,[[{[a[1]+2*a[2]]}, {[a[1]+2*a[2]]}], 
{[4 <= a[1], 1 <= a[2], a[3] = 1, a[4] = 0, a[5] = 1]}]
,[[a[1]+2*a[2]+a[3]], 
{[0 <= a[1], 0 <= a[2], 2 <= a[3], a[4] = 0, a[5] = 1]}]
,[[{[2*a[1]]}, {[a[1]+1]}], 
{[0 <= a[1], a[2] = 0, a[3] = 0, a[4] = 1, a[5] = 1]}]
,[[{[2*a[1]+3*a[2]]}, {[{[a[1]+2*a[2]]}, {[2*a[2]+4]}]}], 
{[0 <= a[1], 1 <= a[2] , a[3] = 0, a[4] = 1, a[5] = 1]}]
,[[{[2*a[1]+3*a[2]+2*a[3]]}, {[a[1]+2*a[2]+a[3]+1]}], 
{[0 <= a[1], 0 <= a[2], 1 <= a[3], a[4] = 1, a[5] = 1]}]
,[[{[2*a[1]+3*a[2]+2*a[3]+a[4]-1]}, {[a[1]+2*a[2]+a[3]+1]}], 
{[0 <= a[1], 0 <= a[2], 0 <= a[3], 2 <= a[4], a[5] = 1]}]
,[[2*a[1]+3*a[2]+2*a[3]+a[4]], 
{[0 <= a[1], 0 <= a[2], 0 <= a[3], 0 <= a[4], 2 <= a[5]]}]

]] 

,[[B, B, F, F, B], [
 
[[-4], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[-1], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[{[a[1]-2]}, {[{[a[1]-2]}, {[3]}]}],
{[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[{[-1]}, {[-1]}], 
{[a[1] = 0, a[2] = 1, a[3] = 0, a[4] = 0]}]
,[[{[-1/2+a[1]]}, {[{[a[1]-1]}, {[{[a[1]-1]}, {[3]}]}]}], 
{[1 <= a[1], a[2] = 1, a[3] = 0, a[4] = 0]}]
,[[{[1/4]}, {[-1/4]}], 
{[a[1] = 0, a[2] = 2, a[3] = 0, a[4] = 0]}]
,[[{[{[2*a[1]]}, {[a[1]+1/2]}]}, {[{[{[a[1]]}, {[a[1]]}]}, {[a[1]]}]}], 
{[1 <= a[1], a[2] = 2, a[3] = 0, a[4] = 0]}]
,[[{[{[2*a[1]+a[2]-2]}, {[a[1]+1/2]}]}, 
{[{[{[{[2*a[1]+a[2]-3]}, {[a[1]+1]}]}, {[a[1]]}]}, {[a[1]]}]}], 
{[0 <= a[1], 3 <= a[2], a[3] = 0, a[4] = 0]}]
,[[-2], {[ a[1] = 0, a[2] = 0, a[3] = 0, 1 <= a[4]]}]
,[[a[1]-1], {[ 1 <= a[1], a[2] = 0, a[3] = 0, 1 <= a[4]]}]
,[[-1/2], {[ a[1] = 0, a[2] = 1, a[3] = 0, 1 <= a[4]]}]
,[[{[a[1]]}, {[a[1]]}], 
{[ 1 <= a[1], a[2] = 1, a[3] = 0, 1 <= a[4]]}]
,[[{[{[-2+2*a[1]+a[2]]}, {[1+a[1]]}]}, {[a[1]]}], 
{[ 0 <= a[1], 2 <= a[2], a[3] = 0, 1 <= a[4]]}]
,[[-1], {[a[1] = 0, a[2] = 0, a[3] = 1, a[4] = 0]}]
,[[-1/2+a[1]], {[1 <= a[1], a[2] = 0, a[3] = 1, a[4] = 0]}]
,[[{[2*a[1]+a[2]-1]}, {[a[1]+1/2]}], 
{[0 <= a[1], 1 <= a[2], a[3] = 1, a[4] = 0]}]
,[[-1], {[ a[1] = 0, a[2] = 0, a[3] = 1, 1 <= a[4]]}]
,[[a[1]], {[ 1 <= a[1], a[2] = 0, a[3] = 1, 1 <= a[4]]}]
,[[{[-1+2*a[1]+a[2]]}, {[1+a[1]]}], 
{[ 0 <= a[1], 1 <= a[2], a[3] = 1, 1 <= a[4]]}]
,[[2*a[1]+a[2]], {[0 <= a[1], 0 <= a[2], 2 <= a[3], 0 <= a[4]]}]

]] 

,[[B, F, B, F, B], [

[[-3], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 0]}] 
,[[{[-1]}, {[-1]}], 
{[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[{[a[1]-2]}, {[3]}], 
{[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[{[a[3]-2]}, {[a[3]-2]}], 
{[a[1] = 0, a[2] = 0, 1 <= a[3], a[4] = 0]}]
,[[a[1]+a[3]-1], 
{[1 <= a[1], a[2] = 0, 1 <= a[3], a[4] = 0]}]
,[[-1], {[a[1] = 0, a[2] = 1, a[3] = 0, a[4] = 0]}]
,[[{[a[1]-1]}, {[{[a[1]-1]}, {[3]}]}], 
{[1 <= a[1], a[2] = 1, a[3] = 0, a[4] = 0]}]
,[[-1/4], {[a[1] = 0, a[2] = 2, a[3] = 0, a[4] = 0]}]
,[[{[{[a[1]]}, {[a[1]]}]}, {[a[1]]}], 
{[1 <= a[1], a[2] = 2, a[3] = 0, a[4] = 0]}]
,[[{[{[{[2*a[1]+a[2]-3]}, {[a[1]+1]}]}, {[a[1]]}]}, {[a[1]]}],
{[0 <= a[1], 3 <= a[2], a[3] = 0, a[4] = 0]}]
,[[a[1]-1/2+a[3]], 
{[0 <= a[1], 1 <= a[2], 1 <= a[3], a[4] = 0]}]
,[[a[3]-1], 
{[a[1] = 0, a[2] = 0, 0 <= a[3], 1 <= a[4]]}]
,[[1/2], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 1]}]
,[[3/2], {[a[1] = 2, a[2] = 0, a[3] = 0, a[4] = 1]}]
,[[5/2], {[a[1] = 3, a[2] = 0, a[3] = 0, a[4] = 1]}]
,[[7/2], {[a[1] = 4, a[2] = 0, a[3] = 0, a[4] = 1]}]
,[[{[a[1]-1]}, {[5]}], 
{[5 <= a[1], a[2] = 0, a[3] = 0, a[4] = 1]}]
,[[a[1]+a[3]-1/2], 
{[1 <= a[1], a[2] = 0, 1 <= a[3], a[4] = 1], 
[1 <= a[1], a[2] = 0, 0 <= a[3], 2 <= a[4]]}]
,[[a[1]+a[3]], 
{[0 <= a[1], 1 <= a[2], 0 <= a[3], 1 <= a[4]]}]

]] 


,[[F, B, B, F, B], [

[[-2], {[a[1] = 0, a[2] = 0, a[3] = 0, a[4] = 0]}] 
,[[-1], {[a[1] = 1, a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[{[a[1]-1]}, {[a[1]-1]}], 
{[2 <= a[1], a[2] = 0, a[3] = 0, a[4] = 0]}]
,[[{[{[a[1]]}, {[a[1]]}]}, {[3]}], 
{[0 <= a[1], a[2] = 1, a[3] = 0, a[4] = 0]}]
,[[{[a[1]+2*a[2]-3]}, {[2*a[2]+1]}], 
{[0 <= a[1], 2 <= a[2], a[3] = 0, a[4] = 0]}]
,[[{[a[1]]}, {[a[1]]}], 
{[0 <= a[1], a[2] = 0, a[3] = 1, a[4] = 0]}]
,[[{[2*a[2]]}, {[2*a[2]]}], 
{[a[1] = 0, 1 <= a[2], a[3] = 1, a[4] = 0]}]
,[[{[1+2*a[2]]}, {[1+2*a[2]]}], 
{[a[1] = 1, 1 <= a[2], a[3] = 1, a[4] = 0]}]
,[[{[2+2*a[2]]}, {[2+2*a[2]]}], 
{[a[1] = 2, 1 <= a[2], a[3] = 1, a[4] = 0]}]
,[[{[2*a[2]+5/2]}, {[2*a[2]+5/2]}], 
{[a[1] = 3, 1 <= a[2], a[3] = 1, a[4] = 0]}]
,[[a[1]+2*a[2]-1], 
{[4 <= a[1], 1 <= a[2], a[3] = 1, a[4] = 0]}]
,[[{[a[1]+2*a[2]+a[3]-1]}, {[a[1]+2*a[2]+a[3]-1]}], 
{[0 <= a[1], 0 <= a[2], 2 <= a[3], a[4] = 0]}]
,[[a[1]], {[0 <= a[1], a[2] = 0, a[3] = 0, a[4] = 1]}]
,[[{[2*a[2]+a[1]-1]}, {[2*a[2]+3]}], 
{[0 <= a[1], 1 <= a[2], a[3] = 0, a[4] = 1]}]
,[[2*a[2]+a[1]+a[3]], 
{[0 <= a[1], 0 <= a[2], 1 <= a[3], a[4] = 1]}]
,[[2*a[2]+a[1]+a[3]], 
{[0 <= a[1], 0 <= a[2], 0 <= a[3], 2 <= a[4]]}]

]] 

,[[B, F, F, B, B], [
 
[[a[3]-2], {[a[1] = 0, a[2] = 0, 0 <= a[3]]}]
,[[{[0]}, {[-1/2]}], 
{[a[1] = 1, a[2] = 0, a[3] = 0]}]
,[[{[1]}, {[1]}], 
{[a[1] = 2, a[2] = 0, a[3] = 0]}]
,[[{[2]}, {[2]}], 
{[a[1] = 3, a[2] = 0, a[3] = 0]}]
,[[11/4], 
{[a[1] = 4, a[2] = 0, a[3] = 0]}]
,[[3], {[5 <= a[1], a[2] = 0, a[3] = 0]}]
,[[{[a[1]+a[3]-1]}, {[a[1]+a[3]-1]}], 
{[1 <= a[1], a[2] = 0, 1 <= a[3]]}]
,[[{[a[1]-1]}, {[3]}], 
{[0 <= a[1], a[2] = 1, a[3] = 0]}]
,[[a[1]+a[3]], {[0 <= a[1], a[2] = 1, 1 <= a[3]]}]
,[[a[1]+a[3]], 
{[0 <= a[1], 2 <= a[2], 0 <= a[3]]}]

]] 

,[[F, B, F, B, B], [

[[-1], {[a[1] = 0, a[2] = 0, a[3] = 0]}]
,[[-1/2], {[a[1] = 1, a[2] = 0, a[3] = 0]}]
,[[{[{[a[1]-1]}, {[a[1]-1]}]}, {[0]}], 
{[2 <= a[1], a[2] = 0, a[3] = 0]}]
,[[{[{[{[a[1]]}, {[a[1]]}]}, {[3]}]}, {[2]}], 
{[0 <= a[1], a[2] = 1, a[3] = 0]}]
,[[{[{[a[1]+2*a[2]-3]}, {[2*a[2]+1]}]}, {[2*a[2]]}], 
{[0 <= a[1], 2 <= a[2], a[3] = 0]}]
,[[{[{[a[1]]}, {[a[1]]}]}, {[3]}], 
{[0 <= a[1], a[2] = 0, a[3] = 1]}]
,[[{[a[1]+2*a[2]-1]}, {[2*a[2]+3]}], 
{[0 <= a[1], 1 <= a[2], a[3] = 1]}]
,[[a[1]+2*a[2]+a[3]-1], 
{[0 <= a[1], 0 <= a[2], 2 <= a[3]]}]

]] 

,[[F, F, B, B, B], [

[[2*a[2]], {[0 <= a[1], 0 <= a[2]]}]

]] 

];
end: