:: LATTICES semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"/\-SemiLattStr"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"/\-SemiLattStr":::(# :::"carrier":::, :::"L_meet"::: #) -> ($#l1_lattices :::"/\-SemiLattStr"::: ) ; sel :::"L_meet"::: "c1" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; definitionattr "c1" is :::"strict"::: ; struct :::"\/-SemiLattStr"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"\/-SemiLattStr":::(# :::"carrier":::, :::"L_join"::: #) -> ($#l2_lattices :::"\/-SemiLattStr"::: ) ; sel :::"L_join"::: "c1" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; definitionattr "c1" is :::"strict"::: ; struct :::"LattStr"::: -> ($#l1_lattices :::"/\-SemiLattStr"::: ) "," ($#l2_lattices :::"\/-SemiLattStr"::: ) ; aggr :::"LattStr":::(# :::"carrier":::, :::"L_join":::, :::"L_meet"::: #) -> ($#l3_lattices :::"LattStr"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "u" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); cluster (Set ($#g2_lattices :::"\/-SemiLattStr"::: ) "(#" "D" "," "u" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; cluster (Set ($#g1_lattices :::"/\-SemiLattStr"::: ) "(#" "D" "," "u" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "u", "n" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); cluster (Set ($#g3_lattices :::"LattStr"::: ) "(#" "D" "," "u" "," "n" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_lattices :::"strict"::: ) for ($#l2_lattices :::"\/-SemiLattStr"::: ) ; cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_lattices :::"strict"::: ) for ($#l1_lattices :::"/\-SemiLattStr"::: ) ; cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v3_lattices :::"strict"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func "p" :::""\/""::: "q" -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: LATTICES:def 1 (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" "G") ($#k5_binop_1 :::"."::: ) "(" "p" "," "q" ")" ); end; :: deftheorem defines :::""\/""::: LATTICES:def 1 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "p")) ($#k1_lattices :::""\/""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "G"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )))); definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lattices :::"/\-SemiLattStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func "p" :::""/\""::: "q" -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: LATTICES:def 2 (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" "G") ($#k5_binop_1 :::"."::: ) "(" "p" "," "q" ")" ); end; :: deftheorem defines :::""/\""::: LATTICES:def 2 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lattices :::"/\-SemiLattStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "p")) ($#k2_lattices :::""/\""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "G"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )))); definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); pred "p" :::"[="::: "q" means :: LATTICES:def 3 (Bool (Set "p" ($#k1_lattices :::""\/""::: ) "q") ($#r1_hidden :::"="::: ) "q"); end; :: deftheorem defines :::"[="::: LATTICES:def 3 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_lattices :::"[="::: ) (Set (Var "q"))) "iff" (Bool (Set (Set (Var "p")) ($#k1_lattices :::""\/""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ))); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) ; attr "IT" is :::"join-commutative"::: means :: LATTICES:def 4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_lattices :::""\/""::: ) (Set (Var "a"))))); attr "IT" is :::"join-associative"::: means :: LATTICES:def 5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k1_lattices :::""\/""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k1_lattices :::""\/""::: ) (Set (Var "c"))))); end; :: deftheorem defines :::"join-commutative"::: LATTICES:def 4 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_lattices :::"join-commutative"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_lattices :::""\/""::: ) (Set (Var "a"))))) ")" )); :: deftheorem defines :::"join-associative"::: LATTICES:def 5 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_lattices :::"join-associative"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k1_lattices :::""\/""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k1_lattices :::""\/""::: ) (Set (Var "c"))))) ")" )); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lattices :::"/\-SemiLattStr"::: ) ; attr "IT" is :::"meet-commutative"::: means :: LATTICES:def 6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k2_lattices :::""/\""::: ) (Set (Var "a"))))); attr "IT" is :::"meet-associative"::: means :: LATTICES:def 7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k2_lattices :::""/\""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "b")) ")" ) ($#k2_lattices :::""/\""::: ) (Set (Var "c"))))); end; :: deftheorem defines :::"meet-commutative"::: LATTICES:def 6 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lattices :::"/\-SemiLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_lattices :::"meet-commutative"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k2_lattices :::""/\""::: ) (Set (Var "a"))))) ")" )); :: deftheorem defines :::"meet-associative"::: LATTICES:def 7 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lattices :::"/\-SemiLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_lattices :::"meet-associative"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k2_lattices :::""/\""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "b")) ")" ) ($#k2_lattices :::""/\""::: ) (Set (Var "c"))))) ")" )); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; attr "IT" is :::"meet-absorbing"::: means :: LATTICES:def 8 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "b")) ")" ) ($#k1_lattices :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))); attr "IT" is :::"join-absorbing"::: means :: LATTICES:def 9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a")))); end; :: deftheorem defines :::"meet-absorbing"::: LATTICES:def 8 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v8_lattices :::"meet-absorbing"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "b")) ")" ) ($#k1_lattices :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" )); :: deftheorem defines :::"join-absorbing"::: LATTICES:def 9 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v9_lattices :::"join-absorbing"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" )); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; attr "IT" is :::"Lattice-like"::: means :: LATTICES:def 10 (Bool "(" (Bool "IT" "is" ($#v4_lattices :::"join-commutative"::: ) ) & (Bool "IT" "is" ($#v5_lattices :::"join-associative"::: ) ) & (Bool "IT" "is" ($#v8_lattices :::"meet-absorbing"::: ) ) & (Bool "IT" "is" ($#v6_lattices :::"meet-commutative"::: ) ) & (Bool "IT" "is" ($#v7_lattices :::"meet-associative"::: ) ) & (Bool "IT" "is" ($#v9_lattices :::"join-absorbing"::: ) ) ")" ); end; :: deftheorem defines :::"Lattice-like"::: LATTICES:def 10 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v10_lattices :::"Lattice-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_lattices :::"join-commutative"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v5_lattices :::"join-associative"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v8_lattices :::"meet-absorbing"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v6_lattices :::"meet-commutative"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v7_lattices :::"meet-associative"::: ) ) & (Bool (Set (Var "IT")) "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"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) for ($#l3_lattices :::"LattStr"::: ) ; 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"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_lattices :::"strict"::: ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) for ($#l2_lattices :::"\/-SemiLattStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_lattices :::"strict"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) for ($#l1_lattices :::"/\-SemiLattStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ($#v10_lattices :::"Lattice-like"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; definitionmode Lattice is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#l3_lattices :::"LattStr"::: ) ; 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" -> ($#m1_subset_1 :::"Element":::) "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; 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" -> ($#m1_subset_1 :::"Element":::) "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 "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; attr "IT" is :::"distributive"::: means :: LATTICES:def 11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k1_lattices :::""\/""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "b")) ")" ) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "c")) ")" )))); end; :: deftheorem defines :::"distributive"::: LATTICES:def 11 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v11_lattices :::"distributive"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k1_lattices :::""\/""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "b")) ")" ) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "c")) ")" )))) ")" )); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; attr "IT" is :::"modular"::: means :: LATTICES:def 12 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) ($#r1_lattices :::"[="::: ) (Set (Var "c")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k2_lattices :::""/\""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k2_lattices :::""/\""::: ) (Set (Var "c"))))); end; :: deftheorem defines :::"modular"::: LATTICES:def 12 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v12_lattices :::"modular"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) ($#r1_lattices :::"[="::: ) (Set (Var "c")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k2_lattices :::""/\""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k2_lattices :::""/\""::: ) (Set (Var "c"))))) ")" )); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lattices :::"/\-SemiLattStr"::: ) ; attr "IT" is :::"lower-bounded"::: means :: LATTICES:def 13 (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Set (Var "c")) ($#k2_lattices :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ))); end; :: deftheorem defines :::"lower-bounded"::: LATTICES:def 13 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lattices :::"/\-SemiLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v13_lattices :::"lower-bounded"::: ) ) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Set (Var "c")) ($#k2_lattices :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ))) ")" )); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) ; attr "IT" is :::"upper-bounded"::: means :: LATTICES:def 14 (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Set (Var "c")) ($#k1_lattices :::""\/""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ))); end; :: deftheorem defines :::"upper-bounded"::: LATTICES:def 14 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v14_lattices :::"upper-bounded"::: ) ) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Set (Var "c")) ($#k1_lattices :::""\/""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ($#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"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; definitionmode D_Lattice is ($#v11_lattices :::"distributive"::: ) ($#l3_lattices :::"Lattice":::); mode M_Lattice is ($#v12_lattices :::"modular"::: ) ($#l3_lattices :::"Lattice":::); mode 0_Lattice is ($#v13_lattices :::"lower-bounded"::: ) ($#l3_lattices :::"Lattice":::); mode 1_Lattice is ($#v14_lattices :::"upper-bounded"::: ) ($#l3_lattices :::"Lattice":::); end; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; attr "IT" is :::"bounded"::: means :: LATTICES:def 15 (Bool "(" (Bool "IT" "is" ($#v13_lattices :::"lower-bounded"::: ) ) & (Bool "IT" "is" ($#v14_lattices :::"upper-bounded"::: ) ) ")" ); end; :: deftheorem defines :::"bounded"::: LATTICES:def 15 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v15_lattices :::"bounded"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v13_lattices :::"lower-bounded"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v14_lattices :::"upper-bounded"::: ) ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_lattices :::"lower-bounded"::: ) ($#v14_lattices :::"upper-bounded"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_lattices :::"bounded"::: ) for ($#l3_lattices :::"LattStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_lattices :::"bounded"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_lattices :::"lower-bounded"::: ) ($#v14_lattices :::"upper-bounded"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ($#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"::: ) ($#v15_lattices :::"bounded"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; definitionmode 01_Lattice is ($#v15_lattices :::"bounded"::: ) ($#l3_lattices :::"Lattice":::); end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lattices :::"/\-SemiLattStr"::: ) ; assume (Bool (Set (Const "L")) "is" ($#v13_lattices :::"lower-bounded"::: ) ) ; func :::"Bottom"::: "L" -> ($#m1_subset_1 :::"Element":::) "of" "L" means :: LATTICES:def 16 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set it ($#k2_lattices :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) it) & (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) it) ($#r1_hidden :::"="::: ) it) ")" )); end; :: deftheorem defines :::"Bottom"::: LATTICES:def 16 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lattices :::"/\-SemiLattStr"::: ) "st" (Bool (Bool (Set (Var "L")) "is" ($#v13_lattices :::"lower-bounded"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k2_lattices :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) & (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" )) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) ; assume (Bool (Set (Const "L")) "is" ($#v14_lattices :::"upper-bounded"::: ) ) ; func :::"Top"::: "L" -> ($#m1_subset_1 :::"Element":::) "of" "L" means :: LATTICES:def 17 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set it ($#k1_lattices :::""\/""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) it) & (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) it) ($#r1_hidden :::"="::: ) it) ")" )); end; :: deftheorem defines :::"Top"::: LATTICES:def 17 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_lattices :::"\/-SemiLattStr"::: ) "st" (Bool (Bool (Set (Var "L")) "is" ($#v14_lattices :::"upper-bounded"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k1_lattices :::""\/""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) & (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" )) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); pred "a" :::"is_a_complement_of"::: "b" means :: LATTICES:def 18 (Bool "(" (Bool (Set "a" ($#k1_lattices :::""\/""::: ) "b") ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) "L")) & (Bool (Set "b" ($#k1_lattices :::""\/""::: ) "a") ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) "L")) & (Bool (Set "a" ($#k2_lattices :::""/\""::: ) "b") ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) "L")) & (Bool (Set "b" ($#k2_lattices :::""/\""::: ) "a") ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) "L")) ")" ); end; :: deftheorem defines :::"is_a_complement_of"::: LATTICES:def 18 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_lattices :::"is_a_complement_of"::: ) (Set (Var "b"))) "iff" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "b")) ($#k1_lattices :::""\/""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "b")) ($#k2_lattices :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")))) ")" ) ")" ))); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; attr "IT" is :::"complemented"::: means :: LATTICES:def 19 (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set (Var "a")) ($#r2_lattices :::"is_a_complement_of"::: ) (Set (Var "b"))))); end; :: deftheorem defines :::"complemented"::: LATTICES:def 19 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v16_lattices :::"complemented"::: ) ) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set (Var "a")) ($#r2_lattices :::"is_a_complement_of"::: ) (Set (Var "b"))))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ($#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"::: ) ($#v15_lattices :::"bounded"::: ) ($#v16_lattices :::"complemented"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; definitionmode C_Lattice is ($#v16_lattices :::"complemented"::: ) ($#l3_lattices :::"01_Lattice":::); end; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; attr "IT" is :::"Boolean"::: means :: LATTICES:def 20 (Bool "(" (Bool "IT" "is" ($#v15_lattices :::"bounded"::: ) ) & (Bool "IT" "is" ($#v16_lattices :::"complemented"::: ) ) & (Bool "IT" "is" ($#v11_lattices :::"distributive"::: ) ) ")" ); end; :: deftheorem defines :::"Boolean"::: LATTICES:def 20 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v17_lattices :::"Boolean"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v15_lattices :::"bounded"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v16_lattices :::"complemented"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v11_lattices :::"distributive"::: ) ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v17_lattices :::"Boolean"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_lattices :::"distributive"::: ) ($#v15_lattices :::"bounded"::: ) ($#v16_lattices :::"complemented"::: ) for ($#l3_lattices :::"LattStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_lattices :::"distributive"::: ) ($#v15_lattices :::"bounded"::: ) ($#v16_lattices :::"complemented"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v17_lattices :::"Boolean"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v17_lattices :::"Boolean"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; definitionmode B_Lattice is ($#v17_lattices :::"Boolean"::: ) ($#l3_lattices :::"Lattice":::); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); reduce ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); reduce ; end; theorem :: LATTICES:1 canceled; theorem :: LATTICES:2 canceled; theorem :: LATTICES:3 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k3_lattices :::""\/""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b")) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "c")) ")" ))) ")" ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k4_lattices :::""/\""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "c")) ")" )))) ")" )) ; theorem :: LATTICES:4 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_lattices :::"[="::: ) (Set (Var "b"))) "iff" (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; theorem :: LATTICES:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "a")) ($#r1_lattices :::"[="::: ) (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")))))) ; theorem :: LATTICES:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b"))) ($#r1_lattices :::"[="::: ) (Set (Var "a"))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); :: original: :::"[="::: redefine pred "a" :::"[="::: "b"; reflexivity (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")) "holds" (Bool ((Set (Const "L")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; end; theorem :: LATTICES:7 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_lattices :::"join-associative"::: ) ($#l2_lattices :::"\/-SemiLattStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_lattices :::"[="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_lattices :::"[="::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r1_lattices :::"[="::: ) (Set (Var "c"))))) ; theorem :: LATTICES:8 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#l2_lattices :::"\/-SemiLattStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_lattices :::"[="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_lattices :::"[="::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: LATTICES:9 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_lattices :::"[="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set (Var "c"))) ($#r1_lattices :::"[="::: ) (Set (Set (Var "b")) ($#k2_lattices :::""/\""::: ) (Set (Var "c")))))) ; theorem :: LATTICES:10 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b")) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k4_lattices :::""/\""::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "c")) ($#k4_lattices :::""/\""::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k3_lattices :::""\/""::: ) (Set (Var "c")) ")" ) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "c")) ($#k3_lattices :::""\/""::: ) (Set (Var "a")) ")" ))) ")" )) "holds" (Bool (Set (Var "L")) "is" ($#v11_lattices :::"distributive"::: ) )) ; theorem :: LATTICES:11 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k4_lattices :::""/\""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "c")) ")" ))))) ; theorem :: LATTICES:12 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "c")) ($#k4_lattices :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k4_lattices :::""/\""::: ) (Set (Var "b")))) & (Bool (Set (Set (Var "c")) ($#k3_lattices :::""\/""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k3_lattices :::""\/""::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: LATTICES:13 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"D_Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k3_lattices :::""\/""::: ) (Set (Var "c")) ")" ) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "c")) ($#k3_lattices :::""\/""::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b")) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k4_lattices :::""/\""::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "c")) ($#k4_lattices :::""/\""::: ) (Set (Var "a")) ")" ))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v11_lattices :::"distributive"::: ) -> ($#v12_lattices :::"modular"::: ) for ($#l3_lattices :::"LattStr"::: ) ; end; registrationlet "L" be ($#l3_lattices :::"0_Lattice":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); reduce ; reduce ; end; theorem :: LATTICES:14 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"0_Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k3_lattices :::""\/""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: LATTICES:15 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"0_Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k4_lattices :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")))))) ; theorem :: LATTICES:16 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"0_Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L"))) ($#r3_lattices :::"[="::: ) (Set (Var "a"))))) ; registrationlet "L" be ($#l3_lattices :::"1_Lattice":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); reduce ; reduce ; end; theorem :: LATTICES:17 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"1_Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "L")) ")" ) ($#k4_lattices :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: LATTICES:18 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"1_Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k6_lattices :::"Top"::: ) (Set (Var "L")) ")" ) ($#k3_lattices :::""\/""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))))) ; theorem :: LATTICES:19 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"1_Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); assume (Bool (Set (Const "L")) "is" ($#v16_lattices :::"complemented"::: ) ($#l3_lattices :::"D_Lattice":::)) ; func "x" :::"`"::: -> ($#m1_subset_1 :::"Element":::) "of" "L" means :: LATTICES:def 21 (Bool it ($#r2_lattices :::"is_a_complement_of"::: ) "x"); end; :: deftheorem defines :::"`"::: LATTICES:def 21 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v16_lattices :::"complemented"::: ) ($#l3_lattices :::"D_Lattice":::))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_lattices :::"`"::: ) )) "iff" (Bool (Set (Var "b3")) ($#r2_lattices :::"is_a_complement_of"::: ) (Set (Var "x"))) ")" )))); theorem :: LATTICES:20 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k7_lattices :::"`"::: ) ")" ) ($#k4_lattices :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")))))) ; theorem :: LATTICES:21 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k7_lattices :::"`"::: ) ")" ) ($#k3_lattices :::""\/""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))))) ; registrationlet "L" be ($#l3_lattices :::"B_Lattice":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); reduce ; end; theorem :: LATTICES:22 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k7_lattices :::"`"::: ) ")" ) ($#k7_lattices :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: LATTICES:23 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b")) ")" ) ($#k7_lattices :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k7_lattices :::"`"::: ) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k7_lattices :::"`"::: ) ")" ))))) ; theorem :: LATTICES:24 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k7_lattices :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k7_lattices :::"`"::: ) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k7_lattices :::"`"::: ) ")" ))))) ; theorem :: LATTICES:25 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "b")) ($#k4_lattices :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")))) "iff" (Bool (Set (Var "b")) ($#r3_lattices :::"[="::: ) (Set (Set (Var "a")) ($#k7_lattices :::"`"::: ) )) ")" ))) ; theorem :: LATTICES:26 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"B_Lattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "b")) ($#k7_lattices :::"`"::: ) ) ($#r3_lattices :::"[="::: ) (Set (Set (Var "a")) ($#k7_lattices :::"`"::: ) )))) ; begin definitionlet "L" be ($#l3_lattices :::"Lattice":::); let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); attr "S" is :::"initial"::: means :: LATTICES:def 22 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "S")) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "S")); attr "S" is :::"final"::: means :: LATTICES:def 23 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "S")) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "S")); attr "S" is :::"meet-closed"::: means :: LATTICES:def 24 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "S") & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "S")) "holds" (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "S")); attr "S" is :::"join-closed"::: means :: LATTICES:def 25 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "S") & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "S")) "holds" (Bool (Set (Set (Var "p")) ($#k3_lattices :::""\/""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "S")); end; :: deftheorem defines :::"initial"::: LATTICES:def 22 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v18_lattices :::"initial"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" ))); :: deftheorem defines :::"final"::: LATTICES:def 23 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v19_lattices :::"final"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" ))); :: deftheorem defines :::"meet-closed"::: LATTICES:def 24 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v20_lattices :::"meet-closed"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" ))); :: deftheorem defines :::"join-closed"::: LATTICES:def 25 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v21_lattices :::"join-closed"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Set (Var "p")) ($#k3_lattices :::""\/""::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" ))); registrationlet "L" be ($#l3_lattices :::"Lattice":::); cluster (Set ($#k2_struct_0 :::"[#]"::: ) "L") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v18_lattices :::"initial"::: ) ($#v19_lattices :::"final"::: ) ; end; registrationlet "L" be ($#l3_lattices :::"Lattice":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v18_lattices :::"initial"::: ) ($#v19_lattices :::"final"::: ) for bbbadM1_SUBSET_1((Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v18_lattices :::"initial"::: ) ($#v19_lattices :::"final"::: ) for bbbadM1_SUBSET_1((Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); cluster ($#v18_lattices :::"initial"::: ) -> ($#v20_lattices :::"meet-closed"::: ) for bbbadM1_SUBSET_1((Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); cluster ($#v19_lattices :::"final"::: ) -> ($#v21_lattices :::"join-closed"::: ) for bbbadM1_SUBSET_1((Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); end; theorem :: LATTICES:27 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v18_lattices :::"initial"::: ) ($#v19_lattices :::"final"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "L")))))) ;