:: NECKLA_2  semantic presentation begin  



theorem :: NECKLA_2:1 (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))) "holds"  (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds"  (Bool (Set (Var "R"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))))) ; 
 
theorem :: NECKLA_2:2 (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "("  ($#k4_necklace :::"Necklace"::: )  (Num 4) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_enumset1 :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Num 1) "," (Num 2) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Num 2) "," (Num 1) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Num 2) "," (Num 3) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Num 3) "," (Num 2) ($#k4_tarski :::"]"::: ) ) ($#k4_enumset1 :::"}"::: ) )) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster   ->   ($#v1_finset_1 :::"finite"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_classes1 :::"Rank"::: )  "n"); 
end; 
theorem :: NECKLA_2:3 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k13_classes2 :::"FinSETS"::: )  ))) "holds"  (Bool (Set (Var "x")) "is"   ($#v1_finset_1 :::"finite"::: )  )) ; 
 registration
cluster   ->   ($#v1_finset_1 :::"finite"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k13_classes2 :::"FinSETS"::: )  ); 
end; definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; attr "G" is  :::"N-free":::  means :: NECKLA_2:def 1 (Bool (Bool  "not" "G"  ($#r1_necklace :::"embeds"::: )  (Set   ($#k4_necklace :::"Necklace"::: )  (Num 4)))); end; 




:: deftheorem    defines :::"N-free"::: NECKLA_2:def 1 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v1_neckla_2 :::"N-free"::: )  ) "iff" (Bool (Bool  "not" (Set (Var "G"))  ($#r1_necklace :::"embeds"::: )  (Set   ($#k4_necklace :::"Necklace"::: )  (Num 4))))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"finite"::: )     ($#v1_orders_2 :::"strict"::: )     ($#v1_neckla_2 :::"N-free"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; definitionlet "R", "S" be    ($#l1_orders_2 :::"RelStr"::: )  ; func  :::"union_of":::  "(" "R" "," "S" ")"  ->   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   means :: NECKLA_2:def 2 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R")  ($#k2_xboole_0 :::"\/"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"))) & (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R")  ($#k2_xboole_0 :::"\/"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "S")))  ")" ); end; 






:: deftheorem    defines :::"union_of"::: NECKLA_2:def 2 :  (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_neckla_2 :::"union_of"::: )   "(" (Set (Var "R")) "," (Set (Var "S")) ")" )) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k2_xboole_0 :::"\/"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))) & (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k2_xboole_0 :::"\/"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "S")))))  ")" )  ")" ))); 
 definitionlet "R", "S" be    ($#l1_orders_2 :::"RelStr"::: )  ; func  :::"sum_of":::  "(" "R" "," "S" ")"  ->   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   means :: NECKLA_2:def 3 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R")  ($#k2_xboole_0 :::"\/"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"))) & (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R")  ($#k2_xboole_0 :::"\/"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "S") ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") ($#k2_zfmisc_1 :::":]"::: ) ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R") ($#k2_zfmisc_1 :::":]"::: ) )))  ")" ); end; 






:: deftheorem    defines :::"sum_of"::: NECKLA_2:def 3 :  (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_neckla_2 :::"sum_of"::: )   "(" (Set (Var "R")) "," (Set (Var "S")) ")" )) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k2_xboole_0 :::"\/"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))) & (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k2_xboole_0 :::"\/"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "S"))) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" )  ")" ))); 
 definitionfunc  :::"fin_RelStr":::  ->    ($#m1_hidden :::"set"::: )   means :: NECKLA_2:def 4 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "R")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "R"))) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#r2_hidden :::"in"::: )  (Set   ($#k13_classes2 :::"FinSETS"::: )  ))  ")" ))  ")" )); end; 




:: deftheorem    defines :::"fin_RelStr"::: NECKLA_2:def 4 :  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_neckla_2 :::"fin_RelStr"::: )  )) "iff" (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) "iff" (Bool  "ex" (Set (Var "R")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "R"))) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#r2_hidden :::"in"::: )  (Set   ($#k13_classes2 :::"FinSETS"::: )  ))  ")" ))  ")" ))  ")" )); 
 registration
cluster (Set   ($#k3_neckla_2 :::"fin_RelStr"::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionfunc  :::"fin_RelStr_sp":::  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_neckla_2 :::"fin_RelStr"::: ) ) means :: NECKLA_2:def 5 (Bool  "("  (Bool  "("   "for" (Set (Var "R")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "is" (Num 1)  ($#v3_card_1 :::"-element"::: )  ) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#r2_hidden :::"in"::: )  (Set   ($#k13_classes2 :::"FinSETS"::: )  ))) "holds"  (Bool (Set (Var "R"))  ($#r2_hidden :::"in"::: )  it)  ")" ) & (Bool  "("   "for" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#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 (Set (Var "H1"))  ($#r2_hidden :::"in"::: )  it) & (Bool (Set (Var "H2"))  ($#r2_hidden :::"in"::: )  it)) "holds"  (Bool  "("  (Bool (Set   ($#k1_neckla_2 :::"union_of"::: )   "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" )  ($#r2_hidden :::"in"::: )  it) & (Bool (Set   ($#k2_neckla_2 :::"sum_of"::: )   "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" )  ($#r2_hidden :::"in"::: )  it)  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_neckla_2 :::"fin_RelStr"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "R")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "is" (Num 1)  ($#v3_card_1 :::"-element"::: )  ) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#r2_hidden :::"in"::: )  (Set   ($#k13_classes2 :::"FinSETS"::: )  ))) "holds"  (Bool (Set (Var "R"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))  ")" ) & (Bool  "("   "for" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#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 (Set (Var "H1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "H2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool  "("  (Bool (Set   ($#k1_neckla_2 :::"union_of"::: )   "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set   ($#k2_neckla_2 :::"sum_of"::: )   "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Var "M")))  ")" )  ")" )) "holds"  (Bool it  ($#r1_tarski :::"c="::: )  (Set (Var "M")))  ")" )  ")" ); end; 




:: deftheorem    defines :::"fin_RelStr_sp"::: NECKLA_2:def 5 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_neckla_2 :::"fin_RelStr"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_neckla_2 :::"fin_RelStr_sp"::: )  )) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "R")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "is" (Num 1)  ($#v3_card_1 :::"-element"::: )  ) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#r2_hidden :::"in"::: )  (Set   ($#k13_classes2 :::"FinSETS"::: )  ))) "holds"  (Bool (Set (Var "R"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1")))  ")" ) & (Bool  "("   "for" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#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 (Set (Var "H1"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) & (Bool (Set (Var "H2"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1")))) "holds"  (Bool  "("  (Bool (Set   ($#k1_neckla_2 :::"union_of"::: )   "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) & (Bool (Set   ($#k2_neckla_2 :::"sum_of"::: )   "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Var "b1")))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_neckla_2 :::"fin_RelStr"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "R")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "is" (Num 1)  ($#v3_card_1 :::"-element"::: )  ) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#r2_hidden :::"in"::: )  (Set   ($#k13_classes2 :::"FinSETS"::: )  ))) "holds"  (Bool (Set (Var "R"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))  ")" ) & (Bool  "("   "for" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#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 (Set (Var "H1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "H2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool  "("  (Bool (Set   ($#k1_neckla_2 :::"union_of"::: )   "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set   ($#k2_neckla_2 :::"sum_of"::: )   "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Var "M")))  ")" )  ")" )) "holds"  (Bool (Set (Var "b1"))  ($#r1_tarski :::"c="::: )  (Set (Var "M")))  ")" )  ")" )  ")" )); 
 registration
cluster (Set   ($#k4_neckla_2 :::"fin_RelStr_sp"::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: NECKLA_2:4 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_neckla_2 :::"fin_RelStr_sp"::: )  ))) "holds"  (Bool (Set (Var "X")) "is"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"finite"::: )     ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )  )) ; 
 
theorem :: NECKLA_2:5 (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  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#r2_hidden :::"in"::: )  (Set   ($#k13_classes2 :::"FinSETS"::: )  ))) ; 
 
theorem :: NECKLA_2:6 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_neckla_2 :::"fin_RelStr_sp"::: )  )) "or" (Bool (Set (Var "X")) "is" (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )  ) "or" (Bool  "ex" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#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 (Set (Var "H1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_neckla_2 :::"fin_RelStr_sp"::: )  )) & (Bool (Set (Var "H2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_neckla_2 :::"fin_RelStr_sp"::: )  )) & (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_neckla_2 :::"union_of"::: )   "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" )) "or" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_neckla_2 :::"sum_of"::: )   "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" ))  ")" )  ")" ))  ")" )) ; 
 
theorem :: NECKLA_2:7 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )     ($#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_neckla_2 :::"N-free"::: )  )) ;