:: SHEFFER1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: SHEFFER1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b being Element of L holds (a + b) ` = (a ` ) *' (b ` )
proof end;

theorem :: SHEFFER1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative join-associative Huntington ComplLattStr
for a, b being Element of L holds (a *' b) ` = (a ` ) + (b ` ) by ROBBINS1:3;

definition
let IT be non empty LattStr ;
attr IT is upper-bounded' means :Def1: :: SHEFFER1:def 1
 ex c being Element of IT st
for a being Element of IT holds
( c "/\" a = a & a "/\" c = a );
end;

:: deftheorem Def1 defines upper-bounded' SHEFFER1:def 1 :
for IT being non empty LattStr holds
( IT is upper-bounded' iff ex c being Element of IT st
for a being Element of IT holds
( c "/\" a = a & a "/\" c = a ) );

definition
let L be non empty LattStr ;
assume A1: L is upper-bounded' ;
func Top' L -> Element of L means :Def2: :: SHEFFER1:def 2
for a being Element of L holds
( it "/\" a = a & a "/\" it = a );
existence
ex b1 being Element of L st
for a being Element of L holds
( b1 "/\" a = a & a "/\" b1 = a ) by A1, Def1;
uniqueness
for b1, b2 being Element of L st ( for a being Element of L holds
( b1 "/\" a = a & a "/\" b1 = a ) ) & ( for a being Element of L holds
( b2 "/\" a = a & a "/\" b2 = a ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Top' SHEFFER1:def 2 :
for L being non empty LattStr st L is upper-bounded' holds
for b2 being Element of L holds
( b2 = Top' L iff for a being Element of L holds
( b2 "/\" a = a & a "/\" b2 = a ) );

definition
let IT be non empty LattStr ;
attr IT is lower-bounded' means :Def3: :: SHEFFER1:def 3
 ex c being Element of IT st
for a being Element of IT holds
( c "\/" a = a & a "\/" c = a );
end;

:: deftheorem Def3 defines lower-bounded' SHEFFER1:def 3 :
for IT being non empty LattStr holds
( IT is lower-bounded' iff ex c being Element of IT st
for a being Element of IT holds
( c "\/" a = a & a "\/" c = a ) );

definition
let L be non empty LattStr ;
assume A1: L is lower-bounded' ;
func Bot' L -> Element of L means :Def4: :: SHEFFER1:def 4
for a being Element of L holds
( it "\/" a = a & a "\/" it = a );
existence
ex b1 being Element of L st
for a being Element of L holds
( b1 "\/" a = a & a "\/" b1 = a ) by A1, Def3;
uniqueness
for b1, b2 being Element of L st ( for a being Element of L holds
( b1 "\/" a = a & a "\/" b1 = a ) ) & ( for a being Element of L holds
( b2 "\/" a = a & a "\/" b2 = a ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Bot' SHEFFER1:def 4 :
for L being non empty LattStr st L is lower-bounded' holds
for b2 being Element of L holds
( b2 = Bot' L iff for a being Element of L holds
( b2 "\/" a = a & a "\/" b2 = a ) );

definition
let IT be non empty LattStr ;
attr IT is distributive' means :Def5: :: SHEFFER1:def 5
for a, b, c being Element of IT holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c);
end;

:: deftheorem Def5 defines distributive' SHEFFER1:def 5 :
for IT being non empty LattStr holds
( IT is distributive' iff for a, b, c being Element of IT holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) );

definition
let L be non empty LattStr ;
let a, b be Element of L;
pred a is_a_complement'_of b means :Def6: :: SHEFFER1:def 6
( b "\/" a = Top' L & a "\/" b = Top' L & b "/\" a = Bot' L & a "/\" b = Bot' L );
end;

:: deftheorem Def6 defines is_a_complement'_of SHEFFER1:def 6 :
for L being non empty LattStr
for a, b being Element of L holds
( a is_a_complement'_of b iff ( b "\/" a = Top' L & a "\/" b = Top' L & b "/\" a = Bot' L & a "/\" b = Bot' L ) );

definition
let IT be non empty LattStr ;
attr IT is complemented' means :Def7: :: SHEFFER1:def 7
for b being Element of IT ex a being Element of IT st a is_a_complement'_of b;
end;

:: deftheorem Def7 defines complemented' SHEFFER1:def 7 :
for IT being non empty LattStr holds
( IT is complemented' iff for b being Element of IT ex a being Element of IT st a is_a_complement'_of b );

definition
let L be non empty LattStr ;
let x be Element of L;
assume A1: ( L is complemented' & L is distributive & L is upper-bounded' & L is meet-commutative ) ;
func x `# -> Element of L means :Def8: :: SHEFFER1:def 8
it is_a_complement'_of x;
existence
ex b1 being Element of L st b1 is_a_complement'_of x by A1, Def7;
uniqueness
for b1, b2 being Element of L st b1 is_a_complement'_of x & b2 is_a_complement'_of x holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines `# SHEFFER1:def 8 :
for L being non empty LattStr
for x being Element of L st L is complemented' & L is distributive & L is upper-bounded' & L is meet-commutative holds
for b3 being Element of L holds
( b3 = x `# iff b3 is_a_complement'_of x );

registration
cluster non empty Lattice-like Boolean join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ;
existence
ex b1 being non empty LattStr st
( b1 is Boolean & b1 is join-idempotent & b1 is upper-bounded' & b1 is complemented' & b1 is distributive' & b1 is lower-bounded' & b1 is Lattice-like )
proof end;
end;

theorem Th3: :: SHEFFER1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' LattStr
for x being Element of L holds x "\/" (x `# ) = Top' L
proof end;

theorem Th4: :: SHEFFER1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' LattStr
for x being Element of L holds x "/\" (x `# ) = Bot' L
proof end;

theorem Th5: :: SHEFFER1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' LattStr
for x being Element of L holds x "\/" (Top' L) = Top' L
proof end;

theorem Th6: :: SHEFFER1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr
for x being Element of L holds x "/\" (Bot' L) = Bot' L
proof end;

theorem Th7: :: SHEFFER1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr
for x, y, z being Element of L holds ((x "\/" y) "\/" z) "/\" x = x
proof end;

theorem Th8: :: SHEFFER1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' LattStr
for x, y, z being Element of L holds ((x "/\" y) "/\" z) "\/" x = x
proof end;

definition
let G be non empty /\-SemiLattStr ;
attr G is meet-idempotent means :Def9: :: SHEFFER1:def 9
for x being Element of G holds x "/\" x = x;
end;

:: deftheorem Def9 defines meet-idempotent SHEFFER1:def 9 :
for G being non empty /\-SemiLattStr holds
( G is meet-idempotent iff for x being Element of G holds x "/\" x = x );

theorem Th9: :: SHEFFER1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is meet-idempotent
proof end;

theorem Th10: :: SHEFFER1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is join-idempotent
proof end;

theorem Th11: :: SHEFFER1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' LattStr holds L is meet-absorbing
proof end;

theorem Th12: :: SHEFFER1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is join-absorbing
proof end;

theorem Th13: :: SHEFFER1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is upper-bounded
proof end;

theorem Th14: :: SHEFFER1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Lattice-like Boolean LattStr holds L is upper-bounded'
proof end;

theorem Th15: :: SHEFFER1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is lower-bounded
proof end;

theorem Th16: :: SHEFFER1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Lattice-like Boolean LattStr holds L is lower-bounded'
proof end;

theorem Th17: :: SHEFFER1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr holds L is join-associative
proof end;

theorem Th18: :: SHEFFER1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' LattStr holds L is meet-associative
proof end;

theorem Th19: :: SHEFFER1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds Top L = Top' L
proof end;

theorem Th20: :: SHEFFER1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds Bottom L = Bot' L
proof end;

theorem Th21: :: SHEFFER1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Lattice-like Boolean distributive' LattStr holds Top L = Top' L
proof end;

theorem Th22: :: SHEFFER1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Lattice-like distributive lower-bounded upper-bounded complemented Boolean distributive' LattStr holds Bottom L = Bot' L
proof end;

theorem :: SHEFFER1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr
for x, y being Element of L holds
( x is_a_complement'_of y iff x is_a_complement_of y )
proof end;

theorem Th24: :: SHEFFER1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is complemented
proof end;

theorem Th25: :: SHEFFER1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Lattice-like Boolean upper-bounded' lower-bounded' distributive' LattStr holds L is complemented'
proof end;

theorem Th26: :: SHEFFER1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty LattStr holds
( L is Boolean Lattice iff ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' ) )
proof end;

registration
cluster non empty Lattice-like Boolean -> non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' LattStr ;
coherence
for b1 being non empty LattStr st b1 is Boolean & b1 is Lattice-like holds
( b1 is lower-bounded' & b1 is upper-bounded' & b1 is complemented' & b1 is join-commutative & b1 is meet-commutative & b1 is distributive & b1 is distributive' ) by Th26;
cluster non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' -> non empty Lattice-like Boolean LattStr ;
coherence
for b1 being non empty LattStr st b1 is lower-bounded' & b1 is upper-bounded' & b1 is complemented' & b1 is join-commutative & b1 is meet-commutative & b1 is distributive & b1 is distributive' holds
( b1 is Boolean & b1 is Lattice-like ) by Th26;
end;

definition
attr c1 is strict;
struct ShefferStr -> 1-sorted ;
aggr ShefferStr(# carrier, stroke #) -> ShefferStr ;
sel stroke c1 -> BinOp of the carrier of c1;
end;

definition
attr c1 is strict;
struct ShefferLattStr -> ShefferStr , LattStr ;
aggr ShefferLattStr(# carrier, L_join, L_meet, stroke #) -> ShefferLattStr ;
end;

definition
attr c1 is strict;
struct ShefferOrthoLattStr -> ShefferStr , OrthoLattStr ;
aggr ShefferOrthoLattStr(# carrier, L_join, L_meet, Compl, stroke #) -> ShefferOrthoLattStr ;
end;

definition
func TrivShefferOrthoLattStr -> ShefferOrthoLattStr equals :: SHEFFER1:def 10
 ShefferOrthoLattStr(# {{} },op2 ,op2 ,op1 ,op2 #);
coherence
ShefferOrthoLattStr(# {{} },op2 ,op2 ,op1 ,op2 #) is ShefferOrthoLattStr ;
end;

:: deftheorem defines TrivShefferOrthoLattStr SHEFFER1:def 10 :
TrivShefferOrthoLattStr = ShefferOrthoLattStr(# {{} },op2 ,op2 ,op1 ,op2 #);

registration
cluster non empty ShefferStr ;
existence
not for b1 being ShefferStr holds b1 is empty
proof end;
cluster non empty ShefferLattStr ;
existence
not for b1 being ShefferLattStr holds b1 is empty
proof end;
cluster non empty ShefferOrthoLattStr ;
existence
not for b1 being ShefferOrthoLattStr holds b1 is empty
proof end;
end;

definition
let L be non empty ShefferStr ;
let x, y be Element of L;
func x | y -> Element of L equals :: SHEFFER1:def 11
the stroke of L . x,y;
coherence
the stroke of L . x,y is Element of L ;
end;

:: deftheorem defines | SHEFFER1:def 11 :
for L being non empty ShefferStr
for x, y being Element of L holds x | y = the stroke of L . x,y;

definition
let L be non empty ShefferOrthoLattStr ;
attr L is properly_defined means :Def12: :: SHEFFER1:def 12
( ( for x being Element of L holds x | x = x ` ) & ( for x, y being Element of L holds x "\/" y = (x | x) | (y | y) ) & ( for x, y being Element of L holds x "/\" y = (x | y) | (x | y) ) & ( for x, y being Element of L holds x | y = (x ` ) + (y ` ) ) );
end;

:: deftheorem Def12 defines properly_defined SHEFFER1:def 12 :
for L being non empty ShefferOrthoLattStr holds
( L is properly_defined iff ( ( for x being Element of L holds x | x = x ` ) & ( for x, y being Element of L holds x "\/" y = (x | x) | (y | y) ) & ( for x, y being Element of L holds x "/\" y = (x | y) | (x | y) ) & ( for x, y being Element of L holds x | y = (x ` ) + (y ` ) ) ) );

definition
let L be non empty ShefferStr ;
attr L is satisfying_Sheffer_1 means :Def13: :: SHEFFER1:def 13
for x being Element of L holds (x | x) | (x | x) = x;
attr L is satisfying_Sheffer_2 means :Def14: :: SHEFFER1:def 14
for x, y being Element of L holds x | (y | (y | y)) = x | x;
attr L is satisfying_Sheffer_3 means :Def15: :: SHEFFER1:def 15
for x, y, z being Element of L holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x);
end;

:: deftheorem Def13 defines satisfying_Sheffer_1 SHEFFER1:def 13 :
for L being non empty ShefferStr holds
( L is satisfying_Sheffer_1 iff for x being Element of L holds (x | x) | (x | x) = x );

:: deftheorem Def14 defines satisfying_Sheffer_2 SHEFFER1:def 14 :
for L being non empty ShefferStr holds
( L is satisfying_Sheffer_2 iff for x, y being Element of L holds x | (y | (y | y)) = x | x );

:: deftheorem Def15 defines satisfying_Sheffer_3 SHEFFER1:def 15 :
for L being non empty ShefferStr holds
( L is satisfying_Sheffer_3 iff for x, y, z being Element of L holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) );

registration
cluster non empty trivial -> non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ;
coherence
for b1 being non empty ShefferStr st b1 is trivial holds
( b1 is satisfying_Sheffer_1 & b1 is satisfying_Sheffer_2 & b1 is satisfying_Sheffer_3 )
proof end;
end;

registration
cluster non empty trivial -> non empty join-commutative join-associative \/-SemiLattStr ;
coherence
for b1 being non empty \/-SemiLattStr st b1 is trivial holds
( b1 is join-commutative & b1 is join-associative )
proof end;
cluster non empty trivial -> non empty meet-commutative meet-associative /\-SemiLattStr ;
coherence
for b1 being non empty /\-SemiLattStr st b1 is trivial holds
( b1 is meet-commutative & b1 is meet-associative )
proof end;
end;

registration
cluster non empty trivial -> non empty meet-absorbing join-absorbing Boolean LattStr ;
coherence
for b1 being non empty LattStr st b1 is trivial holds
( b1 is join-absorbing & b1 is meet-absorbing & b1 is Boolean )
proof end;
end;

registration
cluster TrivShefferOrthoLattStr -> non empty ;
coherence
not TrivShefferOrthoLattStr is empty by STRUCT_0:def 1;
cluster TrivShefferOrthoLattStr -> trivial ;
coherence
TrivShefferOrthoLattStr is trivial by REALSET2:def 5;
cluster TrivShefferOrthoLattStr -> well-complemented properly_defined ;
coherence
( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is well-complemented )
proof end;
end;

registration
cluster non empty join-commutative meet-commutative Lattice-like distributive Boolean well-complemented upper-bounded' lower-bounded' distributive' complemented' properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ;
existence
ex b1 being non empty ShefferOrthoLattStr st
( b1 is properly_defined & b1 is Boolean & b1 is well-complemented & b1 is Lattice-like & b1 is satisfying_Sheffer_1 & b1 is satisfying_Sheffer_2 & b1 is satisfying_Sheffer_3 )
proof end;
end;

theorem :: SHEFFER1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr holds L is satisfying_Sheffer_1
proof end;

theorem :: SHEFFER1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr holds L is satisfying_Sheffer_2
proof end;

theorem :: SHEFFER1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr holds L is satisfying_Sheffer_3
proof end;

definition
let L be non empty ShefferStr ;
let a be Element of L;
func a " -> Element of L equals :: SHEFFER1:def 16
a | a;
coherence
a | a is Element of L ;
end;

:: deftheorem defines " SHEFFER1:def 16 :
for L being non empty ShefferStr
for a being Element of L holds a " = a | a;

theorem Th30: :: SHEFFER1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_3 ShefferOrthoLattStr
for x, y, z being Element of L holds (x | (y | z)) " = ((y " ) | x) | ((z " ) | x) by Def15;

theorem Th31: :: SHEFFER1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_Sheffer_1 ShefferOrthoLattStr
for x being Element of L holds x = (x " ) " by Def13;

theorem Th32: :: SHEFFER1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr
for x, y being Element of L holds x | y = y | x
proof end;

theorem Th33: :: SHEFFER1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr
for x, y being Element of L holds x | (x | x) = y | (y | y)
proof end;

theorem Th34: :: SHEFFER1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is join-commutative
proof end;

theorem Th35: :: SHEFFER1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is meet-commutative
proof end;

theorem Th36: :: SHEFFER1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is distributive
proof end;

theorem Th37: :: SHEFFER1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is distributive'
proof end;

theorem :: SHEFFER1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is Boolean Lattice
proof end;