:: Short {S}heffer Stroke-Based Single Axiom for {B}oolean Algebras
:: by Aneta {\L}ukaszuk and Adam Grabowski
::
:: Received May 31, 2004
:: Copyright (c) 2004-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SHEFFER1, SUBSET_1, RELAT_1, ZFMISC_1, LATTICES,
ROBBINS1, EQREL_1, SHEFFER2;
notations STRUCT_0, LATTICES, ROBBINS1, SHEFFER1;
constructors SHEFFER1;
registrations LATTICES, SHEFFER1, STRUCT_0;
begin :: First Implication
definition
let L be non empty ShefferStr;
attr L is satisfying_Sh_1 means
:: SHEFFER2:def 1
for x, y, z being Element of L holds (x | ((y | x) | x)) | (y | (z | x)) = y;
end;
registration
cluster trivial -> satisfying_Sh_1 for non empty ShefferStr;
end;
registration
cluster satisfying_Sh_1 satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 for non empty ShefferStr;
end;
reserve L for satisfying_Sh_1 non empty ShefferStr;
theorem :: SHEFFER2:1
for x, y, z, u being Element of L holds ((x | (y | z)) | (x | (x
| (y | z)))) | ((z | ((x | z) | z)) | (u | (x | (y | z)))) = z | ((x | z) | z);
theorem :: SHEFFER2:2
for x, y, z being Element of L holds ((x | y) | (((y | ((z | y) |
y)) | (x | y)) | (x | y))) | z = y | ((z | y) | y);
theorem :: SHEFFER2:3
for x, y, z being Element of L holds (x | ((y | x) | x)) | (y | (
z | ((x | z) | z))) = y;
theorem :: SHEFFER2:4
for x, y being Element of L holds x | ((x | ((x | x) | x)) | (y |
(x | ((x | x) | x)))) = x | ((x |x) | x);
theorem :: SHEFFER2:5
for x being Element of L holds x | ((x | x) | x) = x | x;
theorem :: SHEFFER2:6
for x being Element of L holds (x | ((x | x) | x )) | (x | x) = x;
theorem :: SHEFFER2:7
for x, y being Element of L holds (x | x) | (x | (y | x)) = x;
theorem :: SHEFFER2:8
for x, y being Element of L holds (x | (((y | y) | x) | x)) | y = y | y;
theorem :: SHEFFER2:9
for x, y being Element of L holds ((x | y) | (((x | y) | (x | y))
| (x | y))) | ((x | y) | (x | y)) = y | ((((x | y) | (x | y )) | y) | y);
theorem :: SHEFFER2:10
for x, y being Element of L holds x | ((((y | x) | (y | x)) | x
) | x) = y | x;
theorem :: SHEFFER2:11
for x, y being Element of L holds (x | x) | (y | x) = x;
theorem :: SHEFFER2:12
for x, y being Element of L holds x | (y | (x | x)) = x | x;
theorem :: SHEFFER2:13
for x, y being Element of L holds ((x | y) | (x | y)) | y = x | y;
theorem :: SHEFFER2:14
for x, y being Element of L holds x | ((y | x) | x) = y | x;
theorem :: SHEFFER2:15
for x, y, z being Element of L holds (x | y) | (x | (z | y)) = x;
theorem :: SHEFFER2:16
for x, y, z being Element of L holds (x | (y | z)) | (x | z) = x;
theorem :: SHEFFER2:17
for x, y, z being Element of L holds x | ((x | y) | (z | y)) = x | y;
theorem :: SHEFFER2:18
for x, y, z being Element of L holds ((x | (y | z)) | z) | x = x | (y | z);
theorem :: SHEFFER2:19
for x, y being Element of L holds x | ((y | x) | x) = x | y;
theorem :: SHEFFER2:20
for x, y being Element of L holds x | y = y | x;
theorem :: SHEFFER2:21
for x, y being Element of L holds (x | y) | (x | x) = x;
theorem :: SHEFFER2:22
for x, y, z being Element of L holds (x | y) | (y | (z | x)) = y;
theorem :: SHEFFER2:23
for x, y, z being Element of L holds (x | (y | z)) | (z | x) = x;
theorem :: SHEFFER2:24
for x, y, z being Element of L holds (x | y) | (y | (x | z)) = y;
theorem :: SHEFFER2:25
for x, y, z being Element of L holds (x | (y | z)) | (y | x) = x;
theorem :: SHEFFER2:26
for x, y, z being Element of L holds ((x | y) | (x | z)) | z = x | z;
theorem :: SHEFFER2:27
for x, y, z being Element of L holds x | (y | (x | (y | z))) = x | (y | z);
theorem :: SHEFFER2:28
for x, y, z being Element of L holds (x | (y | (x | z))) | y = y | (x | z);
theorem :: SHEFFER2:29
for x, y, z, u being Element of L holds (x | (y | z))| (x | (u |
(y | x))) = (x | (y | z)) | (y | x);
theorem :: SHEFFER2:30
for x, y, z being Element of L holds (x | (y | (x | z))) | y = y | (z | x);
theorem :: SHEFFER2:31
for x, y, z, u being Element of L holds (x | (y | z)) | (x | (u
| (y | x))) = x;
theorem :: SHEFFER2:32
for x, y being Element of L holds x | (y | (x | y)) = x | x;
theorem :: SHEFFER2:33
for x, y, z being Element of L holds x | (y | z) = x | (z | y);
theorem :: SHEFFER2:34
for x, y, z being Element of L holds x | (y | (x | (z | (y | x)) )) = x | x;
theorem :: SHEFFER2:35
for x, y, z being Element of L holds (x | (y | z)) | ((y |x) | x
) = (x | (y | z)) | (x | (y | z));
theorem :: SHEFFER2:36
for x, y being Element of L holds (x | (y | x)) | y = y | y;
theorem :: SHEFFER2:37
for x, y, z being Element of L holds (x | y) | z = z | (y | x);
theorem :: SHEFFER2:38
for x, y, z being Element of L holds x | (y | (z | (x | y))) = x | (y | y);
theorem :: SHEFFER2:39
for x, y, z being Element of L holds ((x | y) | y) | (y | (z | x
)) = (y | (z | x)) | (y | (z | x));
theorem :: SHEFFER2:40
for x, y, z, u being Element of L holds (x | y) | (z | u) = (u | z) | (y | x)
;
theorem :: SHEFFER2:41
for x, y, z being Element of L holds x | (y | ((y | x) | z)) = x | (y | y);
theorem :: SHEFFER2:42
for x, y being Element of L holds x | (y | x) = x | (y | y);
theorem :: SHEFFER2:43
for x, y being Element of L holds (x | y) | y = y | (x | x);
theorem :: SHEFFER2:44
for x, y being Element of L holds x | (y | y) = x | (x | y);
theorem :: SHEFFER2:45
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | y
)) = (x | (z | y)) | (x | (z | y));
theorem :: SHEFFER2:46
for x, y, z being Element of L holds (x | (y | z)) | (x | (y | y
)) = (x | (y | z)) | (x | (y | z));
theorem :: SHEFFER2:47
for x, y, z being Element of L holds x | ((y | y) | (z | (x | (x
| y)))) = x | ((y | y) | (y | y));
theorem :: SHEFFER2:48
for x, y, z being Element of L holds ((x | (y | z)) | (x | (y |
z))) | (y | y) = x | (y | y);
theorem :: SHEFFER2:49
for x, y, z being Element of L holds x | ((y | y) | (z | (x | (x
| y)))) = x | y;
theorem :: SHEFFER2:50
for x, y, z being Element of L holds (((x | y) | (x | y)) | ((z
| ((x | y) | z)) | (x | y))) | (x | x) = (z | ((x | y) | z)) | (x | x);
theorem :: SHEFFER2:51
for x, y, z being Element of L holds (x | ((y | z) | x)) | (y |
y) = (y | z) | (y | y);
theorem :: SHEFFER2:52
for x, y, z being Element of L holds (x | ((y | z) | x)) | (y | y) = y;
theorem :: SHEFFER2:53
for x, y, z being Element of L holds x | ((y | ((x | z) | y)) |
x) = y | ((x | z) | y);
theorem :: SHEFFER2:54
for x, y, z being Element of L holds x | ((y | (y | (z | x))) |
x) = y | ((x | (y | (x | z))) | y);
theorem :: SHEFFER2:55
for x, y, z being Element of L holds x | ((y | (y | (z | x))) |
x) = y | (y | (z | x));
theorem :: SHEFFER2:56
for x, y, z, u being Element of L holds x | (y | (z | (z | (u |
(y | x))))) = x | (y | y);
theorem :: SHEFFER2:57
for x, y, z being Element of L holds x | (y | (y | (z | (x | y))
)) = x | (y | (x | x));
theorem :: SHEFFER2:58
for x, y, z being Element of L holds x | (y | (y | (z | (x | y)) )) = x | x;
theorem :: SHEFFER2:59
for x, y being Element of L holds x | (y | (y | y)) = x | x;
theorem :: SHEFFER2:60
for x, y, z being Element of L holds x | (((y | (z | x)) | (y |
(z | x))) | (z | z)) = x | (y | (z | x));
theorem :: SHEFFER2:61
for x, y, z being Element of L holds x | (y | (z | z)) = x | (y | (z | x));
theorem :: SHEFFER2:62
for x, y, z being Element of L holds x | (y | ((z | z) | x)) = x | (y | z);
theorem :: SHEFFER2:63
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | (
(y | y) | x))) = (x | (z | y)) | (x | (z | y));
theorem :: SHEFFER2:64
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | (
x | (y | y)))) = (x | (z | y)) | (x | (z |y));
theorem :: SHEFFER2:65
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | z
)) = (x | (z | y)) | (x | (z | y));
theorem :: SHEFFER2:66
for x, y, z being Element of L holds ((x | x) | y) | ((z | z) |
y) = (y | (x | z)) | (y | (x | z));
theorem :: SHEFFER2:67
for L being non empty ShefferStr st L is satisfying_Sh_1 holds L
is satisfying_Sheffer_1;
theorem :: SHEFFER2:68
for L being non empty ShefferStr st L is satisfying_Sh_1 holds L
is satisfying_Sheffer_2;
theorem :: SHEFFER2:69
for L being non empty ShefferStr st L is satisfying_Sh_1 holds L
is satisfying_Sheffer_3;
registration
cluster properly_defined Boolean well-complemented Lattice-like de_Morgan
satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 satisfying_Sh_1
for non empty ShefferOrthoLattStr;
end;
registration
cluster satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
properly_defined -> Boolean Lattice-like for
non empty ShefferOrthoLattStr;
cluster Boolean Lattice-like well-complemented properly_defined ->
satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for
non empty
ShefferOrthoLattStr;
end;
begin :: Second Implication
reserve L for satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
non empty ShefferStr;
reserve v,q,p,w,z,y,x for Element of L;
theorem :: SHEFFER2:70
for x,w holds w | ((x | x) | x) = w | w;
theorem :: SHEFFER2:71
for p,x holds x = (x | x) | (p | (p | p));
theorem :: SHEFFER2:72
for y,w holds (w | w) | (w | (y | (y | y))) = w;
theorem :: SHEFFER2:73
for q,p,y,w holds (((w | (y | (y | y))) | p) | ((q | q) | p)) =
((p | (w | q)) | (p | (w | q)));
theorem :: SHEFFER2:74
for q,p,x holds (x | p) | ((q | q) | p) = ((p | ((x | x) | q)) |
(p | ((x | x) | q)));
theorem :: SHEFFER2:75
for w,p,y,q holds (((w | w) | p) | ((q | (y | (y | y))) | p)) =
((p | (w | q)) | (p | (w | q)));
theorem :: SHEFFER2:76
for p,x holds x = (x | x) | ((p | p) | p);
theorem :: SHEFFER2:77
for y,w holds (w | w) | (w | ((y | y) | y)) = w;
theorem :: SHEFFER2:78
for y,w holds ((w | ((y | y) | y)) | (w | w)) = w;
theorem :: SHEFFER2:79
for p,y,w holds ((w | ((y | y) | y)) | (p | (p | p))) = w;
theorem :: SHEFFER2:80
for p,x,y holds (((y | (x | x)) | (y | (x | x))) | (p | (p | p))
) = ((x | x) | y);
theorem :: SHEFFER2:81
for x,y holds y | (x | x) = (x | x) | y;
theorem :: SHEFFER2:82
for y,w holds w | y = ((y | y) | (y | y)) | w;
theorem :: SHEFFER2:83
for y,w holds w | y = y | w;
theorem :: SHEFFER2:84
for x,p holds (p | x) | (p | ((x | x) | (x | x))) = (((x | x) |
(x | x)) | p) | (((x | x) | (x | x)) | p);
theorem :: SHEFFER2:85
for x,p holds (p | x) | (p | x) = (((x | x) | (x | x)) | p) | ((
(x | x) | (x | x)) | p);
theorem :: SHEFFER2:86
for x,p holds (p | x) | (p | x) = (x | p) | (((x | x) | (x | x)) | p);
theorem :: SHEFFER2:87
for x,p holds (p | x) | (p | x) = (x | p) | (x | p);
theorem :: SHEFFER2:88
for y,q,w holds ((w | q) | ((y | y) | y)) | ((w | q) | (w | q))
= ((w | w) | (w | q)) | ((q | q) | (w | q));
theorem :: SHEFFER2:89
for q,w holds w | q = ((w | w) | (w | q)) | ((q | q) | (w | q));
theorem :: SHEFFER2:90
for q,p holds ((p | p) | (p | ((q | q) | q))) = ((((q | q) | (q
| q)) | p) | ((q | q) | p));
theorem :: SHEFFER2:91
for p,q holds p = ((((q | q) | (q | q)) | p) | ((q | q) | p));
theorem :: SHEFFER2:92
for p,q holds p = (q | p) | ((q | q) | p);
theorem :: SHEFFER2:93
for z,w,x holds ((((x | x) | w) | ((z | z) | w)) | ((w | (x | z)
) | (w | (x | z)))) = (((w | w) | (w | (x | z))) | (((x | z) | (x | z)) | (w |
(x | z))));
theorem :: SHEFFER2:94
for z,w,x holds ((((x | x) | w) | ((z | z) | w)) | ((w | (x | z)
) | (w | (x | z)))) = (w | (x | z));
theorem :: SHEFFER2:95
for w,p holds ((p | p) | (p | (w | (w | w)))) = (((w | w) | p) |
(((w | w) | (w | w)) | p));
theorem :: SHEFFER2:96
for p,w holds p = ((w | w) | p) | (((w | w) | (w | w)) | p);
theorem :: SHEFFER2:97
for p,w holds p = (((w | w) | p) | (w | p));
theorem :: SHEFFER2:98
for z,q,x holds ((((x | x) | q) | ((z | z) | q)) | ((q | (x | z)
) | (q | (x | z)))) = ((((z | z) | (z | z)) | ((x | x) | q)) | ((q | q) | ((x |
x) | q)));
theorem :: SHEFFER2:99
for q,z,x holds (q | (x | z)) = ((((z | z) | (z | z)) | ((x | x)
| q)) | ((q | q) | ((x | x) | q)));
theorem :: SHEFFER2:100
for q,z,x holds (q | (x | z)) = ((z | ((x | x) | q)) | ((q | q)
| ((x | x) | q)));
theorem :: SHEFFER2:101
for w,y holds w | w = ((y | y) | y) | w;
theorem :: SHEFFER2:102
for w,p holds ((p | w) | ((w | w) | p)) = p;
theorem :: SHEFFER2:103
for y,w holds ((w | w) | ((w | w) | ((y | y) | y))) = (y | y) | y;
theorem :: SHEFFER2:104
for y,w holds (w | w) | w = (y | y) | y;
theorem :: SHEFFER2:105
for p,w holds (w | p) | (p | (w | w)) = p;
theorem :: SHEFFER2:106
for w,p holds (p | (w | w)) | (w | p) = p;
theorem :: SHEFFER2:107
for p,w holds (w | p) | (w | (p | p)) = w;
theorem :: SHEFFER2:108
for x,y holds (y | (((y | (x | x)) | (y | (x | x))) | (x | y))) = x | y;
theorem :: SHEFFER2:109
for p,w holds (w | (p | p)) | (w | p) = w;
theorem :: SHEFFER2:110
for p,w,q,y holds (((y | y) | y) | q) | ((w | w) | q) = (q | ((
(p | (p | p)) | (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) |
w));
theorem :: SHEFFER2:111
for q,w,p holds (q | q) | ((w | w) | q) = (q | (((p | (p | p))
| (p | (p | p))) | w)) | (q | (((p | (p | p)) | (p | (p | p))) | w));
theorem :: SHEFFER2:112
for w,y,p holds (w | p) | (w | (p | (y | (y | y)))) = w;
theorem :: SHEFFER2:113
for w,y,p holds (w | (p | (y | (y | y)))) | (w | p) = w;
theorem :: SHEFFER2:114
for q,p,y holds (((y | y) | y) | p) | ((q | q) | p) = (p | ((p
| p) | q)) | (p | ((p | p) | q));
theorem :: SHEFFER2:115
for q,z,x holds (((q | ((x | x) | z)) | (q | ((x | x) | z))) |
((x | q) | ((z | z) | q))) = ((((z | z) | (z | z)) | (x | q)) | ((q | q) | (x |
q)));
theorem :: SHEFFER2:116
for q,z,x holds (((q | ((x | x) | z)) | (q | ((x | x) | z))) |
((x | q) | ((z | z) | q))) = ((z | (x | q)) | ((q | q) | (x | q)));
theorem :: SHEFFER2:117
for w,q,z holds (((w | w) | ((z | z) | q)) | ((q | ((q | q) | z
)) | (q | ((q | q) | z)))) = (((z | z) | q) | (w | q)) | (((z | z) | q) | (w |
q));
theorem :: SHEFFER2:118
for q,p,x holds (((p | (x | p)) | (p | (x | p))) | (q | (q | q)
)) = (x | x) | p;
theorem :: SHEFFER2:119
for p,x holds p | (x | p) = (x | x) | p;
theorem :: SHEFFER2:120
for p,y holds (y | p) | ((y | y) | p) = (p | p) | (y | p);
theorem :: SHEFFER2:121
for x,y holds x = (x | x) | (y | x);
theorem :: SHEFFER2:122
for x,y holds (y | x) | x = ((x | (y | y)) | (x | (y | y))) | ( y | x);
theorem :: SHEFFER2:123
for x,z,y holds (((x | ((y | y) | z)) | (x | ((y | y) | z))) |
((y | x) | ((z | z) | x))) = (z | (y | x)) | x;
theorem :: SHEFFER2:124
for x,y,z holds ((x | (((z | (z | z)) | (z | (z | z))) | y)) |
(x | (((z | (z | z)) | (z | (z | z))) | y))) = x;
theorem :: SHEFFER2:125
for x,z,y holds (x | ((y | y) | z)) | z = z | (y | x);
theorem :: SHEFFER2:126
for x,y holds x | ((y | x) | x) = y | x;
theorem :: SHEFFER2:127
for z,y,x holds y = (((x | x) | x) | y) | ((z | z) | y);
theorem :: SHEFFER2:128
for z,y holds (y | ((y | y) | z)) | (y | ((y | y) | z)) = y;
theorem :: SHEFFER2:129
for x,z,y holds (((y | y) | z) | (x | z)) | (((y | y) | z) | (x
| z)) = ((x | x) | ((y | y) | z)) | z;
theorem :: SHEFFER2:130
for x,z,y holds ((((y | y) | z) | (x | z)) | (((y | y) | z) | (
x | z))) = z | (y | (x | x));
theorem :: SHEFFER2:131
for y,x holds ((x | y) | (x | y)) | x = x | y;
theorem :: SHEFFER2:132
for p,w holds (w | w) | (w | p) = w;
theorem :: SHEFFER2:133
for w,p holds (p | w) | (w | w) = w;
theorem :: SHEFFER2:134
for p,y,w holds (w | (y | (y | y))) | (w | p) = w;
theorem :: SHEFFER2:135
for p,w holds ((w | p) | (w | w)) = w;
theorem :: SHEFFER2:136
for y,p,w holds (w | p) | (w | (y | (y | y))) = w;
theorem :: SHEFFER2:137
for p,q,w,y,x holds ((((x | (y | (y | y))) | w) | ((q | q) | w)
) | ((w | (x | q)) | (w | (x | q)))) = (((w | (p | (p | p))) | (w | (x | q))) |
(((x | q) | (x | q)) | (w | (x | q))));
theorem :: SHEFFER2:138
for q,w,y,x holds ((((x | (y | (y | y))) | w) | ((q | q) | w))
| ((w | (x | q)) | (w | (x | q)))) = (w | (((x | q) | (x | q)) | (w | (x | q)))
);
theorem :: SHEFFER2:139
for q,w,y,x holds (((x | (y | (y | y))) | w) | ((q | q) | w)) |
((w | (x | q)) | (w | (x | q))) = w | (x | q);
theorem :: SHEFFER2:140
for z,p,q,y,x holds ((((x | (y | (y | y))) | q) | ((z | z) | q)
) | ((q | (x | z)) | (q | (x | z)))) = ((((z | z) | (p | (p | p))) | ((x | (y |
(y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q)));
theorem :: SHEFFER2:141
for z,p,q,y,x holds q | (x | z) = (((z | z) | (p | (p | p))) |
((x | (y | (y | y))) | q)) | ((q | q) | ((x | (y | (y | y))) | q));
theorem :: SHEFFER2:142
for z,q,y,x holds q | (x | z) = (z | ((x | (y | (y | y))) | q))
| ((q | q) | ((x | (y | (y | y))) | q));
theorem :: SHEFFER2:143
for v,p,y,x holds p | (x | v) = (v | ((x | (y | (y | y))) | p)) | p;
theorem :: SHEFFER2:144
for y,w,z,v,x holds ((w | (z | (x | v))) | (((x | (y | (y | y))
) | z) | ((v | v) | z))) = z | (x | v);
theorem :: SHEFFER2:145
for y,z,x holds ((y | ((x | x) | z)) | (y | ((x | x) | z))) | (
(x | y) | ((z | z) | y)) = y | ((x | x) | z);
theorem :: SHEFFER2:146
for z,y,x holds (z | (x | y)) | y = y | ((x | x) | z);
theorem :: SHEFFER2:147
for x,w,y,z holds ((((x | x) | w) | ((z | (y | (y | y))) | w))
| w) = w | (x | z);
theorem :: SHEFFER2:148
for z,w,x holds (w | (z | ((x | x) | w))) = w | (x | z);
theorem :: SHEFFER2:149
for p,z,y,x holds (((z | (x | p)) | (z | (x | p))) | (((x | (y
| (y | y))) | z) | ((p | p) | z))) = ((((p | p) | z) | ((x | (y | (y | y))) | z
)) | (((p | p) | z) | ((x | (y | (y | y))) | z)));
theorem :: SHEFFER2:150
for p,z,y,x holds (z | (x | p)) = ((((p | p) | z) | ((x | (y |
(y | y))) | z)) | (((p | p) | z) | ((x | (y | (y | y))) | z)));
theorem :: SHEFFER2:151
for z,p,y,x holds z | (x | p) = z | (p | ((x | (y | (y | y))) |
(x | (y | (y | y)))));
theorem :: SHEFFER2:152
for z,p,x holds z | (x | p) = z | (p | x);
theorem :: SHEFFER2:153
for w,q,p holds (p | q) | w = w | (q | p);
theorem :: SHEFFER2:154
for w,p,q holds ((q | p) | w) | q = q | ((p | p) | w);
theorem :: SHEFFER2:155
for z,w,y,x holds w | x = (w | ((x | z) | (((x | (y | (y | y)))
| (x | (y | (y | y)))) | w)));
theorem :: SHEFFER2:156
for w,z,x holds w | x = w | ((x | z) | (x | w));
theorem :: SHEFFER2:157
for q,x,z,y holds ((x | y) | (((x | (y | (z | (z | z)))) | q) |
x)) = ((x | y) | (x | (y | (z | (z | z)))));
theorem :: SHEFFER2:158
for x,q,z,y holds ((x | y) | (x | (((y | (z | (z | z))) | (y |
(z | (z | z)))) | q))) = ((x | y) | (x | (y | (z | (z | z)))));
theorem :: SHEFFER2:159
for z,x,q,y holds (x | y) | (x | (y | q)) = ((x | y) | (x | (y
| (z | (z | z)))));
theorem :: SHEFFER2:160
for x,q,y holds (x | y) | (x | (y | q)) = x;
theorem :: SHEFFER2:161
L is satisfying_Sh_1;
registration
cluster satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ->
satisfying_Sh_1 for non empty ShefferStr;
cluster satisfying_Sh_1 -> satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 for non empty ShefferStr;
end;
registration
cluster satisfying_Sh_1 properly_defined -> Boolean Lattice-like for
non empty
ShefferOrthoLattStr;
cluster Boolean Lattice-like well-complemented properly_defined ->
satisfying_Sh_1 for non empty ShefferOrthoLattStr;
end;