% File: lemmas.txt
%
% There are 4 lists of candidate lemmas (proved or conjectured):
%
%    Lemma List 1: JD supplied lemmas that he knows are true.
%    Lemma List 2: JD supplied lemmas that he believes are true.
%    Lemma List 3: Lemma List 2 with D replaced by R(C,xx,yy).
%    Lemma List 4: MK suggested lemmas.

% -------------------------------------------------------------------------
% Lemma List 1: JD supplied lemmas that he knows are true.
%
% Status as of 2014-aug-19: proved all 17 (lemmas1.{in,out,pf,xml})
% -------------------------------------------------------------------------

formulas(assumptions).

% C^3 is nuclear
a(C * (C * C),x,y) = 1 # label("Lemma 1-1").

a(x,y,C * (C * C)) = 1 # label("Lemma 1-2").
a(x,C * (C * C),y) = 1 # label("Lemma 1-3").

% C associates with cubes
a(C,x * (x * x),y) = 1 # label("Lemma 1-4").
a(C,x,y * (y * y)) = 1 # label("Lemma 1-5").
a(x,C,y * (y * y)) = 1 # label("Lemma 1-6").
a(x * (x * x),C,y) = 1 # label("Lemma 1-7").
a(x * (x * x),y,C) = 1 # label("Lemma 1-8").
a(x,y * (y * y),C) = 1 # label("Lemma 1-9").

% associators with C in an argument cube to zero
a(C,x,y) * (a(C,x,y) * a(C,x,y)) = 1 # label("Lemma 1-10").
a(x,y,C) * (a(x,y,C) * a(x,y,C)) = 1 # label("Lemma 1-11").
a(x,C,y) * (a(x,C,y) * a(x,C,y)) = 1 # label("Lemma 1-12").

% CR(x,y)^3 = C, xR(C,y)^3 = x, xR(y,C)^3 = x
R(R(R(C,x,y),x,y),x,y) = C # label("Lemma 1-13").
R(R(R(x,C,y),C,y),C,y) = x # label("Lemma 1-14").
R(R(R(x,y,C),y,C),y,C) = x # label("Lemma 1-15").

% R(C,y) and R(y,C) are automorphisms
R(u * v,C,y) = R(u,C,y) * R(v,C,y) # label("Lemma 1-16").
R(u * v,y,C) = R(u,y,C) * R(v,y,C) # label("Lemma 1-17").

end_of_list.

% -------------------------------------------------------------------------
% Lemma List 2: JD supplied lemmas that he believes are true.
%
% Status as of 2014-aug-21: proved Normal 2 => all 37
%    {lemmas2.{in,out,pf,xml})
% -------------------------------------------------------------------------

formulas(goals).

% D associates with cubes
a(D,x * (x * x),y) = 1 # label("Lemma 2-1").
a(D,x,y * (y * y)) = 1 # label("Lemma 2-2").
a(x,D,y * (y * y)) = 1 # label("Lemma 2-3").
a(x * (x * x),D,y) = 1 # label("Lemma 2-4").
a(x * (x * x),y,D) = 1 # label("Lemma 2-5").
a(x,y * (y * y),D) = 1 # label("Lemma 2-6").

% associators with D in an argument cube to zero
a(D,x,y) * (a(D,x,y) * a(D,x,y)) = 1 # label("Lemma 2-7").
a(x,y,D) * (a(x,y,D) * a(x,y,D)) = 1 # label("Lemma 2-8").
a(x,D,y) * (a(x,D,y) * a(x,D,y)) = 1 # label("Lemma 2-9").

% DR(x,y)^3 = D, xR(D,y)^3 = x, xR(y,D)^3 = x
R(R(R(D,x,y),x,y),x,y) = D # label("Lemma 2-10").
R(R(R(x,D,y),D,y),D,y) = x # label("Lemma 2-11").
R(R(R(x,y,D),y,D),y,D) = x # label("Lemma 2-12").

% R(D,y) and R(y,D) are automorphisms
R(u * v,D,y) = R(u,D,y) * R(v,D,y) # label("Lemma 2-13").
R(u * v,y,D) = R(u,y,D) * R(v,y,D) # label("Lemma 2-14").

% associator identities involving D
a(D,x',y) = a(x',y,D) # label("Lemma 2-15").
a(D,x',y) = a(D',y,x') # label("Lemma 2-16").
a(D,x',y) = a(y,D,x') # label("Lemma 2-17").
a(D,x',y) = a(x',D,y') # label("Lemma 2-18").
a(D,x',y) = a(D',x,y) # label("Lemma 2-19").
a(D,x',y) = a(D',x',y') # label("Lemma 2-20").
a(D,x',y) = a(y',x',D) # label("Lemma 2-21").
a(D,x',y) = a(D,y',x') # label("Lemma 2-22").
a(D,x',y) = a(D,x,y') # label("Lemma 2-23").
a(D,x',y) = a(x,y',D) # label("Lemma 2-24").
a(D,x',y) = a(D',y',x) # label("Lemma 2-25").
a(D,x',y) = a(y',D,x) # label("Lemma 2-26").
a(D,x',y) = a(y,D',x) # label("Lemma 2-27").
a(D,x',y) = a(x,D',y') # label("Lemma 2-28, 2-36").
a(D,x',y) = a(y',D',x') # label("Lemma 2-29").
a(D,x',y) = a(x',D',y) # label("Lemma 2-30").
a(D,x',y) = a(x,y,D') # label("Lemma 2-31").
a(D,x',y) = a(y,x',D') # label("Lemma 2-32").
a(D,x',y) = a(y',x,D') # label("Lemma 2-33").
a(D,x',y) = a(x',y',D') # label("Lemma 2-34").
a(D,x',y) = a(D,y',x') # label("Lemma 2-35").
% a(D,x',y) = a(x,D',y') # label("Lemma 2-36").
a(D,x',y) = a(D',y,x') # label("Lemma 2-37").

end_of_list.

% -------------------------------------------------------------------------
% Lemma List 3: Lemma List 2 with D replaced by R(C,xx,yy).
% (Suggested by MK.)
%
% Note that I've replaced multiple occurrences of D in a clause
% with the *same* R(C,xx,yy).  We can also look at versions with
% distinct {xx,yy} for each occurrence of D in a clause.
%
% Status as of 2014-aug-16: starting over with these
% -------------------------------------------------------------------------

formulas(goals).

% D associates with cubes
a(R(C,xx,yy),x * (x * x),y) = 1 # label("Lemma 3-1").
a(R(C,xx,yy),x,y * (y * y)) = 1 # label("Lemma 3-2").
a(x,R(C,xx,yy),y * (y * y)) = 1 # label("Lemma 3-3").
a(x * (x * x),R(C,xx,yy),y) = 1 # label("Lemma 3-4").
a(x * (x * x),y,R(C,xx,yy)) = 1 # label("Lemma 3-5").
a(x,y * (y * y),R(C,xx,yy)) = 1 # label("Lemma 3-6").

% associators with D in an argument cube to zero
a(R(C,xx,yy),x,y) * (a(R(C,xx,yy),x,y) * a(R(C,xx,yy),x,y)) = 1 # label("Lemma 3-7").
a(x,y,R(C,xx,yy)) * (a(x,y,R(C,xx,yy)) * a(x,y,R(C,xx,yy))) = 1 # label("Lemma 3-8").
a(x,R(C,xx,yy),y) * (a(x,R(C,xx,yy),y) * a(x,R(C,xx,yy),y)) = 1 # label("Lemma 3-9").

% DR(x,y)^3 = D, xR(D,y)^3 = x, xR(y,D)^3 = x
R(R(R(R(C,xx,yy),x,y),x,y),x,y) = R(C,xx,yy) # label("Lemma 3-10").
R(R(R(x,R(C,xx,yy),y),R(C,xx,yy),y),R(C,xx,yy),y) = x # label("Lemma 3-11").
R(R(R(x,y,R(C,xx,yy)),y,R(C,xx,yy)),y,R(C,xx,yy)) = x # label("Lemma 3-12").

% R(D,y) and R(y,D) are automorphisms
R(u * v,R(C,xx,yy),y) = R(u,R(C,xx,yy),y) * R(v,R(C,xx,yy),y) # label("Lemma 3-13").
R(u * v,y,R(C,xx,yy)) = R(u,y,R(C,xx,yy)) * R(v,y,R(C,xx,yy)) # label("Lemma 3-14").

% associator identities involving D
a(R(C,xx,yy),x',y) = a(x',y,R(C,xx,yy)) # label("Lemma 3-15").
a(R(C,xx,yy),x',y) = a(R(C,xx,yy)',y,x') # label("Lemma 3-16").
a(R(C,xx,yy),x',y) = a(y,R(C,xx,yy),x') # label("Lemma 3-17").
a(R(C,xx,yy),x',y) = a(x',R(C,xx,yy),y') # label("Lemma 3-18").
a(R(C,xx,yy),x',y) = a(R(C,xx,yy)',x,y) # label("Lemma 3-19").
a(R(C,xx,yy),x',y) = a(R(C,xx,yy)',x',y') # label("Lemma 3-20").
a(R(C,xx,yy),x',y) = a(y',x',R(C,xx,yy)) # label("Lemma 3-21").
a(R(C,xx,yy),x',y) = a(R(C,xx,yy),y',x') # label("Lemma 3-22").
a(R(C,xx,yy),x',y) = a(R(C,xx,yy),x,y') # label("Lemma 3-23").
a(R(C,xx,yy),x',y) = a(x,y',R(C,xx,yy)) # label("Lemma 3-24").
a(R(C,xx,yy),x',y) = a(R(C,xx,yy)',y',x) # label("Lemma 3-25").
a(R(C,xx,yy),x',y) = a(y',R(C,xx,yy),x) # label("Lemma 3-26").
a(R(C,xx,yy),x',y) = a(y,R(C,xx,yy)',x) # label("Lemma 3-27").
a(R(C,xx,yy),x',y) = a(x,R(C,xx,yy)',y') # label("Lemma 3-28").
a(R(C,xx,yy),x',y) = a(y',R(C,xx,yy)',x') # label("Lemma 3-29").
a(R(C,xx,yy),x',y) = a(x',R(C,xx,yy)',y) # label("Lemma 3-30").
a(R(C,xx,yy),x',y) = a(x,y,R(C,xx,yy)') # label("Lemma 3-31").
a(R(C,xx,yy),x',y) = a(y,x',R(C,xx,yy)') # label("Lemma 3-32").
a(R(C,xx,yy),x',y) = a(y',x,R(C,xx,yy)') # label("Lemma 3-33").
a(R(C,xx,yy),x',y) = a(x',y',R(C,xx,yy)') # label("Lemma 3-34").
a(R(C,xx,yy),x',y) = a(R(C,xx,yy),y',x') # label("Lemma 3-35").
a(R(C,xx,yy),x',y) = a(x,R(C,xx,yy)',y') # label("Lemma 3-36").
a(R(C,xx,yy),x',y) = a(R(C,xx,yy)',y,x') # label("Lemma 3-37").

end_of_list.

% -------------------------------------------------------------------------
% Lemma List 4: MK suggested lemmas.
%
% Status as of 2014-aug-22:  proved all but Lemmas 4-3 and 4-4
% -------------------------------------------------------------------------

formulas(goals).

R(x,C,y) * R(z,C,y) = R(x * z,C,y) # label("Lemma 4-1").
R(x,y,C) * R(z,y,C) = R(x * z,y,C) # label("Lemma 4-2").
R(x,R(C,y,z),u) * R(w,R(C,y,z),u) = R(x * w,R(C,y,z),u) # label("Lemma 4-3").
R(x,u,R(C,y,z)) * R(w,u,R(C,y,z)) = R(x * w,u,R(C,y,z)) # label("Lemma 4-4").

K(R(C,x,y) * R(C,y,x),z) = 1 # label("Lemma 4-5").

R(C,x * x,y) = R(C,y,x) # label("Lemma 4-6").
R(R(C,x,y),x * x,y) = C # label("Lemma 4-7").
R(R(C,y,x),x * x,y) = R(C,x,y) # label("Lemma 4-8").

R(C,x,y * y) = R(C,y,x) # label("Lemma 4-9").
R(R(C,y,x),x,y * y) = R(C,x,y) # label("Lemma 4-10").
R(R(C,x,y),x,y * y) = C # label("Lemma 4-11").

R(C,x * x,y') = R(C,x,y) # label("Lemma 4-12").
R(R(C,x,y),x * x,y') = R(C,y,x) # label("Lemma 4-13").
R(R(C,y,x),x * x,y') = C # label("Lemma 4-14").

R(R(C,x,y),y * y,x') = C # label("Lemma 4-15").
R(R(C,y,x),y * y,R(C,y,x) * x) = C # label("Lemma 4-16").

end_of_list.