:: STRUCT_0  semantic presentation begin  definitionattr "c1" is  :::"strict"::: ; struct  :::"1-sorted":::  -> ; aggr :::"1-sorted":::(# :::"carrier"::: #) ->    ($#l1_struct_0 :::"1-sorted"::: )  ; sel  :::"carrier"::: "c1" ->    ($#m1_hidden :::"set"::: )  ; end; definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; attr "S" is  :::"empty":::  means :: STRUCT_0:def 1 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "is"   ($#v1_xboole_0 :::"empty"::: )  ); end; 




:: deftheorem    defines :::"empty"::: STRUCT_0:def 1 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_struct_0 :::"1-sorted"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v2_struct_0 :::"empty"::: )  ) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )  ")" )); 
 registration
cluster   ($#v1_struct_0 :::"strict"::: )     ($#v2_struct_0 :::"empty"::: )    for    ($#l1_struct_0 :::"1-sorted"::: )  ; 
end; registration
cluster   ($#v1_struct_0 :::"strict"::: )    ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   for    ($#l1_struct_0 :::"1-sorted"::: )  ; 
end; registrationlet "S" be   ($#v2_struct_0 :::"empty"::: )     ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; mode Element of "S" is    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"); mode Subset of "S" is   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"); mode Subset-Family of "S" is   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"); end; definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "X" be    ($#m1_hidden :::"set"::: )  ; mode Function of "S" "," "X" is   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," "X"; mode Function of "X" "," "S" is   ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"); end; definitionlet "S", "T" be    ($#l1_struct_0 :::"1-sorted"::: )  ; mode Function of "S" "," "T" is   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T"); end; definitionlet "T" be    ($#l1_struct_0 :::"1-sorted"::: )  ; func  :::"{}"::: "T" ->   ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: STRUCT_0:def 2 (Set   ($#k1_xboole_0 :::"{}"::: )  ); func  :::"[#]"::: "T" ->   ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: STRUCT_0:def 3 (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T"); end; 










:: deftheorem    defines :::"{}"::: STRUCT_0:def 2 :  (Bool  "for" (Set (Var "T")) "being"    ($#l1_struct_0 :::"1-sorted"::: )   "holds"  (Bool (Set   ($#k1_struct_0 :::"{}"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))); 
 
:: deftheorem    defines :::"[#]"::: STRUCT_0:def 3 :  (Bool  "for" (Set (Var "T")) "being"    ($#l1_struct_0 :::"1-sorted"::: )   "holds"  (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))))); 
 registrationlet "T" be    ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster (Set   ($#k1_struct_0 :::"{}"::: )  "T") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "T" be   ($#v2_struct_0 :::"empty"::: )     ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster (Set   ($#k2_struct_0 :::"[#]"::: )  "T") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster (Set   ($#k2_struct_0 :::"[#]"::: )  "T") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")); 
end; definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; mode FinSequence of "S" is    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"); end; definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; mode ManySortedSet of "S" is   ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"); end; definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; func  :::"id"::: "S" ->   ($#m1_subset_1 :::"Function":::) "of" "S" "," "S" equals :: STRUCT_0:def 4 (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")); end; 





:: deftheorem    defines :::"id"::: STRUCT_0:def 4 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_struct_0 :::"1-sorted"::: )   "holds"  (Bool (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))))); 
 definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; mode sequence of "S" is   ($#m1_subset_1 :::"sequence":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"); end; definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "X" be    ($#m1_hidden :::"set"::: )  ; mode PartFunc of "S" "," "X" is   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," "X"; mode PartFunc of "X" "," "S" is   ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"); end; definitionlet "S", "T" be    ($#l1_struct_0 :::"1-sorted"::: )  ; mode PartFunc of "S" "," "T" is   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T"); end; definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "x" be    ($#m1_hidden :::"set"::: )  ; pred "x" :::"in"::: "S" means :: STRUCT_0:def 5 (Bool "x"  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")); end; 





:: deftheorem    defines :::"in"::: STRUCT_0:def 5 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_struct_0 :::"in"::: )  (Set (Var "S"))) "iff" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))  ")" ))); 
 definitionattr "c1" is  :::"strict"::: ; struct  :::"ZeroStr":::  ->    ($#l1_struct_0 :::"1-sorted"::: )  ; aggr :::"ZeroStr":::(# :::"carrier":::, :::"ZeroF"::: #) ->    ($#l2_struct_0 :::"ZeroStr"::: )  ; sel  :::"ZeroF"::: "c1" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1"); end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_struct_0 :::"strict"::: )    for    ($#l2_struct_0 :::"ZeroStr"::: )  ; 
end; definitionattr "c1" is  :::"strict"::: ; struct  :::"OneStr":::  ->    ($#l1_struct_0 :::"1-sorted"::: )  ; aggr :::"OneStr":::(# :::"carrier":::, :::"OneF"::: #) ->    ($#l3_struct_0 :::"OneStr"::: )  ; sel  :::"OneF"::: "c1" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1"); end; definitionattr "c1" is  :::"strict"::: ; struct  :::"ZeroOneStr":::  ->    ($#l2_struct_0 :::"ZeroStr"::: )   ","    ($#l3_struct_0 :::"OneStr"::: )  ; aggr :::"ZeroOneStr":::(# :::"carrier":::, :::"ZeroF":::, :::"OneF"::: #) ->    ($#l4_struct_0 :::"ZeroOneStr"::: )  ; end; definitionlet "S" be    ($#l2_struct_0 :::"ZeroStr"::: )  ; func  :::"0."::: "S" ->   ($#m1_subset_1 :::"Element":::) "of" "S" equals :: STRUCT_0:def 6 (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" "S"); end; 





:: deftheorem    defines :::"0."::: STRUCT_0:def 6 :  (Bool  "for" (Set (Var "S")) "being"    ($#l2_struct_0 :::"ZeroStr"::: )   "holds"  (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" (Set (Var "S"))))); 
 definitionlet "S" be    ($#l3_struct_0 :::"OneStr"::: )  ; func  :::"1."::: "S" ->   ($#m1_subset_1 :::"Element":::) "of" "S" equals :: STRUCT_0:def 7 (Set  "the"  ($#u3_struct_0 :::"OneF"::: )  "of" "S"); end; 





:: deftheorem    defines :::"1."::: STRUCT_0:def 7 :  (Bool  "for" (Set (Var "S")) "being"    ($#l3_struct_0 :::"OneStr"::: )   "holds"  (Bool (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u3_struct_0 :::"OneF"::: )  "of" (Set (Var "S"))))); 
 definitionlet "S" be    ($#l4_struct_0 :::"ZeroOneStr"::: )  ; attr "S" is  :::"degenerated":::  means :: STRUCT_0:def 8 (Bool (Set   ($#k4_struct_0 :::"0."::: )  "S")  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  "S")); end; 




:: deftheorem    defines :::"degenerated"::: STRUCT_0:def 8 :  (Bool  "for" (Set (Var "S")) "being"    ($#l4_struct_0 :::"ZeroOneStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v6_struct_0 :::"degenerated"::: )  ) "iff" (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "S"))))  ")" )); 
 definitionlet "IT" be    ($#l1_struct_0 :::"1-sorted"::: )  ; attr "IT" is  :::"trivial":::  means :: STRUCT_0:def 9 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "IT") "is"   ($#v1_zfmisc_1 :::"trivial"::: )  ); end; 




:: deftheorem    defines :::"trivial"::: STRUCT_0:def 9 :  (Bool  "for" (Set (Var "IT")) "being"    ($#l1_struct_0 :::"1-sorted"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v7_struct_0 :::"trivial"::: )  ) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "IT"))) "is"   ($#v1_zfmisc_1 :::"trivial"::: )  )  ")" )); 
 registration
cluster   ($#v2_struct_0 :::"empty"::: )    ->   ($#v7_struct_0 :::"trivial"::: )    for    ($#l1_struct_0 :::"1-sorted"::: )  ; 

cluster  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   for    ($#l1_struct_0 :::"1-sorted"::: )  ; 
end; definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; redefine attr "S" is  :::"trivial":::  means :: STRUCT_0:def 10 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "S" "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))); end; 




:: deftheorem    defines :::"trivial"::: STRUCT_0:def 10 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_struct_0 :::"1-sorted"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v7_struct_0 :::"trivial"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))  ")" )); 
 registration
cluster  ($#~v6_struct_0  "non"   ($#v6_struct_0 :::"degenerated"::: )   )   ->  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   for    ($#l4_struct_0 :::"ZeroOneStr"::: )  ; 
end; registration
cluster   ($#v1_struct_0 :::"strict"::: )    ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_struct_0 :::"trivial"::: )    for    ($#l1_struct_0 :::"1-sorted"::: )  ; 

cluster   ($#v1_struct_0 :::"strict"::: )    ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   for    ($#l1_struct_0 :::"1-sorted"::: )  ; 
end; registrationlet "S" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") ->  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )  ; 
end; registrationlet "S" be   ($#v7_struct_0 :::"trivial"::: )     ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") ->   ($#v1_zfmisc_1 :::"trivial"::: )   ; 
end; begin  definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; attr "S" is  :::"finite":::  means :: STRUCT_0:def 11 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "is"   ($#v1_finset_1 :::"finite"::: )  ); end; 




:: deftheorem    defines :::"finite"::: STRUCT_0:def 11 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_struct_0 :::"1-sorted"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v8_struct_0 :::"finite"::: )  ) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "is"   ($#v1_finset_1 :::"finite"::: )  )  ")" )); 
 registration
cluster   ($#v1_struct_0 :::"strict"::: )    ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"finite"::: )    for    ($#l1_struct_0 :::"1-sorted"::: )  ; 
end; registrationlet "S" be   ($#v8_struct_0 :::"finite"::: )     ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; registration
cluster   ($#v2_struct_0 :::"empty"::: )    ->   ($#v2_struct_0 :::"empty"::: )     ($#v8_struct_0 :::"finite"::: )    for    ($#l1_struct_0 :::"1-sorted"::: )  ; 
end; notationlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; antonym  :::"infinite"::: "S" for  :::"finite"::: ; end; registration
cluster   ($#v1_struct_0 :::"strict"::: )     ($#v8_struct_0 :::"infinite"::: )    for    ($#l1_struct_0 :::"1-sorted"::: )  ; 
end; registrationlet "S" be   ($#v8_struct_0 :::"infinite"::: )     ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") ->   ($#v1_finset_1 :::"infinite"::: )   ; 
end; registration
cluster   ($#v8_struct_0 :::"infinite"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"infinite"::: )    for    ($#l1_struct_0 :::"1-sorted"::: )  ; 
end; registration
cluster   ($#v7_struct_0 :::"trivial"::: )    ->   ($#v8_struct_0 :::"finite"::: )    for    ($#l1_struct_0 :::"1-sorted"::: )  ; 
end; registration
cluster   ($#v8_struct_0 :::"infinite"::: )    ->  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   for    ($#l1_struct_0 :::"1-sorted"::: )  ; 
end; definitionlet "S" be    ($#l2_struct_0 :::"ZeroStr"::: )  ; let "x" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); attr "x" is  :::"zero":::  means :: STRUCT_0:def 12 (Bool "x"  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "S")); end; 





:: deftheorem    defines :::"zero"::: STRUCT_0:def 12 :  (Bool  "for" (Set (Var "S")) "being"    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v9_struct_0 :::"zero"::: )  ) "iff" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "S"))))  ")" ))); 
 registrationlet "S" be    ($#l2_struct_0 :::"ZeroStr"::: )  ; 
cluster (Set   ($#k4_struct_0 :::"0."::: )  "S") ->   ($#v9_struct_0 :::"zero"::: )   ; 
end; registration
cluster   ($#v5_struct_0 :::"strict"::: )    ($#~v6_struct_0  "non"   ($#v6_struct_0 :::"degenerated"::: )   )   for    ($#l4_struct_0 :::"ZeroOneStr"::: )  ; 
end; registrationlet "S" be  ($#~v6_struct_0  "non"   ($#v6_struct_0 :::"degenerated"::: )   )    ($#l4_struct_0 :::"ZeroOneStr"::: )  ; 
cluster (Set   ($#k5_struct_0 :::"1."::: )  "S") ->  ($#~v9_struct_0  "non"   ($#v9_struct_0 :::"zero"::: )   )  ; 
end; definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; mode Cover of "S" is    ($#m1_setfam_1 :::"Cover"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"); end; registrationlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster (Set   ($#k2_struct_0 :::"[#]"::: )  "S") ->  ($#~v1_subset_1  "non"   ($#v1_subset_1 :::"proper"::: )   )  ; 
end; begin  definitionattr "c1" is  :::"strict"::: ; struct  :::"2-sorted":::  ->    ($#l1_struct_0 :::"1-sorted"::: )  ; aggr :::"2-sorted":::(# :::"carrier":::, :::"carrier'"::: #) ->    ($#l5_struct_0 :::"2-sorted"::: )  ; sel  :::"carrier'"::: "c1" ->    ($#m1_hidden :::"set"::: )  ; end; definitionlet "S" be    ($#l5_struct_0 :::"2-sorted"::: )  ; attr "S" is  :::"void":::  means :: STRUCT_0:def 13 (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S") "is"   ($#v1_xboole_0 :::"empty"::: )  ); end; 




:: deftheorem    defines :::"void"::: STRUCT_0:def 13 :  (Bool  "for" (Set (Var "S")) "being"    ($#l5_struct_0 :::"2-sorted"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v11_struct_0 :::"void"::: )  ) "iff" (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )  ")" )); 
 registration
cluster   ($#v2_struct_0 :::"empty"::: )     ($#v10_struct_0 :::"strict"::: )     ($#v11_struct_0 :::"void"::: )    for    ($#l5_struct_0 :::"2-sorted"::: )  ; 
end; registrationlet "S" be   ($#v11_struct_0 :::"void"::: )     ($#l5_struct_0 :::"2-sorted"::: )  ; 
cluster (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_struct_0 :::"strict"::: )    ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   for    ($#l5_struct_0 :::"2-sorted"::: )  ; 
end; registrationlet "S" be  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l5_struct_0 :::"2-sorted"::: )  ; 
cluster (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionlet "X" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )  ; let "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "Y")); func "X" :::"-->"::: "y" ->   ($#m1_subset_1 :::"Function":::) "of" "X" "," "Y" equals :: STRUCT_0:def 14 (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X")  ($#k8_funcop_1 :::"-->"::: )  "y"); end; 







:: deftheorem    defines :::"-->"::: STRUCT_0:def 14 :  (Bool  "for" (Set (Var "X")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Y")) "holds"  (Bool (Set (Set (Var "X"))  ($#k6_struct_0 :::"-->"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  ($#k8_funcop_1 :::"-->"::: )  (Set (Var "y"))))))); 
 registrationlet "S" be    ($#l2_struct_0 :::"ZeroStr"::: )  ; 
cluster   ($#v9_struct_0 :::"zero"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"); 
end; registration
cluster   ($#v3_struct_0 :::"strict"::: )    ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   for    ($#l2_struct_0 :::"ZeroStr"::: )  ; 
end; registrationlet "S" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )  ; 
cluster  ($#~v9_struct_0  "non"   ($#v9_struct_0 :::"zero"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"); 
end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "S" be    ($#l2_struct_0 :::"ZeroStr"::: )  ; let "R" be   ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "S"))); attr "R" is  :::"non-zero":::  means :: STRUCT_0:def 15 (Bool (Bool  "not" (Set   ($#k4_struct_0 :::"0."::: )  "S")  ($#r2_hidden :::"in"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  "R"))); end; 






:: deftheorem    defines :::"non-zero"::: STRUCT_0:def 15 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "S")) "being"    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v12_struct_0 :::"non-zero"::: )  ) "iff" (Bool (Bool  "not" (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "S")))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "R")))))  ")" )))); 
 definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; func  :::"card"::: "S" ->   ($#m1_hidden :::"Cardinal":::) equals :: STRUCT_0:def 16 (Set   ($#k1_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")); end; 





:: deftheorem    defines :::"card"::: STRUCT_0:def 16 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_struct_0 :::"1-sorted"::: )   "holds"  (Bool (Set   ($#k7_struct_0 :::"card"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))))); 
 definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; mode UnOp of "S" is   ($#m1_subset_1 :::"UnOp":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"); mode BinOp of "S" is   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"); end; definitionlet "S" be    ($#l2_struct_0 :::"ZeroStr"::: )  ; func  :::"NonZero"::: "S" ->   ($#m1_subset_1 :::"Subset":::) "of" "S" equals :: STRUCT_0:def 17 (Set (Set  "("  ($#k2_struct_0 :::"[#]"::: )  "S" ")" )  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  "S" ")" ) ($#k1_tarski :::"}"::: ) )); end; 





:: deftheorem    defines :::"NonZero"::: STRUCT_0:def 17 :  (Bool  "for" (Set (Var "S")) "being"    ($#l2_struct_0 :::"ZeroStr"::: )   "holds"  (Bool (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "S")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "S")) ")" ) ($#k1_tarski :::"}"::: ) )))); 
 
theorem :: STRUCT_0:1 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "u"))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "S")))) "iff" (Bool (Bool  "not" (Set (Var "u")) "is"   ($#v9_struct_0 :::"zero"::: )  ))  ")" ))) ; 
 definitionlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )  ; redefine attr "V" is  :::"trivial":::  means :: STRUCT_0:def 18 (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" "V" "holds"  (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "V"))); end; 




:: deftheorem    defines :::"trivial"::: STRUCT_0:def 18 :  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "V")) "is"   ($#v7_struct_0 :::"trivial"::: )  ) "iff" (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))))  ")" )); 
 registrationlet "V" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )  ; 
cluster (Set   ($#k8_struct_0 :::"NonZero"::: )  "V") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_struct_0 :::"trivial"::: )    for    ($#l2_struct_0 :::"ZeroStr"::: )  ; 
end; registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_struct_0 :::"trivial"::: )     ($#l2_struct_0 :::"ZeroStr"::: )  ; 
cluster (Set   ($#k8_struct_0 :::"NonZero"::: )  "S") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_zfmisc_1 :::"trivial"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")); 
end; 
theorem :: STRUCT_0:2 (Bool  "for" (Set (Var "F")) "being"  ($#~v6_struct_0  "non"   ($#v6_struct_0 :::"degenerated"::: )   )    ($#l4_struct_0 :::"ZeroOneStr"::: )   "holds"  (Bool (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "F")))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "F"))))) ; 
 registrationlet "S" be   ($#v8_struct_0 :::"finite"::: )     ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster (Set   ($#k7_struct_0 :::"card"::: )  "S") ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"finite"::: )     ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster (Set   ($#k7_struct_0 :::"card"::: )  "S") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   for  ($#m1_hidden :::"Nat":::); 
end; registrationlet "T" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T")); 
end; 
theorem :: STRUCT_0:3 (Bool  "for" (Set (Var "S")) "being"    ($#l2_struct_0 :::"ZeroStr"::: )    "holds" (Bool (Bool  "not" (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "S")))  ($#r2_hidden :::"in"::: )  (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "S")))))) ; 
 
theorem :: STRUCT_0:4 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )   "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "S")) ")" ) ($#k6_domain_1 :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k8_struct_0 :::"NonZero"::: )  (Set (Var "S")) ")" )))) ; 
 definitionlet "C" be    ($#m1_hidden :::"set"::: )  ; let "X" be    ($#l1_struct_0 :::"1-sorted"::: )  ; attr "X" is "C" :::"-element":::  means :: STRUCT_0:def 19 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "is" "C"  ($#v3_card_1 :::"-element"::: )  ); end; 





:: deftheorem    defines :::"-element"::: STRUCT_0:def 19 :  (Bool  "for" (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"    ($#l1_struct_0 :::"1-sorted"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is" (Set (Var "C"))  ($#v13_struct_0 :::"-element"::: )  ) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "is" (Set (Var "C"))  ($#v3_card_1 :::"-element"::: )  )  ")" ))); 
 registrationlet "C" be   ($#m1_hidden :::"Cardinal":::); 
cluster "C"  ($#v13_struct_0 :::"-element"::: )    for    ($#l1_struct_0 :::"1-sorted"::: )  ; 
end; registrationlet "C" be   ($#m1_hidden :::"Cardinal":::); let "X" be (Set (Const "C"))  ($#v13_struct_0 :::"-element"::: )     ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") -> "C"  ($#v3_card_1 :::"-element"::: )   ; 
end; registration
cluster   ($#v2_struct_0 :::"empty"::: )    -> (Set   ($#k1_xboole_0 :::"0"::: )  )  ($#v13_struct_0 :::"-element"::: )    for    ($#l1_struct_0 :::"1-sorted"::: )  ; 

cluster (Set   ($#k1_xboole_0 :::"0"::: )  )  ($#v13_struct_0 :::"-element"::: )    ->   ($#v2_struct_0 :::"empty"::: )    for    ($#l1_struct_0 :::"1-sorted"::: )  ; 

cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_struct_0 :::"trivial"::: )    -> (Num 1)  ($#v13_struct_0 :::"-element"::: )    for    ($#l1_struct_0 :::"1-sorted"::: )  ; 

cluster (Num 1)  ($#v13_struct_0 :::"-element"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_struct_0 :::"trivial"::: )    for    ($#l1_struct_0 :::"1-sorted"::: )  ; 
end; definitionlet "S" be    ($#l5_struct_0 :::"2-sorted"::: )  ; attr "S" is  :::"feasible":::  means :: STRUCT_0:def 20  "("  (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "is"   ($#v1_xboole_0 :::"empty"::: )  )) "implies" (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S") "is"   ($#v1_xboole_0 :::"empty"::: )  )  ")" ; end; 




:: deftheorem    defines :::"feasible"::: STRUCT_0:def 20 :  (Bool  "for" (Set (Var "S")) "being"    ($#l5_struct_0 :::"2-sorted"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v14_struct_0 :::"feasible"::: )  ) "iff"  "("  (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )) "implies" (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )  ")"   ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ->   ($#v14_struct_0 :::"feasible"::: )    for    ($#l5_struct_0 :::"2-sorted"::: )  ; 

cluster   ($#v11_struct_0 :::"void"::: )    ->   ($#v14_struct_0 :::"feasible"::: )    for    ($#l5_struct_0 :::"2-sorted"::: )  ; 

cluster   ($#v2_struct_0 :::"empty"::: )     ($#v14_struct_0 :::"feasible"::: )    ->   ($#v11_struct_0 :::"void"::: )    for    ($#l5_struct_0 :::"2-sorted"::: )  ; 

cluster  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v14_struct_0 :::"feasible"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   for    ($#l5_struct_0 :::"2-sorted"::: )  ; 
end; definitionlet "S" be    ($#l5_struct_0 :::"2-sorted"::: )  ; attr "S" is  :::"trivial'":::  means :: STRUCT_0:def 21 (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S") "is"   ($#v1_zfmisc_1 :::"trivial"::: )  ); end; 




:: deftheorem    defines :::"trivial'"::: STRUCT_0:def 21 :  (Bool  "for" (Set (Var "S")) "being"    ($#l5_struct_0 :::"2-sorted"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v15_struct_0 :::"trivial'"::: )  ) "iff" (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))) "is"   ($#v1_zfmisc_1 :::"trivial"::: )  )  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_struct_0 :::"trivial"::: )     ($#v10_struct_0 :::"strict"::: )    ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v15_struct_0 :::"trivial'"::: )    for    ($#l5_struct_0 :::"2-sorted"::: )  ; 
end; registrationlet "S" be   ($#v15_struct_0 :::"trivial'"::: )     ($#l5_struct_0 :::"2-sorted"::: )  ; 
cluster (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S") ->   ($#v1_zfmisc_1 :::"trivial"::: )   ; 
end; registration
cluster  ($#~v15_struct_0  "non"   ($#v15_struct_0 :::"trivial'"::: )   )   for    ($#l5_struct_0 :::"2-sorted"::: )  ; 
end; registrationlet "S" be  ($#~v15_struct_0  "non"   ($#v15_struct_0 :::"trivial'"::: )   )    ($#l5_struct_0 :::"2-sorted"::: )  ; 
cluster (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S") ->  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )  ; 
end; registration
cluster   ($#v11_struct_0 :::"void"::: )    ->   ($#v15_struct_0 :::"trivial'"::: )    for    ($#l5_struct_0 :::"2-sorted"::: )  ; 

cluster  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   for    ($#l1_struct_0 :::"1-sorted"::: )  ; 
end;