:: SHEFFER2 semantic presentation

K87() is set
K19(K87()) is set
1 is set
K14() is set
L is non empty ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | a is M2( the U1 of L)
a | ((b | a) | a) is M2( the U1 of L)
c is M2( the U1 of L)
c | a is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
(a | ((b | a) | a)) | (b | (c | a)) is M2( the U1 of L)
TrivShefferOrthoLattStr is non empty trivial V43() V48(1) join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean well-complemented upper-bounded' lower-bounded' distributive' complemented' properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 () ShefferOrthoLattStr
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
a | (a | (b | c)) is M2( the U1 of L)
(a | (b | c)) | (a | (a | (b | c))) is M2( the U1 of L)
a | c is M2( the U1 of L)
(a | c) | c is M2( the U1 of L)
c | ((a | c) | c) is M2( the U1 of L)
y is M2( the U1 of L)
y | (a | (b | c)) is M2( the U1 of L)
(c | ((a | c) | c)) | (y | (a | (b | c))) is M2( the U1 of L)
((a | (b | c)) | (a | (a | (b | c)))) | ((c | ((a | c) | c)) | (y | (a | (b | c)))) is M2( the U1 of L)
(c | ((a | c) | c)) | (a | (b | c)) is M2( the U1 of L)
((c | ((a | c) | c)) | (a | (b | c))) | (a | (b | c)) is M2( the U1 of L)
(a | (b | c)) | (((c | ((a | c) | c)) | (a | (b | c))) | (a | (b | c))) is M2( the U1 of L)
((a | (b | c)) | (((c | ((a | c) | c)) | (a | (b | c))) | (a | (b | c)))) | ((c | ((a | c) | c)) | (y | (a | (b | c)))) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
c is M2( the U1 of L)
c | b is M2( the U1 of L)
(c | b) | b is M2( the U1 of L)
b | ((c | b) | b) is M2( the U1 of L)
(b | ((c | b) | b)) | (a | b) is M2( the U1 of L)
((b | ((c | b) | b)) | (a | b)) | (a | b) is M2( the U1 of L)
(a | b) | (((b | ((c | b) | b)) | (a | b)) | (a | b)) is M2( the U1 of L)
((a | b) | (((b | ((c | b) | b)) | (a | b)) | (a | b))) | c is M2( the U1 of L)
c | (a | b) is M2( the U1 of L)
(b | ((c | b) | b)) | (c | (a | b)) is M2( the U1 of L)
((a | b) | (((b | ((c | b) | b)) | (a | b)) | (a | b))) | ((b | ((c | b) | b)) | (c | (a | b))) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | a is M2( the U1 of L)
a | ((b | a) | a) is M2( the U1 of L)
c is M2( the U1 of L)
a | c is M2( the U1 of L)
(a | c) | c is M2( the U1 of L)
c | ((a | c) | c) is M2( the U1 of L)
b | (c | ((a | c) | c)) is M2( the U1 of L)
(a | ((b | a) | a)) | (b | (c | ((a | c) | c))) is M2( the U1 of L)
(c | ((a | c) | c)) | (a | c) is M2( the U1 of L)
((c | ((a | c) | c)) | (a | c)) | (a | c) is M2( the U1 of L)
(a | c) | (((c | ((a | c) | c)) | (a | c)) | (a | c)) is M2( the U1 of L)
((a | c) | (((c | ((a | c) | c)) | (a | c)) | (a | c))) | a is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | a is M2( the U1 of L)
a | ((a | a) | a) is M2( the U1 of L)
a | (a | ((a | a) | a)) is M2( the U1 of L)
(a | ((a | a) | a)) | (a | (a | ((a | a) | a))) is M2( the U1 of L)
b is M2( the U1 of L)
b | (a | ((a | a) | a)) is M2( the U1 of L)
(a | ((a | a) | a)) | (b | (a | ((a | a) | a))) is M2( the U1 of L)
a | ((a | ((a | a) | a)) | (b | (a | ((a | a) | a)))) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | a is M2( the U1 of L)
a | ((a | a) | a) is M2( the U1 of L)
a | (a | ((a | a) | a)) is M2( the U1 of L)
(a | ((a | a) | a)) | (a | (a | ((a | a) | a))) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | a is M2( the U1 of L)
a | ((a | a) | a) is M2( the U1 of L)
(a | ((a | a) | a)) | (a | a) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
a | (b | a) is M2( the U1 of L)
(a | a) | (a | (b | a)) is M2( the U1 of L)
(a | a) | a is M2( the U1 of L)
a | ((a | a) | a) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
((b | b) | a) | a is M2( the U1 of L)
a | (((b | b) | a) | a) is M2( the U1 of L)
(a | (((b | b) | a) | a)) | b is M2( the U1 of L)
a | b is M2( the U1 of L)
(a | b) | b is M2( the U1 of L)
b | ((a | b) | b) is M2( the U1 of L)
(b | b) | (b | ((a | b) | b)) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
(a | b) | (a | b) is M2( the U1 of L)
((a | b) | (a | b)) | (a | b) is M2( the U1 of L)
(a | b) | (((a | b) | (a | b)) | (a | b)) is M2( the U1 of L)
((a | b) | (((a | b) | (a | b)) | (a | b))) | ((a | b) | (a | b)) is M2( the U1 of L)
((a | b) | (a | b)) | b is M2( the U1 of L)
(((a | b) | (a | b)) | b) | b is M2( the U1 of L)
b | ((((a | b) | (a | b)) | b) | b) is M2( the U1 of L)
(b | ((((a | b) | (a | b)) | b) | b)) | (a | b) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | (b | a) is M2( the U1 of L)
((b | a) | (b | a)) | a is M2( the U1 of L)
(((b | a) | (b | a)) | a) | a is M2( the U1 of L)
a | ((((b | a) | (b | a)) | a) | a) is M2( the U1 of L)
((b | a) | (b | a)) | (b | a) is M2( the U1 of L)
(b | a) | (((b | a) | (b | a)) | (b | a)) is M2( the U1 of L)
((b | a) | (((b | a) | (b | a)) | (b | a))) | ((b | a) | (b | a)) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(a | a) | (b | a) is M2( the U1 of L)
(b | a) | (b | a) is M2( the U1 of L)
((b | a) | (b | a)) | a is M2( the U1 of L)
(((b | a) | (b | a)) | a) | a is M2( the U1 of L)
a | ((((b | a) | (b | a)) | a) | a) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | a is M2( the U1 of L)
b | (a | a) is M2( the U1 of L)
a | (b | (a | a)) is M2( the U1 of L)
(a | a) | (a | a) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
(a | b) | (a | b) is M2( the U1 of L)
((a | b) | (a | b)) | b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | (a | b) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | a is M2( the U1 of L)
a | ((b | a) | a) is M2( the U1 of L)
(b | a) | (b | a) is M2( the U1 of L)
((b | a) | (b | a)) | a is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
c is M2( the U1 of L)
c | b is M2( the U1 of L)
a | (c | b) is M2( the U1 of L)
(a | b) | (a | (c | b)) is M2( the U1 of L)
(a | b) | b is M2( the U1 of L)
b | ((a | b) | b) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
a | c is M2( the U1 of L)
(a | (b | c)) | (a | c) is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | (b | c) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
c is M2( the U1 of L)
c | b is M2( the U1 of L)
(a | b) | (c | b) is M2( the U1 of L)
a | ((a | b) | (c | b)) is M2( the U1 of L)
a | (c | b) is M2( the U1 of L)
(a | b) | (a | (c | b)) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
(a | (b | c)) | c is M2( the U1 of L)
((a | (b | c)) | c) | a is M2( the U1 of L)
a | c is M2( the U1 of L)
(a | (b | c)) | (a | c) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | a is M2( the U1 of L)
a | ((b | a) | a) is M2( the U1 of L)
a | b is M2( the U1 of L)
b | ((b | a) | a) is M2( the U1 of L)
(a | ((b | a) | a)) | (b | ((b | a) | a)) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | a is M2( the U1 of L)
a | ((b | a) | a) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | b) | (a | a) is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | a is M2( the U1 of L)
a | ((b | a) | a) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
c is M2( the U1 of L)
c | a is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
(a | b) | (b | (c | a)) is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | a is M2( the U1 of L)
a | ((b | a) | a) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
c | a is M2( the U1 of L)
(a | (b | c)) | (c | a) is M2( the U1 of L)
a | c is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
c is M2( the U1 of L)
a | c is M2( the U1 of L)
b | (a | c) is M2( the U1 of L)
(a | b) | (b | (a | c)) is M2( the U1 of L)
c | a is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
b | a is M2( the U1 of L)
(a | (b | c)) | (b | a) is M2( the U1 of L)
c | b is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
c is M2( the U1 of L)
a | c is M2( the U1 of L)
(a | b) | (a | c) is M2( the U1 of L)
((a | b) | (a | c)) | c is M2( the U1 of L)
c | (a | b) is M2( the U1 of L)
(a | c) | (c | (a | b)) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
b | (a | (b | c)) is M2( the U1 of L)
a | (b | (a | (b | c))) is M2( the U1 of L)
b | a is M2( the U1 of L)
(a | (b | c)) | (b | a) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
a | c is M2( the U1 of L)
b | (a | c) is M2( the U1 of L)
a | (b | (a | c)) is M2( the U1 of L)
(a | (b | (a | c))) | b is M2( the U1 of L)
a | b is M2( the U1 of L)
(b | (a | c)) | (a | b) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
y is M2( the U1 of L)
b | a is M2( the U1 of L)
y | (b | a) is M2( the U1 of L)
a | (y | (b | a)) is M2( the U1 of L)
(a | (b | c)) | (a | (y | (b | a))) is M2( the U1 of L)
(a | (b | c)) | (b | a) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
a | c is M2( the U1 of L)
b | (a | c) is M2( the U1 of L)
a | (b | (a | c)) is M2( the U1 of L)
(a | (b | (a | c))) | b is M2( the U1 of L)
c | a is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
b | a is M2( the U1 of L)
(a | (b | c)) | (b | a) is M2( the U1 of L)
y is M2( the U1 of L)
y | (b | a) is M2( the U1 of L)
a | (y | (b | a)) is M2( the U1 of L)
(a | (b | c)) | (a | (y | (b | a))) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
b | (a | b) is M2( the U1 of L)
a | (b | (a | b)) is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | b) | b is M2( the U1 of L)
a | ((a | b) | b) is M2( the U1 of L)
(a | b) | (a | ((a | b) | b)) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
c | b is M2( the U1 of L)
a | (c | b) is M2( the U1 of L)
c | (a | (c | b)) is M2( the U1 of L)
(c | (a | (c | b))) | a is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | a is M2( the U1 of L)
c | (b | a) is M2( the U1 of L)
a | (c | (b | a)) is M2( the U1 of L)
b | (a | (c | (b | a))) is M2( the U1 of L)
a | (b | (a | (c | (b | a)))) is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | (b | (a | (c | (b | a))))) | (a | (c | (b | a))) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | a is M2( the U1 of L)
(a | (b | c)) | ((b | a) | a) is M2( the U1 of L)
(a | (b | c)) | (a | (b | c)) is M2( the U1 of L)
(a | (b | c)) | (b | a) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
a | (b | a) is M2( the U1 of L)
(a | (b | a)) | b is M2( the U1 of L)
b | b is M2( the U1 of L)
b | (a | (b | a)) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
c is M2( the U1 of L)
(a | b) | c is M2( the U1 of L)
b | a is M2( the U1 of L)
c | (b | a) is M2( the U1 of L)
c | (a | b) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
a | b is M2( the U1 of L)
c | (a | b) is M2( the U1 of L)
b | (c | (a | b)) is M2( the U1 of L)
a | (b | (c | (a | b))) is M2( the U1 of L)
b | b is M2( the U1 of L)
a | (b | b) is M2( the U1 of L)
b | (a | (b | (c | (a | b)))) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
(a | b) | b is M2( the U1 of L)
c is M2( the U1 of L)
c | a is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
((a | b) | b) | (b | (c | a)) is M2( the U1 of L)
(b | (c | a)) | (b | (c | a)) is M2( the U1 of L)
(b | (c | a)) | (a | b) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
c is M2( the U1 of L)
y is M2( the U1 of L)
c | y is M2( the U1 of L)
(a | b) | (c | y) is M2( the U1 of L)
y | c is M2( the U1 of L)
b | a is M2( the U1 of L)
(y | c) | (b | a) is M2( the U1 of L)
(a | b) | (y | c) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
c is M2( the U1 of L)
(b | a) | c is M2( the U1 of L)
b | ((b | a) | c) is M2( the U1 of L)
a | (b | ((b | a) | c)) is M2( the U1 of L)
b | b is M2( the U1 of L)
a | (b | b) is M2( the U1 of L)
a | b is M2( the U1 of L)
c | (a | b) is M2( the U1 of L)
b | (c | (a | b)) is M2( the U1 of L)
a | (b | (c | (a | b))) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
a | (b | a) is M2( the U1 of L)
b | b is M2( the U1 of L)
a | (b | b) is M2( the U1 of L)
a | b is M2( the U1 of L)
(a | (b | b)) | (a | b) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
(a | b) | b is M2( the U1 of L)
a | a is M2( the U1 of L)
b | (a | a) is M2( the U1 of L)
b | (a | b) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
a | (b | b) is M2( the U1 of L)
a | b is M2( the U1 of L)
a | (a | b) is M2( the U1 of L)
b | a is M2( the U1 of L)
a | (b | a) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
a | (b | b) is M2( the U1 of L)
c is M2( the U1 of L)
c | b is M2( the U1 of L)
a | (c | b) is M2( the U1 of L)
(a | (b | b)) | (a | (c | b)) is M2( the U1 of L)
(a | (c | b)) | (a | (c | b)) is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | a is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
b | b is M2( the U1 of L)
a | (b | b) is M2( the U1 of L)
(a | (b | c)) | (a | (b | b)) is M2( the U1 of L)
(a | (b | c)) | (a | (b | c)) is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | a is M2( the U1 of L)
(a | (b | c)) | ((b | a) | a) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
c is M2( the U1 of L)
a | b is M2( the U1 of L)
a | (a | b) is M2( the U1 of L)
c | (a | (a | b)) is M2( the U1 of L)
(b | b) | (c | (a | (a | b))) is M2( the U1 of L)
a | ((b | b) | (c | (a | (a | b)))) is M2( the U1 of L)
(b | b) | (b | b) is M2( the U1 of L)
a | ((b | b) | (b | b)) is M2( the U1 of L)
a | (b | b) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
(a | (b | c)) | (a | (b | c)) is M2( the U1 of L)
b | b is M2( the U1 of L)
((a | (b | c)) | (a | (b | c))) | (b | b) is M2( the U1 of L)
a | (b | b) is M2( the U1 of L)
(a | (b | c)) | (a | (b | b)) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
c is M2( the U1 of L)
a | b is M2( the U1 of L)
a | (a | b) is M2( the U1 of L)
c | (a | (a | b)) is M2( the U1 of L)
(b | b) | (c | (a | (a | b))) is M2( the U1 of L)
a | ((b | b) | (c | (a | (a | b)))) is M2( the U1 of L)
(b | b) | (b | b) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
(a | b) | (a | b) is M2( the U1 of L)
c is M2( the U1 of L)
(a | b) | c is M2( the U1 of L)
c | ((a | b) | c) is M2( the U1 of L)
(c | ((a | b) | c)) | (a | b) is M2( the U1 of L)
((a | b) | (a | b)) | ((c | ((a | b) | c)) | (a | b)) is M2( the U1 of L)
a | a is M2( the U1 of L)
(((a | b) | (a | b)) | ((c | ((a | b) | c)) | (a | b))) | (a | a) is M2( the U1 of L)
(c | ((a | b) | c)) | (a | a) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | c is M2( the U1 of L)
(b | c) | a is M2( the U1 of L)
a | ((b | c) | a) is M2( the U1 of L)
b | b is M2( the U1 of L)
(a | ((b | c) | a)) | (b | b) is M2( the U1 of L)
(b | c) | (b | b) is M2( the U1 of L)
(b | c) | (b | c) is M2( the U1 of L)
(a | ((b | c) | a)) | (b | c) is M2( the U1 of L)
((b | c) | (b | c)) | ((a | ((b | c) | a)) | (b | c)) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | c is M2( the U1 of L)
(b | c) | a is M2( the U1 of L)
a | ((b | c) | a) is M2( the U1 of L)
b | b is M2( the U1 of L)
(a | ((b | c) | a)) | (b | b) is M2( the U1 of L)
(b | c) | (b | b) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
a | c is M2( the U1 of L)
(a | c) | b is M2( the U1 of L)
b | ((a | c) | b) is M2( the U1 of L)
(b | ((a | c) | b)) | a is M2( the U1 of L)
a | ((b | ((a | c) | b)) | a) is M2( the U1 of L)
a | a is M2( the U1 of L)
(b | ((a | c) | b)) | (a | a) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | a is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
b | (b | (c | a)) is M2( the U1 of L)
(b | (b | (c | a))) | a is M2( the U1 of L)
a | ((b | (b | (c | a))) | a) is M2( the U1 of L)
a | c is M2( the U1 of L)
b | (a | c) is M2( the U1 of L)
a | (b | (a | c)) is M2( the U1 of L)
(a | (b | (a | c))) | b is M2( the U1 of L)
b | ((a | (b | (a | c))) | b) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | a is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
b | (b | (c | a)) is M2( the U1 of L)
(b | (b | (c | a))) | a is M2( the U1 of L)
a | ((b | (b | (c | a))) | a) is M2( the U1 of L)
a | c is M2( the U1 of L)
b | (a | c) is M2( the U1 of L)
a | (b | (a | c)) is M2( the U1 of L)
(a | (b | (a | c))) | b is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
y is M2( the U1 of L)
b | a is M2( the U1 of L)
y | (b | a) is M2( the U1 of L)
c | (y | (b | a)) is M2( the U1 of L)
c | (c | (y | (b | a))) is M2( the U1 of L)
b | (c | (c | (y | (b | a)))) is M2( the U1 of L)
a | (b | (c | (c | (y | (b | a))))) is M2( the U1 of L)
b | b is M2( the U1 of L)
a | (b | b) is M2( the U1 of L)
(c | (c | (y | (b | a)))) | (b | a) is M2( the U1 of L)
(b | a) | ((c | (c | (y | (b | a)))) | (b | a)) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
a | b is M2( the U1 of L)
c | (a | b) is M2( the U1 of L)
b | (c | (a | b)) is M2( the U1 of L)
b | (b | (c | (a | b))) is M2( the U1 of L)
a | (b | (b | (c | (a | b)))) is M2( the U1 of L)
a | a is M2( the U1 of L)
b | (a | a) is M2( the U1 of L)
a | (b | (a | a)) is M2( the U1 of L)
b | (a | (b | (b | (c | (a | b))))) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
a | b is M2( the U1 of L)
c | (a | b) is M2( the U1 of L)
b | (c | (a | b)) is M2( the U1 of L)
b | (b | (c | (a | b))) is M2( the U1 of L)
a | (b | (b | (c | (a | b)))) is M2( the U1 of L)
a | a is M2( the U1 of L)
b | (a | a) is M2( the U1 of L)
a | (b | (a | a)) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
b | (b | b) is M2( the U1 of L)
a | (b | (b | b)) is M2( the U1 of L)
a | a is M2( the U1 of L)
a | b is M2( the U1 of L)
b | (a | b) is M2( the U1 of L)
(b | (a | b)) | (a | b) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | a is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
(b | (c | a)) | (b | (c | a)) is M2( the U1 of L)
c | c is M2( the U1 of L)
((b | (c | a)) | (b | (c | a))) | (c | c) is M2( the U1 of L)
a | (((b | (c | a)) | (b | (c | a))) | (c | c)) is M2( the U1 of L)
a | (b | (c | a)) is M2( the U1 of L)
a | (a | (b | (c | a))) is M2( the U1 of L)
c | (a | (a | (b | (c | a)))) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
b | (c | c) is M2( the U1 of L)
a | (b | (c | c)) is M2( the U1 of L)
c | a is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
a | (b | (c | a)) is M2( the U1 of L)
(b | (c | a)) | (b | (c | a)) is M2( the U1 of L)
((b | (c | a)) | (b | (c | a))) | (c | c) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | a is M2( the U1 of L)
b | ((c | c) | a) is M2( the U1 of L)
a | (b | ((c | c) | a)) is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
(c | c) | (c | c) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
a | (b | b) is M2( the U1 of L)
c is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
c | ((b | b) | a) is M2( the U1 of L)
a | (c | ((b | b) | a)) is M2( the U1 of L)
(a | (b | b)) | (a | (c | ((b | b) | a))) is M2( the U1 of L)
c | b is M2( the U1 of L)
a | (c | b) is M2( the U1 of L)
(a | (c | b)) | (a | (c | b)) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
a | (b | b) is M2( the U1 of L)
c is M2( the U1 of L)
c | (a | (b | b)) is M2( the U1 of L)
a | (c | (a | (b | b))) is M2( the U1 of L)
(a | (b | b)) | (a | (c | (a | (b | b)))) is M2( the U1 of L)
c | b is M2( the U1 of L)
a | (c | b) is M2( the U1 of L)
(a | (c | b)) | (a | (c | b)) is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
a | (b | b) is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
a | (c | c) is M2( the U1 of L)
(a | (b | b)) | (a | (c | c)) is M2( the U1 of L)
c | b is M2( the U1 of L)
a | (c | b) is M2( the U1 of L)
(a | (c | b)) | (a | (c | b)) is M2( the U1 of L)
c | (a | (b | b)) is M2( the U1 of L)
a | (c | (a | (b | b))) is M2( the U1 of L)
(a | (b | b)) | (a | (c | (a | (b | b)))) is M2( the U1 of L)
L is non empty () ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
((a | a) | b) | ((c | c) | b) is M2( the U1 of L)
a | c is M2( the U1 of L)
b | (a | c) is M2( the U1 of L)
(b | (a | c)) | (b | (a | c)) is M2( the U1 of L)
b | (c | c) is M2( the U1 of L)
b | (a | a) is M2( the U1 of L)
(b | (c | c)) | (b | (a | a)) is M2( the U1 of L)
L is non empty ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | (a | a) is M2( the U1 of L)
L is non empty ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
b | (b | b) is M2( the U1 of L)
a | (b | (b | b)) is M2( the U1 of L)
a | a is M2( the U1 of L)
L is non empty ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
(a | (b | c)) | (a | (b | c)) is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | a is M2( the U1 of L)
((b | b) | a) | ((c | c) | a) is M2( the U1 of L)
TrivShefferOrthoLattStr is non empty trivial V43() V48(1) join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V65() complemented Boolean well-complemented upper-bounded' lower-bounded' distributive' complemented' properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 () ShefferOrthoLattStr
the U1 of TrivShefferOrthoLattStr is V11() V12() V28() set
L is M2( the U1 of TrivShefferOrthoLattStr)
a is M2( the U1 of TrivShefferOrthoLattStr)
L "/\" a is M2( the U1 of TrivShefferOrthoLattStr)
L ` is M2( the U1 of TrivShefferOrthoLattStr)
a ` is M2( the U1 of TrivShefferOrthoLattStr)
(L `) "\/" (a `) is M2( the U1 of TrivShefferOrthoLattStr)
((L `) "\/" (a `)) ` is M2( the U1 of TrivShefferOrthoLattStr)
L is non empty ShefferOrthoLattStr
L is non empty ShefferOrthoLattStr
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | a is M2( the U1 of L)
b is M2( the U1 of L)
b | ((a | a) | a) is M2( the U1 of L)
b | b is M2( the U1 of L)
(a | a) | (a | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | (a | (a | a)) is M2( the U1 of L)
(b | b) | (b | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
b | (a | (a | a)) is M2( the U1 of L)
(b | b) | (b | (a | (a | a))) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
y is M2( the U1 of L)
y | (c | (c | c)) is M2( the U1 of L)
(y | (c | (c | c))) | b is M2( the U1 of L)
((y | (c | (c | c))) | b) | ((a | a) | b) is M2( the U1 of L)
y | a is M2( the U1 of L)
b | (y | a) is M2( the U1 of L)
(b | (y | a)) | (b | (y | a)) is M2( the U1 of L)
y | y is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
c is M2( the U1 of L)
c | b is M2( the U1 of L)
(c | b) | ((a | a) | b) is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | a is M2( the U1 of L)
b | ((c | c) | a) is M2( the U1 of L)
(b | ((c | c) | a)) | (b | ((c | c) | a)) is M2( the U1 of L)
(c | c) | (c | c) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
y is M2( the U1 of L)
y | (c | (c | c)) is M2( the U1 of L)
(y | (c | (c | c))) | b is M2( the U1 of L)
((a | a) | b) | ((y | (c | (c | c))) | b) is M2( the U1 of L)
a | y is M2( the U1 of L)
b | (a | y) is M2( the U1 of L)
(b | (a | y)) | (b | (a | y)) is M2( the U1 of L)
y | y is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | ((a | a) | a) is M2( the U1 of L)
(b | b) | (b | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
b | ((a | a) | a) is M2( the U1 of L)
(b | b) | (b | ((a | a) | a)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | a is M2( the U1 of L)
b is M2( the U1 of L)
b | ((a | a) | a) is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | ((a | a) | a)) | (b | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | b is M2( the U1 of L)
c is M2( the U1 of L)
c | ((b | b) | b) is M2( the U1 of L)
(c | ((b | b) | b)) | (a | (a | a)) is M2( the U1 of L)
c | c is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
c is M2( the U1 of L)
c | (b | b) is M2( the U1 of L)
(c | (b | b)) | (c | (b | b)) is M2( the U1 of L)
((c | (b | b)) | (c | (b | b))) | (a | (a | a)) is M2( the U1 of L)
(b | b) | c is M2( the U1 of L)
((b | b) | c) | ((b | b) | c) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
c is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
c | (b | b) is M2( the U1 of L)
(c | (b | b)) | (c | (b | b)) is M2( the U1 of L)
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
((c | (b | b)) | (c | (b | b))) | (a | (a | a)) is M2( the U1 of L)
(b | b) | c is M2( the U1 of L)
b is M2( the U1 of L)
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b | (a | a) is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
((a | a) | (a | a)) | b is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
a | b is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | (a | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
b | ((a | a) | (a | a)) is M2( the U1 of L)
(b | a) | (b | ((a | a) | (a | a))) is M2( the U1 of L)
((a | a) | (a | a)) | b is M2( the U1 of L)
(((a | a) | (a | a)) | b) | (((a | a) | (a | a)) | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | (b | a) is M2( the U1 of L)
((a | a) | (a | a)) | b is M2( the U1 of L)
(((a | a) | (a | a)) | b) | (((a | a) | (a | a)) | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | (b | a) is M2( the U1 of L)
a | b is M2( the U1 of L)
((a | a) | (a | a)) | b is M2( the U1 of L)
(a | b) | (((a | a) | (a | a)) | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | (b | a) is M2( the U1 of L)
a | b is M2( the U1 of L)
(a | b) | (a | b) is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | (a | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
c is M2( the U1 of L)
c | b is M2( the U1 of L)
(c | b) | ((a | a) | a) is M2( the U1 of L)
(c | b) | (c | b) is M2( the U1 of L)
((c | b) | ((a | a) | a)) | ((c | b) | (c | b)) is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | (c | b) is M2( the U1 of L)
(b | b) | (c | b) is M2( the U1 of L)
((c | c) | (c | b)) | ((b | b) | (c | b)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
c is M2( the U1 of L)
b is M2( the U1 of L)
c | b is M2( the U1 of L)
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | a is M2( the U1 of L)
(c | b) | ((a | a) | a) is M2( the U1 of L)
(c | b) | (c | b) is M2( the U1 of L)
((c | b) | ((a | a) | a)) | ((c | b) | (c | b)) is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | (c | b) is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | (c | b) is M2( the U1 of L)
((c | c) | (c | b)) | ((b | b) | (c | b)) is M2( the U1 of L)
b is M2( the U1 of L)
a is M2( the U1 of L)
b | a is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | (b | a) is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | (b | a) is M2( the U1 of L)
((b | b) | (b | a)) | ((a | a) | (b | a)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | a is M2( the U1 of L)
(a | a) | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
b | ((a | a) | a) is M2( the U1 of L)
(b | b) | (b | ((a | a) | a)) is M2( the U1 of L)
((a | a) | (a | a)) | b is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
(((a | a) | (a | a)) | b) | ((a | a) | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | (b | b) is M2( the U1 of L)
((b | b) | (b | b)) | a is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
(((b | b) | (b | b)) | a) | ((b | b) | a) is M2( the U1 of L)
a | a is M2( the U1 of L)
(b | b) | b is M2( the U1 of L)
a | ((b | b) | b) is M2( the U1 of L)
(a | a) | (a | ((b | b) | b)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
(b | a) | ((b | b) | a) is M2( the U1 of L)
(b | b) | (b | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
b | b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
((c | c) | b) | ((a | a) | b) is M2( the U1 of L)
c | a is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
(b | (c | a)) | (b | (c | a)) is M2( the U1 of L)
(((c | c) | b) | ((a | a) | b)) | ((b | (c | a)) | (b | (c | a))) is M2( the U1 of L)
(b | b) | (b | (c | a)) is M2( the U1 of L)
(c | a) | (c | a) is M2( the U1 of L)
((c | a) | (c | a)) | (b | (c | a)) is M2( the U1 of L)
((b | b) | (b | (c | a))) | (((c | a) | (c | a)) | (b | (c | a))) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
((c | c) | b) | ((a | a) | b) is M2( the U1 of L)
c | a is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
(b | (c | a)) | (b | (c | a)) is M2( the U1 of L)
(((c | c) | b) | ((a | a) | b)) | ((b | (c | a)) | (b | (c | a))) is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | (b | (c | a)) is M2( the U1 of L)
(c | a) | (c | a) is M2( the U1 of L)
((c | a) | (c | a)) | (b | (c | a)) is M2( the U1 of L)
((b | b) | (b | (c | a))) | (((c | a) | (c | a)) | (b | (c | a))) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
(a | a) | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
b | (a | (a | a)) is M2( the U1 of L)
(b | b) | (b | (a | (a | a))) is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
((a | a) | (a | a)) | b is M2( the U1 of L)
((a | a) | b) | (((a | a) | (a | a)) | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
(b | b) | (b | b) is M2( the U1 of L)
((b | b) | (b | b)) | a is M2( the U1 of L)
((b | b) | a) | (((b | b) | (b | b)) | a) is M2( the U1 of L)
a | a is M2( the U1 of L)
b | (b | b) is M2( the U1 of L)
a | (b | (b | b)) is M2( the U1 of L)
(a | a) | (a | (b | (b | b))) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
b | a is M2( the U1 of L)
((b | b) | a) | (b | a) is M2( the U1 of L)
(b | b) | (b | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
b | b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
((c | c) | b) | ((a | a) | b) is M2( the U1 of L)
c | a is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
(b | (c | a)) | (b | (c | a)) is M2( the U1 of L)
(((c | c) | b) | ((a | a) | b)) | ((b | (c | a)) | (b | (c | a))) is M2( the U1 of L)
((a | a) | (a | a)) | ((c | c) | b) is M2( the U1 of L)
(b | b) | ((c | c) | b) is M2( the U1 of L)
(((a | a) | (a | a)) | ((c | c) | b)) | ((b | b) | ((c | c) | b)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | (b | b) is M2( the U1 of L)
c is M2( the U1 of L)
c | b is M2( the U1 of L)
a | (c | b) is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | a is M2( the U1 of L)
((b | b) | (b | b)) | ((c | c) | a) is M2( the U1 of L)
(a | a) | ((c | c) | a) is M2( the U1 of L)
(((b | b) | (b | b)) | ((c | c) | a)) | ((a | a) | ((c | c) | a)) is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
((c | c) | a) | ((b | b) | a) is M2( the U1 of L)
(a | (c | b)) | (a | (c | b)) is M2( the U1 of L)
(((c | c) | a) | ((b | b) | a)) | ((a | (c | b)) | (a | (c | b))) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | b is M2( the U1 of L)
a | (c | b) is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | a is M2( the U1 of L)
b | ((c | c) | a) is M2( the U1 of L)
(a | a) | ((c | c) | a) is M2( the U1 of L)
(b | ((c | c) | a)) | ((a | a) | ((c | c) | a)) is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | (b | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | b is M2( the U1 of L)
((b | b) | b) | a is M2( the U1 of L)
a | ((b | b) | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
(b | a) | ((a | a) | b) is M2( the U1 of L)
a | b is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | ((a | a) | a) is M2( the U1 of L)
(b | b) | ((b | b) | ((a | a) | a)) is M2( the U1 of L)
b | ((a | a) | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | b is M2( the U1 of L)
(b | b) | ((a | a) | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
b | b is M2( the U1 of L)
a | (b | b) is M2( the U1 of L)
(b | a) | (a | (b | b)) is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | (a | a) is M2( the U1 of L)
a | b is M2( the U1 of L)
(b | (a | a)) | (a | b) is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
b | (a | a) is M2( the U1 of L)
(b | a) | (b | (a | a)) is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | (a | a) is M2( the U1 of L)
(b | (a | a)) | (b | (a | a)) is M2( the U1 of L)
a | b is M2( the U1 of L)
((b | (a | a)) | (b | (a | a))) | (a | b) is M2( the U1 of L)
b | (((b | (a | a)) | (b | (a | a))) | (a | b)) is M2( the U1 of L)
(a | b) | (b | (a | a)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | (a | a) is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | (a | a)) | (b | a) is M2( the U1 of L)
a | b is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
(a | (a | a)) | (a | (a | a)) is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
((a | (a | a)) | (a | (a | a))) | b is M2( the U1 of L)
c is M2( the U1 of L)
(b | b) | c is M2( the U1 of L)
c | (((a | (a | a)) | (a | (a | a))) | b) is M2( the U1 of L)
(c | (((a | (a | a)) | (a | (a | a))) | b)) | (c | (((a | (a | a)) | (a | (a | a))) | b)) is M2( the U1 of L)
y is M2( the U1 of L)
y | y is M2( the U1 of L)
(y | y) | y is M2( the U1 of L)
((y | y) | y) | c is M2( the U1 of L)
(((y | y) | y) | c) | ((b | b) | c) is M2( the U1 of L)
((a | (a | a)) | (a | (a | a))) | (a | (a | a)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
(a | a) | ((b | b) | a) is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
(c | (c | c)) | (c | (c | c)) is M2( the U1 of L)
((c | (c | c)) | (c | (c | c))) | b is M2( the U1 of L)
a | (((c | (c | c)) | (c | (c | c))) | b) is M2( the U1 of L)
(a | (((c | (c | c)) | (c | (c | c))) | b)) | (a | (((c | (c | c)) | (c | (c | c))) | b)) is M2( the U1 of L)
((c | (c | c)) | (c | (c | c))) | (c | (c | c)) is M2( the U1 of L)
(((c | (c | c)) | (c | (c | c))) | (c | (c | c))) | a is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
b | (b | b) is M2( the U1 of L)
c is M2( the U1 of L)
a | c is M2( the U1 of L)
c | (b | (b | b)) is M2( the U1 of L)
a | (c | (b | (b | b))) is M2( the U1 of L)
(a | c) | (a | (c | (b | (b | b)))) is M2( the U1 of L)
c | c is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
b | (b | b) is M2( the U1 of L)
c is M2( the U1 of L)
c | (b | (b | b)) is M2( the U1 of L)
a | (c | (b | (b | b))) is M2( the U1 of L)
a | c is M2( the U1 of L)
(a | (c | (b | (b | b)))) | (a | c) is M2( the U1 of L)
c | c is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
b | ((b | b) | a) is M2( the U1 of L)
(b | ((b | b) | a)) | (b | ((b | b) | a)) is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | c is M2( the U1 of L)
((c | c) | c) | b is M2( the U1 of L)
(((c | c) | c) | b) | ((a | a) | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
(b | b) | (b | b) is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
a | ((c | c) | b) is M2( the U1 of L)
(a | ((c | c) | b)) | (a | ((c | c) | b)) is M2( the U1 of L)
c | a is M2( the U1 of L)
(c | a) | ((b | b) | a) is M2( the U1 of L)
((a | ((c | c) | b)) | (a | ((c | c) | b))) | ((c | a) | ((b | b) | a)) is M2( the U1 of L)
((b | b) | (b | b)) | (c | a) is M2( the U1 of L)
(a | a) | (c | a) is M2( the U1 of L)
(((b | b) | (b | b)) | (c | a)) | ((a | a) | (c | a)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
a | ((c | c) | b) is M2( the U1 of L)
(a | ((c | c) | b)) | (a | ((c | c) | b)) is M2( the U1 of L)
c | a is M2( the U1 of L)
(c | a) | ((b | b) | a) is M2( the U1 of L)
((a | ((c | c) | b)) | (a | ((c | c) | b))) | ((c | a) | ((b | b) | a)) is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
(a | a) | (c | a) is M2( the U1 of L)
(b | (c | a)) | ((a | a) | (c | a)) is M2( the U1 of L)
(b | b) | (b | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
a | b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
(a | a) | ((c | c) | b) is M2( the U1 of L)
(b | b) | c is M2( the U1 of L)
b | ((b | b) | c) is M2( the U1 of L)
(b | ((b | b) | c)) | (b | ((b | b) | c)) is M2( the U1 of L)
((a | a) | ((c | c) | b)) | ((b | ((b | b) | c)) | (b | ((b | b) | c))) is M2( the U1 of L)
((c | c) | b) | (a | b) is M2( the U1 of L)
(((c | c) | b) | (a | b)) | (((c | c) | b) | (a | b)) is M2( the U1 of L)
(b | b) | ((c | c) | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | b is M2( the U1 of L)
b | (c | b) is M2( the U1 of L)
(b | (c | b)) | (b | (c | b)) is M2( the U1 of L)
((b | (c | b)) | (b | (c | b))) | (a | (a | a)) is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | b is M2( the U1 of L)
((c | c) | b) | ((b | b) | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
b is M2( the U1 of L)
c is M2( the U1 of L)
c | b is M2( the U1 of L)
b | (c | b) is M2( the U1 of L)
(b | (c | b)) | (b | (c | b)) is M2( the U1 of L)
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
((b | (c | b)) | (b | (c | b))) | (a | (a | a)) is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
a | (b | a) is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
(b | a) | ((b | b) | a) is M2( the U1 of L)
(a | a) | (b | a) is M2( the U1 of L)
a | (b | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(a | a) | (b | a) is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
(b | a) | ((b | b) | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | a is M2( the U1 of L)
b | b is M2( the U1 of L)
a | (b | b) is M2( the U1 of L)
(a | (b | b)) | (a | (b | b)) is M2( the U1 of L)
((a | (b | b)) | (a | (b | b))) | (b | a) is M2( the U1 of L)
(a | (b | b)) | (b | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
a | ((c | c) | b) is M2( the U1 of L)
(a | ((c | c) | b)) | (a | ((c | c) | b)) is M2( the U1 of L)
c | a is M2( the U1 of L)
(c | a) | ((b | b) | a) is M2( the U1 of L)
((a | ((c | c) | b)) | (a | ((c | c) | b))) | ((c | a) | ((b | b) | a)) is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
(b | (c | a)) | a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | (c | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
(c | (c | c)) | (c | (c | c)) is M2( the U1 of L)
((c | (c | c)) | (c | (c | c))) | b is M2( the U1 of L)
a | (((c | (c | c)) | (c | (c | c))) | b) is M2( the U1 of L)
(a | (((c | (c | c)) | (c | (c | c))) | b)) | (a | (((c | (c | c)) | (c | (c | c))) | b)) is M2( the U1 of L)
a | a is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
(a | a) | ((b | b) | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
a | ((c | c) | b) is M2( the U1 of L)
(a | ((c | c) | b)) | b is M2( the U1 of L)
c | a is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | ((c | c) | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | a is M2( the U1 of L)
a | ((b | a) | a) is M2( the U1 of L)
b | b is M2( the U1 of L)
a | (b | b) is M2( the U1 of L)
(a | (b | b)) | (a | (b | b)) is M2( the U1 of L)
((a | (b | b)) | (a | (b | b))) | (b | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
b is M2( the U1 of L)
y is M2( the U1 of L)
y | y is M2( the U1 of L)
y | (y | y) is M2( the U1 of L)
(y | (y | y)) | (y | (y | y)) is M2( the U1 of L)
c is M2( the U1 of L)
((y | (y | y)) | (y | (y | y))) | c is M2( the U1 of L)
b | (((y | (y | y)) | (y | (y | y))) | c) is M2( the U1 of L)
(b | (((y | (y | y)) | (y | (y | y))) | c)) | (b | (((y | (y | y)) | (y | (y | y))) | c)) is M2( the U1 of L)
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | a is M2( the U1 of L)
((a | a) | a) | b is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
(((a | a) | a) | b) | ((c | c) | b) is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | c is M2( the U1 of L)
((c | c) | c) | b is M2( the U1 of L)
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
(((c | c) | c) | b) | ((a | a) | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | c is M2( the U1 of L)
b is M2( the U1 of L)
((c | c) | c) | b is M2( the U1 of L)
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
(((c | c) | c) | b) | ((a | a) | b) is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
b | ((b | b) | a) is M2( the U1 of L)
(b | ((b | b) | a)) | (b | ((b | b) | a)) is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
a is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
b | ((b | b) | a) is M2( the U1 of L)
(b | ((b | b) | a)) | (b | ((b | b) | a)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
((c | c) | b) | (a | b) is M2( the U1 of L)
(((c | c) | b) | (a | b)) | (((c | c) | b) | (a | b)) is M2( the U1 of L)
(a | a) | ((c | c) | b) is M2( the U1 of L)
((a | a) | ((c | c) | b)) | b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | c is M2( the U1 of L)
b | ((b | b) | c) is M2( the U1 of L)
(b | ((b | b) | c)) | (b | ((b | b) | c)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
a | b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
((c | c) | b) | (a | b) is M2( the U1 of L)
(((c | c) | b) | (a | b)) | (((c | c) | b) | (a | b)) is M2( the U1 of L)
c | (a | a) is M2( the U1 of L)
b | (c | (a | a)) is M2( the U1 of L)
(a | a) | ((c | c) | b) is M2( the U1 of L)
((a | a) | ((c | c) | b)) | b is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | (b | a) is M2( the U1 of L)
((b | a) | (b | a)) | b is M2( the U1 of L)
a | a is M2( the U1 of L)
b | (a | a) is M2( the U1 of L)
(b | (a | a)) | (b | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | b) | (b | a) is M2( the U1 of L)
a | b is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | (a | a) is M2( the U1 of L)
(a | a) | (b | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
b | (b | b) is M2( the U1 of L)
c is M2( the U1 of L)
c | (b | (b | b)) is M2( the U1 of L)
c | a is M2( the U1 of L)
(c | (b | (b | b))) | (c | a) is M2( the U1 of L)
c | c is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | a) | (b | b) is M2( the U1 of L)
(b | b) | (b | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | b is M2( the U1 of L)
c | (a | (a | a)) is M2( the U1 of L)
(c | b) | (c | (a | (a | a))) is M2( the U1 of L)
c | c is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
c is M2( the U1 of L)
(b | b) | c is M2( the U1 of L)
c | (a | (a | a)) is M2( the U1 of L)
y is M2( the U1 of L)
y | y is M2( the U1 of L)
y | (y | y) is M2( the U1 of L)
x is M2( the U1 of L)
x | (y | (y | y)) is M2( the U1 of L)
(x | (y | (y | y))) | c is M2( the U1 of L)
((x | (y | (y | y))) | c) | ((b | b) | c) is M2( the U1 of L)
x | b is M2( the U1 of L)
c | (x | b) is M2( the U1 of L)
(c | (x | b)) | (c | (x | b)) is M2( the U1 of L)
(((x | (y | (y | y))) | c) | ((b | b) | c)) | ((c | (x | b)) | (c | (x | b))) is M2( the U1 of L)
(c | (a | (a | a))) | (c | (x | b)) is M2( the U1 of L)
(x | b) | (x | b) is M2( the U1 of L)
((x | b) | (x | b)) | (c | (x | b)) is M2( the U1 of L)
((c | (a | (a | a))) | (c | (x | b))) | (((x | b) | (x | b)) | (c | (x | b))) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
c is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
b | (b | b) is M2( the U1 of L)
c | (b | (b | b)) 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)
c | (x | y) is M2( the U1 of L)
(c | (b | (b | b))) | (c | (x | y)) is M2( the U1 of L)
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
x | (a | (a | a)) is M2( the U1 of L)
(x | (a | (a | a))) | c is M2( the U1 of L)
y | y is M2( the U1 of L)
(y | y) | c is M2( the U1 of L)
((x | (a | (a | a))) | c) | ((y | y) | c) is M2( the U1 of L)
(c | (x | y)) | (c | (x | y)) is M2( the U1 of L)
(((x | (a | (a | a))) | c) | ((y | y) | c)) | ((c | (x | y)) | (c | (x | y))) is M2( the U1 of L)
(x | y) | (x | y) is M2( the U1 of L)
((x | y) | (x | y)) | (c | (x | y)) is M2( the U1 of L)
c | (((x | y) | (x | y)) | (c | (x | y))) is M2( the U1 of L)
y is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
y | (c | (c | c)) is M2( the U1 of L)
b is M2( the U1 of L)
(y | (c | (c | c))) | b is M2( the U1 of L)
a is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
((y | (c | (c | c))) | b) | ((a | a) | b) is M2( the U1 of L)
y | a is M2( the U1 of L)
b | (y | a) is M2( the U1 of L)
(b | (y | a)) | (b | (y | a)) is M2( the U1 of L)
(((y | (c | (c | c))) | b) | ((a | a) | b)) | ((b | (y | a)) | (b | (y | a))) is M2( the U1 of L)
(y | a) | (y | a) is M2( the U1 of L)
((y | a) | (y | a)) | (b | (y | a)) is M2( the U1 of L)
b | (((y | a) | (y | a)) | (b | (y | a))) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
y is M2( the U1 of L)
y | (c | (c | c)) is M2( the U1 of L)
(y | (c | (c | c))) | b is M2( the U1 of L)
((y | (c | (c | c))) | b) | ((a | a) | b) is M2( the U1 of L)
y | a is M2( the U1 of L)
b | (y | a) is M2( the U1 of L)
(b | (y | a)) | (b | (y | a)) is M2( the U1 of L)
(((y | (c | (c | c))) | b) | ((a | a) | b)) | ((b | (y | a)) | (b | (y | a))) is M2( the U1 of L)
(y | a) | (y | a) is M2( the U1 of L)
((y | a) | (y | a)) | (b | (y | a)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
b | (b | b) is M2( the U1 of L)
(a | a) | (b | (b | b)) is M2( the U1 of L)
c is M2( the U1 of L)
(a | a) | c is M2( the U1 of L)
c | c is M2( the U1 of L)
y is M2( the U1 of L)
y | y is M2( the U1 of L)
y | (y | y) is M2( the U1 of L)
x is M2( the U1 of L)
x | (y | (y | y)) is M2( the U1 of L)
(x | (y | (y | y))) | c is M2( the U1 of L)
((x | (y | (y | y))) | c) | ((a | a) | c) is M2( the U1 of L)
x | a is M2( the U1 of L)
c | (x | a) is M2( the U1 of L)
(c | (x | a)) | (c | (x | a)) is M2( the U1 of L)
(((x | (y | (y | y))) | c) | ((a | a) | c)) | ((c | (x | a)) | (c | (x | a))) is M2( the U1 of L)
((a | a) | (b | (b | b))) | ((x | (y | (y | y))) | c) is M2( the U1 of L)
(c | c) | ((x | (y | (y | y))) | c) is M2( the U1 of L)
(((a | a) | (b | (b | b))) | ((x | (y | (y | y))) | c)) | ((c | c) | ((x | (y | (y | y))) | c)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
b | (b | b) is M2( the U1 of L)
(a | a) | (b | (b | b)) is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
y is M2( the U1 of L)
y | y is M2( the U1 of L)
y | (y | y) is M2( the U1 of L)
x is M2( the U1 of L)
x | a is M2( the U1 of L)
c | (x | a) is M2( the U1 of L)
x | (y | (y | y)) is M2( the U1 of L)
(x | (y | (y | y))) | c is M2( the U1 of L)
((a | a) | (b | (b | b))) | ((x | (y | (y | y))) | c) is M2( the U1 of L)
(c | c) | ((x | (y | (y | y))) | c) is M2( the U1 of L)
(((a | a) | (b | (b | b))) | ((x | (y | (y | y))) | c)) | ((c | c) | ((x | (y | (y | y))) | c)) is M2( the U1 of L)
(a | a) | c is M2( the U1 of L)
((x | (y | (y | y))) | c) | ((a | a) | c) is M2( the U1 of L)
(c | (x | a)) | (c | (x | a)) is M2( the U1 of L)
(((x | (y | (y | y))) | c) | ((a | a) | c)) | ((c | (x | a)) | (c | (x | a))) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
b is M2( the U1 of L)
b | b is M2( the U1 of L)
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
(b | b) | (a | (a | a)) is M2( the U1 of L)
c is M2( the U1 of L)
x is M2( the U1 of L)
x | b is M2( the U1 of L)
c | (x | b) is M2( the U1 of L)
y is M2( the U1 of L)
y | y is M2( the U1 of L)
y | (y | y) is M2( the U1 of L)
x | (y | (y | y)) is M2( the U1 of L)
(x | (y | (y | y))) | c is M2( the U1 of L)
b | ((x | (y | (y | y))) | c) is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | ((x | (y | (y | y))) | c) is M2( the U1 of L)
(b | ((x | (y | (y | y))) | c)) | ((c | c) | ((x | (y | (y | y))) | c)) is M2( the U1 of L)
b is M2( the U1 of L)
y is M2( the U1 of L)
a is M2( the U1 of L)
y | a is M2( the U1 of L)
b | (y | a) is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
y | (c | (c | c)) is M2( the U1 of L)
(y | (c | (c | c))) | b is M2( the U1 of L)
a | ((y | (c | (c | c))) | b) is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | ((y | (c | (c | c))) | b) is M2( the U1 of L)
(a | ((y | (c | (c | c))) | b)) | ((b | b) | ((y | (c | (c | c))) | b)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
y is M2( the U1 of L)
y | a is M2( the U1 of L)
b | (y | a) is M2( the U1 of L)
y | (c | (c | c)) is M2( the U1 of L)
(y | (c | (c | c))) | b is M2( the U1 of L)
a | ((y | (c | (c | c))) | b) is M2( the U1 of L)
(a | ((y | (c | (c | c))) | b)) | b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | ((y | (c | (c | c))) | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
y is M2( the U1 of L)
y | y is M2( the U1 of L)
(y | y) | c is M2( the U1 of L)
x is M2( the U1 of L)
x | y is M2( the U1 of L)
c | (x | y) is M2( the U1 of L)
b | (c | (x | y)) is M2( the U1 of L)
x | (a | (a | a)) is M2( the U1 of L)
(x | (a | (a | a))) | c is M2( the U1 of L)
((x | (a | (a | a))) | c) | ((y | y) | c) is M2( the U1 of L)
(b | (c | (x | y))) | (((x | (a | (a | a))) | c) | ((y | y) | c)) is M2( the U1 of L)
(c | (x | y)) | (c | (x | y)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
a | ((c | c) | b) is M2( the U1 of L)
(a | ((c | c) | b)) | (a | ((c | c) | b)) is M2( the U1 of L)
c | a is M2( the U1 of L)
(c | a) | ((b | b) | a) is M2( the U1 of L)
((a | ((c | c) | b)) | (a | ((c | c) | b))) | ((c | a) | ((b | b) | a)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | b is M2( the U1 of L)
a | (c | b) is M2( the U1 of L)
(a | (c | b)) | b is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | a is M2( the U1 of L)
b | ((c | c) | a) is M2( the U1 of L)
(b | ((c | c) | a)) | (b | ((c | c) | a)) is M2( the U1 of L)
a | a is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
(c | b) | ((a | a) | b) is M2( the U1 of L)
((b | ((c | c) | a)) | (b | ((c | c) | a))) | ((c | b) | ((a | a) | b)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
y is M2( the U1 of L)
y | (c | (c | c)) is M2( the U1 of L)
(y | (c | (c | c))) | b is M2( the U1 of L)
((a | a) | b) | ((y | (c | (c | c))) | b) is M2( the U1 of L)
(((a | a) | b) | ((y | (c | (c | c))) | b)) | b is M2( the U1 of L)
a | y is M2( the U1 of L)
b | (a | y) is M2( the U1 of L)
(b | (a | y)) | (b | (a | y)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
y is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
y | (c | (c | c)) is M2( the U1 of L)
(y | (c | (c | c))) | b is M2( the U1 of L)
((a | a) | b) | ((y | (c | (c | c))) | b) is M2( the U1 of L)
(((a | a) | b) | ((y | (c | (c | c))) | b)) | b is M2( the U1 of L)
y | ((a | a) | b) is M2( the U1 of L)
b | (y | ((a | a) | b)) is M2( the U1 of L)
a | y is M2( the U1 of L)
b | (a | y) is M2( the U1 of L)
b is M2( the U1 of L)
a is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
(c | c) | b is M2( the U1 of L)
a | ((c | c) | b) is M2( the U1 of L)
b | (a | ((c | c) | b)) is M2( the U1 of L)
c | a is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
y is M2( the U1 of L)
y | a is M2( the U1 of L)
b | (y | a) is M2( the U1 of L)
(b | (y | a)) | (b | (y | a)) is M2( the U1 of L)
y | (c | (c | c)) is M2( the U1 of L)
(y | (c | (c | c))) | b is M2( the U1 of L)
((y | (c | (c | c))) | b) | ((a | a) | b) is M2( the U1 of L)
((b | (y | a)) | (b | (y | a))) | (((y | (c | (c | c))) | b) | ((a | a) | b)) is M2( the U1 of L)
((a | a) | b) | ((y | (c | (c | c))) | b) is M2( the U1 of L)
(((a | a) | b) | ((y | (c | (c | c))) | b)) | (((a | a) | b) | ((y | (c | (c | c))) | b)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
b is M2( the U1 of L)
(a | a) | b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
y is M2( the U1 of L)
y | a is M2( the U1 of L)
b | (y | a) is M2( the U1 of L)
y | (c | (c | c)) is M2( the U1 of L)
(y | (c | (c | c))) | b is M2( the U1 of L)
((a | a) | b) | ((y | (c | (c | c))) | b) is M2( the U1 of L)
(((a | a) | b) | ((y | (c | (c | c))) | b)) | (((a | a) | b) | ((y | (c | (c | c))) | b)) is M2( the U1 of L)
(b | (y | a)) | (b | (y | a)) is M2( the U1 of L)
((y | (c | (c | c))) | b) | ((a | a) | b) is M2( the U1 of L)
((b | (y | a)) | (b | (y | a))) | (((y | (c | (c | c))) | b) | ((a | a) | b)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
y is M2( the U1 of L)
y | b is M2( the U1 of L)
a | (y | b) is M2( the U1 of L)
y | (c | (c | c)) is M2( the U1 of L)
(y | (c | (c | c))) | (y | (c | (c | c))) is M2( the U1 of L)
b | ((y | (c | (c | c))) | (y | (c | (c | c)))) is M2( the U1 of L)
a | (b | ((y | (c | (c | c))) | (y | (c | (c | c))))) is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
(y | (c | (c | c))) | a is M2( the U1 of L)
((b | b) | a) | ((y | (c | (c | c))) | a) is M2( the U1 of L)
(((b | b) | a) | ((y | (c | (c | c))) | a)) | (((b | b) | a) | ((y | (c | (c | c))) | a)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
y is M2( the U1 of L)
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
y | (a | (a | a)) is M2( the U1 of L)
(y | (a | (a | a))) | (y | (a | (a | a))) is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
y | c is M2( the U1 of L)
b | (y | c) is M2( the U1 of L)
c | y is M2( the U1 of L)
b | (c | y) is M2( the U1 of L)
a is M2( the U1 of L)
c is M2( the U1 of L)
b is M2( the U1 of L)
c | b is M2( the U1 of L)
a | (c | b) is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | b is M2( the U1 of L)
(c | b) | a is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
a | (c | b) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | b is M2( the U1 of L)
(b | b) | a is M2( the U1 of L)
c is M2( the U1 of L)
c | b is M2( the U1 of L)
(c | b) | a is M2( the U1 of L)
((c | b) | a) | c is M2( the U1 of L)
c | ((b | b) | a) is M2( the U1 of L)
b | c is M2( the U1 of L)
a | (b | c) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
y is M2( the U1 of L)
b | y is M2( the U1 of L)
y | a is M2( the U1 of L)
y | (c | (c | c)) is M2( the U1 of L)
(y | (c | (c | c))) | (y | (c | (c | c))) is M2( the U1 of L)
((y | (c | (c | c))) | (y | (c | (c | c)))) | b is M2( the U1 of L)
(y | a) | (((y | (c | (c | c))) | (y | (c | (c | c)))) | b) is M2( the U1 of L)
b | ((y | a) | (((y | (c | (c | c))) | (y | (c | (c | c)))) | b)) is M2( the U1 of L)
(y | (c | (c | c))) | (y | a) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
y is M2( the U1 of L)
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
y | (a | (a | a)) is M2( the U1 of L)
(y | (a | (a | a))) | (y | (a | (a | a))) is M2( the U1 of L)
b is M2( the U1 of L)
b | y is M2( the U1 of L)
c is M2( the U1 of L)
y | c is M2( the U1 of L)
y | b is M2( the U1 of L)
(y | c) | (y | b) is M2( the U1 of L)
b | ((y | c) | (y | b)) is M2( the U1 of L)
a is M2( the U1 of L)
c is M2( the U1 of L)
a | c is M2( the U1 of L)
b is M2( the U1 of L)
c | b is M2( the U1 of L)
c | a is M2( the U1 of L)
(c | b) | (c | a) is M2( the U1 of L)
a | ((c | b) | (c | a)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
y is M2( the U1 of L)
b | y is M2( the U1 of L)
y | (c | (c | c)) is M2( the U1 of L)
b | (y | (c | (c | c))) is M2( the U1 of L)
(b | (y | (c | (c | c)))) | a is M2( the U1 of L)
((b | (y | (c | (c | c)))) | a) | b is M2( the U1 of L)
(b | y) | (((b | (y | (c | (c | c)))) | a) | b) is M2( the U1 of L)
(b | y) | (b | (y | (c | (c | c)))) is M2( the U1 of L)
(b | (y | (c | (c | c)))) | (b | y) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
y is M2( the U1 of L)
a | y is M2( the U1 of L)
y | (c | (c | c)) is M2( the U1 of L)
(y | (c | (c | c))) | (y | (c | (c | c))) is M2( the U1 of L)
((y | (c | (c | c))) | (y | (c | (c | c)))) | b is M2( the U1 of L)
a | (((y | (c | (c | c))) | (y | (c | (c | c)))) | b) is M2( the U1 of L)
(a | y) | (a | (((y | (c | (c | c))) | (y | (c | (c | c)))) | b)) is M2( the U1 of L)
a | (y | (c | (c | c))) is M2( the U1 of L)
(a | y) | (a | (y | (c | (c | c)))) is M2( the U1 of L)
(a | (y | (c | (c | c)))) | b is M2( the U1 of L)
((a | (y | (c | (c | c)))) | b) | a is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
a | a is M2( the U1 of L)
a | (a | a) is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
y is M2( the U1 of L)
b | y is M2( the U1 of L)
y | c is M2( the U1 of L)
b | (y | c) is M2( the U1 of L)
(b | y) | (b | (y | c)) is M2( the U1 of L)
y | (a | (a | a)) is M2( the U1 of L)
b | (y | (a | (a | a))) is M2( the U1 of L)
(b | y) | (b | (y | (a | (a | a)))) is M2( the U1 of L)
(y | (a | (a | a))) | (y | (a | (a | a))) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
b is M2( the U1 of L)
y is M2( the U1 of L)
b | y is M2( the U1 of L)
c is M2( the U1 of L)
c | c is M2( the U1 of L)
c | (c | c) is M2( the U1 of L)
y | (c | (c | c)) is M2( the U1 of L)
b | (y | (c | (c | c))) is M2( the U1 of L)
(b | y) | (b | (y | (c | (c | c)))) is M2( the U1 of L)
a is M2( the U1 of L)
y | a is M2( the U1 of L)
b | (y | a) is M2( the U1 of L)
(b | y) | (b | (y | a)) is M2( the U1 of L)
a is M2( the U1 of L)
c is M2( the U1 of L)
a | c is M2( the U1 of L)
b is M2( the U1 of L)
c | b is M2( the U1 of L)
a | (c | b) is M2( the U1 of L)
(a | c) | (a | (c | b)) is M2( the U1 of L)
L is non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr
the U1 of L is V11() set
a is M2( the U1 of L)
b is M2( the U1 of L)
b | a is M2( the U1 of L)
(b | a) | a is M2( the U1 of L)
a | ((b | a) | a) is M2( the U1 of L)
c is M2( the U1 of L)
c | a is M2( the U1 of L)
b | (c | a) is M2( the U1 of L)
(a | ((b | a) | a)) | (b | (c | a)) is M2( the U1 of L)
a | c is M2( the U1 of L)
b | (a | c) is M2( the U1 of L)
(a | ((b | a) | a)) | (b | (a | c)) is M2( the U1 of L)
L is non empty ShefferStr
L is non empty ShefferStr
L is non empty ShefferOrthoLattStr
L is non empty ShefferOrthoLattStr