:: ROBBINS3 semantic presentation begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) ; attr "L" is :::"join-Associative"::: means :: ROBBINS3:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "y")) ($#k1_lattices :::""\/""::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set (Var "z")) ")" )))); end; :: deftheorem defines :::"join-Associative"::: ROBBINS3:def 1 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_robbins3 :::"join-Associative"::: ) ) "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 (Var "x")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "y")) ($#k1_lattices :::""\/""::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set (Var "z")) ")" )))) ")" )); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lattices :::"/\-SemiLattStr"::: ) ; attr "L" is :::"meet-Associative"::: means :: ROBBINS3:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set (Var "x")) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "y")) ($#k2_lattices :::""/\""::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "x")) ($#k2_lattices :::""/\""::: ) (Set (Var "z")) ")" )))); end; :: deftheorem defines :::"meet-Associative"::: ROBBINS3:def 2 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lattices :::"/\-SemiLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_robbins3 :::"meet-Associative"::: ) ) "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 (Var "x")) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "y")) ($#k2_lattices :::""/\""::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "x")) ($#k2_lattices :::""/\""::: ) (Set (Var "z")) ")" )))) ")" )); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; attr "L" is :::"meet-Absorbing"::: means :: ROBBINS3:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "x")) ($#k2_lattices :::""/\""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))); end; :: deftheorem defines :::"meet-Absorbing"::: ROBBINS3:def 3 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_robbins3 :::"meet-Absorbing"::: ) ) "iff" (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 "(" (Set (Var "x")) ($#k2_lattices :::""/\""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )); theorem :: ROBBINS3:1 (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_robbins3 :::"meet-Associative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v1_robbins3 :::"join-Associative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_robbins3 :::"meet-Absorbing"::: ) ) & (Bool (Set (Var "L")) "is" ($#v9_lattices :::"join-absorbing"::: ) )) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v5_sheffer1 :::"meet-idempotent"::: ) ) & (Bool (Set (Var "L")) "is" ($#v7_robbins1 :::"join-idempotent"::: ) ) ")" )) ; theorem :: ROBBINS3: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" ($#v2_robbins3 :::"meet-Associative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v1_robbins3 :::"join-Associative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_robbins3 :::"meet-Absorbing"::: ) ) & (Bool (Set (Var "L")) "is" ($#v9_lattices :::"join-absorbing"::: ) )) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v6_lattices :::"meet-commutative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v4_lattices :::"join-commutative"::: ) ) ")" )) ; theorem :: ROBBINS3:3 (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_robbins3 :::"meet-Associative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v1_robbins3 :::"join-Associative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_robbins3 :::"meet-Absorbing"::: ) ) & (Bool (Set (Var "L")) "is" ($#v9_lattices :::"join-absorbing"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#v8_lattices :::"meet-absorbing"::: ) )) ; theorem :: ROBBINS3: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_robbins3 :::"meet-Associative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v1_robbins3 :::"join-Associative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_robbins3 :::"meet-Absorbing"::: ) ) & (Bool (Set (Var "L")) "is" ($#v9_lattices :::"join-absorbing"::: ) )) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v7_lattices :::"meet-associative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v5_lattices :::"join-associative"::: ) ) ")" )) ; theorem :: ROBBINS3:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v10_lattices :::"Lattice-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_robbins3 :::"meet-Associative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v1_robbins3 :::"join-Associative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_robbins3 :::"meet-Absorbing"::: ) ) & (Bool (Set (Var "L")) "is" ($#v9_lattices :::"join-absorbing"::: ) ) ")" ) ")" )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins3 :::"join-Associative"::: ) ($#v2_robbins3 :::"meet-Associative"::: ) ($#v3_robbins3 :::"meet-Absorbing"::: ) for ($#l3_lattices :::"LattStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_lattices :::"join-absorbing"::: ) ($#v1_robbins3 :::"join-Associative"::: ) ($#v2_robbins3 :::"meet-Associative"::: ) ($#v3_robbins3 :::"meet-Absorbing"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; begin registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_oposet_1 :::"PartialOrdered"::: ) ($#v10_oposet_1 :::"OrderInvolutive"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_oposet_1 :::"Dneg"::: ) ($#v6_oposet_1 :::"PartialOrdered"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; theorem :: ROBBINS3:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_oposet_1 :::"Dneg"::: ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) (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 :: ROBBINS3:7 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_oposet_1 :::"PartialOrdered"::: ) ($#v10_oposet_1 :::"OrderInvolutive"::: ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) )))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_qmax_1 :::"strict"::: ) ($#v1_oposet_1 :::"Dneg"::: ) ($#v6_oposet_1 :::"PartialOrdered"::: ) ($#v7_oposet_1 :::"Pure"::: ) ($#v10_oposet_1 :::"OrderInvolutive"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; notationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); synonym "x" :::"|_|"::: "y" for "x" :::""\/""::: "y"; end; notationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lattices :::"/\-SemiLattStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); synonym "x" :::"|^|"::: "y" for "x" :::""/\""::: "y"; end; notationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); synonym "x" :::""|^|""::: "y" for "x" :::""/\""::: "y"; synonym "x" :::""|_|""::: "y" for "x" :::""\/""::: "y"; end; begin definitionattr "c1" is :::"strict"::: ; struct :::"\/-SemiLattRelStr"::: -> ($#l2_lattices :::"\/-SemiLattStr"::: ) "," ($#l1_orders_2 :::"RelStr"::: ) ; aggr :::"\/-SemiLattRelStr":::(# :::"carrier":::, :::"L_join":::, :::"InternalRel"::: #) -> ($#l1_robbins3 :::"\/-SemiLattRelStr"::: ) ; end; definitionattr "c1" is :::"strict"::: ; struct :::"/\-SemiLattRelStr"::: -> ($#l1_lattices :::"/\-SemiLattStr"::: ) "," ($#l1_orders_2 :::"RelStr"::: ) ; aggr :::"/\-SemiLattRelStr":::(# :::"carrier":::, :::"L_meet":::, :::"InternalRel"::: #) -> ($#l2_robbins3 :::"/\-SemiLattRelStr"::: ) ; end; definitionattr "c1" is :::"strict"::: ; struct :::"LattRelStr"::: -> ($#l2_robbins3 :::"/\-SemiLattRelStr"::: ) "," ($#l1_robbins3 :::"\/-SemiLattRelStr"::: ) "," ($#l3_lattices :::"LattStr"::: ) ; aggr :::"LattRelStr":::(# :::"carrier":::, :::"L_join":::, :::"L_meet":::, :::"InternalRel"::: #) -> ($#l3_robbins3 :::"LattRelStr"::: ) ; end; definitionfunc :::"TrivLattRelStr"::: -> ($#l3_robbins3 :::"LattRelStr"::: ) equals :: ROBBINS3:def 4 (Set ($#g3_robbins3 :::"LattRelStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Num 1) ")" ) "#)" ); end; :: deftheorem defines :::"TrivLattRelStr"::: ROBBINS3:def 4 : (Bool (Set ($#k1_robbins3 :::"TrivLattRelStr"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g3_robbins3 :::"LattRelStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Num 1) ")" ) "#)" )); registration cluster (Set ($#k1_robbins3 :::"TrivLattRelStr"::: ) ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_robbins3 :::"\/-SemiLattRelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l2_robbins3 :::"/\-SemiLattRelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l3_robbins3 :::"LattRelStr"::: ) ; end; theorem :: ROBBINS3:8 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) "is" ($#v4_relat_2 :::"antisymmetric"::: ) ) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) "is" ($#v8_relat_2 :::"transitive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool (Set (Var "R")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) & (Bool (Set (Var "R")) "is" ($#v4_orders_2 :::"transitive"::: ) ) ")" )) ; registration cluster (Set ($#k1_robbins3 :::"TrivLattRelStr"::: ) ) -> ($#v3_orders_2 :::"reflexive"::: ) ; end; registration cluster ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) for ($#l3_robbins3 :::"LattRelStr"::: ) ; end; registration cluster (Set ($#k1_robbins3 :::"TrivLattRelStr"::: ) ) -> ($#v3_robbins3 :::"meet-Absorbing"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) for ($#l3_robbins3 :::"LattRelStr"::: ) ; end; definitionlet "L" be ($#l3_lattices :::"Lattice":::); :: original: :::"LattRel"::: redefine func :::"LattRel"::: "L" -> ($#m1_subset_1 :::"Order":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"); end; begin definitionattr "c1" is :::"strict"::: ; struct :::"OrthoLattRelStr"::: -> ($#l3_robbins3 :::"LattRelStr"::: ) "," ($#l4_robbins1 :::"OrthoLattStr"::: ) "," ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; aggr :::"OrthoLattRelStr":::(# :::"carrier":::, :::"L_join":::, :::"L_meet":::, :::"InternalRel":::, :::"Compl"::: #) -> ($#l4_robbins3 :::"OrthoLattRelStr"::: ) ; end; definitionfunc :::"TrivCLRelStr"::: -> ($#l4_robbins3 :::"OrthoLattRelStr"::: ) equals :: ROBBINS3:def 5 (Set ($#g4_robbins3 :::"OrthoLattRelStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Num 1) ")" ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "#)" ); end; :: deftheorem defines :::"TrivCLRelStr"::: ROBBINS3:def 5 : (Bool (Set ($#k3_robbins3 :::"TrivCLRelStr"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g4_robbins3 :::"OrthoLattRelStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Num 1) ")" ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "#)" )); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_robbins1 :::"ComplStr"::: ) ; attr "L" is :::"involutive"::: means :: ROBBINS3:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x")))); end; :: deftheorem defines :::"involutive"::: ROBBINS3:def 6 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_robbins1 :::"ComplStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v8_robbins3 :::"involutive"::: ) ) "iff" (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")))) ")" )); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; attr "L" is :::"with_Top"::: means :: ROBBINS3:def 7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set (Var "x")) ($#k1_lattices :::"|_|"::: ) (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_lattices :::"|_|"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" )))); end; :: deftheorem defines :::"with_Top"::: ROBBINS3:def 7 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v9_robbins3 :::"with_Top"::: ) ) "iff" (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 "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_lattices :::"|_|"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" )))) ")" )); registration cluster (Set ($#k2_robbins1 :::"TrivOrtLat"::: ) ) -> ($#v8_robbins3 :::"involutive"::: ) ($#v9_robbins3 :::"with_Top"::: ) ; end; registration cluster (Set ($#k3_robbins3 :::"TrivCLRelStr"::: ) ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ; end; registration cluster (Set ($#k3_robbins3 :::"TrivCLRelStr"::: ) ) -> ($#v3_orders_2 :::"reflexive"::: ) ; end; registration cluster (Set ($#k3_robbins3 :::"TrivCLRelStr"::: ) ) -> ($#v8_robbins3 :::"involutive"::: ) ($#v9_robbins3 :::"with_Top"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) bbbadV8_STRUCT_0() (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#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"::: ) ($#v11_lattices :::"distributive"::: ) ($#v12_lattices :::"modular"::: ) ($#v13_lattices :::"lower-bounded"::: ) ($#v14_lattices :::"upper-bounded"::: ) bbbadV15_LATTICES() ($#v16_lattices :::"complemented"::: ) ($#v17_lattices :::"Boolean"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v1_sheffer1 :::"upper-bounded'"::: ) ($#v2_sheffer1 :::"lower-bounded'"::: ) ($#v3_sheffer1 :::"distributive'"::: ) ($#v4_sheffer1 :::"complemented'"::: ) ($#v1_robbins3 :::"join-Associative"::: ) ($#v2_robbins3 :::"meet-Associative"::: ) ($#v3_robbins3 :::"meet-Absorbing"::: ) ($#v8_robbins3 :::"involutive"::: ) ($#v9_robbins3 :::"with_Top"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; definitionmode Ortholattice is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v8_robbins3 :::"involutive"::: ) ($#v9_robbins3 :::"with_Top"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; begin theorem :: ROBBINS3:9 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "K"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) "#)" )) & (Bool (Set (Var "K")) "is" ($#v4_lattices :::"join-commutative"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#v4_lattices :::"join-commutative"::: ) )) ; theorem :: ROBBINS3:10 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "K"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) "#)" )) & (Bool (Set (Var "K")) "is" ($#v6_lattices :::"meet-commutative"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#v6_lattices :::"meet-commutative"::: ) )) ; theorem :: ROBBINS3:11 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "K"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) "#)" )) & (Bool (Set (Var "K")) "is" ($#v5_lattices :::"join-associative"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#v5_lattices :::"join-associative"::: ) )) ; theorem :: ROBBINS3:12 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "K"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) "#)" )) & (Bool (Set (Var "K")) "is" ($#v7_lattices :::"meet-associative"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#v7_lattices :::"meet-associative"::: ) )) ; theorem :: ROBBINS3:13 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "K"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) "#)" )) & (Bool (Set (Var "K")) "is" ($#v9_lattices :::"join-absorbing"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#v9_lattices :::"join-absorbing"::: ) )) ; theorem :: ROBBINS3:14 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "K"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) "#)" )) & (Bool (Set (Var "K")) "is" ($#v8_lattices :::"meet-absorbing"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#v8_lattices :::"meet-absorbing"::: ) )) ; theorem :: ROBBINS3:15 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "K"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) "#)" )) & (Bool (Set (Var "K")) "is" ($#v10_lattices :::"Lattice-like"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#v10_lattices :::"Lattice-like"::: ) )) ; theorem :: ROBBINS3:16 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) "st" (Bool (Bool (Set ($#g2_lattices :::"\/-SemiLattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g2_lattices :::"\/-SemiLattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2")))) "holds" (Bool (Set (Set (Var "a1")) ($#k1_lattices :::""\/""::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k1_lattices :::""\/""::: ) (Set (Var "b2"))))))) ; theorem :: ROBBINS3:17 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lattices :::"/\-SemiLattStr"::: ) "st" (Bool (Bool (Set ($#g1_lattices :::"/\-SemiLattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_lattices :::"/\-SemiLattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2")))) "holds" (Bool (Set (Set (Var "a1")) ($#k2_lattices :::""/\""::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k2_lattices :::""/\""::: ) (Set (Var "b2"))))))) ; theorem :: ROBBINS3:18 (Bool "for" (Set (Var "K")) "," (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 "K")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "K"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "L")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ))))) ; theorem :: ROBBINS3:19 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) "st" (Bool (Bool (Set ($#g2_robbins1 :::"ComplLLattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "K"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g2_robbins1 :::"ComplLLattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "L"))) "#)" )) & (Bool (Set (Var "K")) "is" ($#v9_robbins3 :::"with_Top"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#v9_robbins3 :::"with_Top"::: ) )) ; theorem :: ROBBINS3:20 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins1 :::"OrthoLattStr"::: ) "st" (Bool (Bool (Set ($#g4_robbins1 :::"OrthoLattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "K"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g4_robbins1 :::"OrthoLattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "L"))) "#)" )) & (Bool (Set (Var "K")) "is" ($#v10_robbins1 :::"de_Morgan"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#v10_robbins1 :::"de_Morgan"::: ) )) ; theorem :: ROBBINS3:21 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins1 :::"OrthoLattStr"::: ) "st" (Bool (Bool (Set ($#g4_robbins1 :::"OrthoLattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "K"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g4_robbins1 :::"OrthoLattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "L"))) "#)" )) & (Bool (Set (Var "K")) "is" ($#v8_robbins3 :::"involutive"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#v8_robbins3 :::"involutive"::: ) )) ; begin definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; mode :::"RelAugmentation"::: "of" "R" -> ($#l3_robbins3 :::"LattRelStr"::: ) means :: ROBBINS3:def 8 (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R") "#)" )); end; :: deftheorem defines :::"RelAugmentation"::: ROBBINS3:def 8 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#l3_robbins3 :::"LattRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_robbins3 :::"RelAugmentation"::: ) "of" (Set (Var "R"))) "iff" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b2"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) "#)" )) ")" ))); definitionlet "R" be ($#l3_lattices :::"LattStr"::: ) ; mode :::"LatAugmentation"::: "of" "R" -> ($#l3_robbins3 :::"LattRelStr"::: ) means :: ROBBINS3:def 9 (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" it) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" it) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" "R") "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" "R") "#)" )); end; :: deftheorem defines :::"LatAugmentation"::: ROBBINS3:def 9 : (Bool "for" (Set (Var "R")) "being" ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#l3_robbins3 :::"LattRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_robbins3 :::"LatAugmentation"::: ) "of" (Set (Var "R"))) "iff" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "b2"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "R"))) "#)" )) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; cluster -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#m2_robbins3 :::"LatAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_lattices :::"meet-associative"::: ) ($#l3_lattices :::"LattStr"::: ) ; cluster -> ($#v7_lattices :::"meet-associative"::: ) for ($#m2_robbins3 :::"LatAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_lattices :::"join-associative"::: ) ($#l3_lattices :::"LattStr"::: ) ; cluster -> ($#v5_lattices :::"join-associative"::: ) for ($#m2_robbins3 :::"LatAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_lattices :::"meet-commutative"::: ) ($#l3_lattices :::"LattStr"::: ) ; cluster -> ($#v6_lattices :::"meet-commutative"::: ) for ($#m2_robbins3 :::"LatAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#l3_lattices :::"LattStr"::: ) ; cluster -> ($#v4_lattices :::"join-commutative"::: ) for ($#m2_robbins3 :::"LatAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_lattices :::"join-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) ; cluster -> ($#v9_lattices :::"join-absorbing"::: ) for ($#m2_robbins3 :::"LatAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_lattices :::"meet-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) ; cluster -> ($#v8_lattices :::"meet-absorbing"::: ) for ($#m2_robbins3 :::"LatAugmentation"::: ) "of" "L"; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_robbins3 :::"\/-SemiLattRelStr"::: ) ; attr "L" is :::"naturally_sup-generated"::: means :: ROBBINS3:def 10 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) "iff" (Bool (Set (Set (Var "x")) ($#k1_lattices :::"|_|"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )); end; :: deftheorem defines :::"naturally_sup-generated"::: ROBBINS3:def 10 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_robbins3 :::"\/-SemiLattRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v10_robbins3 :::"naturally_sup-generated"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) "iff" (Bool (Set (Set (Var "x")) ($#k1_lattices :::"|_|"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) ")" )); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins3 :::"/\-SemiLattRelStr"::: ) ; attr "L" is :::"naturally_inf-generated"::: means :: ROBBINS3:def 11 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) "iff" (Bool (Set (Set (Var "x")) ($#k2_lattices :::"|^|"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )); end; :: deftheorem defines :::"naturally_inf-generated"::: ROBBINS3:def 11 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins3 :::"/\-SemiLattRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v11_robbins3 :::"naturally_inf-generated"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) "iff" (Bool (Set (Set (Var "x")) ($#k2_lattices :::"|^|"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) ")" )); registrationlet "L" be ($#l3_lattices :::"Lattice":::); 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"::: ) ($#v1_robbins3 :::"join-Associative"::: ) ($#v2_robbins3 :::"meet-Associative"::: ) ($#v3_robbins3 :::"meet-Absorbing"::: ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) ($#v11_robbins3 :::"naturally_inf-generated"::: ) for ($#m2_robbins3 :::"LatAugmentation"::: ) "of" "L"; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v3_orders_2 :::"reflexive"::: ) for ($#l3_robbins3 :::"LattRelStr"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v3_orders_2 :::"reflexive"::: ) for ($#l4_robbins3 :::"OrthoLattRelStr"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v3_orders_2 :::"reflexive"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v8_robbins1 :::"well-complemented"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v8_robbins3 :::"involutive"::: ) ($#v9_robbins3 :::"with_Top"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v3_orders_2 :::"reflexive"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v6_oposet_1 :::"PartialOrdered"::: ) ($#v7_oposet_1 :::"Pure"::: ) ($#v10_oposet_1 :::"OrderInvolutive"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v3_orders_2 :::"reflexive"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) ($#v11_robbins3 :::"naturally_inf-generated"::: ) for ($#l3_robbins3 :::"LattRelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v6_oposet_1 :::"PartialOrdered"::: ) ($#v7_oposet_1 :::"Pure"::: ) ($#v10_oposet_1 :::"OrderInvolutive"::: ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) ($#v11_robbins3 :::"naturally_inf-generated"::: ) for ($#l4_robbins3 :::"OrthoLattRelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) ($#v11_robbins3 :::"naturally_inf-generated"::: ) for ($#l3_robbins3 :::"LattRelStr"::: ) ; end; theorem :: ROBBINS3:22 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) ($#l3_robbins3 :::"LattRelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) "iff" (Bool (Set (Var "x")) ($#r1_lattices :::"[="::: ) (Set (Var "y"))) ")" ))) ; theorem :: ROBBINS3:23 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) ($#l3_robbins3 :::"LattRelStr"::: ) "holds" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k3_lattice3 :::"LattPOSet"::: ) (Set (Var "L"))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) for ($#l3_robbins3 :::"LattRelStr"::: ) ; end; begin definitionlet "R" be ($#l4_robbins1 :::"OrthoLattStr"::: ) ; mode :::"CLatAugmentation"::: "of" "R" -> ($#l4_robbins3 :::"OrthoLattRelStr"::: ) means :: ROBBINS3:def 12 (Bool (Set ($#g4_robbins1 :::"OrthoLattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" it) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" it) "," (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" it) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g4_robbins1 :::"OrthoLattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" "R") "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" "R") "," (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" "R") "#)" )); end; :: deftheorem defines :::"CLatAugmentation"::: ROBBINS3:def 12 : (Bool "for" (Set (Var "R")) "being" ($#l4_robbins1 :::"OrthoLattStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#l4_robbins3 :::"OrthoLattRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m3_robbins3 :::"CLatAugmentation"::: ) "of" (Set (Var "R"))) "iff" (Bool (Set ($#g4_robbins1 :::"OrthoLattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "b2"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g4_robbins1 :::"OrthoLattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "R"))) "#)" )) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins1 :::"OrthoLattStr"::: ) ; cluster -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#m3_robbins3 :::"CLatAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_lattices :::"meet-associative"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) ; cluster -> ($#v7_lattices :::"meet-associative"::: ) for ($#m3_robbins3 :::"CLatAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_lattices :::"join-associative"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) ; cluster -> ($#v5_lattices :::"join-associative"::: ) for ($#m3_robbins3 :::"CLatAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_lattices :::"meet-commutative"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) ; cluster -> ($#v6_lattices :::"meet-commutative"::: ) for ($#m3_robbins3 :::"CLatAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) ; cluster -> ($#v4_lattices :::"join-commutative"::: ) for ($#m3_robbins3 :::"CLatAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_lattices :::"meet-absorbing"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) ; cluster -> ($#v8_lattices :::"meet-absorbing"::: ) for ($#m3_robbins3 :::"CLatAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_lattices :::"join-absorbing"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) ; cluster -> ($#v9_lattices :::"join-absorbing"::: ) for ($#m3_robbins3 :::"CLatAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_robbins3 :::"with_Top"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) ; cluster -> ($#v9_robbins3 :::"with_Top"::: ) for ($#m3_robbins3 :::"CLatAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#l4_robbins1 :::"Ortholattice":::); 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"::: ) ($#v1_robbins3 :::"join-Associative"::: ) ($#v2_robbins3 :::"meet-Associative"::: ) ($#v3_robbins3 :::"meet-Absorbing"::: ) ($#v9_robbins3 :::"with_Top"::: ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) ($#v11_robbins3 :::"naturally_inf-generated"::: ) for ($#m3_robbins3 :::"CLatAugmentation"::: ) "of" "L"; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v8_robbins1 :::"well-complemented"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v8_robbins3 :::"involutive"::: ) ($#v9_robbins3 :::"with_Top"::: ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) for ($#l4_robbins3 :::"OrthoLattRelStr"::: ) ; end; theorem :: ROBBINS3:24 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v6_oposet_1 :::"PartialOrdered"::: ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_lattice3 :::""|_|""::: ) (Set (Var "y")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_lattice3 :::""|^|""::: ) (Set (Var "y")))) ")" ))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_lattices :::"meet-commutative"::: ) ($#l1_lattices :::"/\-SemiLattStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); :: original: :::"|^|"::: redefine func "a" :::"|^|"::: "b" -> bbbadM1_SUBSET_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")); commutativity (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")) "holds" (Bool (Set (Set (Var "a")) ($#k2_lattices :::"|^|"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k2_lattices :::"|^|"::: ) (Set (Var "a"))))) ; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#l2_lattices :::"\/-SemiLattStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); :: original: :::"|_|"::: redefine func "a" :::"|_|"::: "b" -> bbbadM1_SUBSET_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")); commutativity (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")) "holds" (Bool (Set (Set (Var "a")) ($#k1_lattices :::"|_|"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_lattices :::"|_|"::: ) (Set (Var "a"))))) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) for ($#l3_robbins3 :::"LattRelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_lattices :::"join-associative"::: ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) for ($#l3_robbins3 :::"LattRelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) for ($#l3_robbins3 :::"LattRelStr"::: ) ; end; theorem :: ROBBINS3:25 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) ($#l4_robbins3 :::"OrthoLattRelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k10_lattice3 :::""|_|""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_robbins3 :::"|_|"::: ) (Set (Var "y")))))) ; theorem :: ROBBINS3:26 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) ($#l4_robbins3 :::"OrthoLattRelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k11_lattice3 :::""|^|""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_robbins3 :::"|^|"::: ) (Set (Var "y")))))) ; theorem :: ROBBINS3:27 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v6_oposet_1 :::"PartialOrdered"::: ) ($#v10_oposet_1 :::"OrderInvolutive"::: ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) ($#v11_robbins3 :::"naturally_inf-generated"::: ) ($#l4_robbins3 :::"OrthoLattRelStr"::: ) "holds" (Bool (Set (Var "L")) "is" ($#v10_robbins1 :::"de_Morgan"::: ) )) ; registrationlet "L" be ($#l4_robbins1 :::"Ortholattice":::); cluster -> ($#v8_robbins3 :::"involutive"::: ) for ($#m3_robbins3 :::"CLatAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#l4_robbins1 :::"Ortholattice":::); cluster -> ($#v10_robbins1 :::"de_Morgan"::: ) for ($#m3_robbins3 :::"CLatAugmentation"::: ) "of" "L"; end; theorem :: ROBBINS3:28 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins3 :::"OrthoLattRelStr"::: ) "st" (Bool (Bool (Set (Var "L")) "is" ($#v8_robbins3 :::"involutive"::: ) ) & (Bool (Set (Var "L")) "is" ($#v9_robbins3 :::"with_Top"::: ) ) & (Bool (Set (Var "L")) "is" ($#v10_robbins1 :::"de_Morgan"::: ) ) & (Bool (Set (Var "L")) "is" ($#v10_lattices :::"Lattice-like"::: ) ) & (Bool (Set (Var "L")) "is" ($#v10_robbins3 :::"naturally_sup-generated"::: ) )) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v12_oposet_1 :::"Orthocomplemented"::: ) ) & (Bool (Set (Var "L")) "is" ($#v6_oposet_1 :::"PartialOrdered"::: ) ) ")" )) ; theorem :: ROBBINS3:29 (Bool "for" (Set (Var "L")) "being" ($#l4_robbins1 :::"Ortholattice":::) (Bool "for" (Set (Var "E")) "being" ($#v10_robbins3 :::"naturally_sup-generated"::: ) ($#m3_robbins3 :::"CLatAugmentation"::: ) "of" (Set (Var "L")) "holds" (Bool (Set (Var "E")) "is" ($#v12_oposet_1 :::"Orthocomplemented"::: ) ))) ; registrationlet "L" be ($#l4_robbins1 :::"Ortholattice":::); cluster ($#v10_robbins3 :::"naturally_sup-generated"::: ) -> ($#v12_oposet_1 :::"Orthocomplemented"::: ) ($#v10_robbins3 :::"naturally_sup-generated"::: ) for ($#m3_robbins3 :::"CLatAugmentation"::: ) "of" "L"; end; theorem :: ROBBINS3:30 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins1 :::"OrthoLattStr"::: ) "st" (Bool (Bool (Set (Var "L")) "is" ($#v17_lattices :::"Boolean"::: ) ) & (Bool (Set (Var "L")) "is" ($#v8_robbins1 :::"well-complemented"::: ) ) & (Bool (Set (Var "L")) "is" ($#v10_lattices :::"Lattice-like"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#l4_robbins1 :::"Ortholattice":::))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) ($#v8_robbins1 :::"well-complemented"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v8_robbins3 :::"involutive"::: ) ($#v9_robbins3 :::"with_Top"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end;