:: SHEFFER1 semantic presentation begin theorem :: SHEFFER1:1 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_robbins1 :::"Huntington"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ))))) ; begin definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; attr "IT" is :::"upper-bounded'"::: means :: SHEFFER1:def 1 (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Set (Var "c")) ($#k2_lattices :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))); end; :: deftheorem defines :::"upper-bounded'"::: SHEFFER1:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_sheffer1 :::"upper-bounded'"::: ) ) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Set (Var "c")) ($#k2_lattices :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ")" )); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; assume (Bool (Set (Const "L")) "is" ($#v1_sheffer1 :::"upper-bounded'"::: ) ) ; func :::"Top'"::: "L" -> ($#m1_subset_1 :::"Element":::) "of" "L" means :: SHEFFER1:def 2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set it ($#k2_lattices :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) it) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )); end; :: deftheorem defines :::"Top'"::: SHEFFER1:def 2 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "st" (Bool (Bool (Set (Var "L")) "is" ($#v1_sheffer1 :::"upper-bounded'"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_sheffer1 :::"Top'"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k2_lattices :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )) ")" ))); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; attr "IT" is :::"lower-bounded'"::: means :: SHEFFER1:def 3 (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Set (Var "c")) ($#k1_lattices :::""\/""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))); end; :: deftheorem defines :::"lower-bounded'"::: SHEFFER1:def 3 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_sheffer1 :::"lower-bounded'"::: ) ) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Set (Var "c")) ($#k1_lattices :::""\/""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ")" )); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; assume (Bool (Set (Const "L")) "is" ($#v2_sheffer1 :::"lower-bounded'"::: ) ) ; func :::"Bot'"::: "L" -> ($#m1_subset_1 :::"Element":::) "of" "L" means :: SHEFFER1:def 4 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set it ($#k1_lattices :::""\/""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) it) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )); end; :: deftheorem defines :::"Bot'"::: SHEFFER1:def 4 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "st" (Bool (Bool (Set (Var "L")) "is" ($#v2_sheffer1 :::"lower-bounded'"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_sheffer1 :::"Bot'"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k1_lattices :::""\/""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )) ")" ))); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; attr "IT" is :::"distributive'"::: means :: SHEFFER1:def 5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k2_lattices :::""/\""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "c")) ")" )))); end; :: deftheorem defines :::"distributive'"::: SHEFFER1:def 5 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_sheffer1 :::"distributive'"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k2_lattices :::""/\""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "c")) ")" )))) ")" )); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); pred "a" :::"is_a_complement'_of"::: "b" means :: SHEFFER1:def 6 (Bool "(" (Bool (Set "b" ($#k1_lattices :::""\/""::: ) "a") ($#r1_hidden :::"="::: ) (Set ($#k1_sheffer1 :::"Top'"::: ) "L")) & (Bool (Set "a" ($#k1_lattices :::""\/""::: ) "b") ($#r1_hidden :::"="::: ) (Set ($#k1_sheffer1 :::"Top'"::: ) "L")) & (Bool (Set "b" ($#k2_lattices :::""/\""::: ) "a") ($#r1_hidden :::"="::: ) (Set ($#k2_sheffer1 :::"Bot'"::: ) "L")) & (Bool (Set "a" ($#k2_lattices :::""/\""::: ) "b") ($#r1_hidden :::"="::: ) (Set ($#k2_sheffer1 :::"Bot'"::: ) "L")) ")" ); end; :: deftheorem defines :::"is_a_complement'_of"::: SHEFFER1:def 6 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_sheffer1 :::"is_a_complement'_of"::: ) (Set (Var "b"))) "iff" (Bool "(" (Bool (Set (Set (Var "b")) ($#k1_lattices :::""\/""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_sheffer1 :::"Top'"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k1_sheffer1 :::"Top'"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "b")) ($#k2_lattices :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k2_sheffer1 :::"Bot'"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k2_sheffer1 :::"Bot'"::: ) (Set (Var "L")))) ")" ) ")" ))); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; attr "IT" is :::"complemented'"::: means :: SHEFFER1:def 7 (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set (Var "a")) ($#r1_sheffer1 :::"is_a_complement'_of"::: ) (Set (Var "b"))))); end; :: deftheorem defines :::"complemented'"::: SHEFFER1:def 7 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_sheffer1 :::"complemented'"::: ) ) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set (Var "a")) ($#r1_sheffer1 :::"is_a_complement'_of"::: ) (Set (Var "b"))))) ")" )); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); assume (Bool "(" (Bool (Set (Const "L")) "is" ($#v4_sheffer1 :::"complemented'"::: ) ) & (Bool (Set (Const "L")) "is" ($#v11_lattices :::"distributive"::: ) ) & (Bool (Set (Const "L")) "is" ($#v1_sheffer1 :::"upper-bounded'"::: ) ) & (Bool (Set (Const "L")) "is" ($#v6_lattices :::"meet-commutative"::: ) ) ")" ) ; func "x" :::"`#"::: -> ($#m1_subset_1 :::"Element":::) "of" "L" means :: SHEFFER1:def 8 (Bool it ($#r1_sheffer1 :::"is_a_complement'_of"::: ) "x"); end; :: deftheorem defines :::"`#"::: SHEFFER1:def 8 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v4_sheffer1 :::"complemented'"::: ) ) & (Bool (Set (Var "L")) "is" ($#v11_lattices :::"distributive"::: ) ) & (Bool (Set (Var "L")) "is" ($#v1_sheffer1 :::"upper-bounded'"::: ) ) & (Bool (Set (Var "L")) "is" ($#v6_lattices :::"meet-commutative"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_sheffer1 :::"`#"::: ) )) "iff" (Bool (Set (Var "b3")) ($#r1_sheffer1 :::"is_a_complement'_of"::: ) (Set (Var "x"))) ")" )))); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV7_STRUCT_0() bbbadV8_STRUCT_0() (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v2_sheffer1 :::"lower-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; theorem :: SHEFFER1:2 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "x")) ($#k3_sheffer1 :::"`#"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_sheffer1 :::"Top'"::: ) (Set (Var "L")))))) ; theorem :: SHEFFER1:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "x")) ($#k3_sheffer1 :::"`#"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_sheffer1 :::"Bot'"::: ) (Set (Var "L")))))) ; theorem :: SHEFFER1:4 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k3_lattices :::""\/""::: ) (Set "(" ($#k1_sheffer1 :::"Top'"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_sheffer1 :::"Top'"::: ) (Set (Var "L")))))) ; theorem :: SHEFFER1:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v2_sheffer1 :::"lower-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k4_lattices :::""/\""::: ) (Set "(" ($#k2_sheffer1 :::"Bot'"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_sheffer1 :::"Bot'"::: ) (Set (Var "L")))))) ; theorem :: SHEFFER1:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v11_lattices :::"distributive"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k3_lattices :::""\/""::: ) (Set (Var "y")) ")" ) ($#k3_lattices :::""\/""::: ) (Set (Var "z")) ")" ) ($#k4_lattices :::""/\""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: SHEFFER1:7 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k4_lattices :::""/\""::: ) (Set (Var "y")) ")" ) ($#k4_lattices :::""/\""::: ) (Set (Var "z")) ")" ) ($#k3_lattices :::""\/""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lattices :::"/\-SemiLattStr"::: ) ; attr "G" is :::"meet-idempotent"::: means :: SHEFFER1:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "holds" (Bool (Set (Set (Var "x")) ($#k2_lattices :::""/\""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))); end; :: deftheorem defines :::"meet-idempotent"::: SHEFFER1:def 9 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lattices :::"/\-SemiLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v5_sheffer1 :::"meet-idempotent"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "x")) ($#k2_lattices :::""/\""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )); theorem :: SHEFFER1:8 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v2_sheffer1 :::"lower-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v5_sheffer1 :::"meet-idempotent"::: ) )) ; theorem :: SHEFFER1:9 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v2_sheffer1 :::"lower-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v7_robbins1 :::"join-idempotent"::: ) )) ; theorem :: SHEFFER1:10 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v8_lattices :::"meet-absorbing"::: ) )) ; theorem :: SHEFFER1:11 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v2_sheffer1 :::"lower-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v9_lattices :::"join-absorbing"::: ) )) ; theorem :: SHEFFER1:12 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v2_sheffer1 :::"lower-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v14_lattices :::"upper-bounded"::: ) )) ; theorem :: SHEFFER1:13 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v1_sheffer1 :::"upper-bounded'"::: ) )) ; theorem :: SHEFFER1:14 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v2_sheffer1 :::"lower-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v13_lattices :::"lower-bounded"::: ) )) ; theorem :: SHEFFER1:15 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v2_sheffer1 :::"lower-bounded'"::: ) )) ; theorem :: SHEFFER1:16 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v11_lattices :::"distributive"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v5_lattices :::"join-associative"::: ) )) ; theorem :: SHEFFER1:17 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v7_lattices :::"meet-associative"::: ) )) ; theorem :: SHEFFER1:18 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v2_sheffer1 :::"lower-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_sheffer1 :::"Top'"::: ) (Set (Var "L"))))) ; theorem :: SHEFFER1:19 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v2_sheffer1 :::"lower-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k2_sheffer1 :::"Bot'"::: ) (Set (Var "L"))))) ; theorem :: SHEFFER1:20 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_sheffer1 :::"Top'"::: ) (Set (Var "L"))))) ; theorem :: SHEFFER1:21 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v11_lattices :::"distributive"::: ) ($#v13_lattices :::"lower-bounded"::: ) ($#v14_lattices :::"upper-bounded"::: ) ($#v16_lattices :::"complemented"::: ) ($#v17_lattices :::"Boolean"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k2_sheffer1 :::"Bot'"::: ) (Set (Var "L"))))) ; theorem :: SHEFFER1:22 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v2_sheffer1 :::"lower-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_sheffer1 :::"is_a_complement'_of"::: ) (Set (Var "y"))) "iff" (Bool (Set (Var "x")) ($#r2_lattices :::"is_a_complement_of"::: ) (Set (Var "y"))) ")" ))) ; theorem :: SHEFFER1:23 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v2_sheffer1 :::"lower-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v16_lattices :::"complemented"::: ) )) ; theorem :: SHEFFER1:24 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v2_sheffer1 :::"lower-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v4_sheffer1 :::"complemented'"::: ) )) ; theorem :: SHEFFER1:25 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::)) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_sheffer1 :::"lower-bounded'"::: ) ) & (Bool (Set (Var "L")) "is" ($#v1_sheffer1 :::"upper-bounded'"::: ) ) & (Bool (Set (Var "L")) "is" ($#v4_lattices :::"join-commutative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v6_lattices :::"meet-commutative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v11_lattices :::"distributive"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_sheffer1 :::"distributive'"::: ) ) & (Bool (Set (Var "L")) "is" ($#v4_sheffer1 :::"complemented'"::: ) ) ")" ) ")" )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v2_sheffer1 :::"lower-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) for ($#l3_lattices :::"LattStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v11_lattices :::"distributive"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v2_sheffer1 :::"lower-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; begin definitionattr "c1" is :::"strict"::: ; struct :::"ShefferStr"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"ShefferStr":::(# :::"carrier":::, :::"stroke"::: #) -> ($#l1_sheffer1 :::"ShefferStr"::: ) ; sel :::"stroke"::: "c1" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; definitionattr "c1" is :::"strict"::: ; struct :::"ShefferLattStr"::: -> ($#l1_sheffer1 :::"ShefferStr"::: ) "," ($#l3_lattices :::"LattStr"::: ) ; aggr :::"ShefferLattStr":::(# :::"carrier":::, :::"L_join":::, :::"L_meet":::, :::"stroke"::: #) -> ($#l2_sheffer1 :::"ShefferLattStr"::: ) ; end; definitionattr "c1" is :::"strict"::: ; struct :::"ShefferOrthoLattStr"::: -> ($#l1_sheffer1 :::"ShefferStr"::: ) "," ($#l4_robbins1 :::"OrthoLattStr"::: ) ; aggr :::"ShefferOrthoLattStr":::(# :::"carrier":::, :::"L_join":::, :::"L_meet":::, :::"Compl":::, :::"stroke"::: #) -> ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) ; end; definitionfunc :::"TrivShefferOrthoLattStr"::: -> ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) equals :: SHEFFER1:def 10 (Set ($#g3_sheffer1 :::"ShefferOrthoLattStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "#)" ); end; :: deftheorem defines :::"TrivShefferOrthoLattStr"::: SHEFFER1:def 10 : (Bool (Set ($#k4_sheffer1 :::"TrivShefferOrthoLattStr"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g3_sheffer1 :::"ShefferOrthoLattStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "#)" )); registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) for ($#l1_sheffer1 :::"ShefferStr"::: ) ; cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) for ($#l2_sheffer1 :::"ShefferLattStr"::: ) ; cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) for ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) ; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_sheffer1 :::"ShefferStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "x" :::"|"::: "y" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: SHEFFER1:def 11 (Set (Set "the" ($#u1_sheffer1 :::"stroke"::: ) "of" "L") ($#k5_binop_1 :::"."::: ) "(" "x" "," "y" ")" ); end; :: deftheorem defines :::"|"::: SHEFFER1:def 11 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_sheffer1 :::"ShefferStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_sheffer1 :::"stroke"::: ) "of" (Set (Var "L"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) ; attr "L" is :::"properly_defined"::: means :: SHEFFER1:def 12 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x")) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "y")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set (Var "x")) ($#k2_lattices :::""/\""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "y")) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "y")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"properly_defined"::: SHEFFER1:def 12 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v9_sheffer1 :::"properly_defined"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x")) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "y")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k2_lattices :::""/\""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "y")) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "y")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ))) ")" ) ")" ) ")" )); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_sheffer1 :::"ShefferStr"::: ) ; attr "L" is :::"satisfying_Sheffer_1"::: means :: SHEFFER1:def 13 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x")) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))); attr "L" is :::"satisfying_Sheffer_2"::: means :: SHEFFER1:def 14 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "y")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x"))))); attr "L" is :::"satisfying_Sheffer_3"::: means :: SHEFFER1:def 15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "z")) ")" ) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "y")) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x")) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "z")) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"satisfying_Sheffer_1"::: SHEFFER1:def 13 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_sheffer1 :::"ShefferStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x")) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )); :: deftheorem defines :::"satisfying_Sheffer_2"::: SHEFFER1:def 14 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_sheffer1 :::"ShefferStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "y")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x"))))) ")" )); :: deftheorem defines :::"satisfying_Sheffer_3"::: SHEFFER1:def 15 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_sheffer1 :::"ShefferStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "z")) ")" ) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "y")) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x")) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "z")) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x")) ")" )))) ")" )); registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: ) ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: ) ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: ) for ($#l1_sheffer1 :::"ShefferStr"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) for ($#l2_lattices :::"\/-SemiLattStr"::: ) ; cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) for ($#l1_lattices :::"/\-SemiLattStr"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v17_lattices :::"Boolean"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; registration cluster (Set ($#k4_sheffer1 :::"TrivShefferOrthoLattStr"::: ) ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ; cluster (Set ($#k4_sheffer1 :::"TrivShefferOrthoLattStr"::: ) ) -> ($#v8_robbins1 :::"well-complemented"::: ) ($#v9_sheffer1 :::"properly_defined"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) ($#v8_robbins1 :::"well-complemented"::: ) ($#v9_sheffer1 :::"properly_defined"::: ) ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: ) ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: ) ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: ) for ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) ; end; theorem :: SHEFFER1:26 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) ($#v8_robbins1 :::"well-complemented"::: ) ($#v9_sheffer1 :::"properly_defined"::: ) ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: ) )) ; theorem :: SHEFFER1:27 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) ($#v8_robbins1 :::"well-complemented"::: ) ($#v9_sheffer1 :::"properly_defined"::: ) ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: ) )) ; theorem :: SHEFFER1:28 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) ($#v8_robbins1 :::"well-complemented"::: ) ($#v9_sheffer1 :::"properly_defined"::: ) ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: ) )) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_sheffer1 :::"ShefferStr"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "a" :::"""::: -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: SHEFFER1:def 16 (Set "a" ($#k5_sheffer1 :::"|"::: ) "a"); end; :: deftheorem defines :::"""::: SHEFFER1:def 16 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_sheffer1 :::"ShefferStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k6_sheffer1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "a")))))); theorem :: SHEFFER1:29 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: ) ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "z")) ")" ) ")" ) ($#k6_sheffer1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "y")) ($#k6_sheffer1 :::"""::: ) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x")) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k6_sheffer1 :::"""::: ) ")" ) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x")) ")" ))))) ; theorem :: SHEFFER1:30 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: ) ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k6_sheffer1 :::"""::: ) ")" ) ($#k6_sheffer1 :::"""::: ) )))) ; theorem :: SHEFFER1:31 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_sheffer1 :::"properly_defined"::: ) ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: ) ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: ) ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: ) ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x")))))) ; theorem :: SHEFFER1:32 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_sheffer1 :::"properly_defined"::: ) ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: ) ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: ) ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: ) ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "x")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set "(" (Set (Var "y")) ($#k5_sheffer1 :::"|"::: ) (Set (Var "y")) ")" ))))) ; theorem :: SHEFFER1:33 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_sheffer1 :::"properly_defined"::: ) ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: ) ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: ) ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: ) ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v4_lattices :::"join-commutative"::: ) )) ; theorem :: SHEFFER1:34 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_sheffer1 :::"properly_defined"::: ) ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: ) ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: ) ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: ) ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v6_lattices :::"meet-commutative"::: ) )) ; theorem :: SHEFFER1:35 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_sheffer1 :::"properly_defined"::: ) ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: ) ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: ) ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: ) ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v11_lattices :::"distributive"::: ) )) ; theorem :: SHEFFER1:36 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_sheffer1 :::"properly_defined"::: ) ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: ) ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: ) ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: ) ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v3_sheffer1 :::"distributive'"::: ) )) ; theorem :: SHEFFER1:37 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_sheffer1 :::"properly_defined"::: ) ($#v10_sheffer1 :::"satisfying_Sheffer_1"::: ) ($#v11_sheffer1 :::"satisfying_Sheffer_2"::: ) ($#v12_sheffer1 :::"satisfying_Sheffer_3"::: ) ($#l3_sheffer1 :::"ShefferOrthoLattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::))) ;