:: LATTICE8 semantic presentation begin definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "L" is :::"finitely_typed"::: means :: LATTICE8:def 1 (Bool "ex" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))) "holds" (Bool (Set (Var "e")) "is" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "A"))) ")" ) & (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) & (Bool (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "e1")) ($#k5_eqrel_1 :::""\/""::: ) (Set (Var "e2"))))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "o"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_lattice5 :::"are_joint_by"::: ) (Set (Var "F")) "," (Set (Var "e1")) "," (Set (Var "e2"))) ")" ))))) ")" )); end; :: deftheorem defines :::"finitely_typed"::: LATTICE8:def 1 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_lattice8 :::"finitely_typed"::: ) ) "iff" (Bool "ex" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) "holds" (Bool (Set (Var "e")) "is" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "A"))) ")" ) & (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "e1")) ($#k5_eqrel_1 :::""\/""::: ) (Set (Var "e2"))))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "o"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_lattice5 :::"are_joint_by"::: ) (Set (Var "F")) "," (Set (Var "e1")) "," (Set (Var "e2"))) ")" ))))) ")" )) ")" )); definitionlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); pred "L" :::"has_a_representation_of_type<="::: "n" means :: LATTICE8:def 2 (Bool "ex" (Set (Var "A")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" "L" "," (Set "(" ($#k1_lattice5 :::"EqRelLATT"::: ) (Set (Var "A")) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" bbbadV2_FUNCT_1()) & (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "f"))) "is" ($#v1_lattice8 :::"finitely_typed"::: ) ) & (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "e")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "A")))) ")" )) & (Bool (Set ($#k2_lattice5 :::"type_of"::: ) (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "f")) ")" )) ($#r1_xxreal_0 :::"<="::: ) "n") ")" ))); end; :: deftheorem defines :::"has_a_representation_of_type<="::: LATTICE8:def 2 : (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "L")) ($#r1_lattice8 :::"has_a_representation_of_type<="::: ) (Set (Var "n"))) "iff" (Bool "ex" (Set (Var "A")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "L")) "," (Set "(" ($#k1_lattice5 :::"EqRelLATT"::: ) (Set (Var "A")) ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" bbbadV2_FUNCT_1()) & (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "f"))) "is" ($#v1_lattice8 :::"finitely_typed"::: ) ) & (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "e")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "A")))) ")" )) & (Bool (Set ($#k2_lattice5 :::"type_of"::: ) (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "f")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ))) ")" ))); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_waybel_1 :::"distributive"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registrationlet "A" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v5_yellow_0 :::"meet-inheriting"::: ) ($#v6_yellow_0 :::"join-inheriting"::: ) ($#v1_lattice8 :::"finitely_typed"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set ($#k1_lattice5 :::"EqRelLATT"::: ) "A"); end; theorem :: LATTICE8:1 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "A")) "," (Set (Var "L")) "holds" (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_ordinal1 :::"c="::: ) (Set ($#k7_lattice5 :::"DistEsti"::: ) (Set (Var "d"))))))) ; theorem :: LATTICE8:2 (Bool "for" (Set (Var "L")) "being" ($#v7_struct_0 :::"trivial"::: ) ($#l1_orders_2 :::"Semilattice":::) "holds" (Bool (Set (Var "L")) "is" ($#v1_yellow11 :::"modular"::: ) )) ; theorem :: LATTICE8:3 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_yellow_0 :::"Sublattice":::) "of" (Set ($#k1_lattice5 :::"EqRelLATT"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v7_struct_0 :::"trivial"::: ) ) "or" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool (Set (Var "e")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "A")))) ")" )) ")" ))) ; theorem :: LATTICE8:4 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ) & (Bool (Set (Var "f")) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v19_waybel_0 :::"meet-preserving"::: ) ) & (Bool (Set (Var "f")) "is" ($#v20_waybel_0 :::"join-preserving"::: ) ) ")" ))) ; theorem :: LATTICE8:5 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "L1")) "," (Set (Var "L2")) ($#r5_waybel_1 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "L1")) "is" ($#v1_yellow11 :::"modular"::: ) )) "holds" (Bool (Set (Var "L2")) "is" ($#v1_yellow11 :::"modular"::: ) )) ; theorem :: LATTICE8:6 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#v5_orders_3 :::"monotone"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool (Set ($#k1_yellow_2 :::"Image"::: ) (Set (Var "f"))) "is" ($#v1_yellow_0 :::"lower-bounded"::: ) )))) ; theorem :: LATTICE8:7 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "L")) "," (Set "(" ($#k1_lattice5 :::"EqRelLATT"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" bbbadV2_FUNCT_1()) & (Bool (Set (Set "(" ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r3_orders_2 :::"<="::: ) (Set (Set "(" ($#k2_waybel_1 :::"corestr"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y"))))))) ; begin theorem :: LATTICE8:8 (Bool "for" (Set (Var "A")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v1_lattice8 :::"finitely_typed"::: ) ($#m1_yellow_0 :::"Sublattice":::) "of" (Set ($#k1_lattice5 :::"EqRelLATT"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool (Set (Var "e")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "A")))) & (Bool (Set ($#k2_lattice5 :::"type_of"::: ) (Set (Var "L"))) ($#r1_xxreal_0 :::"<="::: ) (Num 2))) "holds" (Bool (Set (Var "L")) "is" ($#v1_yellow11 :::"modular"::: ) )))) ; theorem :: LATTICE8:9 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "L")) ($#r1_lattice8 :::"has_a_representation_of_type<="::: ) (Num 2))) "holds" (Bool (Set (Var "L")) "is" ($#v1_yellow11 :::"modular"::: ) )) ; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"new_set2"::: "A" -> ($#m1_hidden :::"set"::: ) equals :: LATTICE8:def 3 (Set "A" ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_tarski :::"}"::: ) )); end; :: deftheorem defines :::"new_set2"::: LATTICE8:def 3 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_lattice8 :::"new_set2"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_tarski :::"}"::: ) )))); registrationlet "A" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_lattice8 :::"new_set2"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::); let "d" be ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Const "A")) "," (Set (Const "L")); let "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "A")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))) ($#k4_zfmisc_1 :::":]"::: ) ); func :::"new_bi_fun2"::: "(" "d" "," "q" ")" -> ($#m1_subset_1 :::"BiFunction":::) "of" (Set "(" ($#k1_lattice8 :::"new_set2"::: ) "A" ")" ) "," "L" means :: LATTICE8:def 4 (Bool "(" (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set "d" ($#k3_lattice5 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" )) ")" ) & (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) "L")) & (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) "L")) & (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "d" ($#k3_lattice5 :::"."::: ) "(" (Set "(" "q" ($#k4_mcart_1 :::"`1_4"::: ) ")" ) "," (Set "(" "q" ($#k5_mcart_1 :::"`2_4"::: ) ")" ) ")" ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" "q" ($#k6_mcart_1 :::"`3_4"::: ) ")" ) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" "q" ($#k7_mcart_1 :::"`4_4"::: ) ")" ))) & (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "d" ($#k3_lattice5 :::"."::: ) "(" (Set "(" "q" ($#k4_mcart_1 :::"`1_4"::: ) ")" ) "," (Set "(" "q" ($#k5_mcart_1 :::"`2_4"::: ) ")" ) ")" ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" "q" ($#k6_mcart_1 :::"`3_4"::: ) ")" ) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" "q" ($#k7_mcart_1 :::"`4_4"::: ) ")" ))) & (Bool "(" "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool "(" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "d" ($#k3_lattice5 :::"."::: ) "(" (Set (Var "u")) "," (Set "(" "q" ($#k4_mcart_1 :::"`1_4"::: ) ")" ) ")" ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" "q" ($#k6_mcart_1 :::"`3_4"::: ) ")" ))) & (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) "," (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "d" ($#k3_lattice5 :::"."::: ) "(" (Set (Var "u")) "," (Set "(" "q" ($#k4_mcart_1 :::"`1_4"::: ) ")" ) ")" ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" "q" ($#k6_mcart_1 :::"`3_4"::: ) ")" ))) & (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "d" ($#k3_lattice5 :::"."::: ) "(" (Set (Var "u")) "," (Set "(" "q" ($#k5_mcart_1 :::"`2_4"::: ) ")" ) ")" ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" "q" ($#k6_mcart_1 :::"`3_4"::: ) ")" ))) & (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) "A" ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "d" ($#k3_lattice5 :::"."::: ) "(" (Set (Var "u")) "," (Set "(" "q" ($#k5_mcart_1 :::"`2_4"::: ) ")" ) ")" ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" "q" ($#k6_mcart_1 :::"`3_4"::: ) ")" ))) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"new_bi_fun2"::: LATTICE8:def 4 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k4_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set "(" ($#k1_lattice8 :::"new_set2"::: ) (Set (Var "A")) ")" ) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k2_lattice8 :::"new_bi_fun2"::: ) "(" (Set (Var "d")) "," (Set (Var "q")) ")" )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b5")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "d")) ($#k3_lattice5 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" )) ")" ) & (Bool (Set (Set (Var "b5")) ($#k1_binop_1 :::"."::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "b5")) ($#k1_binop_1 :::"."::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "b5")) ($#k1_binop_1 :::"."::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "d")) ($#k3_lattice5 :::"."::: ) "(" (Set "(" (Set (Var "q")) ($#k4_mcart_1 :::"`1_4"::: ) ")" ) "," (Set "(" (Set (Var "q")) ($#k5_mcart_1 :::"`2_4"::: ) ")" ) ")" ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "q")) ($#k6_mcart_1 :::"`3_4"::: ) ")" ) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" (Set (Var "q")) ($#k7_mcart_1 :::"`4_4"::: ) ")" ))) & (Bool (Set (Set (Var "b5")) ($#k1_binop_1 :::"."::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "d")) ($#k3_lattice5 :::"."::: ) "(" (Set "(" (Set (Var "q")) ($#k4_mcart_1 :::"`1_4"::: ) ")" ) "," (Set "(" (Set (Var "q")) ($#k5_mcart_1 :::"`2_4"::: ) ")" ) ")" ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "q")) ($#k6_mcart_1 :::"`3_4"::: ) ")" ) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" (Set (Var "q")) ($#k7_mcart_1 :::"`4_4"::: ) ")" ))) & (Bool "(" "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Set (Var "b5")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "d")) ($#k3_lattice5 :::"."::: ) "(" (Set (Var "u")) "," (Set "(" (Set (Var "q")) ($#k4_mcart_1 :::"`1_4"::: ) ")" ) ")" ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "q")) ($#k6_mcart_1 :::"`3_4"::: ) ")" ))) & (Bool (Set (Set (Var "b5")) ($#k1_binop_1 :::"."::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "d")) ($#k3_lattice5 :::"."::: ) "(" (Set (Var "u")) "," (Set "(" (Set (Var "q")) ($#k4_mcart_1 :::"`1_4"::: ) ")" ) ")" ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "q")) ($#k6_mcart_1 :::"`3_4"::: ) ")" ))) & (Bool (Set (Set (Var "b5")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "d")) ($#k3_lattice5 :::"."::: ) "(" (Set (Var "u")) "," (Set "(" (Set (Var "q")) ($#k5_mcart_1 :::"`2_4"::: ) ")" ) ")" ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "q")) ($#k6_mcart_1 :::"`3_4"::: ) ")" ))) & (Bool (Set (Set (Var "b5")) ($#k1_binop_1 :::"."::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "d")) ($#k3_lattice5 :::"."::: ) "(" (Set (Var "u")) "," (Set "(" (Set (Var "q")) ($#k5_mcart_1 :::"`2_4"::: ) ")" ) ")" ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "q")) ($#k6_mcart_1 :::"`3_4"::: ) ")" ))) ")" ) ")" ) ")" ) ")" )))))); theorem :: LATTICE8:10 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "d")) "is" ($#v2_lattice5 :::"zeroed"::: ) )) "holds" (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k4_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k2_lattice8 :::"new_bi_fun2"::: ) "(" (Set (Var "d")) "," (Set (Var "q")) ")" ) "is" ($#v2_lattice5 :::"zeroed"::: ) ))))) ; theorem :: LATTICE8:11 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "d")) "is" ($#v1_lattice5 :::"symmetric"::: ) )) "holds" (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k4_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k2_lattice8 :::"new_bi_fun2"::: ) "(" (Set (Var "d")) "," (Set (Var "q")) ")" ) "is" ($#v1_lattice5 :::"symmetric"::: ) ))))) ; theorem :: LATTICE8:12 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v1_yellow11 :::"modular"::: ) )) "holds" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "d")) "is" ($#v1_lattice5 :::"symmetric"::: ) ) & (Bool (Set (Var "d")) "is" ($#v3_lattice5 :::"u.t.i."::: ) )) "holds" (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k4_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Set (Var "d")) ($#k3_lattice5 :::"."::: ) "(" (Set "(" (Set (Var "q")) ($#k4_mcart_1 :::"`1_4"::: ) ")" ) "," (Set "(" (Set (Var "q")) ($#k5_mcart_1 :::"`2_4"::: ) ")" ) ")" ) ($#r3_orders_2 :::"<="::: ) (Set (Set "(" (Set (Var "q")) ($#k6_mcart_1 :::"`3_4"::: ) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "q")) ($#k7_mcart_1 :::"`4_4"::: ) ")" )))) "holds" (Bool (Set ($#k2_lattice8 :::"new_bi_fun2"::: ) "(" (Set (Var "d")) "," (Set (Var "q")) ")" ) "is" ($#v3_lattice5 :::"u.t.i."::: ) ))))) ; theorem :: LATTICE8:13 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k4_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Var "d")) ($#r1_relset_1 :::"c="::: ) (Set ($#k2_lattice8 :::"new_bi_fun2"::: ) "(" (Set (Var "d")) "," (Set (Var "q")) ")" )))))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "O" be ($#m1_hidden :::"Ordinal":::); func :::"ConsecutiveSet2"::: "(" "A" "," "O" ")" -> ($#m1_hidden :::"set"::: ) means :: LATTICE8:def 5 (Bool "ex" (Set (Var "L0")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "L0")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "L0"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "O")) & (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) "A") & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "O"))) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_lattice8 :::"new_set2"::: ) (Set "(" (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "O")) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "L0")) ($#k5_relat_1 :::"|"::: ) (Set (Var "C")) ")" ) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"ConsecutiveSet2"::: LATTICE8:def 5 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" (Set (Var "A")) "," (Set (Var "O")) ")" )) "iff" (Bool "ex" (Set (Var "L0")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "L0")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "L0"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O")))) & (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O"))))) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_lattice8 :::"new_set2"::: ) (Set "(" (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O")))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "L0")) ($#k5_relat_1 :::"|"::: ) (Set (Var "C")) ")" ) ")" ))) ")" ) ")" )) ")" )))); theorem :: LATTICE8:14 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" (Set (Var "A")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "A")))) ; theorem :: LATTICE8:15 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_lattice8 :::"new_set2"::: ) (Set "(" ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" (Set (Var "A")) "," (Set (Var "O")) ")" ")" ))))) ; theorem :: LATTICE8:16 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool (Bool (Set (Var "O")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "O")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) ) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Var "O"))) & (Bool "(" "for" (Set (Var "O1")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "O1")) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "O1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" (Set (Var "A")) "," (Set (Var "O1")) ")" )) ")" )) "holds" (Bool (Set ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" (Set (Var "A")) "," (Set (Var "O")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "T")) ")" )))))) ; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "O" be ($#m1_hidden :::"Ordinal":::); cluster (Set ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" "A" "," "O" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: LATTICE8:17 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" (Set (Var "A")) "," (Set (Var "O")) ")" )))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::); let "d" be ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Const "A")) "," (Set (Const "L")); let "q" be ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Const "d")); let "O" be ($#m1_hidden :::"Ordinal":::); assume (Bool (Set (Const "O")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "q")))) ; func :::"Quadr2"::: "(" "q" "," "O" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" "A" "," "O" ")" ")" ) "," (Set "(" ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" "A" "," "O" ")" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k4_zfmisc_1 :::":]"::: ) ) equals :: LATTICE8:def 6 (Set "q" ($#k1_funct_1 :::"."::: ) "O"); end; :: deftheorem defines :::"Quadr2"::: LATTICE8:def 6 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "q")) "being" ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "O")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q"))))) "holds" (Bool (Set ($#k4_lattice8 :::"Quadr2"::: ) "(" (Set (Var "q")) "," (Set (Var "O")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "O"))))))))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::); let "d" be ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Const "A")) "," (Set (Const "L")); let "q" be ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Const "d")); let "O" be ($#m1_hidden :::"Ordinal":::); func :::"ConsecutiveDelta2"::: "(" "q" "," "O" ")" -> ($#m1_hidden :::"set"::: ) means :: LATTICE8:def 7 (Bool "ex" (Set (Var "L0")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "L0")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "L0"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "O")) & (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) "d") & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "O"))) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_lattice8 :::"new_bi_fun2"::: ) "(" (Set "(" ($#k10_lattice5 :::"BiFun"::: ) "(" (Set "(" (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" "A" "," (Set (Var "C")) ")" ")" ) "," "L" ")" ")" ) "," (Set "(" ($#k4_lattice8 :::"Quadr2"::: ) "(" "q" "," (Set (Var "C")) ")" ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "O")) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "L0")) ($#k5_relat_1 :::"|"::: ) (Set (Var "C")) ")" ) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"ConsecutiveDelta2"::: LATTICE8:def 7 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "q")) "being" ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b6")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k5_lattice8 :::"ConsecutiveDelta2"::: ) "(" (Set (Var "q")) "," (Set (Var "O")) ")" )) "iff" (Bool "ex" (Set (Var "L0")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "L0")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "L0"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O")))) & (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O"))))) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_lattice8 :::"new_bi_fun2"::: ) "(" (Set "(" ($#k10_lattice5 :::"BiFun"::: ) "(" (Set "(" (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ")" ) "," (Set (Var "L")) ")" ")" ) "," (Set "(" ($#k4_lattice8 :::"Quadr2"::: ) "(" (Set (Var "q")) "," (Set (Var "C")) ")" ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O")))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "L0")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "L0")) ($#k5_relat_1 :::"|"::: ) (Set (Var "C")) ")" ) ")" ))) ")" ) ")" )) ")" ))))))); theorem :: LATTICE8:18 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "q")) "being" ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Var "d")) "holds" (Bool (Set ($#k5_lattice8 :::"ConsecutiveDelta2"::: ) "(" (Set (Var "q")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "d"))))))) ; theorem :: LATTICE8:19 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "q")) "being" ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k5_lattice8 :::"ConsecutiveDelta2"::: ) "(" (Set (Var "q")) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "O")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_lattice8 :::"new_bi_fun2"::: ) "(" (Set "(" ($#k10_lattice5 :::"BiFun"::: ) "(" (Set "(" ($#k5_lattice8 :::"ConsecutiveDelta2"::: ) "(" (Set (Var "q")) "," (Set (Var "O")) ")" ")" ) "," (Set "(" ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" (Set (Var "A")) "," (Set (Var "O")) ")" ")" ) "," (Set (Var "L")) ")" ")" ) "," (Set "(" ($#k4_lattice8 :::"Quadr2"::: ) "(" (Set (Var "q")) "," (Set (Var "O")) ")" ")" ) ")" ))))))) ; theorem :: LATTICE8:20 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "q")) "being" ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"T-Sequence":::) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "O")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "O")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) ) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Var "O"))) & (Bool "(" "for" (Set (Var "O1")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "O1")) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "O1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_lattice8 :::"ConsecutiveDelta2"::: ) "(" (Set (Var "q")) "," (Set (Var "O1")) ")" )) ")" )) "holds" (Bool (Set ($#k5_lattice8 :::"ConsecutiveDelta2"::: ) "(" (Set (Var "q")) "," (Set (Var "O")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "T")) ")" ))))))))) ; theorem :: LATTICE8:21 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "," (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "O1")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "O2")))) "holds" (Bool (Set ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" (Set (Var "A")) "," (Set (Var "O1")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" (Set (Var "A")) "," (Set (Var "O2")) ")" )))) ; theorem :: LATTICE8:22 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "q")) "being" ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k5_lattice8 :::"ConsecutiveDelta2"::: ) "(" (Set (Var "q")) "," (Set (Var "O")) ")" ) "is" ($#m1_subset_1 :::"BiFunction":::) "of" (Set "(" ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" (Set (Var "A")) "," (Set (Var "O")) ")" ")" ) "," (Set (Var "L")))))))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::); let "d" be ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Const "A")) "," (Set (Const "L")); let "q" be ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Const "d")); let "O" be ($#m1_hidden :::"Ordinal":::); :: original: :::"ConsecutiveDelta2"::: redefine func :::"ConsecutiveDelta2"::: "(" "q" "," "O" ")" -> ($#m1_subset_1 :::"BiFunction":::) "of" (Set "(" ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" "A" "," "O" ")" ")" ) "," "L"; end; theorem :: LATTICE8:23 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "q")) "being" ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Var "d")) ($#r1_relset_1 :::"c="::: ) (Set ($#k6_lattice8 :::"ConsecutiveDelta2"::: ) "(" (Set (Var "q")) "," (Set (Var "O")) ")" ))))))) ; theorem :: LATTICE8:24 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "O1")) "," (Set (Var "O2")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "q")) "being" ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Var "O1")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "O2")))) "holds" (Bool (Set ($#k6_lattice8 :::"ConsecutiveDelta2"::: ) "(" (Set (Var "q")) "," (Set (Var "O1")) ")" ) ($#r1_relset_1 :::"c="::: ) (Set ($#k6_lattice8 :::"ConsecutiveDelta2"::: ) "(" (Set (Var "q")) "," (Set (Var "O2")) ")" ))))))) ; theorem :: LATTICE8:25 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "d")) "is" ($#v2_lattice5 :::"zeroed"::: ) )) "holds" (Bool "for" (Set (Var "q")) "being" ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k6_lattice8 :::"ConsecutiveDelta2"::: ) "(" (Set (Var "q")) "," (Set (Var "O")) ")" ) "is" ($#v2_lattice5 :::"zeroed"::: ) )))))) ; theorem :: LATTICE8:26 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "d")) "is" ($#v1_lattice5 :::"symmetric"::: ) )) "holds" (Bool "for" (Set (Var "q")) "being" ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k6_lattice8 :::"ConsecutiveDelta2"::: ) "(" (Set (Var "q")) "," (Set (Var "O")) ")" ) "is" ($#v1_lattice5 :::"symmetric"::: ) )))))) ; theorem :: LATTICE8:27 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v1_yellow11 :::"modular"::: ) )) "holds" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "d")) "is" ($#v1_lattice5 :::"symmetric"::: ) ) & (Bool (Set (Var "d")) "is" ($#v3_lattice5 :::"u.t.i."::: ) )) "holds" (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "q")) "being" ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Var "O")) ($#r1_ordinal1 :::"c="::: ) (Set ($#k7_lattice5 :::"DistEsti"::: ) (Set (Var "d"))))) "holds" (Bool (Set ($#k6_lattice8 :::"ConsecutiveDelta2"::: ) "(" (Set (Var "q")) "," (Set (Var "O")) ")" ) "is" ($#v3_lattice5 :::"u.t.i."::: ) )))))) ; theorem :: LATTICE8:28 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_yellow11 :::"modular"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "q")) "being" ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Var "O")) ($#r1_ordinal1 :::"c="::: ) (Set ($#k7_lattice5 :::"DistEsti"::: ) (Set (Var "d"))))) "holds" (Bool (Set ($#k6_lattice8 :::"ConsecutiveDelta2"::: ) "(" (Set (Var "q")) "," (Set (Var "O")) ")" ) "is" ($#m1_subset_1 :::"distance_function":::) "of" (Set "(" ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" (Set (Var "A")) "," (Set (Var "O")) ")" ")" ) "," (Set (Var "L")))))))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::); let "d" be ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Const "A")) "," (Set (Const "L")); func :::"NextSet2"::: "d" -> ($#m1_hidden :::"set"::: ) equals :: LATTICE8:def 8 (Set ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" "A" "," (Set "(" ($#k7_lattice5 :::"DistEsti"::: ) "d" ")" ) ")" ); end; :: deftheorem defines :::"NextSet2"::: LATTICE8:def 8 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) "holds" (Bool (Set ($#k7_lattice8 :::"NextSet2"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k3_lattice8 :::"ConsecutiveSet2"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k7_lattice5 :::"DistEsti"::: ) (Set (Var "d")) ")" ) ")" ))))); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::); let "d" be ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Const "A")) "," (Set (Const "L")); cluster (Set ($#k7_lattice8 :::"NextSet2"::: ) "d") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::); let "d" be ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Const "A")) "," (Set (Const "L")); let "q" be ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Const "d")); func :::"NextDelta2"::: "q" -> ($#m1_hidden :::"set"::: ) equals :: LATTICE8:def 9 (Set ($#k6_lattice8 :::"ConsecutiveDelta2"::: ) "(" "q" "," (Set "(" ($#k7_lattice5 :::"DistEsti"::: ) "d" ")" ) ")" ); end; :: deftheorem defines :::"NextDelta2"::: LATTICE8:def 9 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"BiFunction":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "q")) "being" ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Var "d")) "holds" (Bool (Set ($#k8_lattice8 :::"NextDelta2"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k6_lattice8 :::"ConsecutiveDelta2"::: ) "(" (Set (Var "q")) "," (Set "(" ($#k7_lattice5 :::"DistEsti"::: ) (Set (Var "d")) ")" ) ")" )))))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_yellow11 :::"modular"::: ) ($#l1_orders_2 :::"LATTICE":::); let "d" be ($#m1_subset_1 :::"distance_function":::) "of" (Set (Const "A")) "," (Set (Const "L")); let "q" be ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Const "d")); :: original: :::"NextDelta2"::: redefine func :::"NextDelta2"::: "q" -> ($#m1_subset_1 :::"distance_function":::) "of" (Set "(" ($#k7_lattice8 :::"NextSet2"::: ) "d" ")" ) "," "L"; end; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::); let "d" be ($#m1_subset_1 :::"distance_function":::) "of" (Set (Const "A")) "," (Set (Const "L")); let "Aq" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "dq" be ($#m1_subset_1 :::"distance_function":::) "of" (Set (Const "Aq")) "," (Set (Const "L")); pred "Aq" "," "dq" :::"is_extension2_of"::: "A" "," "d" means :: LATTICE8:def 10 (Bool "ex" (Set (Var "q")) "being" ($#m1_lattice5 :::"QuadrSeq"::: ) "of" "d" "st" (Bool "(" (Bool "Aq" ($#r1_hidden :::"="::: ) (Set ($#k7_lattice8 :::"NextSet2"::: ) "d")) & (Bool "dq" ($#r1_hidden :::"="::: ) (Set ($#k8_lattice8 :::"NextDelta2"::: ) (Set (Var "q")))) ")" )); end; :: deftheorem defines :::"is_extension2_of"::: LATTICE8:def 10 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "Aq")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "dq")) "being" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "Aq")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "Aq")) "," (Set (Var "dq")) ($#r2_lattice8 :::"is_extension2_of"::: ) (Set (Var "A")) "," (Set (Var "d"))) "iff" (Bool "ex" (Set (Var "q")) "being" ($#m1_lattice5 :::"QuadrSeq"::: ) "of" (Set (Var "d")) "st" (Bool "(" (Bool (Set (Var "Aq")) ($#r1_hidden :::"="::: ) (Set ($#k7_lattice8 :::"NextSet2"::: ) (Set (Var "d")))) & (Bool (Set (Var "dq")) ($#r1_hidden :::"="::: ) (Set ($#k8_lattice8 :::"NextDelta2"::: ) (Set (Var "q")))) ")" )) ")" )))))); theorem :: LATTICE8:29 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "Aq")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "dq")) "being" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "Aq")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "Aq")) "," (Set (Var "dq")) ($#r2_lattice8 :::"is_extension2_of"::: ) (Set (Var "A")) "," (Set (Var "d")))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "d")) ($#k3_lattice5 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b"))))) "holds" (Bool "ex" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Aq")) "st" (Bool "(" (Bool (Set (Set (Var "dq")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "z1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "dq")) ($#k3_lattice5 :::"."::: ) "(" (Set (Var "z1")) "," (Set (Var "z2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "d")) ($#k3_lattice5 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k13_lattice3 :::""\/""::: ) (Set (Var "a")) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")))) & (Bool (Set (Set (Var "dq")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "z2")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))))))))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_yellow11 :::"modular"::: ) ($#l1_orders_2 :::"LATTICE":::); let "d" be ($#m1_subset_1 :::"distance_function":::) "of" (Set (Const "A")) "," (Set (Const "L")); mode :::"ExtensionSeq2"::: "of" "A" "," "d" -> ($#m1_hidden :::"Function":::) means :: LATTICE8:def 11 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) "A" "," "d" ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "A9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "d9")) "being" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "A9")) "," "L"(Bool "ex" (Set (Var "Aq")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "dq")) "being" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "Aq")) "," "L" "st" (Bool "(" (Bool (Set (Var "Aq")) "," (Set (Var "dq")) ($#r2_lattice8 :::"is_extension2_of"::: ) (Set (Var "A9")) "," (Set (Var "d9"))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "A9")) "," (Set (Var "d9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "Aq")) "," (Set (Var "dq")) ($#k4_tarski :::"]"::: ) )) ")" ))))) ")" ) ")" ); end; :: deftheorem defines :::"ExtensionSeq2"::: LATTICE8:def 11 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_yellow11 :::"modular"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m1_lattice8 :::"ExtensionSeq2"::: ) "of" (Set (Var "A")) "," (Set (Var "d"))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "A9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "d9")) "being" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "A9")) "," (Set (Var "L"))(Bool "ex" (Set (Var "Aq")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "dq")) "being" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "Aq")) "," (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "Aq")) "," (Set (Var "dq")) ($#r2_lattice8 :::"is_extension2_of"::: ) (Set (Var "A9")) "," (Set (Var "d9"))) & (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "A9")) "," (Set (Var "d9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "Aq")) "," (Set (Var "dq")) ($#k4_tarski :::"]"::: ) )) ")" ))))) ")" ) ")" ) ")" ))))); theorem :: LATTICE8:30 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_yellow11 :::"modular"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "S")) "being" ($#m1_lattice8 :::"ExtensionSeq2"::: ) "of" (Set (Var "A")) "," (Set (Var "d")) (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l")))) "holds" (Bool (Set (Set "(" (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "l")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ))))))) ; theorem :: LATTICE8:31 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_yellow11 :::"modular"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "A")) "," (Set (Var "L")) (Bool "for" (Set (Var "S")) "being" ($#m1_lattice8 :::"ExtensionSeq2"::: ) "of" (Set (Var "A")) "," (Set (Var "d")) (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l")))) "holds" (Bool (Set (Set "(" (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "l")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ))))))) ; theorem :: LATTICE8:32 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_yellow11 :::"modular"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lattice8 :::"ExtensionSeq2"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set ($#k16_lattice5 :::"BasicDF"::: ) (Set (Var "L"))) (Bool "for" (Set (Var "FS")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "FS")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool verum) "}" ))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool verum) "}" ) "is" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "FS")) "," (Set (Var "L")))))) ; theorem :: LATTICE8:33 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_yellow11 :::"modular"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lattice8 :::"ExtensionSeq2"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set ($#k16_lattice5 :::"BasicDF"::: ) (Set (Var "L"))) (Bool "for" (Set (Var "FS")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "FD")) "being" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "FS")) "," (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "FS")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "FS")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool verum) "}" )) & (Bool (Set (Var "FD")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool verum) "}" )) & (Bool (Set (Set (Var "FD")) ($#k3_lattice5 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b"))))) "holds" (Bool "ex" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "FS")) "st" (Bool "(" (Bool (Set (Set (Var "FD")) ($#k3_lattice5 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "z1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "FD")) ($#k3_lattice5 :::"."::: ) "(" (Set (Var "z1")) "," (Set (Var "z2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "FD")) ($#k3_lattice5 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k13_lattice3 :::""\/""::: ) (Set (Var "a")) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")))) & (Bool (Set (Set (Var "FD")) ($#k3_lattice5 :::"."::: ) "(" (Set (Var "z2")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )))))))) ; theorem :: LATTICE8:34 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_yellow11 :::"modular"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lattice8 :::"ExtensionSeq2"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set ($#k16_lattice5 :::"BasicDF"::: ) (Set (Var "L"))) (Bool "for" (Set (Var "FS")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "FD")) "being" ($#m1_subset_1 :::"distance_function":::) "of" (Set (Var "FS")) "," (Set (Var "L")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "L")) "," (Set "(" ($#k1_lattice5 :::"EqRelLATT"::: ) (Set (Var "FS")) ")" ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "FS")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set ($#k4_lattice5 :::"alpha"::: ) (Set (Var "FD")))) & (Bool (Set (Var "FS")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool verum) "}" )) & (Bool (Set (Var "FD")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "(" (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool verum) "}" )) & (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_yellow_2 :::"Image"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "e1")) ($#k5_eqrel_1 :::""\/""::: ) (Set (Var "e2"))))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "FS")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k2_nat_1 :::"+"::: ) (Num 2))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_lattice5 :::"are_joint_by"::: ) (Set (Var "F")) "," (Set (Var "e1")) "," (Set (Var "e2"))) ")" ))))))))) ; theorem :: LATTICE8:35 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_yellow11 :::"modular"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set (Var "L")) ($#r1_lattice8 :::"has_a_representation_of_type<="::: ) (Num 2))) ; theorem :: LATTICE8:36 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) ($#r1_lattice8 :::"has_a_representation_of_type<="::: ) (Num 2)) "iff" (Bool (Set (Var "L")) "is" ($#v1_yellow11 :::"modular"::: ) ) ")" )) ;