:: NECKLACE  semantic presentation begin  















theorem :: NECKLACE:1 (Bool (Num 4)  ($#r1_hidden :::"="::: )  (Set  ($#k2_enumset1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) ($#k2_enumset1 :::"}"::: ) )) ; 
 
theorem :: NECKLACE:2 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) "," (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k1_enumset1 :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k7_enumset1 :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y3")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x2")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x2")) "," (Set (Var "y3")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x3")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x3")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x3")) "," (Set (Var "y3")) ($#k4_tarski :::"]"::: ) ) ($#k7_enumset1 :::"}"::: ) ))) ; 
 
theorem :: NECKLACE:3 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Nat":::)))) ; 
 
theorem :: NECKLACE:4 (Bool  "for" (Set (Var "x")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "x")))) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k11_funct_3 :::"delta"::: )  "X") ->   ($#v2_funct_1 :::"one-to-one"::: )   ; 
end; 
theorem :: NECKLACE:5 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) ; 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_zfmisc_1 :::"trivial"::: )    ->   ($#v2_funct_1 :::"one-to-one"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: NECKLACE:6 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g"))))) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "f"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g")) ")" )))) ; 
 
theorem :: NECKLACE:7 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v2_funct_1 :::"one-to-one"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "g")) ")" )  ($#k2_funct_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set (Var "g"))  ($#k2_funct_1 :::"""::: )  ")" )))) ; 
 
theorem :: NECKLACE:8 (Bool  "for" (Set (Var "A")) "," (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "a")) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set (Var "A"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "b"))))) ; 
 
theorem :: NECKLACE:9 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "b")) ")" )  ($#k2_funct_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "a"))))) ; 
 
theorem :: NECKLACE:10 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "not" (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "implies" (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Var "d")))  ")"  &  "("  (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Var "d")))) "implies" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")"  & (Bool (Bool  "not" (Set (Set  "("  "(" (Set (Var "a")) "," (Set (Var "b")) ")"   ($#k4_funct_4 :::"-->"::: )   "(" (Set (Var "c")) "," (Set (Var "d")) ")"  ")" )  ($#k2_funct_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "c")) "," (Set (Var "d")) ")"   ($#k4_funct_4 :::"-->"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))  ")" ))) ; 
 scheme  :: NECKLACE:sch 1 Convers{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->   ($#m1_hidden :::"Relation":::), F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool (Set (Set F2 "("  ")" )  ($#k2_relat_1 :::"~"::: )  )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k4_tarski :::"["::: ) (Set F3 "(" (Set (Var "x")) ")" ) "," (Set F4 "(" (Set (Var "x")) ")" ) ($#k4_tarski :::"]"::: ) ) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) : (Bool P1[(Set (Var "x"))])  "}"  )
 provided
(Bool (Set F2 "("  ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k4_tarski :::"["::: ) (Set F4 "(" (Set (Var "x")) ")" ) "," (Set F3 "(" (Set (Var "x")) ")" ) ($#k4_tarski :::"]"::: ) ) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) : (Bool P1[(Set (Var "x"))])  "}"  )
 proof 


end; 
theorem :: NECKLACE:11 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "n")))) ; 
 begin  definitionlet "R", "S" be    ($#l1_orders_2 :::"RelStr"::: )  ; pred "S" :::"embeds"::: "R" means :: NECKLACE:def 1 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" "R" "," "S" "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "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" "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" "S"))  ")" )  ")" )  ")" )); end; 





:: deftheorem    defines :::"embeds"::: NECKLACE:def 1 :  (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S"))  ($#r1_necklace :::"embeds"::: )  (Set (Var "R"))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R")) "," (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (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"))))  ")" )  ")" )  ")" ))  ")" )); 
 definitionlet "R", "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; :: original: :::"embeds"::: redefine pred "S" :::"embeds"::: "R"; reflexivity  
(Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool ((Set (Var "b1")) "," (Set (Var "b1")))))
 ; end; 
theorem :: NECKLACE:12 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "R"))  ($#r2_necklace :::"embeds"::: )  (Set (Var "S"))) & (Bool (Set (Var "S"))  ($#r2_necklace :::"embeds"::: )  (Set (Var "T")))) "holds"  (Bool (Set (Var "R"))  ($#r2_necklace :::"embeds"::: )  (Set (Var "T")))) ; 
 definitionlet "R", "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; pred "R" :::"is_equimorphic_to"::: "S" means :: NECKLACE:def 2 (Bool  "("  (Bool "R"  ($#r2_necklace :::"embeds"::: )  "S") & (Bool "S"  ($#r2_necklace :::"embeds"::: )  "R")  ")" ); reflexivity  
(Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r2_necklace :::"embeds"::: )  (Set (Var "R"))) & (Bool (Set (Var "R"))  ($#r2_necklace :::"embeds"::: )  (Set (Var "R")))  ")" ))
 ; symmetry  
(Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "R"))  ($#r2_necklace :::"embeds"::: )  (Set (Var "S"))) & (Bool (Set (Var "S"))  ($#r2_necklace :::"embeds"::: )  (Set (Var "R")))) "holds"  (Bool  "("  (Bool (Set (Var "S"))  ($#r2_necklace :::"embeds"::: )  (Set (Var "R"))) & (Bool (Set (Var "R"))  ($#r2_necklace :::"embeds"::: )  (Set (Var "S")))  ")" ))
 ; end; 





:: deftheorem    defines :::"is_equimorphic_to"::: NECKLACE:def 2 :  (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r3_necklace :::"is_equimorphic_to"::: )  (Set (Var "S"))) "iff" (Bool  "("  (Bool (Set (Var "R"))  ($#r2_necklace :::"embeds"::: )  (Set (Var "S"))) & (Bool (Set (Var "S"))  ($#r2_necklace :::"embeds"::: )  (Set (Var "R")))  ")" )  ")" )); 
 
theorem :: NECKLACE:13 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "R"))  ($#r3_necklace :::"is_equimorphic_to"::: )  (Set (Var "S"))) & (Bool (Set (Var "S"))  ($#r3_necklace :::"is_equimorphic_to"::: )  (Set (Var "T")))) "holds"  (Bool (Set (Var "R"))  ($#r3_necklace :::"is_equimorphic_to"::: )  (Set (Var "T")))) ; 
 notationlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; synonym  :::"parallel"::: "R" for  :::"connected"::: ; end; definitionlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; attr "R" is  :::"symmetric":::  means :: NECKLACE:def 3 (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R")  ($#r3_relat_2 :::"is_symmetric_in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R")); end; 




:: deftheorem    defines :::"symmetric"::: NECKLACE:def 3 :  (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_necklace :::"symmetric"::: )  ) "iff" (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#r3_relat_2 :::"is_symmetric_in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))))  ")" )); 
 definitionlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; attr "R" is  :::"asymmetric":::  means :: NECKLACE:def 4 (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R") "is"   ($#v5_relat_2 :::"asymmetric"::: )  ); end; 




:: deftheorem    defines :::"asymmetric"::: NECKLACE:def 4 :  (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v2_necklace :::"asymmetric"::: )  ) "iff" (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R"))) "is"   ($#v5_relat_2 :::"asymmetric"::: )  )  ")" )); 
 
theorem :: NECKLACE:14 (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_necklace :::"asymmetric"::: )  )) "holds"  (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k3_relset_1 :::"~"::: )  ))) ; 
 definitionlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; attr "R" is  :::"irreflexive":::  means :: NECKLACE:def 5 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R"))) "holds"  (Bool  "not" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R")))); end; 




:: deftheorem    defines :::"irreflexive"::: NECKLACE:def 5 :  (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v3_necklace :::"irreflexive"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))))) "holds"  (Bool  "not" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R"))))))  ")" )); 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); func "n" :::"-SuccRelStr":::  ->   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   means :: NECKLACE:def 6 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  "n") & (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" it)  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) where i "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  "n")  "}"  )  ")" ); end; 





:: deftheorem    defines :::"-SuccRelStr"::: NECKLACE:def 6 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_necklace :::"-SuccRelStr"::: )  )) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) where i "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))  "}"  )  ")" )  ")" ))); 
 
theorem :: NECKLACE:15 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "n"))  ($#k1_necklace :::"-SuccRelStr"::: )  ) "is"   ($#v2_necklace :::"asymmetric"::: )  )) ; 
 
theorem :: NECKLACE:16 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "(" (Set (Var "n"))  ($#k1_necklace :::"-SuccRelStr"::: )  ")" )))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1)))) ; 
 definitionlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; func  :::"SymRelStr"::: "R" ->   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   means :: NECKLACE:def 7 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R")) & (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R")  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R")  ($#k3_relset_1 :::"~"::: )  ")" )))  ")" ); end; 





:: deftheorem    defines :::"SymRelStr"::: NECKLACE:def 7 :  (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_necklace :::"SymRelStr"::: )  (Set (Var "R")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))) & (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k3_relset_1 :::"~"::: )  ")" )))  ")" )  ")" ))); 
 registrationlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set   ($#k2_necklace :::"SymRelStr"::: )  "R") ->   ($#v1_orders_2 :::"strict"::: )     ($#v1_necklace :::"symmetric"::: )   ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_necklace :::"symmetric"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; registrationlet "R" be   ($#v1_necklace :::"symmetric"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R") ->   ($#v3_relat_2 :::"symmetric"::: )   ; 
end; definitionlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; func  :::"ComplRelStr"::: "R" ->   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   means :: NECKLACE:def 8 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R")) & (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R")  ($#k3_subset_1 :::"`"::: )  ")" )  ($#k7_subset_1 :::"\"::: )  (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R") ")" )))  ")" ); end; 





:: deftheorem    defines :::"ComplRelStr"::: NECKLACE:def 8 :  (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_necklace :::"ComplRelStr"::: )  (Set (Var "R")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))) & (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k3_subset_1 :::"`"::: )  ")" )  ($#k7_subset_1 :::"\"::: )  (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) ")" )))  ")" )  ")" ))); 
 registrationlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set   ($#k3_necklace :::"ComplRelStr"::: )  "R") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )   ; 
end; 
theorem :: NECKLACE:17 (Bool  "for" (Set (Var "S")) "," (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "R"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "S"))))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))))) ; 
 begin  definitionlet "n" be   ($#m1_hidden :::"Nat":::); func  :::"Necklace"::: "n" ->   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   equals :: NECKLACE:def 9 (Set   ($#k2_necklace :::"SymRelStr"::: )  (Set  "(" "n"  ($#k1_necklace :::"-SuccRelStr"::: )  ")" )); end; 





:: deftheorem    defines :::"Necklace"::: NECKLACE:def 9 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k4_necklace :::"Necklace"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_necklace :::"SymRelStr"::: )  (Set  "(" (Set (Var "n"))  ($#k1_necklace :::"-SuccRelStr"::: )  ")" )))); 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k4_necklace :::"Necklace"::: )  "n") ->   ($#v1_orders_2 :::"strict"::: )     ($#v1_necklace :::"symmetric"::: )   ; 
end; 
theorem :: NECKLACE:18 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "("  ($#k4_necklace :::"Necklace"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set  "{"  (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) where i "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))  "}"    ($#k2_xboole_0 :::"\/"::: )   "{"  (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "i")) ($#k4_tarski :::"]"::: ) ) where i "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))  "}"  ))) ; 
 
theorem :: NECKLACE:19 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "("  ($#k4_necklace :::"Necklace"::: )  (Set (Var "n")) ")" ))) "iff" (Bool  "ex" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) & (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k4_tarski :::"]"::: ) )) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "i")) ($#k4_tarski :::"]"::: ) ))  ")" )  ")" ))  ")" ))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k4_necklace :::"Necklace"::: )  "n") ->   ($#v1_orders_2 :::"strict"::: )     ($#v3_necklace :::"irreflexive"::: )   ; 
end; 
theorem :: NECKLACE:20 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_necklace :::"Necklace"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) ; 
 registrationlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k4_necklace :::"Necklace"::: )  "n") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )   ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_necklace :::"Necklace"::: )  "n" ")" )) ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: NECKLACE:21 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "("  ($#k4_necklace :::"Necklace"::: )  (Set (Var "n")) ")" )))) ; 
 
theorem :: NECKLACE:22 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_necklace :::"Necklace"::: )  (Set (Var "n")) ")" )))) "holds"  (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) ; 
 
theorem :: NECKLACE:23 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set   ($#k4_necklace :::"Necklace"::: )  (Set (Var "n"))) "is"   ($#v3_orders_3 :::"connected"::: )  )) ; 
 
theorem :: NECKLACE:24 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "("  ($#k4_necklace :::"Necklace"::: )  (Set (Var "n")) ")" ))) "or" (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "j"))  ($#k1_nat_1 :::"+"::: )  (Num 1))) "or" (Bool (Set (Var "j"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))  ")" )) ; 
 
theorem :: NECKLACE:25 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool  "("  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "j"))  ($#k1_nat_1 :::"+"::: )  (Num 1))) "or" (Bool (Set (Var "j"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))  ")" ) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_necklace :::"Necklace"::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_necklace :::"Necklace"::: )  (Set (Var "n")) ")" )))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "("  ($#k4_necklace :::"Necklace"::: )  (Set (Var "n")) ")" )))) ; 
 
theorem :: NECKLACE:26 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "i")) ($#k4_tarski :::"]"::: ) ) where i "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))  "}"  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1)))) ; 
 
theorem :: NECKLACE:27 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "("  ($#k4_necklace :::"Necklace"::: )  (Set (Var "n")) ")" )))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1) ")" )))) ; 
 
theorem :: NECKLACE:28 (Bool (Set   ($#k4_necklace :::"Necklace"::: )  (Num 1)) "," (Set   ($#k3_necklace :::"ComplRelStr"::: )  (Set  "("  ($#k4_necklace :::"Necklace"::: )  (Num 1) ")" ))  ($#r5_waybel_1 :::"are_isomorphic"::: )  ) ; 
 
theorem :: NECKLACE:29 (Bool (Set   ($#k4_necklace :::"Necklace"::: )  (Num 4)) "," (Set   ($#k3_necklace :::"ComplRelStr"::: )  (Set  "("  ($#k4_necklace :::"Necklace"::: )  (Num 4) ")" ))  ($#r5_waybel_1 :::"are_isomorphic"::: )  ) ; 
 
theorem :: NECKLACE:30 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set   ($#k4_necklace :::"Necklace"::: )  (Set (Var "n"))) "," (Set   ($#k3_necklace :::"ComplRelStr"::: )  (Set  "("  ($#k4_necklace :::"Necklace"::: )  (Set (Var "n")) ")" ))  ($#r5_waybel_1 :::"are_isomorphic"::: )  ) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 4))  ")" )) ;