:: 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-2017 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;
theorems ROBBINS1, SHEFFER1, STRUCT_0;
begin :: First Implication
definition
let L be non empty ShefferStr;
attr L is satisfying_Sh_1 means
:Def1:
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;
coherence
by STRUCT_0:def 10;
end;
registration
cluster satisfying_Sh_1 satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 for non empty ShefferStr;
existence
proof
take TrivShefferOrthoLattStr;
thus thesis;
end;
end;
reserve L for satisfying_Sh_1 non empty ShefferStr;
theorem Th1:
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)
proof
let x, y, z, u be Element of L;
set Y = z | ((x | z) | z);
set X = x | (y | z);
(X | ((Y | X) | X)) | (Y | (u | X)) = Y by Def1;
hence thesis by Def1;
end;
theorem Th2:
for x, y, z being Element of L holds ((x | y) | (((y | ((z | y) |
y)) | (x | y)) | (x | y))) | z = y | ((z | y) | y)
proof
let x, y, z be Element of L;
set X = x | y;
set Y = y | ((z | y) | y);
(X | ((Y | X) | X)) | (Y | (z | X)) = Y by Def1;
hence thesis by Def1;
end;
theorem Th3:
for x, y, z being Element of L holds (x | ((y | x) | x)) | (y | (
z | ((x | z) | z))) = y
proof
let x, y, z be Element of L;
set X = (x | z);
set Y = (z | ((x | z) | z));
(X | ((Y | X) | X)) | x = Y by Th2;
hence thesis by Def1;
end;
theorem Th4:
for x, y being Element of L holds x | ((x | ((x | x) | x)) | (y |
(x | ((x | x) | x)))) = x | ((x |x) | x)
proof
let x be Element of L;
(x | ((x | x) | x)) | (x | (x | ((x | x) | x))) = x by Th3;
hence thesis by Th1;
end;
theorem Th5:
for x being Element of L holds x | ((x | x) | x) = x | x
proof
let x be Element of L;
(x | ((x | x) | x)) | (x | (x | ((x | x) | x))) = x by Th3;
hence thesis by Th4;
end;
theorem Th6:
for x being Element of L holds (x | ((x | x) | x )) | (x | x) = x
proof
let x be Element of L;
x | ((x | x) | x) = x | x by Th5;
hence thesis by Def1;
end;
theorem Th7:
for x, y being Element of L holds (x | x) | (x | (y | x)) = x
proof
let x, y be Element of L;
x | ((x | x) | x) = x | x by Th5;
hence thesis by Def1;
end;
theorem Th8:
for x, y being Element of L holds (x | (((y | y) | x) | x)) | y = y | y
proof
let x, y be Element of L;
set Y = y | y;
set X = x | y;
Y | (y | (X | y)) = y by Th7;
hence thesis by Th3;
end;
theorem Th9:
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)
proof
let x, y be Element of L;
y | ((((x | y) | (x | y)) | y) | y) | (x | y) = (x | y) | (x | y) by Th8;
hence thesis by Th2;
end;
theorem Th10:
for x, y being Element of L holds x | ((((y | x) | (y | x)) | x
) | x) = y | x
proof
let x, y be Element of L;
((y | x) | (((y | x) | (y | x)) | (y | x))) |((y | x) | (y | x)) = y | x
by Th6;
hence thesis by Th9;
end;
theorem Th11:
for x, y being Element of L holds (x | x) | (y | x) = x
proof
let x, y be Element of L;
set Y = y | x;
x | (((Y | Y) | x) | x) = Y by Th10;
hence thesis by Th7;
end;
theorem Th12:
for x, y being Element of L holds x | (y | (x | x)) = x | x
proof
let x, y be Element of L;
set Y = (x | x);
Y | (x | x) = x by Th11;
hence thesis by Th11;
end;
theorem Th13:
for x, y being Element of L holds ((x | y) | (x | y)) | y = x | y
proof
let x, y be Element of L;
(y | y) | (x | y) = y by Th11;
hence thesis by Th11;
end;
theorem Th14:
for x, y being Element of L holds x | ((y | x) | x) = y | x
proof
let x, y be Element of L;
((y | x) | (y | x)) | x = y | x by Th13;
hence thesis by Th10;
end;
theorem Th15:
for x, y, z being Element of L holds (x | y) | (x | (z | y)) = x
proof
let x, y, z be Element of L;
y | ((x | y) | y) = x | y by Th14;
hence thesis by Def1;
end;
theorem Th16:
for x, y, z being Element of L holds (x | (y | z)) | (x | z) = x
proof
let x, y, z be Element of L;
(z | z) | (y | z) = z by Th11;
hence thesis by Th15;
end;
theorem Th17:
for x, y, z being Element of L holds x | ((x | y) | (z | y)) = x | y
proof
let x, y, z be Element of L;
(x | y) | (x | (z | y)) = x by Th15;
hence thesis by Th16;
end;
theorem Th18:
for x, y, z being Element of L holds ((x | (y | z)) | z) | x = x | (y | z)
proof
let x, y, z be Element of L;
set X = y | z;
(x | X) | (x | z) = x by Th16;
hence thesis by Th15;
end;
theorem Th19:
for x, y being Element of L holds x | ((y | x) | x) = x | y
proof
let x, y be Element of L;
(x | ((y | x) | x)) | (y | ((y | x) | x)) = y by Def1;
hence thesis by Th17;
end;
theorem Th20:
for x, y being Element of L holds x | y = y | x
proof
let x, y be Element of L;
x | ((y | x) | x) = y | x by Th14;
hence thesis by Th19;
end;
theorem Th21:
for x, y being Element of L holds (x | y) | (x | x) = x
proof
let x, y be Element of L;
set X = x | y;
x | ((y | x) | x) = X by Th19;
hence thesis by Th16;
end;
theorem Th22:
for x, y, z being Element of L holds (x | y) | (y | (z | x)) = y
proof
let x, y, z be Element of L;
set Y = x | ((y | x) | x);
Y = x | y by Th19;
hence thesis by Def1;
end;
theorem Th23:
for x, y, z being Element of L holds (x | (y | z)) | (z | x) = x
proof
let x, y, z be Element of L;
z | x = x | z by Th20;
hence thesis by Th16;
end;
theorem Th24:
for x, y, z being Element of L holds (x | y) | (y | (x | z)) = y
proof
let x, y, z be Element of L;
z | x = x | z by Th20;
hence thesis by Th22;
end;
theorem Th25:
for x, y, z being Element of L holds (x | (y | z)) | (y | x) = x
proof
let x, y, z be Element of L;
z | y = y | z by Th20;
hence thesis by Th23;
end;
theorem Th26:
for x, y, z being Element of L holds ((x | y) | (x | z)) | z = x | z
proof
let x, y, z be Element of L;
(x | z) | (z | (x | y)) = z by Th24;
hence thesis by Th22;
end;
theorem Th27:
for x, y, z being Element of L holds x | (y | (x | (y | z))) = x | (y | z)
proof
let x, y, z be Element of L;
set Y = y | x;
(x | (y | z)) | Y = x by Th25;
hence thesis by Th25;
end;
theorem Th28:
for x, y, z being Element of L holds (x | (y | (x | z))) | y = y | (x | z)
proof
let x, y, z be Element of L;
set Y = y | (x | z);
Y | (x | y) = y by Th25;
hence thesis by Th24;
end;
theorem Th29:
for x, y, z, u being Element of L holds (x | (y | z))| (x | (u |
(y | x))) = (x | (y | z)) | (y | x)
proof
let x, y, z, u be Element of L;
set X = x | (y | z);
set Y = y | x;
X | Y = x by Th25;
hence thesis by Th17;
end;
theorem Th30:
for x, y, z being Element of L holds (x | (y | (x | z))) | y = y | (z | x)
proof
let x, y, z be Element of L;
z | x = x | z by Th20;
hence thesis by Th28;
end;
theorem Th31:
for x, y, z, u being Element of L holds (x | (y | z)) | (x | (u
| (y | x))) = x
proof
let x, y, z be Element of L;
(x | (y | z)) | (y | x) = x by Th25;
hence thesis by Th29;
end;
theorem Th32:
for x, y being Element of L holds x | (y | (x | y)) = x | x
proof
let x, y be Element of L;
(x | y) | (x | ((x | y) | y)) = x by Th15;
hence thesis by Th30;
end;
theorem Th33:
for x, y, z being Element of L holds x | (y | z) = x | (z | y)
proof
let x, y, z be Element of L;
(z | (x | (z | y))) | x = x | (z | y) by Th28;
hence thesis by Th30;
end;
theorem Th34:
for x, y, z being Element of L holds x | (y | (x | (z | (y | x)) )) = x | x
proof
let x, y, z be Element of L;
(x | (y | (x | (z | (y | x))))) | (x | (z | (y | x))) = x by Th31;
hence thesis by Th18;
end;
theorem Th35:
for x, y, z being Element of L holds (x | (y | z)) | ((y |x) | x
) = (x | (y | z)) | (x | (y | z))
proof
let x, y, z be Element of L;
set X = x | (y | z);
X | (y | x) = x by Th25;
hence thesis by Th32;
end;
theorem Th36:
for x, y being Element of L holds (x | (y | x)) | y = y | y
proof
let x, y be Element of L;
set X = x;
set Y = y;
Y | (X | (Y | X)) = (X | (Y | X)) | Y by Th20;
hence thesis by Th32;
end;
theorem Th37:
for x, y, z being Element of L holds (x | y) | z = z | (y | x)
proof
let x, y, z be Element of L;
set X = x | y;
X | z = z | X by Th20;
hence thesis by Th33;
end;
theorem Th38:
for x, y, z being Element of L holds x | (y | (z | (x | y))) = x | (y | y)
proof
let x, y, z be Element of L;
set Y = z;
y | (x | (y | (Y | (x | y)))) = y | y by Th34;
hence thesis by Th27;
end;
theorem Th39:
for x, y, z being Element of L holds ((x | y) | y) | (y | (z | x
)) = (y | (z | x)) | (y | (z | x))
proof
let x, y, z be Element of L;
set X = y | (z | x);
X | (x | y) = y by Th23;
hence thesis by Th36;
end;
theorem Th40:
for x, y, z, u being Element of L holds (x | y) | (z | u) = (u | z) | (y | x)
proof
let x, y, z, u be Element of L;
(x | y) | (z | u) = (x | y) | (u | z) by Th33;
hence thesis by Th37;
end;
theorem Th41:
for x, y, z being Element of L holds x | (y | ((y | x) | z)) = x | (y | y)
proof
let x, y, z be Element of L;
x | (y | (z | (x | y))) = x | (y | ((y | x) | z)) by Th37;
hence thesis by Th38;
end;
theorem Th42:
for x, y being Element of L holds x | (y | x) = x | (y | y)
proof
let x, y be Element of L;
set Y = x | (y | y);
Y | (x | y) = x by Th16;
hence thesis by Th38;
end;
theorem Th43:
for x, y being Element of L holds (x | y) | y = y | (x | x)
proof
let x, y be Element of L;
set X = x;
set Y = y;
Y | (X | Y) = (X | Y) | Y by Th20;
hence thesis by Th42;
end;
theorem Th44:
for x, y being Element of L holds x | (y | y) = x | (x | y)
proof
let x, y be Element of L;
x | (y | x) = x | (y | y) by Th42;
hence thesis by Th33;
end;
theorem Th45:
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | y
)) = (x | (z | y)) | (x | (z | y))
proof
let x, y, z be Element of L;
set Y = y;
set X = x;
(Y | X) | X = X | (Y | Y) by Th43;
hence thesis by Th39;
end;
theorem Th46:
for x, y, z being Element of L holds (x | (y | z)) | (x | (y | y
)) = (x | (y | z)) | (x | (y | z))
proof
let x, y, z be Element of L;
(x | (y | z)) | ((y |x) | x) = (x | (y | z)) | (x | (y | y)) by Th43;
hence thesis by Th35;
end;
theorem Th47:
for x, y, z being Element of L holds x | ((y | y) | (z | (x | (x
| y)))) = x | ((y | y) | (y | y))
proof
let x, y, z be Element of L;
x | (y | y) = x | (x | y) by Th44;
hence thesis by Th38;
end;
theorem Th48:
for x, y, z being Element of L holds ((x | (y | z)) | (x | (y |
z))) | (y | y) = x | (y | y)
proof
let x, y, z be Element of L;
set Z = (y | y);
set Y = (y | z);
(x | Y) | (x | Y) = (x | Y) | (x | Z) by Th46;
hence thesis by Th26;
end;
theorem Th49:
for x, y, z being Element of L holds x | ((y | y) | (z | (x | (x
| y)))) = x | y
proof
let x, y, z be Element of L;
(y | y) | (y | y) = y by Th21;
hence thesis by Th47;
end;
theorem Th50:
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)
proof
let x, y, z be Element of L;
set Y = z;
set X = x | y;
(Y | (X | Y)) | X = X | X by Th36;
hence thesis by Th48;
end;
theorem Th51:
for x, y, z being Element of L holds (x | ((y | z) | x)) | (y |
y) = (y | z) | (y | y)
proof
let x, y, z be Element of L;
set Y = y | z;
set X = x | ((y | z) | x);
(Y | Y) | (X | Y) = Y by Th11;
hence thesis by Th50;
end;
theorem Th52:
for x, y, z being Element of L holds (x | ((y | z) | x)) | (y | y) = y
proof
let x, y, z be Element of L;
(y | z) | (y | y) = y by Th21;
hence thesis by Th51;
end;
theorem Th53:
for x, y, z being Element of L holds x | ((y | ((x | z) | y)) |
x) = y | ((x | z) | y)
proof
let x, y, z be Element of L;
(y | ((x | z) | y)) | (x | x) = x by Th52;
hence thesis by Th16;
end;
theorem Th54:
for x, y, z being Element of L holds x | ((y | (y | (z | x))) |
x) = y | ((x | (y | (x | z))) | y)
proof
let x, y, z be Element of L;
set Z = y | (x | z);
(x | Z) | y = y | (z | x) by Th30;
hence thesis by Th53;
end;
theorem Th55:
for x, y, z being Element of L holds x | ((y | (y | (z | x))) |
x) = y | (y | (z | x))
proof
let x, y, z be Element of L;
y | (z | x) = (x | (y | (x | z))) | y by Th30;
hence thesis by Th54;
end;
theorem Th56:
for x, y, z, u being Element of L holds x | (y | (z | (z | (u |
(y | x))))) = x | (y | y)
proof
let x, y, z, u be Element of L;
(y | x) | (z | (z | (u | (y | x))) | (y | x)) = z | (z | (u | (y | x)))
by Th55;
hence thesis by Th41;
end;
theorem Th57:
for x, y, z being Element of L holds x | (y | (y | (z | (x | y))
)) = x | (y | (x | x))
proof
let x, y, z be Element of L;
y | (x | (y | (y | (z | (x | y))))) = y | (x | x) by Th56;
hence thesis by Th27;
end;
theorem Th58:
for x, y, z being Element of L holds x | (y | (y | (z | (x | y)) )) = x | x
proof
let x, y, z be Element of L;
x | (y | (x | x)) = x | x by Th12;
hence thesis by Th57;
end;
theorem Th59:
for x, y being Element of L holds x | (y | (y | y)) = x | x
proof
let x, y be Element of L;
set Y = y | (x | y);
Y | (x | y) = y by Th25;
hence thesis by Th58;
end;
theorem Th60:
for x, y, z being Element of L holds x | (((y | (z | x)) | (y |
(z | x))) | (z | z)) = x | (y | (z | x))
proof
let x, y, z be Element of L;
set Y = y | (z | x);
z | (x | (x | Y)) = z | z by Th58;
hence thesis by Th49;
end;
theorem Th61:
for x, y, z being Element of L holds x | (y | (z | z)) = x | (y | (z | x))
proof
let x, y, z be Element of L;
(y | (z | x)) | (y | (z | x)) | (z | z) = y | (z | z) by Th48;
hence thesis by Th60;
end;
theorem Th62:
for x, y, z being Element of L holds x | (y | ((z | z) | x)) = x | (y | z)
proof
let x, y, z be Element of L;
set X = z | z;
X | (z | z) = z by Th21;
hence thesis by Th61;
end;
theorem Th63:
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | (
(y | y) | x))) = (x | (z | y)) | (x | (z | y))
proof
let x, y, z be Element of L;
(x | (z | ((y | y) | x))) = (x | (z | y)) by Th62;
hence thesis by Th45;
end;
theorem Th64:
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | (
x | (y | y)))) = (x | (z | y)) | (x | (z |y))
proof
let x, y, z be Element of L;
x | (y | y) = (y | y) | x by Th37;
hence thesis by Th63;
end;
theorem Th65:
for x, y, z being Element of L holds (x | (y | y)) | (x | (z | z
)) = (x | (z | y)) | (x | (z | y))
proof
let x, y, z be Element of L;
set X = x | (y | y);
(x | (y | y)) | (x | (z | z)) = (x | (y | y)) | (x | (z | X)) by Th61;
hence thesis by Th64;
end;
theorem Th66:
for x, y, z being Element of L holds ((x | x) | y) | ((z | z) |
y) = (y | (x | z)) | (y | (x | z))
proof
let x, y, z be Element of L;
(y | (z | z)) | (y | (x | x)) = ((x | x) | y) | ((z | z) | y) by Th40;
hence thesis by Th65;
end;
theorem Th67:
for L being non empty ShefferStr st L is satisfying_Sh_1 holds L
is satisfying_Sheffer_1
proof
let L be non empty ShefferStr;
assume L is satisfying_Sh_1;
then for x being Element of L holds (x | x) | (x | x) = x by Th21;
hence thesis by SHEFFER1:def 13;
end;
theorem Th68:
for L being non empty ShefferStr st L is satisfying_Sh_1 holds L
is satisfying_Sheffer_2
proof
let L be non empty ShefferStr;
assume L is satisfying_Sh_1;
then for x, y being Element of L holds x | (y | (y | y)) = x | x by Th59;
hence thesis by SHEFFER1:def 14;
end;
theorem Th69:
for L being non empty ShefferStr st L is satisfying_Sh_1 holds L
is satisfying_Sheffer_3
proof
let L be non empty ShefferStr;
assume L is satisfying_Sh_1;
then
for x, y, z being Element of L holds (x | (y | z)) | (x | (y | z)) = ((y
| y) | x) | ((z | z) | x) by Th66;
hence thesis by SHEFFER1:def 15;
end;
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;
existence
proof
take TrivShefferOrthoLattStr;
for x, y being Element of TrivShefferOrthoLattStr holds x "/\" y = (x`
"\/" y`)` by STRUCT_0:def 10;
hence thesis by ROBBINS1:def 23;
end;
end;
registration
cluster satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3
properly_defined -> Boolean Lattice-like for
non empty ShefferOrthoLattStr;
coherence by SHEFFER1:37;
cluster Boolean Lattice-like well-complemented properly_defined ->
satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for
non empty
ShefferOrthoLattStr;
coherence by SHEFFER1:26,27,28;
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 Th70:
for x,w holds w | ((x | x) | x) = w | w
proof
let x,w;
(x | x) | (x | x) = x by SHEFFER1:def 13;
hence thesis by SHEFFER1:def 14;
end;
theorem Th71:
for p,x holds x = (x | x) | (p | (p | p))
proof
let p,x;
(x | x) | (x | x) = x by SHEFFER1:def 13;
hence thesis by SHEFFER1:def 14;
end;
theorem Th72:
for y,w holds (w | w) | (w | (y | (y | y))) = w
proof
let y,w;
w | w = w | (y | (y | y)) by SHEFFER1:def 14;
hence thesis by SHEFFER1:def 13;
end;
theorem Th73:
for q,p,y,w holds (((w | (y | (y | y))) | p) | ((q | q) | p)) =
((p | (w | q)) | (p | (w | q)))
proof
let q,p,y,w;
(w | w) = (w | (y | (y | y))) by SHEFFER1:def 14;
hence thesis by SHEFFER1:def 15;
end;
theorem Th74:
for q,p,x holds (x | p) | ((q | q) | p) = ((p | ((x | x) | q)) |
(p | ((x | x) | q)))
proof
let q,p,x;
(x | x) | (x | x) = x by SHEFFER1:def 13;
hence thesis by SHEFFER1:def 15;
end;
theorem Th75:
for w,p,y,q holds (((w | w) | p) | ((q | (y | (y | y))) | p)) =
((p | (w | q)) | (p | (w | q)))
proof
let w,p,y,q;
q | q = q | (y | (y | y)) by SHEFFER1:def 14;
hence thesis by SHEFFER1:def 15;
end;
theorem Th76:
for p,x holds x = (x | x) | ((p | p) | p)
proof
let p,x;
(x | x) | (x | x) = x by SHEFFER1:def 13;
hence thesis by Th70;
end;
theorem Th77:
for y,w holds (w | w) | (w | ((y | y) | y)) = w
proof
let y,w;
w | w = w | ((y | y) | y) by Th70;
hence thesis by SHEFFER1:def 13;
end;
theorem Th78:
for y,w holds ((w | ((y | y) | y)) | (w | w)) = w
proof
let y,w;
w | w = w | ((y | y) | y) by Th70;
hence thesis by SHEFFER1:def 13;
end;
theorem Th79:
for p,y,w holds ((w | ((y | y) | y)) | (p | (p | p))) = w
proof
let p,y,w;
w | w = (w | ((y | y) | y)) by Th70;
hence thesis by Th71;
end;
theorem Th80:
for p,x,y holds (((y | (x | x)) | (y | (x | x))) | (p | (p | p))
) = ((x | x) | y)
proof
let p,x,y;
(((x | x) | y) | ((x | x) | y)) = ((y | (x | x)) | (y | (x | x))) by
SHEFFER1:def 15;
hence thesis by Th71;
end;
theorem Th81:
for x,y holds y | (x | x) = (x | x) | y
proof
now
let p,x,y;
(((y | (x | x)) | (y | (x | x))) | (p | (p | p))) = y | (x | x) by Th71;
hence y | (x | x) = (x | x) | y by Th80;
end;
hence thesis;
end;
theorem Th82:
for y,w holds w | y = ((y | y) | (y | y)) | w
proof
let y,w;
(y | y) | (y | y) = y by SHEFFER1:def 13;
hence thesis by Th81;
end;
theorem Th83:
for y,w holds w | y = y | w
proof
let y,w;
(y | y) | (y | y) = y by SHEFFER1:def 13;
hence thesis by Th82;
end;
theorem Th84:
for x,p holds (p | x) | (p | ((x | x) | (x | x))) = (((x | x) |
(x | x)) | p) | (((x | x) | (x | x)) | p)
proof
let x,p;
(x | x) | (x | x) = x by SHEFFER1:def 13;
hence thesis by SHEFFER1:def 15;
end;
theorem Th85:
for x,p holds (p | x) | (p | x) = (((x | x) | (x | x)) | p) | ((
(x | x) | (x | x)) | p)
proof
let x,p;
(x | x) | (x | x) = x by SHEFFER1:def 13;
hence thesis by Th84;
end;
theorem Th86:
for x,p holds (p | x) | (p | x) = (x | p) | (((x | x) | (x | x)) | p)
proof
let x,p;
(x | x) | (x | x) = x by SHEFFER1:def 13;
hence thesis by Th85;
end;
theorem Th87:
for x,p holds (p | x) | (p | x) = (x | p) | (x | p)
proof
let x,p;
(x | x) | (x | x) = x by SHEFFER1:def 13;
hence thesis by Th86;
end;
theorem Th88:
for y,q,w holds ((w | q) | ((y | y) | y)) | ((w | q) | (w | q))
= ((w | w) | (w | q)) | ((q | q) | (w | q))
proof
let y,q,w;
(w | q) | (w | q) = (w | q) | ((y | y) | y) by Th70;
hence thesis by SHEFFER1:def 15;
end;
theorem Th89:
for q,w holds w | q = ((w | w) | (w | q)) | ((q | q) | (w | q))
proof
now
let y,q,w;
(((w | q) | ((y | y) | y)) | ((w | q) | (w | q))) = (w | q) by Th78;
hence w | q = ((w | w) | (w | q)) | ((q | q) | (w | q)) by Th88;
end;
hence thesis;
end;
theorem Th90:
for q,p holds ((p | p) | (p | ((q | q) | q))) = ((((q | q) | (q
| q)) | p) | ((q | q) | p))
proof
let q,p;
p | ((q | q) | q) = p | p by Th70;
hence thesis by SHEFFER1:def 15;
end;
theorem Th91:
for p,q holds p = ((((q | q) | (q | q)) | p) | ((q | q) | p))
proof
let p,q;
(p | p) | (p | ((q | q) | q)) = p by Th77;
hence thesis by Th90;
end;
theorem Th92:
for p,q holds p = (q | p) | ((q | q) | p)
proof
let p,q;
(q | q) | (q | q) = q by SHEFFER1:def 13;
hence thesis by Th91;
end;
theorem Th93:
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))))
proof
let z,w,x;
((w | (x | z)) | (w | (x | z))) = (((x | x) | w) | ((z | z) | w)) by
SHEFFER1:def 15;
hence thesis by SHEFFER1:def 15;
end;
theorem Th94:
for z,w,x holds ((((x | x) | w) | ((z | z) | w)) | ((w | (x | z)
) | (w | (x | z)))) = (w | (x | z))
proof
let z,w,x;
(((w | w) | (w | (x | z))) | (((x | z) | (x | z)) | (w | (x | z)))) = (w
| (x | z)) by Th89;
hence thesis by Th93;
end;
theorem Th95:
for w,p holds ((p | p) | (p | (w | (w | w)))) = (((w | w) | p) |
(((w | w) | (w | w)) | p))
proof
let w,p;
p | (w | (w | w)) = p | p by SHEFFER1:def 14;
hence thesis by SHEFFER1:def 15;
end;
theorem Th96:
for p,w holds p = ((w | w) | p) | (((w | w) | (w | w)) | p)
proof
let p,w;
(p | p) | (p | (w | (w | w))) = p by Th72;
hence thesis by Th95;
end;
theorem Th97:
for p,w holds p = (((w | w) | p) | (w | p))
proof
let p,w;
(w | w) | (w | w) = w by SHEFFER1:def 13;
hence thesis by Th96;
end;
theorem Th98:
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)))
proof
let z,q,x;
(((x | x) | q) | ((z | z) | q)) = ((q | (x | z)) | (q | (x | z))) by
SHEFFER1:def 15;
hence thesis by SHEFFER1:def 15;
end;
theorem Th99:
for q,z,x holds (q | (x | z)) = ((((z | z) | (z | z)) | ((x | x)
| q)) | ((q | q) | ((x | x) | q)))
proof
let q,z,x;
((((x | x) | q) | ((z | z) | q)) | ((q | (x | z)) | (q | (x | z)))) = (q
| (x | z)) by Th94;
hence thesis by Th98;
end;
theorem Th100:
for q,z,x holds (q | (x | z)) = ((z | ((x | x) | q)) | ((q | q)
| ((x | x) | q)))
proof
let q,z,x;
(z | z) | (z | z) = z by SHEFFER1:def 13;
hence thesis by Th99;
end;
theorem Th101:
for w,y holds w | w = ((y | y) | y) | w
proof
let w,y;
w | ((y | y) | y) = w | w by Th70;
hence thesis by Th83;
end;
theorem Th102:
for w,p holds ((p | w) | ((w | w) | p)) = p
proof
let w,p;
w | p = p | w by Th83;
hence thesis by Th92;
end;
theorem Th103:
for y,w holds ((w | w) | ((w | w) | ((y | y) | y))) = (y | y) | y
proof
let y,w;
w | ((y | y) | y) = w | w by Th70;
hence thesis by Th92;
end;
theorem Th104:
for y,w holds (w | w) | w = (y | y) | y
proof
let y,w;
(w | w) | ((y | y) | y) = w by Th76;
hence thesis by Th103;
end;
theorem Th105:
for p,w holds (w | p) | (p | (w | w)) = p
proof
let p,w;
(w | w) | p = p | (w | w) by Th83;
hence thesis by Th92;
end;
theorem Th106:
for w,p holds (p | (w | w)) | (w | p) = p
proof
let w,p;
(w | w) | p = p | (w | w) by Th83;
hence thesis by Th97;
end;
theorem Th107:
for p,w holds (w | p) | (w | (p | p)) = w
proof
let p,w;
(p | p) | w = w | (p | p) by Th83;
hence thesis by Th102;
end;
theorem Th108:
for x,y holds (y | (((y | (x | x)) | (y | (x | x))) | (x | y))) = x | y
proof
let x,y;
(x | y) | (y | (x | x)) = y by Th105;
hence thesis by Th102;
end;
theorem Th109:
for p,w holds (w | (p | p)) | (w | p) = w
proof
let p,w;
p | w = w | p by Th83;
hence thesis by Th106;
end;
theorem Th110:
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))
proof
let p,w,q,y;
(((p | (p | p)) | (p | (p | p))) | (p | (p | p))) = (y | y) | y by Th104;
hence thesis by Th73;
end;
theorem Th111:
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))
proof
let q,w,p;
(((p | (p | p)) | (p | (p | p))) | (p | (p | p))) | q = q | q by Th101;
hence thesis by Th73;
end;
theorem Th112:
for w,y,p holds (w | p) | (w | (p | (y | (y | y)))) = w
proof
let w,y,p;
p | p = p | (y | (y | y)) by SHEFFER1:def 14;
hence thesis by Th107;
end;
theorem Th113:
for w,y,p holds (w | (p | (y | (y | y)))) | (w | p) = w
proof
let w,y,p;
p | p = p | (y | (y | y)) by SHEFFER1:def 14;
hence thesis by Th109;
end;
theorem Th114:
for q,p,y holds (((y | y) | y) | p) | ((q | q) | p) = (p | ((p
| p) | q)) | (p | ((p | p) | q))
proof
let q,p,y;
p | p = ((y | y) | y) | p by Th101;
hence thesis by Th74;
end;
theorem Th115:
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)))
proof
let q,z,x;
((x | q) | ((z | z) | q)) = ((q | ((x | x) | z)) | (q | ((x | x) | z)))
by Th74;
hence thesis by SHEFFER1:def 15;
end;
theorem Th116:
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)))
proof
let q,z,x;
(z | z) | (z | z) = z by SHEFFER1:def 13;
hence thesis by Th115;
end;
theorem Th117:
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))
proof
let w,q,z;
(q | q) | ((z | z) | q) = ((q | ((q | q) | z)) | (q | ((q | q) | z))) by Th74
;
hence thesis by SHEFFER1:def 15;
end;
theorem Th118:
for q,p,x holds (((p | (x | p)) | (p | (x | p))) | (q | (q | q)
)) = (x | x) | p
proof
let q,p,x;
(((x | x) | p) | ((p | p) | p)) = ((p | (x | p)) | (p | (x | p))) by
SHEFFER1:def 15;
hence thesis by Th79;
end;
theorem Th119:
for p,x holds p | (x | p) = (x | x) | p
proof
now
let q,p,x;
(((p | (x | p)) | (p | (x | p))) | (q | (q | q))) = (p | (x | p)) by Th71;
hence p | (x | p) = (x | x) | p by Th118;
end;
hence thesis;
end;
theorem Th120:
for p,y holds (y | p) | ((y | y) | p) = (p | p) | (y | p)
proof
let p,y;
p | (y | p) = (y | y) | p by Th119;
hence thesis by Th119;
end;
theorem Th121:
for x,y holds x = (x | x) | (y | x)
proof
let x,y;
(y | x) | ((y | y) | x) = x by Th92;
hence thesis by Th120;
end;
theorem Th122:
for x,y holds (y | x) | x = ((x | (y | y)) | (x | (y | y))) | ( y | x)
proof
let x,y;
(x | (y | y)) | (y | x) = x by Th106;
hence thesis by Th119;
end;
theorem Th123:
for x,z,y holds (((x | ((y | y) | z)) | (x | ((y | y) | z))) |
((y | x) | ((z | z) | x))) = (z | (y | x)) | x
proof
let x,z,y;
(x | x) | (y | x) = x by Th121;
hence thesis by Th116;
end;
theorem Th124:
for x,y,z holds ((x | (((z | (z | z)) | (z | (z | z))) | y)) |
(x | (((z | (z | z)) | (z | (z | z))) | y))) = x
proof
let x,y,z;
(x | x) | ((y | y) | x) = x by Th121;
hence thesis by Th111;
end;
theorem Th125:
for x,z,y holds (x | ((y | y) | z)) | z = z | (y | x)
proof
let x,z,y;
(z | z) | ((y | y) | z) = z by Th121;
hence thesis by Th100;
end;
theorem Th126:
for x,y holds x | ((y | x) | x) = y | x
proof
let x,y;
((x | (y | y)) | (x | (y | y))) | (y | x) = (y | x) | x by Th122;
hence thesis by Th108;
end;
theorem Th127:
for z,y,x holds y = (((x | x) | x) | y) | ((z | z) | y)
proof
now
let x,y,z,p;
((y | (((p | (p | p)) | (p | (p | p))) | z)) | (y | (((p | (p | p)) |
(p | (p | p))) | z))) = y by Th124;
hence y = (((x | x) | x) | y) | ((z | z) | y) by Th110;
end;
hence thesis;
end;
theorem Th128:
for z,y holds (y | ((y | y) | z)) | (y | ((y | y) | z)) = y
proof
now
let z,y,x;
(((x | x) | x) | y) | ((z | z) | y) = y by Th127;
hence (y | ((y | y) | z)) | (y | ((y | y) | z)) = y by Th114;
end;
hence thesis;
end;
theorem Th129:
for x,z,y holds (((y | y) | z) | (x | z)) | (((y | y) | z) | (x
| z)) = ((x | x) | ((y | y) | z)) | z
proof
let x,z,y;
((z | ((z | z) | y)) | (z | ((z | z) | y))) = z by Th128;
hence thesis by Th117;
end;
theorem Th130:
for x,z,y holds ((((y | y) | z) | (x | z)) | (((y | y) | z) | (
x | z))) = z | (y | (x | x))
proof
let x,z,y;
(((x | x) | ((y | y) | z)) | z) = z | (y | (x | x)) by Th125;
hence thesis by Th129;
end;
theorem Th131:
for y,x holds ((x | y) | (x | y)) | x = x | y
proof
let y,x;
(x | (y | y)) | (x | y) = x by Th109;
hence thesis by Th121;
end;
theorem Th132:
for p,w holds (w | w) | (w | p) = w
proof
let p,w;
p | w = w | p by Th83;
hence thesis by Th121;
end;
theorem Th133:
for w,p holds (p | w) | (w | w) = w
proof
let w,p;
((w | w) | (p | w)) = (p | w) | (w | w) by Th83;
hence thesis by Th121;
end;
theorem Th134:
for p,y,w holds (w | (y | (y | y))) | (w | p) = w
proof
let p,y,w;
(w | w) = (w | (y | (y | y))) by SHEFFER1:def 14;
hence thesis by Th132;
end;
theorem Th135:
for p,w holds ((w | p) | (w | w)) = w
proof
let p,w;
((w | w) | (w | p)) = ((w | p) | (w | w)) by Th83;
hence thesis by Th132;
end;
theorem Th136:
for y,p,w holds (w | p) | (w | (y | (y | y))) = w
proof
let y,p,w;
w | w = (w | (y | (y | y))) by SHEFFER1:def 14;
hence thesis by Th135;
end;
theorem Th137:
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))))
proof
let p,q,w,y,x;
((w | (x | q)) | (w | (x | q))) = (((x | (y | (y | y))) | w) | ((q | q)
| w)) by Th73;
hence thesis by Th73;
end;
theorem Th138:
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)))
)
proof
now
let y,p,w,q,x;
((w | (p | (p | p))) | (w | (x | q))) = w by Th134;
hence ((((x | (y | (y | y))) | w) | ((q | q) | w)) | ((w | (x | q)) | (w |
(x | q)))) = (w | (((x | q) | (x | q)) | (w | (x | q)))) by Th137;
end;
hence thesis;
end;
theorem Th139:
for q,w,y,x holds (((x | (y | (y | y))) | w) | ((q | q) | w)) |
((w | (x | q)) | (w | (x | q))) = w | (x | q)
proof
let q,w,y,x;
((x | q) | (x | q)) | (w | (x | q)) = x | q by Th121;
hence thesis by Th138;
end;
theorem Th140:
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)))
proof
let z,p,q,y,x;
(((x | (y | (y | y))) | q) | ((z | z) | q)) = ((q | (x | z)) | (q | (x |
z))) by Th73;
hence thesis by Th73;
end;
theorem Th141:
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))
proof
let z,p,q,y,x;
((((x | (y | (y | y))) | q) | ((z | z) | q)) | ((q | (x | z)) | (q | (x
| z)))) = (q | (x | z)) by Th139;
hence thesis by Th140;
end;
theorem Th142:
for z,q,y,x holds q | (x | z) = (z | ((x | (y | (y | y))) | q))
| ((q | q) | ((x | (y | (y | y))) | q))
proof
now
let p,z,q,y,x;
(z | z) | (p | (p | p)) = z by Th71;
hence
(q | (x | z)) = ((z | ((x | (y | (y | y))) | q)) | ((q | q) | ((x | (
y | (y | y))) | q))) by Th141;
end;
hence thesis;
end;
theorem Th143:
for v,p,y,x holds p | (x | v) = (v | ((x | (y | (y | y))) | p)) | p
proof
let v,p,y,x;
(p | p) | ((x | (y | (y | y))) | p) = p by Th121;
hence thesis by Th142;
end;
theorem Th144:
for y,w,z,v,x holds ((w | (z | (x | v))) | (((x | (y | (y | y))
) | z) | ((v | v) | z))) = z | (x | v)
proof
let y,w,z,v,x;
(z | (x | v)) | (z | (x | v)) = ((x | (y | (y | y))) | z) | ((v | v) | z
) by Th73;
hence thesis by Th133;
end;
theorem Th145:
for y,z,x holds ((y | ((x | x) | z)) | (y | ((x | x) | z))) | (
(x | y) | ((z | z) | y)) = y | ((x | x) | z)
proof
let y,z,x;
(y | ((x | x) | z)) | (y | ((x | x) | z)) = (x | y) | ((z | z) | y) by Th74;
hence thesis by Th121;
end;
theorem Th146:
for z,y,x holds (z | (x | y)) | y = y | ((x | x) | z)
proof
let z,y,x;
(((y | ((x | x) | z)) | (y | ((x | x) | z))) | ((x | y) | ((z | z) | y))
) = ((z | (x | y)) | y) by Th123;
hence thesis by Th145;
end;
theorem Th147:
for x,w,y,z holds ((((x | x) | w) | ((z | (y | (y | y))) | w))
| w) = w | (x | z)
proof
let x,w,y,z;
(w | (x | z)) | (w | (x | z)) = ((x | x) | w) | ((z | (y | (y | y))) | w
) by Th75;
hence thesis by Th131;
end;
theorem Th148:
for z,w,x holds (w | (z | ((x | x) | w))) = w | (x | z)
proof
now
let x,w,p,z;
((((x | x) | w) | ((z | (p | (p | p))) | w)) | w) = w | (z | ((x | x)
| w)) by Th143;
hence w | (z | ((x | x) | w)) = w | (x | z) by Th147;
end;
hence thesis;
end;
theorem Th149:
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)))
proof
let p,z,y,x;
(((x | (y | (y | y))) | z) | ((p | p) | z)) = ((z | (x | p)) | (z | (x |
p))) by Th73;
hence thesis by Th87;
end;
theorem Th150:
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)))
proof
let p,z,y,x;
(((z | (x | p)) | (z | (x | p))) | (((x | (y | (y | y))) | z) | ((p | p)
| z))) = z | (x | p) by Th144;
hence thesis by Th149;
end;
theorem Th151:
for z,p,y,x holds z | (x | p) = z | (p | ((x | (y | (y | y))) |
(x | (y | (y | y)))))
proof
let z,p,y,x;
(((p | p) | z) | ((x | (y | (y | y))) | z)) | (((p | p) | z) | ((x | (y
| (y | y))) | z)) = z | (p | ((x | (y | (y | y))) | (x | (y | (y | y))))) by
Th130;
hence thesis by Th150;
end;
theorem Th152:
for z,p,x holds z | (x | p) = z | (p | x)
proof
now
let y,z,p,x;
(x | (y | (y | y))) | (x | (y | (y | y))) = x by Th136;
hence z | (x | p) = z | (p | x) by Th151;
end;
hence thesis;
end;
theorem Th153:
for w,q,p holds (p | q) | w = w | (q | p)
proof
let w,q,p;
w | (p | q) = (p | q) | w by Th83;
hence thesis by Th152;
end;
theorem Th154:
for w,p,q holds ((q | p) | w) | q = q | ((p | p) | w)
proof
let w,p,q;
w | (p | q) = (q | p) | w by Th153;
hence thesis by Th146;
end;
theorem Th155:
for z,w,y,x holds w | x = (w | ((x | z) | (((x | (y | (y | y)))
| (x | (y | (y | y)))) | w)))
proof
let z,w,y,x;
(x | (y | (y | y))) | (x | z) = x by Th134;
hence thesis by Th148;
end;
theorem Th156:
for w,z,x holds w | x = w | ((x | z) | (x | w))
proof
now
let y,w,z,x;
(x | (y | (y | y))) | (x | (y | (y | y))) = x by Th136;
hence w | x = w | ((x | z) | (x | w)) by Th155;
end;
hence thesis;
end;
theorem Th157:
for q,x,z,y holds ((x | y) | (((x | (y | (z | (z | z)))) | q) |
x)) = ((x | y) | (x | (y | (z | (z | z)))))
proof
let q,x,z,y;
(x | (y | (z | (z | z)))) | (x | y) = x by Th113;
hence thesis by Th156;
end;
theorem Th158:
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)))))
proof
let x,q,z,y;
(((x | (y | (z | (z | z)))) | q) | x) = (x | (((y | (z | (z | z))) | (y
| (z | (z | z)))) | q)) by Th154;
hence thesis by Th157;
end;
theorem Th159:
for z,x,q,y holds (x | y) | (x | (y | q)) = ((x | y) | (x | (y
| (z | (z | z)))))
proof
let z,x,q,y;
((y | (z | (z | z))) | (y | (z | (z | z)))) = y by Th136;
hence thesis by Th158;
end;
theorem Th160:
for x,q,y holds (x | y) | (x | (y | q)) = x
proof
now
let q,x,z,y;
(x | y) | (x | (y | (z | (z | z)))) = x by Th112;
hence (x | y) | (x | (y | q)) = x by Th159;
end;
hence thesis;
end;
theorem Th161:
L is satisfying_Sh_1
proof
given a, b, c being Element of L such that
A1: (a | ((b | a) | a)) | (b | (c | a)) <> b;
A2: a | ((b | a) | a) = b | a by Th126;
not ((a | ((b | a) | a)) | (b | (a | c))) = b by A1,Th83;
hence thesis by A2,Th160;
end;
registration
cluster satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ->
satisfying_Sh_1 for non empty ShefferStr;
coherence by Th161;
cluster satisfying_Sh_1 -> satisfying_Sheffer_1 satisfying_Sheffer_2
satisfying_Sheffer_3 for non empty ShefferStr;
coherence by Th67,Th68,Th69;
end;
registration
cluster satisfying_Sh_1 properly_defined -> Boolean Lattice-like for
non empty
ShefferOrthoLattStr;
coherence;
cluster Boolean Lattice-like well-complemented properly_defined ->
satisfying_Sh_1 for non empty ShefferOrthoLattStr;
coherence;
end;