:: ROBBINS1 semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"ComplStr"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"ComplStr":::(# :::"carrier":::, :::"Compl"::: #) -> ($#l1_robbins1 :::"ComplStr"::: ) ; sel :::"Compl"::: "c1" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; definitionattr "c1" is :::"strict"::: ; struct :::"ComplLLattStr"::: -> ($#l2_lattices :::"\/-SemiLattStr"::: ) "," ($#l1_robbins1 :::"ComplStr"::: ) ; aggr :::"ComplLLattStr":::(# :::"carrier":::, :::"L_join":::, :::"Compl"::: #) -> ($#l2_robbins1 :::"ComplLLattStr"::: ) ; end; definitionattr "c1" is :::"strict"::: ; struct :::"ComplULattStr"::: -> ($#l1_lattices :::"/\-SemiLattStr"::: ) "," ($#l1_robbins1 :::"ComplStr"::: ) ; aggr :::"ComplULattStr":::(# :::"carrier":::, :::"L_meet":::, :::"Compl"::: #) -> ($#l3_robbins1 :::"ComplULattStr"::: ) ; end; definitionattr "c1" is :::"strict"::: ; struct :::"OrthoLattStr"::: -> ($#l2_robbins1 :::"ComplLLattStr"::: ) "," ($#l3_lattices :::"LattStr"::: ) ; aggr :::"OrthoLattStr":::(# :::"carrier":::, :::"L_join":::, :::"L_meet":::, :::"Compl"::: #) -> ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; definitionfunc :::"TrivComplLat"::: -> ($#v2_robbins1 :::"strict"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) equals :: ROBBINS1:def 1 (Set ($#g2_robbins1 :::"ComplLLattStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "#)" ); end; :: deftheorem defines :::"TrivComplLat"::: ROBBINS1:def 1 : (Bool (Set ($#k1_robbins1 :::"TrivComplLat"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g2_robbins1 :::"ComplLLattStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "#)" )); definitionfunc :::"TrivOrtLat"::: -> ($#v4_robbins1 :::"strict"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) equals :: ROBBINS1:def 2 (Set ($#g4_robbins1 :::"OrthoLattStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "#)" ); end; :: deftheorem defines :::"TrivOrtLat"::: ROBBINS1:def 2 : (Bool (Set ($#k2_robbins1 :::"TrivOrtLat"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g4_robbins1 :::"OrthoLattStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "#)" )); registration cluster (Set ($#k1_robbins1 :::"TrivComplLat"::: ) ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_robbins1 :::"strict"::: ) ; cluster (Set ($#k2_robbins1 :::"TrivOrtLat"::: ) ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v4_robbins1 :::"strict"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v4_robbins1 :::"strict"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_robbins1 :::"strict"::: ) for ($#l2_robbins1 :::"ComplLLattStr"::: ) ; end; registrationlet "L" be (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; cluster (Set ($#g1_robbins1 :::"ComplStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" "L") "#)" ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_robbins1 :::"strict"::: ) for ($#l1_robbins1 :::"ComplStr"::: ) ; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_robbins1 :::"ComplStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "x" :::"`"::: -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: ROBBINS1:def 3 (Set (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" "L") ($#k3_funct_2 :::"."::: ) "x"); end; :: deftheorem defines :::"`"::: ROBBINS1:def 3 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_robbins1 :::"ComplStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "L"))) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))))); notationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); synonym "x" :::"+"::: "y" for "x" :::""\/""::: "y"; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "x" :::"*'"::: "y" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: ROBBINS1:def 4 (Set (Set "(" (Set "(" "x" ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::""\/""::: ) (Set "(" "y" ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ); end; :: deftheorem defines :::"*'"::: ROBBINS1:def 4 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k4_robbins1 :::"*'"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) )))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; attr "L" is :::"Robbins"::: means :: ROBBINS1:def 5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x")))); attr "L" is :::"Huntington"::: means :: ROBBINS1:def 6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))); end; :: deftheorem defines :::"Robbins"::: ROBBINS1:def 5 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v5_robbins1 :::"Robbins"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )); :: deftheorem defines :::"Huntington"::: ROBBINS1:def 6 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v6_robbins1 :::"Huntington"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )); definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) ; attr "G" is :::"join-idempotent"::: means :: ROBBINS1:def 7 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "holds" (Bool (Set (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))); end; :: deftheorem defines :::"join-idempotent"::: ROBBINS1:def 7 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v7_robbins1 :::"join-idempotent"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )); registration cluster (Set ($#k1_robbins1 :::"TrivComplLat"::: ) ) -> ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v2_robbins1 :::"strict"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#v6_robbins1 :::"Huntington"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ; cluster (Set ($#k2_robbins1 :::"TrivOrtLat"::: ) ) -> ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v4_robbins1 :::"strict"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#v6_robbins1 :::"Huntington"::: ) ; end; registration cluster (Set ($#k2_robbins1 :::"TrivOrtLat"::: ) ) -> ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v4_robbins1 :::"strict"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v2_robbins1 :::"strict"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#v6_robbins1 :::"Huntington"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) for ($#l2_robbins1 :::"ComplLLattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v4_robbins1 :::"strict"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#v6_robbins1 :::"Huntington"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); :: original: :::"+"::: redefine func "x" :::"+"::: "y" -> bbbadM1_SUBSET_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")); commutativity (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")) "holds" (Bool (Set (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "x"))))) ; end; theorem :: ROBBINS1: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")) ($#k4_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k4_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: ROBBINS1:2 (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")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ))))) ; theorem :: ROBBINS1:3 (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 "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: ROBBINS1:4 (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 (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ))))) ; theorem :: ROBBINS1:5 (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"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "c")) ($#k5_robbins1 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Set (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" )))) ; theorem :: ROBBINS1:6 (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"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v14_lattices :::"upper-bounded"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_robbins1 :::"Huntington"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v14_lattices :::"upper-bounded"::: ) for ($#l2_robbins1 :::"ComplLLattStr"::: ) ; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_robbins1 :::"Huntington"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; redefine func :::"Top"::: "L" means :: ROBBINS1:def 8 (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" )))); end; :: deftheorem defines :::"Top"::: ROBBINS1:def 8 : (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"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "b2")) "being" bbbadM1_SUBSET_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1")))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" )))) ")" ))); theorem :: ROBBINS1:7 (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"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "c")) ($#k4_robbins1 :::"*'"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" )))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); :: original: :::"*'"::: redefine func "x" :::"*'"::: "y" -> ($#m1_subset_1 :::"Element":::) "of" "L"; commutativity (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")) "holds" (Bool (Set (Set (Var "x")) ($#k4_robbins1 :::"*'"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k4_robbins1 :::"*'"::: ) (Set (Var "x"))))) ; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_robbins1 :::"Huntington"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; func :::"Bot"::: "L" -> ($#m1_subset_1 :::"Element":::) "of" "L" means :: ROBBINS1:def 9 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set it ($#k6_robbins1 :::"*'"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) it)); end; :: deftheorem defines :::"Bot"::: ROBBINS1:def 9 : (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"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_robbins1 :::"Bot"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "b2")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b2")))) ")" ))); theorem :: ROBBINS1:8 (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"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k7_robbins1 :::"Bot"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS1:9 (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"::: ) ($#v7_robbins1 :::"join-idempotent"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "L")) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_robbins1 :::"Bot"::: ) (Set (Var "L")))) & (Bool (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_robbins1 :::"Bot"::: ) (Set (Var "L")) ")" ) ($#k3_robbins1 :::"`"::: ) )) ")" )) ; theorem :: ROBBINS1:10 (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")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: ROBBINS1:11 (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 (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: ROBBINS1:12 (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")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_robbins1 :::"Huntington"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_robbins1 :::"join-idempotent"::: ) for ($#l2_robbins1 :::"ComplLLattStr"::: ) ; end; theorem :: ROBBINS1:13 (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")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set "(" ($#k7_robbins1 :::"Bot"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: ROBBINS1:14 (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")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: ROBBINS1:15 (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")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_robbins1 :::"Bot"::: ) (Set (Var "L")))))) ; theorem :: ROBBINS1:16 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")))))) ; theorem :: ROBBINS1:17 (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 (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS1:18 (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")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: ROBBINS1:19 (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")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))))) ; theorem :: ROBBINS1:20 (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 (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: ROBBINS1:21 (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 (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: ROBBINS1:22 (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")) "st" (Bool (Bool (Set (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))) & (Bool (Set (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: ROBBINS1:23 (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")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k7_robbins1 :::"Bot"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: ROBBINS1:24 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "c")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "c")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "c")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "c")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))))) ; theorem :: ROBBINS1:25 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "c")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_robbins1 :::"Bot"::: ) (Set (Var "L")))) & (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_robbins1 :::"Bot"::: ) (Set (Var "L")))) & (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_robbins1 :::"Bot"::: ) (Set (Var "L")))) & (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_robbins1 :::"Bot"::: ) (Set (Var "L")))) & (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "c")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "c")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_robbins1 :::"Bot"::: ) (Set (Var "L")))) ")" ))) ; theorem :: ROBBINS1:26 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "c")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" ))))) ; theorem :: ROBBINS1:27 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k5_robbins1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "c")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "c")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "c")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ))))) ; theorem :: ROBBINS1:28 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k5_robbins1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))))) ; theorem :: ROBBINS1:29 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" ) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k5_robbins1 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_robbins1 :::"Bot"::: ) (Set (Var "L")))))) ; theorem :: ROBBINS1:30 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "b")) ($#k5_robbins1 :::"+"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "b")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" ))))) ; theorem :: ROBBINS1:31 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k6_robbins1 :::"*'"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k6_robbins1 :::"*'"::: ) (Set "(" (Set (Var "a")) ($#k5_robbins1 :::"+"::: ) (Set (Var "c")) ")" ))))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins1 :::"OrthoLattStr"::: ) ; attr "L" is :::"well-complemented"::: means :: ROBBINS1:def 10 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ) ($#r2_lattices :::"is_a_complement_of"::: ) (Set (Var "a")))); end; :: deftheorem defines :::"well-complemented"::: ROBBINS1:def 10 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins1 :::"OrthoLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v8_robbins1 :::"well-complemented"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ) ($#r2_lattices :::"is_a_complement_of"::: ) (Set (Var "a")))) ")" )); registration cluster (Set ($#k2_robbins1 :::"TrivOrtLat"::: ) ) -> ($#v17_lattices :::"Boolean"::: ) ($#v4_robbins1 :::"strict"::: ) ($#v8_robbins1 :::"well-complemented"::: ) ; end; definitionmode preOrthoLattice is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) ($#v4_robbins1 :::"strict"::: ) ($#v8_robbins1 :::"well-complemented"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; theorem :: ROBBINS1:32 (Bool "for" (Set (Var "L")) "being" ($#v11_lattices :::"distributive"::: ) ($#v8_robbins1 :::"well-complemented"::: ) ($#l4_robbins1 :::"preOrthoLattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: ROBBINS1:33 (Bool "for" (Set (Var "L")) "being" ($#v11_lattices :::"distributive"::: ) ($#v15_lattices :::"bounded"::: ) ($#v8_robbins1 :::"well-complemented"::: ) ($#l4_robbins1 :::"preOrthoLattice":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k4_lattices :::""/\""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; func :::"CLatt"::: "L" -> ($#v4_robbins1 :::"strict"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) means :: ROBBINS1:def 11 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) & (Bool (Set "the" ($#u2_lattices :::"L_join"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_lattices :::"L_join"::: ) "of" "L")) & (Bool (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" "L")) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" it) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_robbins1 :::"*'"::: ) (Set (Var "b")))) ")" ) ")" ); end; :: deftheorem defines :::"CLatt"::: ROBBINS1:def 11 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v4_robbins1 :::"strict"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_robbins1 :::"CLatt"::: ) (Set (Var "L")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L")))) & (Bool (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "L")))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "b2"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_robbins1 :::"*'"::: ) (Set (Var "b")))) ")" ) ")" ) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; cluster (Set ($#k8_robbins1 :::"CLatt"::: ) "L") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_robbins1 :::"strict"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; cluster (Set ($#k8_robbins1 :::"CLatt"::: ) "L") -> ($#v4_lattices :::"join-commutative"::: ) ($#v4_robbins1 :::"strict"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_lattices :::"join-associative"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; cluster (Set ($#k8_robbins1 :::"CLatt"::: ) "L") -> ($#v5_lattices :::"join-associative"::: ) ($#v4_robbins1 :::"strict"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; cluster (Set ($#k8_robbins1 :::"CLatt"::: ) "L") -> ($#v6_lattices :::"meet-commutative"::: ) ($#v4_robbins1 :::"strict"::: ) ; end; theorem :: ROBBINS1:34 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k8_robbins1 :::"CLatt"::: ) (Set (Var "L")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a9"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9")))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k4_robbins1 :::"*'"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a9")) ($#k2_lattices :::""/\""::: ) (Set (Var "b9")))) & (Bool (Set (Set (Var "a")) ($#k1_lattices :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a9")) ($#k1_lattices :::""\/""::: ) (Set (Var "b9")))) & (Bool (Set (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a9")) ($#k3_robbins1 :::"`"::: ) )) ")" )))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_robbins1 :::"Huntington"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; cluster (Set ($#k8_robbins1 :::"CLatt"::: ) "L") -> ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v4_robbins1 :::"strict"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_robbins1 :::"Huntington"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; cluster (Set ($#k8_robbins1 :::"CLatt"::: ) "L") -> ($#v4_robbins1 :::"strict"::: ) ($#v6_robbins1 :::"Huntington"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_robbins1 :::"Huntington"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; cluster (Set ($#k8_robbins1 :::"CLatt"::: ) "L") -> ($#v13_lattices :::"lower-bounded"::: ) ($#v4_robbins1 :::"strict"::: ) ; end; theorem :: ROBBINS1:35 (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"::: ) "holds" (Bool (Set ($#k7_robbins1 :::"Bot"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set "(" ($#k8_robbins1 :::"CLatt"::: ) (Set (Var "L")) ")" )))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_robbins1 :::"Huntington"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; cluster (Set ($#k8_robbins1 :::"CLatt"::: ) "L") -> ($#v11_lattices :::"distributive"::: ) ($#v15_lattices :::"bounded"::: ) ($#v16_lattices :::"complemented"::: ) ($#v4_robbins1 :::"strict"::: ) ; end; begin notationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); synonym :::"-"::: "x" for "x" :::"`"::: ; end; definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; redefine attr "G" is :::"Huntington"::: means :: ROBBINS1:def 12 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "holds" (Bool (Set (Set "(" ($#k3_robbins1 :::"-"::: ) (Set "(" (Set "(" ($#k3_robbins1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" ($#k3_robbins1 :::"-"::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" ($#k3_robbins1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set "(" ($#k3_robbins1 :::"-"::: ) (Set (Var "y")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "y")))); end; :: deftheorem defines :::"Huntington"::: ROBBINS1:def 12 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v6_robbins1 :::"Huntington"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" ($#k3_robbins1 :::"-"::: ) (Set "(" (Set "(" ($#k3_robbins1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" ($#k3_robbins1 :::"-"::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" ($#k3_robbins1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set "(" ($#k3_robbins1 :::"-"::: ) (Set (Var "y")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ")" )); definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; attr "G" is :::"with_idempotent_element"::: means :: ROBBINS1:def 13 (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "st" (Bool (Set (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))); end; :: deftheorem defines :::"with_idempotent_element"::: ROBBINS1:def 13 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v9_robbins1 :::"with_idempotent_element"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )); definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func :::"\delta"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: ROBBINS1:def 14 (Set ($#k3_robbins1 :::"-"::: ) (Set "(" (Set "(" ($#k3_robbins1 :::"-"::: ) "x" ")" ) ($#k1_lattices :::"+"::: ) "y" ")" )); end; :: deftheorem defines :::"\delta"::: ROBBINS1:def 14 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_robbins1 :::"-"::: ) (Set "(" (Set "(" ($#k3_robbins1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ))))); definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func :::"Expand"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: ROBBINS1:def 15 (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set "(" "x" ($#k1_lattices :::"+"::: ) "y" ")" ) "," (Set "(" ($#k9_robbins1 :::"\delta"::: ) "(" "x" "," "y" ")" ")" ) ")" ); end; :: deftheorem defines :::"Expand"::: ROBBINS1:def 15 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k10_robbins1 :::"Expand"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) "," (Set "(" ($#k9_robbins1 :::"\delta"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )))); definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func "x" :::"_0"::: -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: ROBBINS1:def 16 (Set ($#k3_robbins1 :::"-"::: ) (Set "(" (Set "(" ($#k3_robbins1 :::"-"::: ) "x" ")" ) ($#k1_lattices :::"+"::: ) "x" ")" )); func :::"Double"::: "x" -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: ROBBINS1:def 17 (Set "x" ($#k1_lattices :::"+"::: ) "x"); end; :: deftheorem defines :::"_0"::: ROBBINS1:def 16 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "x")) ($#k11_robbins1 :::"_0"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_robbins1 :::"-"::: ) (Set "(" (Set "(" ($#k3_robbins1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ))))); :: deftheorem defines :::"Double"::: ROBBINS1:def 17 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k12_robbins1 :::"Double"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "x")))))); definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func "x" :::"_1"::: -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: ROBBINS1:def 18 (Set (Set "(" "x" ($#k11_robbins1 :::"_0"::: ) ")" ) ($#k1_lattices :::"+"::: ) "x"); func "x" :::"_2"::: -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: ROBBINS1:def 19 (Set (Set "(" "x" ($#k11_robbins1 :::"_0"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" ($#k12_robbins1 :::"Double"::: ) "x" ")" )); func "x" :::"_3"::: -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: ROBBINS1:def 20 (Set (Set "(" "x" ($#k11_robbins1 :::"_0"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" ($#k12_robbins1 :::"Double"::: ) "x" ")" ) ($#k1_lattices :::"+"::: ) "x" ")" )); func "x" :::"_4"::: -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: ROBBINS1:def 21 (Set (Set "(" "x" ($#k11_robbins1 :::"_0"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" ($#k12_robbins1 :::"Double"::: ) "x" ")" ) ($#k1_lattices :::"+"::: ) (Set "(" ($#k12_robbins1 :::"Double"::: ) "x" ")" ) ")" )); end; :: deftheorem defines :::"_1"::: ROBBINS1:def 18 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "x")) ($#k13_robbins1 :::"_1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k11_robbins1 :::"_0"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "x")))))); :: deftheorem defines :::"_2"::: ROBBINS1:def 19 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "x")) ($#k14_robbins1 :::"_2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k11_robbins1 :::"_0"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" ($#k12_robbins1 :::"Double"::: ) (Set (Var "x")) ")" ))))); :: deftheorem defines :::"_3"::: ROBBINS1:def 20 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "x")) ($#k15_robbins1 :::"_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k11_robbins1 :::"_0"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" ($#k12_robbins1 :::"Double"::: ) (Set (Var "x")) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ))))); :: deftheorem defines :::"_4"::: ROBBINS1:def 21 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "x")) ($#k16_robbins1 :::"_4"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k11_robbins1 :::"_0"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" ($#k12_robbins1 :::"Double"::: ) (Set (Var "x")) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" ($#k12_robbins1 :::"Double"::: ) (Set (Var "x")) ")" ) ")" ))))); theorem :: ROBBINS1:36 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) "," (Set "(" ($#k9_robbins1 :::"\delta"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ROBBINS1:37 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k10_robbins1 :::"Expand"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ROBBINS1:38 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set "(" (Set "(" ($#k3_robbins1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_robbins1 :::"-"::: ) (Set "(" (Set "(" ($#k9_robbins1 :::"\delta"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ))))) ; theorem :: ROBBINS1:39 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set (Var "x")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_robbins1 :::"_0"::: ) )))) ; theorem :: ROBBINS1:40 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set "(" ($#k12_robbins1 :::"Double"::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "x")) ($#k11_robbins1 :::"_0"::: ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: ROBBINS1:41 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set "(" (Set (Var "x")) ($#k14_robbins1 :::"_2"::: ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_robbins1 :::"_0"::: ) )))) ; theorem :: ROBBINS1:42 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k16_robbins1 :::"_4"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k11_robbins1 :::"_0"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k15_robbins1 :::"_3"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k13_robbins1 :::"_1"::: ) ")" ))))) ; theorem :: ROBBINS1:43 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k15_robbins1 :::"_3"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k11_robbins1 :::"_0"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k14_robbins1 :::"_2"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k13_robbins1 :::"_1"::: ) ")" ))))) ; theorem :: ROBBINS1:44 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k15_robbins1 :::"_3"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k16_robbins1 :::"_4"::: ) )))) ; theorem :: ROBBINS1:45 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set "(" (Set (Var "x")) ($#k15_robbins1 :::"_3"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k11_robbins1 :::"_0"::: ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: ROBBINS1:46 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k3_robbins1 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_robbins1 :::"-"::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" )))) ; theorem :: ROBBINS1:47 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k3_robbins1 :::"-"::: ) (Set (Var "y")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set (Var "y")) "," (Set "(" ($#k3_robbins1 :::"-"::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: ROBBINS1:48 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set "(" (Set (Var "x")) ($#k15_robbins1 :::"_3"::: ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_robbins1 :::"_0"::: ) )))) ; theorem :: ROBBINS1:49 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set "(" (Set "(" (Set (Var "x")) ($#k13_robbins1 :::"_1"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k15_robbins1 :::"_3"::: ) ")" ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_robbins1 :::"_0"::: ) )))) ; theorem :: ROBBINS1:50 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set "(" (Set "(" (Set (Var "x")) ($#k13_robbins1 :::"_1"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k14_robbins1 :::"_2"::: ) ")" ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_robbins1 :::"_0"::: ) )))) ; theorem :: ROBBINS1:51 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set "(" (Set "(" (Set (Var "x")) ($#k13_robbins1 :::"_1"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k15_robbins1 :::"_3"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "x")) ($#k11_robbins1 :::"_0"::: ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func :::"\beta"::: "x" -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: ROBBINS1:def 22 (Set (Set "(" (Set "(" ($#k3_robbins1 :::"-"::: ) (Set "(" (Set "(" "x" ($#k13_robbins1 :::"_1"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" "x" ($#k15_robbins1 :::"_3"::: ) ")" ) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) "x" ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" ($#k3_robbins1 :::"-"::: ) (Set "(" "x" ($#k15_robbins1 :::"_3"::: ) ")" ) ")" )); end; :: deftheorem defines :::"\beta"::: ROBBINS1:def 22 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k17_robbins1 :::"\beta"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_robbins1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k13_robbins1 :::"_1"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k15_robbins1 :::"_3"::: ) ")" ) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" ($#k3_robbins1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k15_robbins1 :::"_3"::: ) ")" ) ")" ))))); theorem :: ROBBINS1:52 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set "(" ($#k17_robbins1 :::"\beta"::: ) (Set (Var "x")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_robbins1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k15_robbins1 :::"_3"::: ) ")" ))))) ; theorem :: ROBBINS1:53 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k9_robbins1 :::"\delta"::: ) "(" (Set "(" ($#k17_robbins1 :::"\beta"::: ) (Set (Var "x")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_robbins1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k13_robbins1 :::"_1"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k15_robbins1 :::"_3"::: ) ")" ) ")" ))))) ; theorem :: ROBBINS1:54 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set ($#k3_robbins1 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_robbins1 :::"-"::: ) (Set (Var "z")))))) ; begin theorem :: ROBBINS1:55 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) "st" (Bool (Bool "(" "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_robbins1 :::"-"::: ) (Set "(" ($#k3_robbins1 :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" )) "holds" (Bool (Set (Var "G")) "is" ($#v6_robbins1 :::"Huntington"::: ) )) ; theorem :: ROBBINS1:56 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) "st" (Bool (Bool (Set (Var "G")) "is" ($#v9_robbins1 :::"with_idempotent_element"::: ) )) "holds" (Bool (Set (Var "G")) "is" ($#v6_robbins1 :::"Huntington"::: ) )) ; registration cluster (Set ($#k1_robbins1 :::"TrivComplLat"::: ) ) -> ($#v2_robbins1 :::"strict"::: ) ($#v9_robbins1 :::"with_idempotent_element"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#v9_robbins1 :::"with_idempotent_element"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#v6_robbins1 :::"Huntington"::: ) for ($#l2_robbins1 :::"ComplLLattStr"::: ) ; end; theorem :: ROBBINS1:57 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) "st" (Bool (Bool "ex" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Set (Var "c")) ($#k5_robbins1 :::"+"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) "holds" (Bool (Set (Var "G")) "is" ($#v6_robbins1 :::"Huntington"::: ) )) ; theorem :: ROBBINS1:58 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "z"))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v5_robbins1 :::"Robbins"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_robbins1 :::"Huntington"::: ) for ($#l2_robbins1 :::"ComplLLattStr"::: ) ; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins1 :::"OrthoLattStr"::: ) ; attr "L" is :::"de_Morgan"::: means :: ROBBINS1:def 23 (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 "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ))); end; :: deftheorem defines :::"de_Morgan"::: ROBBINS1:def 23 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins1 :::"OrthoLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v10_robbins1 :::"de_Morgan"::: ) ) "iff" (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 "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ))) ")" )); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; cluster (Set ($#k8_robbins1 :::"CLatt"::: ) "L") -> ($#v4_robbins1 :::"strict"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ; end; theorem :: ROBBINS1:59 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_robbins1 :::"well-complemented"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "x")) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")))) ")" ))) ; theorem :: ROBBINS1:60 (Bool "for" (Set (Var "L")) "being" ($#v11_lattices :::"distributive"::: ) ($#v15_lattices :::"bounded"::: ) ($#v8_robbins1 :::"well-complemented"::: ) ($#l4_robbins1 :::"preOrthoLattice":::) "holds" (Bool (Set (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "L")) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L"))))) ; registration cluster (Set ($#k2_robbins1 :::"TrivOrtLat"::: ) ) -> ($#v4_robbins1 :::"strict"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) ($#v4_robbins1 :::"strict"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#v6_robbins1 :::"Huntington"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_lattices :::"meet-commutative"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; theorem :: ROBBINS1:61 (Bool "for" (Set (Var "L")) "being" ($#v6_robbins1 :::"Huntington"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#l4_robbins1 :::"preOrthoLattice":::) "holds" (Bool (Set ($#k7_robbins1 :::"Bot"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L"))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) ($#v8_robbins1 :::"well-complemented"::: ) -> ($#v6_robbins1 :::"Huntington"::: ) ($#v8_robbins1 :::"well-complemented"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v6_robbins1 :::"Huntington"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) -> ($#v17_lattices :::"Boolean"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v5_robbins1 :::"Robbins"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) -> ($#v17_lattices :::"Boolean"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) ($#v8_robbins1 :::"well-complemented"::: ) -> ($#v5_robbins1 :::"Robbins"::: ) ($#v8_robbins1 :::"well-complemented"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end;