:: QUANTAL1 semantic presentation begin scheme :: QUANTAL1:sch 1 DenestFraenkel{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F3 "(" (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "{" (Set F4 "(" (Set (Var "b")) ")" ) where b "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "b"))]) "}" ) "}" ($#r1_hidden :::"="::: ) "{" (Set F3 "(" (Set F4 "(" (Set (Var "a")) ")" ) ")" ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "a"))]) "}" ) proof end; scheme :: QUANTAL1:sch 2 EmptyFraenkel{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F2 "(" (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "a"))]) "}" ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) provided (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool P1[(Set (Var "a"))])) proof end; theorem :: QUANTAL1:1 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2")))) "holds" (Bool "(" (Bool (Set (Set (Var "a1")) ($#k1_lattices :::""\/""::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k1_lattices :::""\/""::: ) (Set (Var "b2")))) & (Bool (Set (Set (Var "a1")) ($#k2_lattices :::""/\""::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k2_lattices :::""/\""::: ) (Set (Var "b2")))) & "(" (Bool (Bool (Set (Var "a1")) ($#r1_lattices :::"[="::: ) (Set (Var "b1")))) "implies" (Bool (Set (Var "a2")) ($#r1_lattices :::"[="::: ) (Set (Var "b2"))) ")" & "(" (Bool (Bool (Set (Var "a2")) ($#r1_lattices :::"[="::: ) (Set (Var "b2")))) "implies" (Bool (Set (Var "a1")) ($#r1_lattices :::"[="::: ) (Set (Var "b1"))) ")" ")" )))) ; theorem :: QUANTAL1:2 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r3_lattice3 :::"is_less_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "b")) ($#r3_lattice3 :::"is_less_than"::: ) (Set (Var "X"))) ")" & "(" (Bool (Bool (Set (Var "b")) ($#r3_lattice3 :::"is_less_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "a")) ($#r3_lattice3 :::"is_less_than"::: ) (Set (Var "X"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r4_lattice3 :::"is_greater_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "b")) ($#r4_lattice3 :::"is_greater_than"::: ) (Set (Var "X"))) ")" & "(" (Bool (Bool (Set (Var "b")) ($#r4_lattice3 :::"is_greater_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "a")) ($#r4_lattice3 :::"is_greater_than"::: ) (Set (Var "X"))) ")" ")" ))))) ; definitionlet "L" be ($#l1_struct_0 :::"1-sorted"::: ) ; mode UnOp of "L" is ($#m1_subset_1 :::"Function":::) "of" "L" "," "L"; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); attr "X" is :::"directed"::: means :: QUANTAL1:def 1 (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "X" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "Y")) "," "L" ")" ) ($#r1_lattices :::"[="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") ")" ))); end; :: deftheorem defines :::"directed"::: QUANTAL1:def 1 : (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 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_quantal1 :::"directed"::: ) ) "iff" (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ) ($#r1_lattices :::"[="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ))) ")" ))); theorem :: QUANTAL1:3 (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 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_quantal1 :::"directed"::: ) )) "holds" (Bool "not" (Bool (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; definitionattr "c1" is :::"strict"::: ; struct :::"QuantaleStr"::: -> ($#l3_lattices :::"LattStr"::: ) "," ($#l3_algstr_0 :::"multMagma"::: ) ; aggr :::"QuantaleStr":::(# :::"carrier":::, :::"L_join":::, :::"L_meet":::, :::"multF"::: #) -> ($#l1_quantal1 :::"QuantaleStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_quantal1 :::"QuantaleStr"::: ) ; end; definitionattr "c1" is :::"strict"::: ; struct :::"QuasiNetStr"::: -> ($#l1_quantal1 :::"QuantaleStr"::: ) "," ($#l4_algstr_0 :::"multLoopStr"::: ) ; aggr :::"QuasiNetStr":::(# :::"carrier":::, :::"L_join":::, :::"L_meet":::, :::"multF":::, :::"OneF"::: #) -> ($#l2_quantal1 :::"QuasiNetStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l2_quantal1 :::"QuasiNetStr"::: ) ; end; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; attr "IT" is :::"with_left-zero"::: means :: QUANTAL1:def 2 (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))); attr "IT" is :::"with_right-zero"::: means :: QUANTAL1:def 3 (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))))); end; :: deftheorem defines :::"with_left-zero"::: QUANTAL1:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_quantal1 :::"with_left-zero"::: ) ) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ")" )); :: deftheorem defines :::"with_right-zero"::: QUANTAL1:def 3 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_quantal1 :::"with_right-zero"::: ) ) "iff" (Bool "ex" (Set (Var "b")) "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 (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ")" )); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; attr "IT" is :::"with_zero"::: means :: QUANTAL1:def 4 (Bool "(" (Bool "IT" "is" ($#v4_quantal1 :::"with_left-zero"::: ) ) & (Bool "IT" "is" ($#v5_quantal1 :::"with_right-zero"::: ) ) ")" ); end; :: deftheorem defines :::"with_zero"::: QUANTAL1:def 4 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_quantal1 :::"with_zero"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_quantal1 :::"with_left-zero"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v5_quantal1 :::"with_right-zero"::: ) ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_quantal1 :::"with_zero"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_quantal1 :::"with_left-zero"::: ) ($#v5_quantal1 :::"with_right-zero"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_quantal1 :::"with_left-zero"::: ) ($#v5_quantal1 :::"with_right-zero"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_quantal1 :::"with_zero"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_quantal1 :::"with_zero"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_quantal1 :::"QuantaleStr"::: ) ; attr "IT" is :::"right-distributive"::: means :: QUANTAL1:def 5 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "X")) "," "IT" ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b")) ")" ) where b "is" ($#m1_subset_1 :::"Element":::) "of" "IT" : (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," "IT" ")" )))); attr "IT" is :::"left-distributive"::: means :: QUANTAL1:def 6 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "X")) "," "IT" ")" ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "a")) ")" ) where b "is" ($#m1_subset_1 :::"Element":::) "of" "IT" : (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," "IT" ")" )))); attr "IT" is :::"times-additive"::: means :: QUANTAL1:def 7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "c")) ")" ) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "c")) ")" ))) & (Bool (Set (Set (Var "c")) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "a")) ")" ) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "c")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b")) ")" ))) ")" )); attr "IT" is :::"times-continuous"::: means :: QUANTAL1:def 8 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_subset_1 :::"Subset":::) "of" "IT" "st" (Bool (Bool (Set (Var "X1")) "is" ($#v1_quantal1 :::"directed"::: ) ) & (Bool (Set (Var "X2")) "is" ($#v1_quantal1 :::"directed"::: ) )) "holds" (Bool (Set (Set "(" ($#k15_lattice3 :::""\/""::: ) (Set (Var "X1")) ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" ($#k15_lattice3 :::""\/""::: ) (Set (Var "X2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b")) ")" ) where a, b "is" ($#m1_subset_1 :::"Element":::) "of" "IT" : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X1"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X2"))) ")" ) "}" "," "IT" ")" ))); end; :: deftheorem defines :::"right-distributive"::: QUANTAL1:def 5 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_quantal1 :::"QuantaleStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_quantal1 :::"right-distributive"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "IT")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b")) ")" ) where b "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) : (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," (Set (Var "IT")) ")" )))) ")" )); :: deftheorem defines :::"left-distributive"::: QUANTAL1:def 6 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_quantal1 :::"QuantaleStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v8_quantal1 :::"left-distributive"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "IT")) ")" ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "a")) ")" ) where b "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) : (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," (Set (Var "IT")) ")" )))) ")" )); :: deftheorem defines :::"times-additive"::: QUANTAL1:def 7 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_quantal1 :::"QuantaleStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v9_quantal1 :::"times-additive"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "c")) ")" ) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "c")) ")" ))) & (Bool (Set (Set (Var "c")) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "a")) ")" ) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "c")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b")) ")" ))) ")" )) ")" )); :: deftheorem defines :::"times-continuous"::: QUANTAL1:def 8 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_quantal1 :::"QuantaleStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v10_quantal1 :::"times-continuous"::: ) ) "iff" (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#v1_quantal1 :::"directed"::: ) ) & (Bool (Set (Var "X2")) "is" ($#v1_quantal1 :::"directed"::: ) )) "holds" (Bool (Set (Set "(" ($#k15_lattice3 :::""\/""::: ) (Set (Var "X1")) ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" ($#k15_lattice3 :::""\/""::: ) (Set (Var "X2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b")) ")" ) where a, b "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X1"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X2"))) ")" ) "}" "," (Set (Var "IT")) ")" ))) ")" )); theorem :: QUANTAL1:4 (Bool "for" (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_quantal1 :::"QuantaleStr"::: ) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Q"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "Q"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "Q"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k1_lattice3 :::"BooleLatt"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "Q")) "is" ($#v3_group_1 :::"associative"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v5_group_1 :::"commutative"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v1_group_1 :::"unital"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v6_quantal1 :::"with_zero"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v4_lattice3 :::"complete"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v7_quantal1 :::"right-distributive"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v8_quantal1 :::"left-distributive"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v10_lattices :::"Lattice-like"::: ) ) ")" )) ; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "b1", "b2", "b3" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); cluster (Set ($#g1_quantal1 :::"QuantaleStr"::: ) "(#" "A" "," "b1" "," "b2" "," "b3" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v4_lattice3 :::"complete"::: ) ($#v6_quantal1 :::"with_zero"::: ) ($#v7_quantal1 :::"right-distributive"::: ) ($#v8_quantal1 :::"left-distributive"::: ) for ($#l1_quantal1 :::"QuantaleStr"::: ) ; end; scheme :: QUANTAL1:sch 3 LUBFraenkelDistr{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v4_lattice3 :::"complete"::: ) ($#l1_quantal1 :::"QuantaleStr"::: ) , F2( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ), F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_hidden :::"set"::: ) } : (Bool (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set "(" ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) where b "is" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) : (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set F4 "(" ")" )) "}" "," (Set F1 "(" ")" ) ")" ")" ) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) "}" "," (Set F1 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) where a, b "is" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set F4 "(" ")" )) ")" ) "}" "," (Set F1 "(" ")" ) ")" )) proof end; theorem :: QUANTAL1:5 (Bool "for" (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v4_lattice3 :::"complete"::: ) ($#v7_quantal1 :::"right-distributive"::: ) ($#v8_quantal1 :::"left-distributive"::: ) ($#l1_quantal1 :::"QuantaleStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "Q")) ")" ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "Q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b")) ")" ) where a, b "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" ) "}" "," (Set (Var "Q")) ")" )))) ; theorem :: QUANTAL1:6 (Bool "for" (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v4_lattice3 :::"complete"::: ) ($#v7_quantal1 :::"right-distributive"::: ) ($#v8_quantal1 :::"left-distributive"::: ) ($#l1_quantal1 :::"QuantaleStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "c")) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "c")) ")" ))) & (Bool (Set (Set (Var "c")) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "a")) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "c")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b")) ")" ))) ")" ))) ; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "b1", "b2", "b3" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); let "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); cluster (Set ($#g2_quantal1 :::"QuasiNetStr"::: ) "(#" "A" "," "b1" "," "b2" "," "b3" "," "e" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v4_lattice3 :::"complete"::: ) for ($#l2_quantal1 :::"QuasiNetStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v4_lattice3 :::"complete"::: ) ($#v7_quantal1 :::"right-distributive"::: ) ($#v8_quantal1 :::"left-distributive"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v4_lattice3 :::"complete"::: ) ($#v9_quantal1 :::"times-additive"::: ) ($#v10_quantal1 :::"times-continuous"::: ) for ($#l2_quantal1 :::"QuasiNetStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v4_lattice3 :::"complete"::: ) ($#v4_quantal1 :::"with_left-zero"::: ) ($#v6_quantal1 :::"with_zero"::: ) ($#v7_quantal1 :::"right-distributive"::: ) ($#v8_quantal1 :::"left-distributive"::: ) for ($#l2_quantal1 :::"QuasiNetStr"::: ) ; end; definitionmode Quantale is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v4_lattice3 :::"complete"::: ) ($#v7_quantal1 :::"right-distributive"::: ) ($#v8_quantal1 :::"left-distributive"::: ) ($#l1_quantal1 :::"QuantaleStr"::: ) ; mode QuasiNet is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v4_lattice3 :::"complete"::: ) ($#v4_quantal1 :::"with_left-zero"::: ) ($#v9_quantal1 :::"times-additive"::: ) ($#v10_quantal1 :::"times-continuous"::: ) ($#l2_quantal1 :::"QuasiNetStr"::: ) ; end; definitionmode BlikleNet is ($#v6_quantal1 :::"with_zero"::: ) ($#l2_quantal1 :::"QuasiNet":::); end; theorem :: QUANTAL1:7 (Bool "for" (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l2_quantal1 :::"QuasiNetStr"::: ) "st" (Bool (Bool (Set (Var "Q")) "is" ($#l1_quantal1 :::"Quantale":::))) "holds" (Bool (Set (Var "Q")) "is" ($#l2_quantal1 :::"BlikleNet":::))) ; theorem :: QUANTAL1:8 (Bool "for" (Set (Var "Q")) "being" ($#l1_quantal1 :::"Quantale":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "c"))) ($#r3_lattices :::"[="::: ) (Set (Set (Var "b")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "c")))) & (Bool (Set (Set (Var "c")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set (Set (Var "c")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b")))) ")" ))) ; theorem :: QUANTAL1:9 (Bool "for" (Set (Var "Q")) "being" ($#l1_quantal1 :::"Quantale":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r3_lattices :::"[="::: ) (Set (Var "d")))) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "c"))) ($#r3_lattices :::"[="::: ) (Set (Set (Var "b")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "d")))))) ; definitionlet "f" be ($#m1_hidden :::"Function":::); attr "f" is :::"idempotent"::: means :: QUANTAL1:def 9 (Bool (Set "f" ($#k3_relat_1 :::"*"::: ) "f") ($#r1_hidden :::"="::: ) "f"); end; :: deftheorem defines :::"idempotent"::: QUANTAL1:def 9 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v11_quantal1 :::"idempotent"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" )); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; let "IT" be ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "L")); attr "IT" is :::"inflationary"::: means :: QUANTAL1:def 10 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Var "p")) ($#r1_lattices :::"[="::: ) (Set "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "p"))))); attr "IT" is :::"deflationary"::: means :: QUANTAL1:def 11 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_lattices :::"[="::: ) (Set (Var "p")))); attr "IT" is :::"monotone"::: means :: QUANTAL1:def 12 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "p")) ($#r1_lattices :::"[="::: ) (Set (Var "q")))) "holds" (Bool (Set "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_lattices :::"[="::: ) (Set "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "q"))))); attr "IT" is :::"\/-distributive"::: means :: QUANTAL1:def 13 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" "L" "holds" (Bool (Set "IT" ($#k3_funct_2 :::"."::: ) (Set "(" ($#k15_lattice3 :::""\/""::: ) (Set (Var "X")) ")" )) ($#r1_lattices :::"[="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," "L" ")" ))); end; :: deftheorem defines :::"inflationary"::: QUANTAL1:def 10 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v12_quantal1 :::"inflationary"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "p")) ($#r1_lattices :::"[="::: ) (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))))) ")" ))); :: deftheorem defines :::"deflationary"::: QUANTAL1:def 11 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v13_quantal1 :::"deflationary"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_lattices :::"[="::: ) (Set (Var "p")))) ")" ))); :: deftheorem defines :::"monotone"::: QUANTAL1:def 12 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v14_quantal1 :::"monotone"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r1_lattices :::"[="::: ) (Set (Var "q")))) "holds" (Bool (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_lattices :::"[="::: ) (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "q"))))) ")" ))); :: deftheorem defines :::"\/-distributive"::: QUANTAL1:def 13 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v15_quantal1 :::"\/-distributive"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k15_lattice3 :::""\/""::: ) (Set (Var "X")) ")" )) ($#r1_lattices :::"[="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," (Set (Var "L")) ")" ))) ")" ))); registrationlet "L" be ($#l3_lattices :::"Lattice":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v12_quantal1 :::"inflationary"::: ) ($#v13_quantal1 :::"deflationary"::: ) ($#v14_quantal1 :::"monotone"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: QUANTAL1:10 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "j")) "is" ($#v14_quantal1 :::"monotone"::: ) )) "holds" (Bool "(" (Bool (Set (Var "j")) "is" ($#v15_quantal1 :::"\/-distributive"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "j")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k15_lattice3 :::""\/""::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "j")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," (Set (Var "L")) ")" ))) ")" ))) ; definitionlet "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_quantal1 :::"QuantaleStr"::: ) ; let "IT" be ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "Q")); attr "IT" is :::"times-monotone"::: means :: QUANTAL1:def 14 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "Q" "holds" (Bool (Set (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" )) ($#r1_lattices :::"[="::: ) (Set "IT" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b")) ")" )))); end; :: deftheorem defines :::"times-monotone"::: QUANTAL1:def 14 : (Bool "for" (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_quantal1 :::"QuantaleStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "Q")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v16_quantal1 :::"times-monotone"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool (Set (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" )) ($#r1_lattices :::"[="::: ) (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b")) ")" )))) ")" ))); definitionlet "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_quantal1 :::"QuantaleStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "Q")); func "a" :::"-r>"::: "b" -> ($#m1_subset_1 :::"Element":::) "of" "Q" equals :: QUANTAL1:def 15 (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set (Var "c")) where c "is" ($#m1_subset_1 :::"Element":::) "of" "Q" : (Bool (Set (Set (Var "c")) ($#k6_algstr_0 :::"[*]"::: ) "a") ($#r1_lattices :::"[="::: ) "b") "}" "," "Q" ")" ); func "a" :::"-l>"::: "b" -> ($#m1_subset_1 :::"Element":::) "of" "Q" equals :: QUANTAL1:def 16 (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set (Var "c")) where c "is" ($#m1_subset_1 :::"Element":::) "of" "Q" : (Bool (Set "a" ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "c"))) ($#r1_lattices :::"[="::: ) "b") "}" "," "Q" ")" ); end; :: deftheorem defines :::"-r>"::: QUANTAL1:def 15 : (Bool "for" (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_quantal1 :::"QuantaleStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool (Set (Set (Var "a")) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set (Var "c")) where c "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) : (Bool (Set (Set (Var "c")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "a"))) ($#r1_lattices :::"[="::: ) (Set (Var "b"))) "}" "," (Set (Var "Q")) ")" )))); :: deftheorem defines :::"-l>"::: QUANTAL1:def 16 : (Bool "for" (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_quantal1 :::"QuantaleStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool (Set (Set (Var "a")) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set (Var "c")) where c "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) : (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "c"))) ($#r1_lattices :::"[="::: ) (Set (Var "b"))) "}" "," (Set (Var "Q")) ")" )))); theorem :: QUANTAL1:11 (Bool "for" (Set (Var "Q")) "being" ($#l1_quantal1 :::"Quantale":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b"))) ($#r3_lattices :::"[="::: ) (Set (Var "c"))) "iff" (Bool (Set (Var "b")) ($#r3_lattices :::"[="::: ) (Set (Set (Var "a")) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "c")))) ")" ))) ; theorem :: QUANTAL1:12 (Bool "for" (Set (Var "Q")) "being" ($#l1_quantal1 :::"Quantale":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b"))) ($#r3_lattices :::"[="::: ) (Set (Var "c"))) "iff" (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Set (Var "b")) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "c")))) ")" ))) ; theorem :: QUANTAL1:13 (Bool "for" (Set (Var "Q")) "being" ($#l1_quantal1 :::"Quantale":::) (Bool "for" (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Set (Var "b")) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s"))) ($#r3_lattices :::"[="::: ) (Set (Set (Var "a")) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s")))) & (Bool (Set (Set (Var "b")) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "s"))) ($#r3_lattices :::"[="::: ) (Set (Set (Var "a")) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "s")))) ")" ))) ; theorem :: QUANTAL1:14 (Bool "for" (Set (Var "Q")) "being" ($#l1_quantal1 :::"Quantale":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "Q")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool (Set (Set (Var "j")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s")) ")" ) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s")))) ")" )) "holds" (Bool (Set (Var "j")) "is" ($#v14_quantal1 :::"monotone"::: ) )))) ; definitionlet "Q" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_quantal1 :::"QuantaleStr"::: ) ; let "IT" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "Q")); attr "IT" is :::"dualizing"::: means :: QUANTAL1:def 17 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "Q" "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_quantal1 :::"-r>"::: ) "IT" ")" ) ($#k2_quantal1 :::"-l>"::: ) "IT") ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k2_quantal1 :::"-l>"::: ) "IT" ")" ) ($#k1_quantal1 :::"-r>"::: ) "IT") ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )); attr "IT" is :::"cyclic"::: means :: QUANTAL1:def 18 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "Q" "holds" (Bool (Set (Set (Var "a")) ($#k1_quantal1 :::"-r>"::: ) "IT") ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_quantal1 :::"-l>"::: ) "IT"))); end; :: deftheorem defines :::"dualizing"::: QUANTAL1:def 17 : (Bool "for" (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_quantal1 :::"QuantaleStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v17_quantal1 :::"dualizing"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "IT")) ")" ) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "IT"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "IT")) ")" ) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "IT"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )) ")" ))); :: deftheorem defines :::"cyclic"::: QUANTAL1:def 18 : (Bool "for" (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_quantal1 :::"QuantaleStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v18_quantal1 :::"cyclic"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool (Set (Set (Var "a")) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "IT"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "IT"))))) ")" ))); theorem :: QUANTAL1:15 (Bool "for" (Set (Var "Q")) "being" ($#l1_quantal1 :::"Quantale":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool "(" (Bool (Set (Var "c")) "is" ($#v18_quantal1 :::"cyclic"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b"))) ($#r3_lattices :::"[="::: ) (Set (Var "c")))) "holds" (Bool (Set (Set (Var "b")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "a"))) ($#r3_lattices :::"[="::: ) (Set (Var "c")))) ")" ))) ; theorem :: QUANTAL1:16 (Bool "for" (Set (Var "Q")) "being" ($#l1_quantal1 :::"Quantale":::) (Bool "for" (Set (Var "s")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v18_quantal1 :::"cyclic"::: ) )) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s")) ")" ) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s")))) & (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "s")) ")" ) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "s")))) ")" ))) ; theorem :: QUANTAL1:17 (Bool "for" (Set (Var "Q")) "being" ($#l1_quantal1 :::"Quantale":::) (Bool "for" (Set (Var "s")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v18_quantal1 :::"cyclic"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s")) ")" ) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s")) ")" ) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s")))) & (Bool (Set (Set (Var "a")) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "s")) ")" ) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "s")) ")" ) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "s")))) ")" ))) ; theorem :: QUANTAL1:18 (Bool "for" (Set (Var "Q")) "being" ($#l1_quantal1 :::"Quantale":::) (Bool "for" (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s")) ")" ) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s")) ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s")) ")" ) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s")) ")" )) ($#r3_lattices :::"[="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b")) ")" ) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s")) ")" ) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "s")))))) ; theorem :: QUANTAL1:19 (Bool "for" (Set (Var "Q")) "being" ($#l1_quantal1 :::"Quantale":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "D")) "is" ($#v17_quantal1 :::"dualizing"::: ) )) "holds" (Bool "(" (Bool (Set (Var "Q")) "is" ($#v1_group_1 :::"unital"::: ) ) & (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "Q")))) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "D")))) & (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "Q")))) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "D")))) ")" ))) ; theorem :: QUANTAL1:20 (Bool "for" (Set (Var "Q")) "being" ($#l1_quantal1 :::"Quantale":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "a")) "is" ($#v17_quantal1 :::"dualizing"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "b")) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" (Set (Var "c")) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "a")) ")" ) ")" ) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "b")) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "c")) ($#k1_quantal1 :::"-r>"::: ) (Set (Var "a")) ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b")) ")" ) ($#k2_quantal1 :::"-l>"::: ) (Set (Var "a")))) ")" ))) ; definitionattr "c1" is :::"strict"::: ; struct :::"Girard-QuantaleStr"::: -> ($#l2_quantal1 :::"QuasiNetStr"::: ) ; aggr :::"Girard-QuantaleStr":::(# :::"carrier":::, :::"L_join":::, :::"L_meet":::, :::"multF":::, :::"OneF":::, :::"absurd"::: #) -> ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) ; sel :::"absurd"::: "c1" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) ; end; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) ; attr "IT" is :::"cyclic"::: means :: QUANTAL1:def 19 (Bool (Set "the" ($#u1_quantal1 :::"absurd"::: ) "of" "IT") "is" ($#v18_quantal1 :::"cyclic"::: ) ); attr "IT" is :::"dualized"::: means :: QUANTAL1:def 20 (Bool (Set "the" ($#u1_quantal1 :::"absurd"::: ) "of" "IT") "is" ($#v17_quantal1 :::"dualizing"::: ) ); end; :: deftheorem defines :::"cyclic"::: QUANTAL1:def 19 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v20_quantal1 :::"cyclic"::: ) ) "iff" (Bool (Set "the" ($#u1_quantal1 :::"absurd"::: ) "of" (Set (Var "IT"))) "is" ($#v18_quantal1 :::"cyclic"::: ) ) ")" )); :: deftheorem defines :::"dualized"::: QUANTAL1:def 20 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v21_quantal1 :::"dualized"::: ) ) "iff" (Bool (Set "the" ($#u1_quantal1 :::"absurd"::: ) "of" (Set (Var "IT"))) "is" ($#v17_quantal1 :::"dualizing"::: ) ) ")" )); theorem :: QUANTAL1:21 (Bool "for" (Set (Var "Q")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Q"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "Q"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "Q"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k1_lattice3 :::"BooleLatt"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "Q")) "is" ($#v20_quantal1 :::"cyclic"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v21_quantal1 :::"dualized"::: ) ) ")" )) ; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "b1", "b2", "b3" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); let "e1", "e2" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); cluster (Set ($#g3_quantal1 :::"Girard-QuantaleStr"::: ) "(#" "A" "," "b1" "," "b2" "," "b3" "," "e1" "," "e2" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v4_lattice3 :::"complete"::: ) ($#v7_quantal1 :::"right-distributive"::: ) ($#v8_quantal1 :::"left-distributive"::: ) ($#v19_quantal1 :::"strict"::: ) ($#v20_quantal1 :::"cyclic"::: ) ($#v21_quantal1 :::"dualized"::: ) for ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) ; end; definitionmode Girard-Quantale is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v4_lattice3 :::"complete"::: ) ($#v7_quantal1 :::"right-distributive"::: ) ($#v8_quantal1 :::"left-distributive"::: ) ($#v20_quantal1 :::"cyclic"::: ) ($#v21_quantal1 :::"dualized"::: ) ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) ; end; definitionlet "G" be ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) ; func :::"Bottom"::: "G" -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: QUANTAL1:def 21 (Set "the" ($#u1_quantal1 :::"absurd"::: ) "of" "G"); end; :: deftheorem defines :::"Bottom"::: QUANTAL1:def 21 : (Bool "for" (Set (Var "G")) "being" ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) "holds" (Bool (Set ($#k3_quantal1 :::"Bottom"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_quantal1 :::"absurd"::: ) "of" (Set (Var "G"))))); definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) ; func :::"Top"::: "G" -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: QUANTAL1:def 22 (Set (Set "(" ($#k3_quantal1 :::"Bottom"::: ) "G" ")" ) ($#k1_quantal1 :::"-r>"::: ) (Set "(" ($#k3_quantal1 :::"Bottom"::: ) "G" ")" )); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func :::"Bottom"::: "a" -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: QUANTAL1:def 23 (Set "a" ($#k1_quantal1 :::"-r>"::: ) (Set "(" ($#k3_quantal1 :::"Bottom"::: ) "G" ")" )); end; :: deftheorem defines :::"Top"::: QUANTAL1:def 22 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) "holds" (Bool (Set ($#k4_quantal1 :::"Top"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_quantal1 :::"Bottom"::: ) (Set (Var "G")) ")" ) ($#k1_quantal1 :::"-r>"::: ) (Set "(" ($#k3_quantal1 :::"Bottom"::: ) (Set (Var "G")) ")" )))); :: deftheorem defines :::"Bottom"::: QUANTAL1:def 23 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k5_quantal1 :::"Bottom"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_quantal1 :::"-r>"::: ) (Set "(" ($#k3_quantal1 :::"Bottom"::: ) (Set (Var "G")) ")" ))))); definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) ; func :::"Negation"::: "G" -> ($#m1_subset_1 :::"UnOp":::) "of" "G" means :: QUANTAL1:def 24 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k5_quantal1 :::"Bottom"::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"Negation"::: QUANTAL1:def 24 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_quantal1 :::"Negation"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k5_quantal1 :::"Bottom"::: ) (Set (Var "a"))))) ")" ))); definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) ; let "u" be ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "G")); func :::"Bottom"::: "u" -> ($#m1_subset_1 :::"UnOp":::) "of" "G" equals :: QUANTAL1:def 25 (Set (Set "(" ($#k6_quantal1 :::"Negation"::: ) "G" ")" ) ($#k1_partfun1 :::"*"::: ) "u"); end; :: deftheorem defines :::"Bottom"::: QUANTAL1:def 25 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k7_quantal1 :::"Bottom"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_quantal1 :::"Negation"::: ) (Set (Var "G")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "u")))))); definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) ; let "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "G")); func :::"Bottom"::: "o" -> ($#m1_subset_1 :::"BinOp":::) "of" "G" equals :: QUANTAL1:def 26 (Set (Set "(" ($#k6_quantal1 :::"Negation"::: ) "G" ")" ) ($#k1_partfun1 :::"*"::: ) "o"); end; :: deftheorem defines :::"Bottom"::: QUANTAL1:def 26 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_quantal1 :::"Girard-QuantaleStr"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k8_quantal1 :::"Bottom"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_quantal1 :::"Negation"::: ) (Set (Var "G")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "o")))))); theorem :: QUANTAL1:22 (Bool "for" (Set (Var "Q")) "being" ($#l3_quantal1 :::"Girard-Quantale":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool (Set ($#k5_quantal1 :::"Bottom"::: ) (Set "(" ($#k5_quantal1 :::"Bottom"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: QUANTAL1:23 (Bool "for" (Set (Var "Q")) "being" ($#l3_quantal1 :::"Girard-Quantale":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k5_quantal1 :::"Bottom"::: ) (Set (Var "b"))) ($#r3_lattices :::"[="::: ) (Set ($#k5_quantal1 :::"Bottom"::: ) (Set (Var "a")))))) ; theorem :: QUANTAL1:24 (Bool "for" (Set (Var "Q")) "being" ($#l3_quantal1 :::"Girard-Quantale":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_quantal1 :::"Bottom"::: ) (Set "(" ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "Q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_lattice3 :::""/\""::: ) "(" "{" (Set "(" ($#k5_quantal1 :::"Bottom"::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," (Set (Var "Q")) ")" )))) ; theorem :: QUANTAL1:25 (Bool "for" (Set (Var "Q")) "being" ($#l3_quantal1 :::"Girard-Quantale":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_quantal1 :::"Bottom"::: ) (Set "(" ($#k16_lattice3 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "Q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set "(" ($#k5_quantal1 :::"Bottom"::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," (Set (Var "Q")) ")" )))) ; theorem :: QUANTAL1:26 (Bool "for" (Set (Var "Q")) "being" ($#l3_quantal1 :::"Girard-Quantale":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool "(" (Bool (Set ($#k5_quantal1 :::"Bottom"::: ) (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_quantal1 :::"Bottom"::: ) (Set (Var "a")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" ($#k5_quantal1 :::"Bottom"::: ) (Set (Var "b")) ")" ))) & (Bool (Set ($#k5_quantal1 :::"Bottom"::: ) (Set "(" (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_quantal1 :::"Bottom"::: ) (Set (Var "a")) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" ($#k5_quantal1 :::"Bottom"::: ) (Set (Var "b")) ")" ))) ")" ))) ; definitionlet "Q" be ($#l3_quantal1 :::"Girard-Quantale":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "Q")); func "a" :::"delta"::: "b" -> ($#m1_subset_1 :::"Element":::) "of" "Q" equals :: QUANTAL1:def 27 (Set ($#k5_quantal1 :::"Bottom"::: ) (Set "(" (Set "(" ($#k5_quantal1 :::"Bottom"::: ) "a" ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" ($#k5_quantal1 :::"Bottom"::: ) "b" ")" ) ")" )); end; :: deftheorem defines :::"delta"::: QUANTAL1:def 27 : (Bool "for" (Set (Var "Q")) "being" ($#l3_quantal1 :::"Girard-Quantale":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool (Set (Set (Var "a")) ($#k9_quantal1 :::"delta"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k5_quantal1 :::"Bottom"::: ) (Set "(" (Set "(" ($#k5_quantal1 :::"Bottom"::: ) (Set (Var "a")) ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" ($#k5_quantal1 :::"Bottom"::: ) (Set (Var "b")) ")" ) ")" ))))); theorem :: QUANTAL1:27 (Bool "for" (Set (Var "Q")) "being" ($#l3_quantal1 :::"Girard-Quantale":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "Q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b")) ")" ) where b "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) : (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," (Set (Var "Q")) ")" )) & (Bool (Set (Set (Var "a")) ($#k9_quantal1 :::"delta"::: ) (Set "(" ($#k16_lattice3 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "Q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_lattice3 :::""/\""::: ) "(" "{" (Set "(" (Set (Var "a")) ($#k9_quantal1 :::"delta"::: ) (Set (Var "c")) ")" ) where c "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," (Set (Var "Q")) ")" )) ")" )))) ; theorem :: QUANTAL1:28 (Bool "for" (Set (Var "Q")) "being" ($#l3_quantal1 :::"Girard-Quantale":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "Q")) ")" ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "a")) ")" ) where b "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) : (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," (Set (Var "Q")) ")" )) & (Bool (Set (Set "(" ($#k16_lattice3 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "Q")) ")" ")" ) ($#k9_quantal1 :::"delta"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k16_lattice3 :::""/\""::: ) "(" "{" (Set "(" (Set (Var "c")) ($#k9_quantal1 :::"delta"::: ) (Set (Var "a")) ")" ) where c "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) : (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," (Set (Var "Q")) ")" )) ")" )))) ; theorem :: QUANTAL1:29 (Bool "for" (Set (Var "Q")) "being" ($#l3_quantal1 :::"Girard-Quantale":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k9_quantal1 :::"delta"::: ) (Set "(" (Set (Var "b")) ($#k4_lattices :::""/\""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_quantal1 :::"delta"::: ) (Set (Var "b")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k9_quantal1 :::"delta"::: ) (Set (Var "c")) ")" ))) & (Bool (Set (Set "(" (Set (Var "b")) ($#k4_lattices :::""/\""::: ) (Set (Var "c")) ")" ) ($#k9_quantal1 :::"delta"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b")) ($#k9_quantal1 :::"delta"::: ) (Set (Var "a")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "c")) ($#k9_quantal1 :::"delta"::: ) (Set (Var "a")) ")" ))) ")" ))) ; theorem :: QUANTAL1:30 (Bool "for" (Set (Var "Q")) "being" ($#l3_quantal1 :::"Girard-Quantale":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "a1")) ($#r3_lattices :::"[="::: ) (Set (Var "b1"))) & (Bool (Set (Var "a2")) ($#r3_lattices :::"[="::: ) (Set (Var "b2")))) "holds" (Bool (Set (Set (Var "a1")) ($#k9_quantal1 :::"delta"::: ) (Set (Var "a2"))) ($#r3_lattices :::"[="::: ) (Set (Set (Var "b1")) ($#k9_quantal1 :::"delta"::: ) (Set (Var "b2")))))) ; theorem :: QUANTAL1:31 (Bool "for" (Set (Var "Q")) "being" ($#l3_quantal1 :::"Girard-Quantale":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_quantal1 :::"delta"::: ) (Set (Var "b")) ")" ) ($#k9_quantal1 :::"delta"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_quantal1 :::"delta"::: ) (Set "(" (Set (Var "b")) ($#k9_quantal1 :::"delta"::: ) (Set (Var "c")) ")" ))))) ; theorem :: QUANTAL1:32 (Bool "for" (Set (Var "Q")) "being" ($#l3_quantal1 :::"Girard-Quantale":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set "(" ($#k4_quantal1 :::"Top"::: ) (Set (Var "Q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" ($#k4_quantal1 :::"Top"::: ) (Set (Var "Q")) ")" ) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; theorem :: QUANTAL1:33 (Bool "for" (Set (Var "Q")) "being" ($#l3_quantal1 :::"Girard-Quantale":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Q")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k9_quantal1 :::"delta"::: ) (Set "(" ($#k3_quantal1 :::"Bottom"::: ) (Set (Var "Q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" ($#k3_quantal1 :::"Bottom"::: ) (Set (Var "Q")) ")" ) ($#k9_quantal1 :::"delta"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; theorem :: QUANTAL1:34 (Bool "for" (Set (Var "Q")) "being" ($#l1_quantal1 :::"Quantale":::) (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "Q")) "st" (Bool (Bool (Set (Var "j")) "is" ($#v14_quantal1 :::"monotone"::: ) ) & (Bool (Set (Var "j")) "is" ($#v11_quantal1 :::"idempotent"::: ) ) & (Bool (Set (Var "j")) "is" ($#v15_quantal1 :::"\/-distributive"::: ) )) "holds" (Bool "ex" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "j")))) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k15_lattice3 :::""\/""::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "Q")) ")" ")" ))) ")" ) ")" )))) ;