:: NECKLA_3 semantic presentation begin theorem :: NECKLA_3:1 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "B"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: NECKLA_3:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k2_enumset1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "d")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: NECKLA_3:3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k2_enumset1 :::"}"::: ) ) "," (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ($#k2_enumset1 :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "g")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "h")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "h")) ($#k4_tarski :::"]"::: ) ) ($#k6_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "d")) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "d")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "g")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "h")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "d")) "," (Set (Var "g")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "d")) "," (Set (Var "h")) ($#k4_tarski :::"]"::: ) ) ($#k6_enumset1 :::"}"::: ) )))) ; registrationlet "X", "Y" be ($#v1_zfmisc_1 :::"trivial"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_zfmisc_1 :::"trivial"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: NECKLA_3:4 (Bool "for" (Set (Var "X")) "being" ($#v1_zfmisc_1 :::"trivial"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Bool "not" (Set (Var "R")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))))) ; registrationlet "X" be ($#v1_zfmisc_1 :::"trivial"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_zfmisc_1 :::"trivial"::: ) ($#v1_relat_2 :::"reflexive"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#v7_relat_2 :::"strongly_connected"::: ) ($#v8_relat_2 :::"transitive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "X" ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: NECKLA_3:5 (Bool "for" (Set (Var "X")) "being" (Num 1) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "R")) ($#r3_relat_2 :::"is_symmetric_in"::: ) (Set (Var "X"))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v1_orders_2 :::"strict"::: ) ($#v1_necklace :::"symmetric"::: ) ($#v3_necklace :::"irreflexive"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registrationlet "L" be ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v4_yellow_0 :::"full"::: ) -> ($#v4_yellow_0 :::"full"::: ) ($#v3_necklace :::"irreflexive"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; registrationlet "L" be ($#v1_necklace :::"symmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v4_yellow_0 :::"full"::: ) -> ($#v4_yellow_0 :::"full"::: ) ($#v1_necklace :::"symmetric"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; theorem :: NECKLA_3:6 (Bool "for" (Set (Var "R")) "being" ($#v1_necklace :::"symmetric"::: ) ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) )) & (Bool "(" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) )) "or" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ))) ; begin registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k1_neckla_2 :::"union_of"::: ) "(" "R" "," "S" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; cluster (Set ($#k2_neckla_2 :::"sum_of"::: ) "(" "R" "," "S" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k1_neckla_2 :::"union_of"::: ) "(" "R" "," "S" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; cluster (Set ($#k2_neckla_2 :::"sum_of"::: ) "(" "R" "," "S" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "R", "S" be ($#v8_struct_0 :::"finite"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k1_neckla_2 :::"union_of"::: ) "(" "R" "," "S" ")" ) -> ($#v8_struct_0 :::"finite"::: ) ; cluster (Set ($#k2_neckla_2 :::"sum_of"::: ) "(" "R" "," "S" ")" ) -> ($#v8_struct_0 :::"finite"::: ) ; end; registrationlet "R", "S" be ($#v1_necklace :::"symmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k1_neckla_2 :::"union_of"::: ) "(" "R" "," "S" ")" ) -> ($#v1_necklace :::"symmetric"::: ) ; cluster (Set ($#k2_neckla_2 :::"sum_of"::: ) "(" "R" "," "S" ")" ) -> ($#v1_necklace :::"symmetric"::: ) ; end; registrationlet "R", "S" be ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k1_neckla_2 :::"union_of"::: ) "(" "R" "," "S" ")" ) -> ($#v3_necklace :::"irreflexive"::: ) ; end; theorem :: NECKLA_3:7 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ($#r1_xboole_0 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set ($#k2_neckla_2 :::"sum_of"::: ) "(" (Set (Var "R")) "," (Set (Var "S")) ")" ) "is" ($#v3_necklace :::"irreflexive"::: ) )) ; theorem :: NECKLA_3:8 (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set ($#k1_neckla_2 :::"union_of"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_neckla_2 :::"union_of"::: ) "(" (Set (Var "R2")) "," (Set (Var "R1")) ")" )) & (Bool (Set ($#k2_neckla_2 :::"sum_of"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_neckla_2 :::"sum_of"::: ) "(" (Set (Var "R2")) "," (Set (Var "R1")) ")" )) ")" )) ; theorem :: NECKLA_3:9 (Bool "for" (Set (Var "G")) "being" ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k1_neckla_2 :::"union_of"::: ) "(" (Set (Var "G1")) "," (Set (Var "G2")) ")" )) "or" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k2_neckla_2 :::"sum_of"::: ) "(" (Set (Var "G1")) "," (Set (Var "G2")) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Var "G1")) "is" ($#v3_necklace :::"irreflexive"::: ) ) & (Bool (Set (Var "G2")) "is" ($#v3_necklace :::"irreflexive"::: ) ) ")" ))) ; theorem :: NECKLA_3:10 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_xboole_0 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2")))) & (Bool "(" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "G"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k1_neckla_2 :::"union_of"::: ) "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" )) "or" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "G"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k2_neckla_2 :::"sum_of"::: ) "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Var "H1")) "is" ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "G"))) & (Bool (Set (Var "H2")) "is" ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "G"))) ")" ))) ; begin theorem :: NECKLA_3:11 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set "(" ($#k4_necklace :::"Necklace"::: ) (Num 4) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_domain_1 :::"{"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 2) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 3) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 3) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k11_domain_1 :::"}"::: ) )) ; registrationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_necklace :::"ComplRelStr"::: ) "R") -> ($#v3_necklace :::"irreflexive"::: ) ; end; registrationlet "R" be ($#v1_necklace :::"symmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_necklace :::"ComplRelStr"::: ) "R") -> ($#v1_necklace :::"symmetric"::: ) ; end; theorem :: NECKLA_3:12 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r1_xboole_0 :::"misses"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" )))) ; theorem :: NECKLA_3:13 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) ($#r1_xboole_0 :::"misses"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" )))) ; theorem :: NECKLA_3:14 (Bool "for" (Set (Var "G")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" ) ($#k3_eqrel_1 :::"\/"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "G"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "G")) ")" ))))) ; theorem :: NECKLA_3:15 (Bool "for" (Set (Var "G")) "being" ($#v1_orders_2 :::"strict"::: ) ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "G")) "is" ($#v7_struct_0 :::"trivial"::: ) )) "holds" (Bool (Set ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Var "G")))) ; theorem :: NECKLA_3:16 (Bool "for" (Set (Var "G")) "being" ($#v1_orders_2 :::"strict"::: ) ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k3_necklace :::"ComplRelStr"::: ) (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "G")))) ; theorem :: NECKLA_3:17 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G1"))) ($#r1_xboole_0 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G2"))))) "holds" (Bool (Set ($#k3_necklace :::"ComplRelStr"::: ) (Set "(" ($#k1_neckla_2 :::"union_of"::: ) "(" (Set (Var "G1")) "," (Set (Var "G2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_neckla_2 :::"sum_of"::: ) "(" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "G1")) ")" ) "," (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "G2")) ")" ) ")" ))) ; theorem :: NECKLA_3:18 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G1"))) ($#r1_xboole_0 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G2"))))) "holds" (Bool (Set ($#k3_necklace :::"ComplRelStr"::: ) (Set "(" ($#k2_neckla_2 :::"sum_of"::: ) "(" (Set (Var "G1")) "," (Set (Var "G2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_neckla_2 :::"union_of"::: ) "(" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "G1")) ")" ) "," (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "G2")) ")" ) ")" ))) ; theorem :: NECKLA_3:19 (Bool "for" (Set (Var "G")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "H")) "being" ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "G")) "holds" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "G")) ")" )) ($#k2_wellord1 :::"|_2"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "H")) ")" )))))) ; theorem :: NECKLA_3:20 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "G")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9")))) "holds" (Bool (Set ($#k3_necklace :::"ComplRelStr"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set "(" (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "G")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set "(" (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "G")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x9")) ($#k6_domain_1 :::"}"::: ) ) ")" )))))) ; begin registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) ($#v1_orders_2 :::"strict"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_neckla_2 :::"N-free"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; theorem :: NECKLA_3:21 (Bool "for" (Set (Var "R")) "being" ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R")) "," (Set (Var "S")) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S")))) ")" ))) "iff" (Bool (Set (Var "S")) ($#r1_necklace :::"embeds"::: ) (Set (Var "R"))) ")" ))) ; theorem :: NECKLA_3:22 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Var "G")) ($#r2_necklace :::"embeds"::: ) (Set (Var "H"))))) ; theorem :: NECKLA_3:23 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v1_neckla_2 :::"N-free"::: ) )) "holds" (Bool (Set (Var "H")) "is" ($#v1_neckla_2 :::"N-free"::: ) ))) ; theorem :: NECKLA_3:24 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r2_necklace :::"embeds"::: ) (Set ($#k4_necklace :::"Necklace"::: ) (Num 4))) "iff" (Bool (Set ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "G"))) ($#r2_necklace :::"embeds"::: ) (Set ($#k4_necklace :::"Necklace"::: ) (Num 4))) ")" )) ; theorem :: NECKLA_3:25 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_neckla_2 :::"N-free"::: ) ) "iff" (Bool (Set ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "G"))) "is" ($#v1_neckla_2 :::"N-free"::: ) ) ")" )) ; begin definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; mode path of "R" is ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R"); end; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "R" is :::"path-connected"::: means :: NECKLA_3:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Bool "not" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R") ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "x")) "," (Set (Var "y"))))) "holds" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R") ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "y")) "," (Set (Var "x")))); end; :: deftheorem defines :::"path-connected"::: NECKLA_3:def 1 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_neckla_3 :::"path-connected"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Bool "not" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "x")) "," (Set (Var "y"))))) "holds" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "y")) "," (Set (Var "x")))) ")" )); registration cluster ($#v2_struct_0 :::"empty"::: ) -> ($#v1_neckla_3 :::"path-connected"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_neckla_3 :::"path-connected"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; theorem :: NECKLA_3:26 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v1_neckla_3 :::"path-connected"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v16_waybel_0 :::"connected"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; theorem :: NECKLA_3:27 (Bool "for" (Set (Var "R")) "being" ($#v1_necklace :::"symmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "y")) "," (Set (Var "x"))))) ; definitionlet "R" be ($#v1_necklace :::"symmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; redefine attr "R" is :::"path-connected"::: means :: NECKLA_3:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R") ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "x")) "," (Set (Var "y")))); end; :: deftheorem defines :::"path-connected"::: NECKLA_3:def 2 : (Bool "for" (Set (Var "R")) "being" ($#v1_necklace :::"symmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_neckla_3 :::"path-connected"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "x")) "," (Set (Var "y")))) ")" )); definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); func :::"component"::: "x" -> ($#m1_subset_1 :::"Subset":::) "of" "R" equals :: NECKLA_3:def 3 (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_msualg_5 :::"EqCl"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R") ")" ) "," "x" ")" ); end; :: deftheorem defines :::"component"::: NECKLA_3:def 3 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k1_neckla_3 :::"component"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_msualg_5 :::"EqCl"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ")" ) "," (Set (Var "x")) ")" )))); registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); cluster (Set ($#k1_neckla_3 :::"component"::: ) "x") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: NECKLA_3:28 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_neckla_3 :::"component"::: ) (Set (Var "x"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_msualg_5 :::"EqCl"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))))))) ; theorem :: NECKLA_3:29 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_neckla_3 :::"component"::: ) (Set (Var "x")))) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_msualg_5 :::"EqCl"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))))) ")" )) ")" )))) ; theorem :: NECKLA_3:30 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_necklace :::"symmetric"::: ) ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "R")) "is" ($#v1_neckla_3 :::"path-connected"::: ) ))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_necklace :::"symmetric"::: ) ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G1"))) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G2")))) & (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k1_neckla_2 :::"union_of"::: ) "(" (Set (Var "G1")) "," (Set (Var "G2")) ")" )) ")" ))) ; theorem :: NECKLA_3:31 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_necklace :::"symmetric"::: ) ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Bool "not" (Set ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R"))) "is" ($#v1_neckla_3 :::"path-connected"::: ) ))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v1_necklace :::"symmetric"::: ) ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G1"))) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G2")))) & (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k2_neckla_2 :::"sum_of"::: ) "(" (Set (Var "G1")) "," (Set (Var "G2")) ")" )) ")" ))) ; theorem :: NECKLA_3:32 (Bool "for" (Set (Var "G")) "being" ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set ($#k4_neckla_2 :::"fin_RelStr_sp"::: ) ))) "holds" (Bool (Set ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_neckla_2 :::"fin_RelStr_sp"::: ) ))) ; theorem :: NECKLA_3:33 (Bool "for" (Set (Var "R")) "being" ($#v1_necklace :::"symmetric"::: ) ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ($#r2_hidden :::"in"::: ) (Set ($#k13_classes2 :::"FinSETS"::: ) ))) "holds" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) "#)" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_neckla_2 :::"fin_RelStr_sp"::: ) ))) ; theorem :: NECKLA_3:34 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r2_hidden :::"in"::: ) (Set ($#k4_neckla_2 :::"fin_RelStr_sp"::: ) ))) "holds" (Bool (Set (Var "R")) "is" ($#v1_necklace :::"symmetric"::: ) )) ; theorem :: NECKLA_3:35 (Bool "for" (Set (Var "G")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H2")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k1_neckla_2 :::"union_of"::: ) "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" )) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))) "holds" (Bool "not" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "G"))))))))) ; theorem :: NECKLA_3:36 (Bool "for" (Set (Var "G")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H2")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k2_neckla_2 :::"sum_of"::: ) "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" ))) "holds" (Bool "not" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "G")) ")" )))))))) ; theorem :: NECKLA_3:37 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_necklace :::"symmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R1"))) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R2")))) & (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set "(" (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "G")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_neckla_2 :::"union_of"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" )) & (Bool (Set (Var "G")) "is" ($#v1_neckla_3 :::"path-connected"::: ) )) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R1")) "st" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "x")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "G")))))))) ; theorem :: NECKLA_3:38 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_necklace :::"symmetric"::: ) ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k9_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k9_domain_1 :::"}"::: ) )) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "G")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "G")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "G")))) & (Bool (Bool "not" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "G"))))) & (Bool (Bool "not" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "G"))))) & (Bool (Bool "not" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "G")))))) "holds" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "Z"))) ($#r1_necklace :::"embeds"::: ) (Set ($#k4_necklace :::"Necklace"::: ) (Num 4)))))) ; theorem :: NECKLA_3:39 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_necklace :::"symmetric"::: ) ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R1"))) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R2")))) & (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set "(" (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "G")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_neckla_2 :::"union_of"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" )) & (Bool (Bool "not" (Set (Var "G")) "is" ($#v7_struct_0 :::"trivial"::: ) )) & (Bool (Set (Var "G")) "is" ($#v1_neckla_3 :::"path-connected"::: ) ) & (Bool (Set ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "G"))) "is" ($#v1_neckla_3 :::"path-connected"::: ) )) "holds" (Bool (Set (Var "G")) ($#r2_necklace :::"embeds"::: ) (Set ($#k4_necklace :::"Necklace"::: ) (Num 4)))))) ; theorem :: NECKLA_3:40 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v1_orders_2 :::"strict"::: ) ($#v1_necklace :::"symmetric"::: ) ($#v3_necklace :::"irreflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "G")) "is" ($#v1_neckla_2 :::"N-free"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set ($#k13_classes2 :::"FinSETS"::: ) ))) "holds" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "G"))) "#)" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_neckla_2 :::"fin_RelStr_sp"::: ) ))) ;