:: BOOLEALG semantic presentation

K87() is set
K19(K87()) is set
1 is set

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(L,Y,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)

the U1 of L is set

the U1 of L is set

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
Z is M2( the U1 of L)
X "/\" (X "\/" Y) is M2( the U1 of L)
X "/\" Z is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
Z is M2( the U1 of L)
X "\/" Z is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
(L,X,Z) is M2( the U1 of L)
Z ` is M2( the U1 of L)
X "/\" (Z `) is M2( the U1 of L)
Y "/\" (Z `) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
Z is M2( the U1 of L)
(L,Y,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
Y "\/" Z is M2( the U1 of L)
S1 is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
Y "/\" Z is M2( the U1 of L)
S1 is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
Bottom L is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
X is M2( the U1 of L)
X "/\" X is M2( the U1 of L)

the U1 of L is set
Z is M2( the U1 of L)
S1 is M2( the U1 of L)
Z is M2( the U1 of L)
S1 is M2( the U1 of L)
(L,Z,S1) is M2( the U1 of L)
(L,Z,S1) is M2( the U1 of L)
S1 ` is M2( the U1 of L)
Z "/\" (S1 `) is M2( the U1 of L)
(L,S1,Z) is M2( the U1 of L)
Z ` is M2( the U1 of L)
S1 "/\" (Z `) is M2( the U1 of L)
(L,Z,S1) "\/" (L,S1,Z) is M2( the U1 of L)
(L,S1,Z) is M2( the U1 of L)
(L,S1,Z) "\/" (L,Z,S1) is M2( the U1 of L)
Z is M2( the U1 of L)
S1 is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
Z is M2( the U1 of L)
X "/\" Z is M2( the U1 of L)
(X "/\" Y) "\/" (X "/\" Z) is M2( the U1 of L)
Y "\/" Z is M2( the U1 of L)
X "/\" (Y "\/" Z) is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
X is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
Y "/\" Z is M2( the U1 of L)
Bottom L is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
Y "/\" Z is M2( the U1 of L)
Bottom L is M2( the U1 of L)
X "/\" Z is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
Bottom L is M2( the U1 of L)
X "/\" Z is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
Y "/\" Z is M2( the U1 of L)
X "/\" (Y "/\" Z) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
X "/\" Z is M2( the U1 of L)
(X "/\" Z) "/\" Y is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(X "/\" Y) "/\" Z is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
(L,Y,Z) is M2( the U1 of L)
Z ` is M2( the U1 of L)
Y "/\" (Z `) is M2( the U1 of L)
X "/\" (L,Y,Z) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(X "/\" Y) "/\" (Z `) is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
X is M2( the U1 of L)
X "/\" () is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
Y "/\" Z is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
Y "/\" Z is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
Z "/\" X is M2( the U1 of L)
Z "/\" Y is M2( the U1 of L)
(Z "/\" X) "/\" (Z "/\" Y) is M2( the U1 of L)
Y "/\" Z is M2( the U1 of L)
X "/\" (Y "/\" Z) is M2( the U1 of L)
Z "/\" (X "/\" (Y "/\" Z)) is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(X "/\" Y) "/\" Z is M2( the U1 of L)
Z "/\" ((X "/\" Y) "/\" Z) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
Z "/\" () is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
Z is M2( the U1 of L)
Y "\/" Z is M2( the U1 of L)
Y "\/" (X "/\" (Y `)) is M2( the U1 of L)
Y "\/" X is M2( the U1 of L)
Y "\/" (Y `) is M2( the U1 of L)
(Y "\/" X) "/\" (Y "\/" (Y `)) is M2( the U1 of L)
Top L is M2( the U1 of L)
(Y "\/" X) "/\" (Top L) is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
(L,Z,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
Z "/\" (Y `) is M2( the U1 of L)
(L,Z,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
Z "/\" (X `) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
(L,Y,Z) is M2( the U1 of L)
Z ` is M2( the U1 of L)
Y "/\" (Z `) is M2( the U1 of L)
S1 is M2( the U1 of L)
(L,X,S1) is M2( the U1 of L)
S1 ` is M2( the U1 of L)
X "/\" (S1 `) is M2( the U1 of L)
(L,Y,S1) is M2( the U1 of L)
Y "/\" (S1 `) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
Z is M2( the U1 of L)
Y "\/" Z is M2( the U1 of L)
(Y "\/" Z) "/\" (Y `) is M2( the U1 of L)
Y "/\" (Y `) is M2( the U1 of L)
Z "/\" (Y `) is M2( the U1 of L)
(Y "/\" (Y `)) "\/" (Z "/\" (Y `)) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "\/" (Z "/\" (Y `)) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
X ` is M2( the U1 of L)
Y is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(X "/\" Y) ` is M2( the U1 of L)
Y ` is M2( the U1 of L)
(X `) "\/" (Y `) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
X ` is M2( the U1 of L)
Y is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
(X "\/" Y) ` is M2( the U1 of L)
Y ` is M2( the U1 of L)
(X `) "/\" (Y `) is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,Y,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
X "/\" (Y "/\" (X `)) is M2( the U1 of L)
(X `) "/\" X is M2( the U1 of L)
Y "/\" ((X `) "/\" X) is M2( the U1 of L)
Y "/\" () is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,Y,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
X "\/" (L,Y,X) is M2( the U1 of L)
Top L is M2( the U1 of L)
Y "/\" (Top L) is M2( the U1 of L)
X "\/" (X `) is M2( the U1 of L)
Y "/\" (X "\/" (X `)) is M2( the U1 of L)
Y "/\" X is M2( the U1 of L)
(Y "/\" X) "\/" (Y "/\" (X `)) is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(Y `) ` is M2( the U1 of L)
(Y `) "/\" Y is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
Y "\/" Z is M2( the U1 of L)
X "/\" Z is M2( the U1 of L)
X "/\" (Y "\/" Z) is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(X "/\" Y) "\/" () is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(L,X,Y) "\/" Y is M2( the U1 of L)
Top L is M2( the U1 of L)
(X "\/" Y) "/\" (Top L) is M2( the U1 of L)
(Y `) "\/" Y is M2( the U1 of L)
(X "\/" Y) "/\" ((Y `) "\/" Y) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
(L,X,(X "\/" Y)) is M2( the U1 of L)
(X "\/" Y) ` is M2( the U1 of L)
X "/\" ((X "\/" Y) `) is M2( the U1 of L)
Bottom L is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(L,X,(X "/\" Y)) is M2( the U1 of L)
(X "/\" Y) ` is M2( the U1 of L)
X "/\" ((X "/\" Y) `) is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
X ` is M2( the U1 of L)
(X `) "\/" (Y `) is M2( the U1 of L)
X "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)
X "/\" (X `) is M2( the U1 of L)
(X "/\" (X `)) "\/" (X "/\" (Y `)) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "\/" (X "/\" (Y `)) is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(L,X,Y) "/\" Y is M2( the U1 of L)
(Y `) "/\" Y is M2( the U1 of L)
X "/\" ((Y `) "/\" Y) is M2( the U1 of L)
X "/\" () is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,Y,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
X "\/" (L,Y,X) is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
X "\/" (X `) is M2( the U1 of L)
(X "\/" Y) "/\" (X "\/" (X `)) is M2( the U1 of L)
Top L is M2( the U1 of L)
(X "\/" Y) "/\" (Top L) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(X "/\" Y) "\/" (L,X,Y) is M2( the U1 of L)
(X "/\" Y) "\/" X is M2( the U1 of L)
(X "/\" Y) "\/" (Y `) is M2( the U1 of L)
((X "/\" Y) "\/" X) "/\" ((X "/\" Y) "\/" (Y `)) is M2( the U1 of L)
X "/\" ((X "/\" Y) "\/" (Y `)) is M2( the U1 of L)
X "\/" (Y `) is M2( the U1 of L)
Y "\/" (Y `) is M2( the U1 of L)
(X "\/" (Y `)) "/\" (Y "\/" (Y `)) is M2( the U1 of L)
X "/\" ((X "\/" (Y `)) "/\" (Y "\/" (Y `))) is M2( the U1 of L)
Top L is M2( the U1 of L)
(X "\/" (Y `)) "/\" (Top L) is M2( the U1 of L)
X "/\" ((X "\/" (Y `)) "/\" (Top L)) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
Z is M2( the U1 of L)
(L,Y,Z) is M2( the U1 of L)
Z ` is M2( the U1 of L)
Y "/\" (Z `) is M2( the U1 of L)
(L,X,(L,Y,Z)) is M2( the U1 of L)
(L,Y,Z) ` is M2( the U1 of L)
X "/\" ((L,Y,Z) `) is M2( the U1 of L)
X "/\" Z is M2( the U1 of L)
(L,X,Y) "\/" (X "/\" Z) is M2( the U1 of L)
(Z `) ` is M2( the U1 of L)
(Y `) "\/" ((Z `) `) is M2( the U1 of L)
X "/\" ((Y `) "\/" ((Z `) `)) is M2( the U1 of L)
(Y `) "\/" Z is M2( the U1 of L)
X "/\" ((Y `) "\/" Z) is M2( the U1 of L)
(X "/\" (Y `)) "\/" (X "/\" Z) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(L,X,(L,X,Y)) is M2( the U1 of L)
(L,X,Y) ` is M2( the U1 of L)
X "/\" ((L,X,Y) `) is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
X ` is M2( the U1 of L)
(Y `) ` is M2( the U1 of L)
(X `) "\/" ((Y `) `) is M2( the U1 of L)
X "/\" ((X `) "\/" ((Y `) `)) is M2( the U1 of L)
(X `) "\/" Y is M2( the U1 of L)
X "/\" ((X `) "\/" Y) is M2( the U1 of L)
X "/\" (X `) is M2( the U1 of L)
(X "/\" (X `)) "\/" (X "/\" Y) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "\/" (X "/\" Y) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
(L,(X "\/" Y),Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
(X "\/" Y) "/\" (Y `) is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
Y "/\" (Y `) is M2( the U1 of L)
(X "/\" (Y `)) "\/" (Y "/\" (Y `)) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
(X "/\" (Y `)) "\/" () is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
X "/\" X is M2( the U1 of L)
X ` is M2( the U1 of L)
(Y `) ` is M2( the U1 of L)
(X `) "\/" ((Y `) `) is M2( the U1 of L)
(X `) "\/" Y is M2( the U1 of L)
X "/\" ((X `) "\/" Y) is M2( the U1 of L)
X "/\" (X `) is M2( the U1 of L)
(X "/\" (X `)) "\/" (X "/\" Y) is M2( the U1 of L)
() "\/" (X "/\" Y) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
Z is M2( the U1 of L)
Y "\/" Z is M2( the U1 of L)
(L,X,(Y "\/" Z)) is M2( the U1 of L)
(Y "\/" Z) ` is M2( the U1 of L)
X "/\" ((Y "\/" Z) `) is M2( the U1 of L)
(L,X,Z) is M2( the U1 of L)
Z ` is M2( the U1 of L)
X "/\" (Z `) is M2( the U1 of L)
(L,X,Y) "/\" (L,X,Z) is M2( the U1 of L)
(Y `) "/\" (Z `) is M2( the U1 of L)
X "/\" ((Y `) "/\" (Z `)) is M2( the U1 of L)
X "/\" X is M2( the U1 of L)
(X "/\" X) "/\" (Y `) is M2( the U1 of L)
((X "/\" X) "/\" (Y `)) "/\" (Z `) is M2( the U1 of L)
X "/\" (X "/\" (Y `)) is M2( the U1 of L)
(X "/\" (X "/\" (Y `))) "/\" (Z `) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
Z is M2( the U1 of L)
Y "/\" Z is M2( the U1 of L)
(L,X,(Y "/\" Z)) is M2( the U1 of L)
(Y "/\" Z) ` is M2( the U1 of L)
X "/\" ((Y "/\" Z) `) is M2( the U1 of L)
(L,X,Z) is M2( the U1 of L)
Z ` is M2( the U1 of L)
X "/\" (Z `) is M2( the U1 of L)
(L,X,Y) "\/" (L,X,Z) is M2( the U1 of L)
(Y `) "\/" (Z `) is M2( the U1 of L)
X "/\" ((Y `) "\/" (Z `)) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
Z is M2( the U1 of L)
(L,Y,Z) is M2( the U1 of L)
Z ` is M2( the U1 of L)
Y "/\" (Z `) is M2( the U1 of L)
X "/\" (L,Y,Z) is M2( the U1 of L)
X "/\" Z is M2( the U1 of L)
(L,(X "/\" Y),(X "/\" Z)) is M2( the U1 of L)
(X "/\" Z) ` is M2( the U1 of L)
(X "/\" Y) "/\" ((X "/\" Z) `) is M2( the U1 of L)
(L,(X "/\" Y),X) is M2( the U1 of L)
X ` is M2( the U1 of L)
(X "/\" Y) "/\" (X `) is M2( the U1 of L)
(L,(X "/\" Y),Z) is M2( the U1 of L)
(X "/\" Y) "/\" (Z `) is M2( the U1 of L)
(L,(X "/\" Y),X) "\/" (L,(X "/\" Y),Z) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "\/" (L,(X "/\" Y),Z) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(L,(X "\/" Y),(X "/\" Y)) is M2( the U1 of L)
(X "/\" Y) ` is M2( the U1 of L)
(X "\/" Y) "/\" ((X "/\" Y) `) is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(L,Y,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)
(X `) "\/" (Y `) is M2( the U1 of L)
(X "\/" Y) "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)
(X "\/" Y) "/\" (X `) is M2( the U1 of L)
(X "\/" Y) "/\" (Y `) is M2( the U1 of L)
((X "\/" Y) "/\" (X `)) "\/" ((X "\/" Y) "/\" (Y `)) is M2( the U1 of L)
X "/\" (X `) is M2( the U1 of L)
(X "/\" (X `)) "\/" (Y "/\" (X `)) is M2( the U1 of L)
((X "/\" (X `)) "\/" (Y "/\" (X `))) "\/" ((X "\/" Y) "/\" (Y `)) is M2( the U1 of L)
Y "/\" (Y `) is M2( the U1 of L)
(X "/\" (Y `)) "\/" (Y "/\" (Y `)) is M2( the U1 of L)
((X "/\" (X `)) "\/" (Y "/\" (X `))) "\/" ((X "/\" (Y `)) "\/" (Y "/\" (Y `))) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "\/" (Y "/\" (X `)) is M2( the U1 of L)
(() "\/" (Y "/\" (X `))) "\/" ((X "/\" (Y `)) "\/" (Y "/\" (Y `))) is M2( the U1 of L)
(X "/\" (Y `)) "\/" () is M2( the U1 of L)
(Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" ()) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
Z is M2( the U1 of L)
(L,(L,X,Y),Z) is M2( the U1 of L)
Z ` is M2( the U1 of L)
(L,X,Y) "/\" (Z `) is M2( the U1 of L)
Y "\/" Z is M2( the U1 of L)
(L,X,(Y "\/" Z)) is M2( the U1 of L)
(Y "\/" Z) ` is M2( the U1 of L)
X "/\" ((Y "\/" Z) `) is M2( the U1 of L)
(Y `) "/\" (Z `) is M2( the U1 of L)
X "/\" ((Y `) "/\" (Z `)) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(L,Y,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
(X "/\" (Y `)) "/\" X is M2( the U1 of L)
(X `) "/\" X is M2( the U1 of L)
Y "/\" ((X `) "/\" X) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
Y "/\" () is M2( the U1 of L)
X "/\" X is M2( the U1 of L)
(X "/\" X) "/\" (Y `) is M2( the U1 of L)
(X "/\" (Y `)) "\/" (X `) is M2( the U1 of L)
X "/\" (X `) is M2( the U1 of L)
(X "/\" (X `)) "\/" (X `) is M2( the U1 of L)
X "\/" (X `) is M2( the U1 of L)
(Y `) "\/" (X `) is M2( the U1 of L)
(X "\/" (X `)) "/\" ((Y `) "\/" (X `)) is M2( the U1 of L)
Top L is M2( the U1 of L)
(Top L) "/\" ((Y `) "\/" (X `)) is M2( the U1 of L)
(Y `) "/\" (X `) is M2( the U1 of L)
(X `) ` is M2( the U1 of L)
(Y `) ` is M2( the U1 of L)
(Y `) "/\" Y is M2( the U1 of L)
X "/\" ((Y `) "/\" Y) is M2( the U1 of L)
(Y "/\" (X `)) "/\" Y is M2( the U1 of L)
X "/\" () is M2( the U1 of L)
Y "/\" Y is M2( the U1 of L)
(X `) "/\" (Y "/\" Y) is M2( the U1 of L)
(X `) "/\" Y is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
X is M2( the U1 of L)
(L,X,()) is M2( the U1 of L)
() ` is M2( the U1 of L)
X "/\" (() `) is M2( the U1 of L)
Top L is M2( the U1 of L)
X "/\" (Top L) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
X ` is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(L,X,Y) ` is M2( the U1 of L)
(X `) "\/" Y is M2( the U1 of L)
(Y `) ` is M2( the U1 of L)
(X `) "\/" ((Y `) `) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
Y "\/" Z is M2( the U1 of L)
X "/\" (Y "\/" Z) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
X "/\" Z is M2( the U1 of L)
(X "/\" Y) "\/" (X "/\" Z) is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
X "/\" Z is M2( the U1 of L)
(X "/\" Y) "\/" (X "/\" Z) is M2( the U1 of L)
X "/\" (Y "\/" Z) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
X "/\" Z is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(X "/\" Z) "\/" (X "/\" Y) is M2( the U1 of L)
X "/\" (Y "\/" Z) is M2( the U1 of L)
Bottom L is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(X "/\" Y) "/\" (L,X,Y) is M2( the U1 of L)
(X "/\" Y) "/\" (Y `) is M2( the U1 of L)
((X "/\" Y) "/\" (Y `)) "/\" X is M2( the U1 of L)
Y "/\" (Y `) is M2( the U1 of L)
X "/\" (Y "/\" (Y `)) is M2( the U1 of L)
(X "/\" (Y "/\" (Y `))) "/\" X is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "/\" X is M2( the U1 of L)

the U1 of L is set

the U1 of S1 is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
Z is M2( the U1 of L)
Y "\/" Z is M2( the U1 of L)
S2 is M2( the U1 of S1)
S3 is M2( the U1 of S1)
S4 is M2( the U1 of S1)
S3 "\/" S4 is M2( the U1 of S1)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(L,X,Y) "/\" Y is M2( the U1 of L)
(Y `) "/\" Y is M2( the U1 of L)
X "/\" ((Y `) "/\" Y) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
X "/\" () is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
(L,(X "\/" Y),Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
(X "\/" Y) "/\" (Y `) is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
Bottom L is M2( the U1 of L)
X ` is M2( the U1 of L)
(X `) "\/" (X "/\" Y) is M2( the U1 of L)
(X `) "\/" X is M2( the U1 of L)
(X `) "\/" Y is M2( the U1 of L)
((X `) "\/" X) "/\" ((X `) "\/" Y) is M2( the U1 of L)
Top L is M2( the U1 of L)
(Top L) "/\" ((X `) "\/" Y) is M2( the U1 of L)
((X `) "\/" Y) ` is M2( the U1 of L)
(X `) ` is M2( the U1 of L)
((X `) `) "/\" (Y `) is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
Y "/\" (Y `) is M2( the U1 of L)
(X "/\" (Y `)) "\/" (Y "/\" (Y `)) is M2( the U1 of L)
(X "/\" (Y `)) "\/" () is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
X ` is M2( the U1 of L)
Y is M2( the U1 of L)
Y ` is M2( the U1 of L)
(X `) "\/" (Y `) is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
X "/\" (X `) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
Y "/\" (Y `) is M2( the U1 of L)
(Y `) "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)
(Y `) "/\" X is M2( the U1 of L)
((Y `) "/\" X) "\/" () is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
(Y "/\" (X `)) "\/" (Y "/\" (Y `)) is M2( the U1 of L)
Y "/\" (X "\/" Y) is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(X "/\" (X `)) "\/" (X "/\" (Y `)) is M2( the U1 of L)
X "/\" (X "\/" Y) is M2( the U1 of L)
(X `) "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)
(X `) "/\" Y is M2( the U1 of L)
() "\/" ((X `) "/\" Y) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
X ` is M2( the U1 of L)
Y is M2( the U1 of L)
Y ` is M2( the U1 of L)
(X `) "\/" (Y `) is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
X "\/" (X `) is M2( the U1 of L)
(X "\/" Y) "/\" (X "\/" (X `)) is M2( the U1 of L)
X "\/" () is M2( the U1 of L)
Top L is M2( the U1 of L)
(X "\/" Y) "/\" (Top L) is M2( the U1 of L)
Y "/\" X is M2( the U1 of L)
(Y "/\" X) ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
Y "\/" X is M2( the U1 of L)
Y "\/" (Y `) is M2( the U1 of L)
(Y "\/" X) "/\" (Y "\/" (Y `)) is M2( the U1 of L)
Y "\/" () is M2( the U1 of L)
(Y "\/" X) "/\" (Top L) is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(X "/\" Y) ` is M2( the U1 of L)
(Y `) "\/" Y is M2( the U1 of L)
(Y `) "\/" (X `) is M2( the U1 of L)
((Y `) "\/" Y) "/\" ((Y `) "\/" (X `)) is M2( the U1 of L)
(Y `) "\/" () is M2( the U1 of L)
(Top L) "/\" ((Y `) "\/" (X `)) is M2( the U1 of L)
(X `) "/\" (Y `) is M2( the U1 of L)
((X `) "/\" (Y `)) ` is M2( the U1 of L)
(X `) ` is M2( the U1 of L)
(Y `) ` is M2( the U1 of L)
((X `) `) "\/" ((Y `) `) is M2( the U1 of L)
X "\/" ((Y `) `) is M2( the U1 of L)
(X `) "\/" X is M2( the U1 of L)
((X `) "\/" X) "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)
(X `) "\/" () is M2( the U1 of L)
(Top L) "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)
(Y `) "/\" (X `) is M2( the U1 of L)
((Y `) "/\" (X `)) ` is M2( the U1 of L)
((Y `) `) "\/" ((X `) `) is M2( the U1 of L)
((Y `) `) "\/" X is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
X is M2( the U1 of L)
(L,X,()) is M2( the U1 of L)
(L,X,()) is M2( the U1 of L)
() ` is M2( the U1 of L)
X "/\" (() `) is M2( the U1 of L)
(L,(),X) is M2( the U1 of L)
X ` is M2( the U1 of L)
() "/\" (X `) is M2( the U1 of L)
(L,X,()) "\/" (L,(),X) is M2( the U1 of L)
X "\/" () is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
(L,X,X) is M2( the U1 of L)
(L,X,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
X "/\" (X `) is M2( the U1 of L)
(L,X,X) "\/" (L,X,X) is M2( the U1 of L)
Bottom L is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(L,Y,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
(L,Y,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
(L,X,(L,Y,X)) is M2( the U1 of L)
(L,X,(L,Y,X)) is M2( the U1 of L)
(L,Y,X) ` is M2( the U1 of L)
X "/\" ((L,Y,X) `) is M2( the U1 of L)
(L,(L,Y,X),X) is M2( the U1 of L)
(L,Y,X) "/\" (X `) is M2( the U1 of L)
(L,X,(L,Y,X)) "\/" (L,(L,Y,X),X) is M2( the U1 of L)
Top L is M2( the U1 of L)
(X "\/" Y) "/\" (Top L) is M2( the U1 of L)
X "\/" (X `) is M2( the U1 of L)
(X "\/" Y) "/\" (X "\/" (X `)) is M2( the U1 of L)
X "\/" (Y "/\" (X `)) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
X "/\" X is M2( the U1 of L)
(X "/\" (Y `)) "\/" (X "/\" X) is M2( the U1 of L)
((X "/\" (Y `)) "\/" (X "/\" X)) "\/" (Y "/\" (X `)) is M2( the U1 of L)
(X `) ` is M2( the U1 of L)
X "/\" ((X `) `) is M2( the U1 of L)
(X "/\" (Y `)) "\/" (X "/\" ((X `) `)) is M2( the U1 of L)
(X `) "/\" (X `) is M2( the U1 of L)
Y "/\" ((X `) "/\" (X `)) is M2( the U1 of L)
((X "/\" (Y `)) "\/" (X "/\" ((X `) `))) "\/" (Y "/\" ((X `) "/\" (X `))) is M2( the U1 of L)
(Y `) "\/" ((X `) `) is M2( the U1 of L)
X "/\" ((Y `) "\/" ((X `) `)) is M2( the U1 of L)
(X "/\" ((Y `) "\/" ((X `) `))) "\/" (Y "/\" ((X `) "/\" (X `))) is M2( the U1 of L)
(Y "/\" (X `)) ` is M2( the U1 of L)
X "/\" ((Y "/\" (X `)) `) is M2( the U1 of L)
(X "/\" ((Y "/\" (X `)) `)) "\/" (Y "/\" ((X `) "/\" (X `))) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(L,X,(X "/\" Y)) is M2( the U1 of L)
(L,X,(X "/\" Y)) is M2( the U1 of L)
(X "/\" Y) ` is M2( the U1 of L)
X "/\" ((X "/\" Y) `) is M2( the U1 of L)
(L,(X "/\" Y),X) is M2( the U1 of L)
X ` is M2( the U1 of L)
(X "/\" Y) "/\" (X `) is M2( the U1 of L)
(L,X,(X "/\" Y)) "\/" (L,(X "/\" Y),X) is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
X "/\" (X `) is M2( the U1 of L)
Y "/\" (X "/\" (X `)) is M2( the U1 of L)
(X "/\" ((X "/\" Y) `)) "\/" (Y "/\" (X "/\" (X `))) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
Y "/\" () is M2( the U1 of L)
(X "/\" ((X "/\" Y) `)) "\/" (Y "/\" ()) is M2( the U1 of L)
(X `) "\/" (Y `) is M2( the U1 of L)
X "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)
(X "/\" (X `)) "\/" (X "/\" (Y `)) is M2( the U1 of L)
() "\/" (X "/\" (Y `)) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(L,Y,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(L,X,Y) "\/" (X "/\" Y) is M2( the U1 of L)
(L,Y,X) "\/" X is M2( the U1 of L)
(L,X,Y) "\/" (X "/\" Y) is M2( the U1 of L)
(L,Y,X) "\/" ((L,X,Y) "\/" (X "/\" Y)) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(L,Y,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)
(L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)
(L,X,Y) ` is M2( the U1 of L)
(X "\/" Y) "/\" ((L,X,Y) `) is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(X "/\" (Y `)) ` is M2( the U1 of L)
(Y "/\" (X `)) ` is M2( the U1 of L)
((X "/\" (Y `)) `) "/\" ((Y "/\" (X `)) `) is M2( the U1 of L)
(X "\/" Y) "/\" (((X "/\" (Y `)) `) "/\" ((Y "/\" (X `)) `)) is M2( the U1 of L)
(X `) ` is M2( the U1 of L)
(Y `) "\/" ((X `) `) is M2( the U1 of L)
((X "/\" (Y `)) `) "/\" ((Y `) "\/" ((X `) `)) is M2( the U1 of L)
(X "\/" Y) "/\" (((X "/\" (Y `)) `) "/\" ((Y `) "\/" ((X `) `))) is M2( the U1 of L)
(Y `) ` is M2( the U1 of L)
(X `) "\/" ((Y `) `) is M2( the U1 of L)
((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `)) is M2( the U1 of L)
(X "\/" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `))) is M2( the U1 of L)
(Y `) "\/" X is M2( the U1 of L)
((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" X) is M2( the U1 of L)
(X "\/" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" X)) is M2( the U1 of L)
(X `) "\/" Y is M2( the U1 of L)
((X `) "\/" Y) "/\" ((Y `) "\/" X) is M2( the U1 of L)
(X "\/" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" X)) is M2( the U1 of L)
(X "\/" Y) "/\" ((X `) "\/" Y) is M2( the U1 of L)
((X "\/" Y) "/\" ((X `) "\/" Y)) "/\" ((Y `) "\/" X) is M2( the U1 of L)
(X "\/" Y) "/\" (X `) is M2( the U1 of L)
(X "\/" Y) "/\" Y is M2( the U1 of L)
((X "\/" Y) "/\" (X `)) "\/" ((X "\/" Y) "/\" Y) is M2( the U1 of L)
(((X "\/" Y) "/\" (X `)) "\/" ((X "\/" Y) "/\" Y)) "/\" ((Y `) "\/" X) is M2( the U1 of L)
((X "\/" Y) "/\" (X `)) "\/" Y is M2( the U1 of L)
(((X "\/" Y) "/\" (X `)) "\/" Y) "/\" ((Y `) "\/" X) is M2( the U1 of L)
X "/\" (X `) is M2( the U1 of L)
(X "/\" (X `)) "\/" (Y "/\" (X `)) is M2( the U1 of L)
((X "/\" (X `)) "\/" (Y "/\" (X `))) "\/" Y is M2( the U1 of L)
(((X "/\" (X `)) "\/" (Y "/\" (X `))) "\/" Y) "/\" ((Y `) "\/" X) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "\/" (Y "/\" (X `)) is M2( the U1 of L)
(() "\/" (Y "/\" (X `))) "\/" Y is M2( the U1 of L)
((() "\/" (Y "/\" (X `))) "\/" Y) "/\" ((Y `) "\/" X) is M2( the U1 of L)
Y "/\" ((Y `) "\/" X) is M2( the U1 of L)
Y "/\" (Y `) is M2( the U1 of L)
Y "/\" X is M2( the U1 of L)
(Y "/\" (Y `)) "\/" (Y "/\" X) is M2( the U1 of L)
() "\/" (Y "/\" X) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(L,Y,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(L,(L,X,Y),(X "/\" Y)) is M2( the U1 of L)
(L,(L,X,Y),(X "/\" Y)) is M2( the U1 of L)
(X "/\" Y) ` is M2( the U1 of L)
(L,X,Y) "/\" ((X "/\" Y) `) is M2( the U1 of L)
(L,(X "/\" Y),(L,X,Y)) is M2( the U1 of L)
(L,X,Y) ` is M2( the U1 of L)
(X "/\" Y) "/\" ((L,X,Y) `) is M2( the U1 of L)
(L,(L,X,Y),(X "/\" Y)) "\/" (L,(X "/\" Y),(L,X,Y)) is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
(X `) "\/" (Y `) is M2( the U1 of L)
(L,X,Y) "/\" ((X `) "\/" (Y `)) is M2( the U1 of L)
((L,X,Y) "/\" ((X `) "\/" (Y `))) "\/" ((X "/\" Y) "/\" ((L,X,Y) `)) is M2( the U1 of L)
(L,X,Y) "/\" (X `) is M2( the U1 of L)
(L,X,Y) "/\" (Y `) is M2( the U1 of L)
((L,X,Y) "/\" (X `)) "\/" ((L,X,Y) "/\" (Y `)) is M2( the U1 of L)
(((L,X,Y) "/\" (X `)) "\/" ((L,X,Y) "/\" (Y `))) "\/" ((X "/\" Y) "/\" ((L,X,Y) `)) is M2( the U1 of L)
(L,(L,X,Y),X) is M2( the U1 of L)
(L,(L,X,Y),Y) is M2( the U1 of L)
(L,(L,X,Y),X) "\/" (L,(L,X,Y),Y) is M2( the U1 of L)
(X "/\" (Y `)) ` is M2( the U1 of L)
(Y "/\" (X `)) ` is M2( the U1 of L)
((X "/\" (Y `)) `) "/\" ((Y "/\" (X `)) `) is M2( the U1 of L)
(X "/\" Y) "/\" (((X "/\" (Y `)) `) "/\" ((Y "/\" (X `)) `)) is M2( the U1 of L)
((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" Y) "/\" (((X "/\" (Y `)) `) "/\" ((Y "/\" (X `)) `))) is M2( the U1 of L)
(Y `) ` is M2( the U1 of L)
(X `) "\/" ((Y `) `) is M2( the U1 of L)
((X `) "\/" ((Y `) `)) "/\" ((Y "/\" (X `)) `) is M2( the U1 of L)
(X "/\" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y "/\" (X `)) `)) is M2( the U1 of L)
((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y "/\" (X `)) `))) is M2( the U1 of L)
(X `) ` is M2( the U1 of L)
(Y `) "\/" ((X `) `) is M2( the U1 of L)
((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `)) is M2( the U1 of L)
(X "/\" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `))) is M2( the U1 of L)
((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `)))) is M2( the U1 of L)
(X `) "\/" Y is M2( the U1 of L)
((X `) "\/" Y) "/\" ((Y `) "\/" ((X `) `)) is M2( the U1 of L)
(X "/\" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" ((X `) `))) is M2( the U1 of L)
((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" ((X `) `)))) is M2( the U1 of L)
(Y `) "\/" X is M2( the U1 of L)
((X `) "\/" Y) "/\" ((Y `) "\/" X) is M2( the U1 of L)
(X "/\" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" X)) is M2( the U1 of L)
((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" X))) is M2( the U1 of L)
(X "/\" Y) "/\" ((X `) "\/" Y) is M2( the U1 of L)
((X "/\" Y) "/\" ((X `) "\/" Y)) "/\" ((Y `) "\/" X) is M2( the U1 of L)
((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" (((X "/\" Y) "/\" ((X `) "\/" Y)) "/\" ((Y `) "\/" X)) is M2( the U1 of L)
(X "/\" Y) "/\" (X `) is M2( the U1 of L)
(X "/\" Y) "/\" Y is M2( the U1 of L)
((X "/\" Y) "/\" (X `)) "\/" ((X "/\" Y) "/\" Y) is M2( the U1 of L)
(((X "/\" Y) "/\" (X `)) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X) is M2( the U1 of L)
((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((((X "/\" Y) "/\" (X `)) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X)) is M2( the U1 of L)
X "/\" (X `) is M2( the U1 of L)
Y "/\" (X "/\" (X `)) is M2( the U1 of L)
(Y "/\" (X "/\" (X `))) "\/" ((X "/\" Y) "/\" Y) is M2( the U1 of L)
((Y "/\" (X "/\" (X `))) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X) is M2( the U1 of L)
((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" (((Y "/\" (X "/\" (X `))) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X)) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
Y "/\" () is M2( the U1 of L)
(Y "/\" ()) "\/" ((X "/\" Y) "/\" Y) is M2( the U1 of L)
((Y "/\" ()) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X) is M2( the U1 of L)
((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" (((Y "/\" ()) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X)) is M2( the U1 of L)
Y "/\" Y is M2( the U1 of L)
X "/\" (Y "/\" Y) is M2( the U1 of L)
(X "/\" (Y "/\" Y)) "/\" ((Y `) "\/" X) is M2( the U1 of L)
((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" (Y "/\" Y)) "/\" ((Y `) "\/" X)) is M2( the U1 of L)
(X "/\" Y) "/\" (Y `) is M2( the U1 of L)
(X "/\" Y) "/\" X is M2( the U1 of L)
((X "/\" Y) "/\" (Y `)) "\/" ((X "/\" Y) "/\" X) is M2( the U1 of L)
((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" (((X "/\" Y) "/\" (Y `)) "\/" ((X "/\" Y) "/\" X)) is M2( the U1 of L)
Y "/\" (Y `) is M2( the U1 of L)
X "/\" (Y "/\" (Y `)) is M2( the U1 of L)
(X "/\" (Y "/\" (Y `))) "\/" ((X "/\" Y) "/\" X) is M2( the U1 of L)
((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" (Y "/\" (Y `))) "\/" ((X "/\" Y) "/\" X)) is M2( the U1 of L)
X "/\" () is M2( the U1 of L)
(X "/\" ()) "\/" ((X "/\" Y) "/\" X) is M2( the U1 of L)
((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" ((X "/\" ()) "\/" ((X "/\" Y) "/\" X)) is M2( the U1 of L)
X "/\" X is M2( the U1 of L)
Y "/\" (X "/\" X) is M2( the U1 of L)
((L,(L,X,Y),X) "\/" (L,(L,X,Y),Y)) "\/" (Y "/\" (X "/\" X)) is M2( the U1 of L)
(X "/\" (Y `)) "/\" (X `) is M2( the U1 of L)
(Y "/\" (X `)) "/\" (X `) is M2( the U1 of L)
((X "/\" (Y `)) "/\" (X `)) "\/" ((Y "/\" (X `)) "/\" (X `)) is M2( the U1 of L)
((L,X,Y) "\/" (L,Y,X)) "/\" (Y `) is M2( the U1 of L)
(((X "/\" (Y `)) "/\" (X `)) "\/" ((Y "/\" (X `)) "/\" (X `))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `)) is M2( the U1 of L)
Y "/\" X is M2( the U1 of L)
((((X "/\" (Y `)) "/\" (X `)) "\/" ((Y "/\" (X `)) "/\" (X `))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `))) "\/" (Y "/\" X) is M2( the U1 of L)
(Y `) "/\" (X "/\" (X `)) is M2( the U1 of L)
((Y `) "/\" (X "/\" (X `))) "\/" ((Y "/\" (X `)) "/\" (X `)) is M2( the U1 of L)
(((Y `) "/\" (X "/\" (X `))) "\/" ((Y "/\" (X `)) "/\" (X `))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `)) is M2( the U1 of L)
((((Y `) "/\" (X "/\" (X `))) "\/" ((Y "/\" (X `)) "/\" (X `))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `))) "\/" (Y "/\" X) is M2( the U1 of L)
(X `) "/\" (X `) is M2( the U1 of L)
Y "/\" ((X `) "/\" (X `)) is M2( the U1 of L)
((Y `) "/\" (X "/\" (X `))) "\/" (Y "/\" ((X `) "/\" (X `))) is M2( the U1 of L)
(((Y `) "/\" (X "/\" (X `))) "\/" (Y "/\" ((X `) "/\" (X `)))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `)) is M2( the U1 of L)
((((Y `) "/\" (X "/\" (X `))) "\/" (Y "/\" ((X `) "/\" (X `)))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `))) "\/" (Y "/\" X) is M2( the U1 of L)
(Y `) "/\" () is M2( the U1 of L)
((Y `) "/\" ()) "\/" (Y "/\" ((X `) "/\" (X `))) is M2( the U1 of L)
(((Y `) "/\" ()) "\/" (Y "/\" ((X `) "/\" (X `)))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `)) is M2( the U1 of L)
((((Y `) "/\" ()) "\/" (Y "/\" ((X `) "/\" (X `)))) "\/" (((L,X,Y) "\/" (L,Y,X)) "/\" (Y `))) "\/" (Y "/\" X) is M2( the U1 of L)
(X "/\" (Y `)) "/\" (Y `) is M2( the U1 of L)
(Y "/\" (X `)) "/\" (Y `) is M2( the U1 of L)
((X "/\" (Y `)) "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" (Y `)) is M2( the U1 of L)
(Y "/\" (X `)) "\/" (((X "/\" (Y `)) "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" (Y `))) is M2( the U1 of L)
((Y "/\" (X `)) "\/" (((X "/\" (Y `)) "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" (Y `)))) "\/" (Y "/\" X) is M2( the U1 of L)
(Y `) "/\" (Y `) is M2( the U1 of L)
X "/\" ((Y `) "/\" (Y `)) is M2( the U1 of L)
(X "/\" ((Y `) "/\" (Y `))) "\/" ((Y "/\" (X `)) "/\" (Y `)) is M2( the U1 of L)
(Y "/\" (X `)) "\/" ((X "/\" ((Y `) "/\" (Y `))) "\/" ((Y "/\" (X `)) "/\" (Y `))) is M2( the U1 of L)
((Y "/\" (X `)) "\/" ((X "/\" ((Y `) "/\" (Y `))) "\/" ((Y "/\" (X `)) "/\" (Y `)))) "\/" (Y "/\" X) is M2( the U1 of L)
(X `) "/\" (Y "/\" (Y `)) is M2( the U1 of L)
(X "/\" (Y `)) "\/" ((X `) "/\" (Y "/\" (Y `))) is M2( the U1 of L)
(Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" ((X `) "/\" (Y "/\" (Y `)))) is M2( the U1 of L)
((Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" ((X `) "/\" (Y "/\" (Y `))))) "\/" (Y "/\" X) is M2( the U1 of L)
(X `) "/\" () is M2( the U1 of L)
(X "/\" (Y `)) "\/" ((X `) "/\" ()) is M2( the U1 of L)
(Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" ((X `) "/\" ())) is M2( the U1 of L)
((Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" ((X `) "/\" ()))) "\/" (Y "/\" X) is M2( the U1 of L)
(X "/\" (Y `)) "\/" (Y "/\" X) is M2( the U1 of L)
(Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" (Y "/\" X)) is M2( the U1 of L)
(Y `) "\/" Y is M2( the U1 of L)
X "/\" ((Y `) "\/" Y) is M2( the U1 of L)
(Y "/\" (X `)) "\/" (X "/\" ((Y `) "\/" Y)) is M2( the U1 of L)
Top L is M2( the U1 of L)
X "/\" (Top L) is M2( the U1 of L)
(Y "/\" (X `)) "\/" (X "/\" (Top L)) is M2( the U1 of L)
Y "\/" X is M2( the U1 of L)
(X `) "\/" X is M2( the U1 of L)
(Y "\/" X) "/\" ((X `) "\/" X) is M2( the U1 of L)
(Y "\/" X) "/\" (Top L) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(L,Y,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
(L,(L,X,Y),(X "\/" Y)) is M2( the U1 of L)
(L,(L,X,Y),(X "\/" Y)) is M2( the U1 of L)
(X "\/" Y) ` is M2( the U1 of L)
(L,X,Y) "/\" ((X "\/" Y) `) is M2( the U1 of L)
(L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)
(L,X,Y) ` is M2( the U1 of L)
(X "\/" Y) "/\" ((L,X,Y) `) is M2( the U1 of L)
(L,(L,X,Y),(X "\/" Y)) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(X `) "/\" (Y `) is M2( the U1 of L)
(L,X,Y) "/\" ((X `) "/\" (Y `)) is M2( the U1 of L)
((L,X,Y) "/\" ((X `) "/\" (Y `))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)
(X "/\" (Y `)) "/\" ((X `) "/\" (Y `)) is M2( the U1 of L)
(Y "/\" (X `)) "/\" ((X `) "/\" (Y `)) is M2( the U1 of L)
((X "/\" (Y `)) "/\" ((X `) "/\" (Y `))) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `))) is M2( the U1 of L)
(((X "/\" (Y `)) "/\" ((X `) "/\" (Y `))) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `)))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)
(Y `) "/\" (X `) is M2( the U1 of L)
(Y `) "/\" ((Y `) "/\" (X `)) is M2( the U1 of L)
X "/\" ((Y `) "/\" ((Y `) "/\" (X `))) is M2( the U1 of L)
(X "/\" ((Y `) "/\" ((Y `) "/\" (X `)))) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `))) is M2( the U1 of L)
((X "/\" ((Y `) "/\" ((Y `) "/\" (X `)))) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `)))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)
(Y `) "/\" (Y `) is M2( the U1 of L)
((Y `) "/\" (Y `)) "/\" (X `) is M2( the U1 of L)
X "/\" (((Y `) "/\" (Y `)) "/\" (X `)) is M2( the U1 of L)
(X "/\" (((Y `) "/\" (Y `)) "/\" (X `))) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `))) is M2( the U1 of L)
((X "/\" (((Y `) "/\" (Y `)) "/\" (X `))) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `)))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)
X "/\" (X `) is M2( the U1 of L)
(X "/\" (X `)) "/\" (Y `) is M2( the U1 of L)
((X "/\" (X `)) "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `))) is M2( the U1 of L)
(((X "/\" (X `)) "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `)))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "/\" (Y `) is M2( the U1 of L)
(() "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `))) is M2( the U1 of L)
((() "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `)))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)
(X `) "/\" ((X `) "/\" (Y `)) is M2( the U1 of L)
Y "/\" ((X `) "/\" ((X `) "/\" (Y `))) is M2( the U1 of L)
(Y "/\" ((X `) "/\" ((X `) "/\" (Y `)))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)
(X `) "/\" (X `) is M2( the U1 of L)
((X `) "/\" (X `)) "/\" (Y `) is M2( the U1 of L)
Y "/\" (((X `) "/\" (X `)) "/\" (Y `)) is M2( the U1 of L)
(Y "/\" (((X `) "/\" (X `)) "/\" (Y `))) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)
Y "/\" (Y `) is M2( the U1 of L)
(Y "/\" (Y `)) "/\" (X `) is M2( the U1 of L)
((Y "/\" (Y `)) "/\" (X `)) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)
() "/\" (X `) is M2( the U1 of L)
(() "/\" (X `)) "\/" (L,(X "\/" Y),(L,X,Y)) is M2( the U1 of L)
Y "/\" X is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
(L,X,Y) is M2( the U1 of L)
Y ` is M2( the U1 of L)
X "/\" (Y `) is M2( the U1 of L)
(L,Y,X) is M2( the U1 of L)
X ` is M2( the U1 of L)
Y "/\" (X `) is M2( the U1 of L)
(L,X,Y) "\/" (L,Y,X) is M2( the U1 of L)
X "\/" Y is M2( the U1 of L)
X "/\" Y is M2( the U1 of L)
(L,(X "\/" Y),(X "/\" Y)) is M2( the U1 of L)
(X "/\" Y) ` is M2( the U1 of L)
(X "\/" Y) "/\" ((X "/\" Y) `) is M2( the U1 of L)
(L,X,(X "/\" Y)) is M2( the U1 of L)
X "/\" ((X "/\" Y) `) is M2( the U1 of L)
(L,X,(X "/\" Y)) "\/" (L,Y,X) is M2( the U1 of L)
(L,Y,(X "/\" Y)) is M2( the U1 of L)
Y "/\" ((X "/\" Y) `) is M2( the U1 of L)
(L,X,(X "/\" Y)) "\/" (L,Y,(X "/\" Y)) is M2( the U1 of L)

the U1 of L is set
X is M2( the U1 of L)
Y is M2( the U1 of L)
(L,X,Y) is M2( the U1 of