:: 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