:: ROBBINS2 semantic presentation begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; attr "L" is :::"satisfying_DN_1"::: means :: ROBBINS2:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "z")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k1_lattices :::"+"::: ) (Set (Var "u")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "z")))); end; :: deftheorem defines :::"satisfying_DN_1"::: ROBBINS2:def 1 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_robbins2 :::"satisfying_DN_1"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "z")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k1_lattices :::"+"::: ) (Set (Var "u")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ")" )); registration cluster (Set ($#k1_robbins1 :::"TrivComplLat"::: ) ) -> ($#v1_robbins2 :::"satisfying_DN_1"::: ) ; cluster (Set ($#k2_robbins1 :::"TrivOrtLat"::: ) ) -> ($#v1_robbins2 :::"satisfying_DN_1"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) for ($#l2_robbins1 :::"ComplLLattStr"::: ) ; end; theorem :: ROBBINS2:1 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "," (Set (Var "v")) "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 "(" (Set "(" (Set "(" (Set "(" (Set (Var "z")) ($#k1_lattices :::"+"::: ) (Set (Var "u")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "v")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ROBBINS2:2 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "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 "(" (Set "(" (Set (Var "z")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "u")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ROBBINS2:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:4 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "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 "(" (Set "(" (Set (Var "z")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "u")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ROBBINS2:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "z")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ROBBINS2:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (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 "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ROBBINS2:7 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: ROBBINS2:8 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:9 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "z"))))) ; theorem :: ROBBINS2:10 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:11 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:12 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:13 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "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 "(" (Set "(" (Set (Var "z")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "u")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ROBBINS2:14 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:15 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:16 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:17 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:18 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: ROBBINS2:19 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (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 (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ROBBINS2:20 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:21 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:22 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:23 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#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 :: ROBBINS2:24 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:25 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "x")))))) ; theorem :: ROBBINS2:26 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (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 "(" (Set "(" (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:27 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#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")) ($#k1_lattices :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set (Var "x")))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) for ($#l2_robbins1 :::"ComplLLattStr"::: ) ; end; theorem :: ROBBINS2:28 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ROBBINS2:29 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: ROBBINS2:30 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#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")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: ROBBINS2:31 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:32 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:33 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:34 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:35 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:36 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ROBBINS2:37 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (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")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")))))) ; theorem :: ROBBINS2:38 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (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")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "z")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")))))) ; theorem :: ROBBINS2:39 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (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")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")))))) ; theorem :: ROBBINS2:40 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ROBBINS2:41 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ROBBINS2:42 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (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")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: ROBBINS2:43 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:44 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ))))) ; theorem :: ROBBINS2:45 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:46 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: ROBBINS2:47 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_robbins1 :::"`"::: ) )))) ; theorem :: ROBBINS2:48 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")))))) ; theorem :: ROBBINS2:49 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ))))) ; theorem :: ROBBINS2:50 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ))))) ; theorem :: ROBBINS2:51 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ))))) ; theorem :: ROBBINS2:52 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ))))) ; theorem :: ROBBINS2:53 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ))))) ; theorem :: ROBBINS2:54 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ))))) ; theorem :: ROBBINS2:55 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (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")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ))))) ; theorem :: ROBBINS2:56 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (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")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k5_robbins1 :::"+"::: ) (Set (Var "x")) ")" ))))) ; theorem :: ROBBINS2:57 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k5_robbins1 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_robbins1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_robbins1 :::"+"::: ) (Set (Var "z")) ")" ))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_lattices :::"join-associative"::: ) for ($#l2_robbins1 :::"ComplLLattStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_robbins1 :::"Robbins"::: ) for ($#l2_robbins1 :::"ComplLLattStr"::: ) ; end; theorem :: ROBBINS2:58 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v4_lattices :::"join-commutative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v5_lattices :::"join-associative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v6_robbins1 :::"Huntington"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" ) ($#k4_robbins1 :::"*'"::: ) (Set "(" (Set (Var "z")) ($#k1_lattices :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "z"))))) ; theorem :: ROBBINS2:59 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#l2_robbins1 :::"ComplLLattStr"::: ) "st" (Bool (Bool (Set (Var "L")) "is" ($#v5_robbins1 :::"Robbins"::: ) )) "holds" (Bool (Set (Var "L")) "is" ($#v1_robbins2 :::"satisfying_DN_1"::: ) )) ; 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"::: ) ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) for ($#l2_robbins1 :::"ComplLLattStr"::: ) ; 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"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) -> ($#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"::: ) -> ($#v8_robbins1 :::"well-complemented"::: ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) ; attr "L" is :::"satisfying_MD_1"::: means :: ROBBINS2:def 2 (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 (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))); attr "L" is :::"satisfying_MD_2"::: means :: ROBBINS2:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set (Var "z")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set "(" (Set (Var "z")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"satisfying_MD_1"::: ROBBINS2:def 2 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_robbins2 :::"satisfying_MD_1"::: ) ) "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 (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )); :: deftheorem defines :::"satisfying_MD_2"::: ROBBINS2:def 3 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_robbins1 :::"ComplLLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_robbins2 :::"satisfying_MD_2"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::"+"::: ) (Set "(" (Set (Var "z")) ($#k1_lattices :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_lattices :::"+"::: ) (Set "(" (Set (Var "z")) ($#k1_lattices :::"+"::: ) (Set (Var "x")) ")" )))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_robbins2 :::"satisfying_MD_1"::: ) ($#v3_robbins2 :::"satisfying_MD_2"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_robbins1 :::"Huntington"::: ) for ($#l2_robbins1 :::"ComplLLattStr"::: ) ; 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"::: ) ) ($#v2_robbins2 :::"satisfying_MD_1"::: ) ($#v3_robbins2 :::"satisfying_MD_2"::: ) for ($#l2_robbins1 :::"ComplLLattStr"::: ) ; 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"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v1_robbins2 :::"satisfying_DN_1"::: ) ($#v2_robbins2 :::"satisfying_MD_1"::: ) ($#v3_robbins2 :::"satisfying_MD_2"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v2_robbins2 :::"satisfying_MD_1"::: ) ($#v3_robbins2 :::"satisfying_MD_2"::: ) -> ($#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"::: ) -> ($#v8_robbins1 :::"well-complemented"::: ) ($#v2_robbins2 :::"satisfying_MD_1"::: ) ($#v3_robbins2 :::"satisfying_MD_2"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end;