:: ABIAN  semantic presentation begin  




















definitionlet "i" be   ($#m1_hidden :::"Integer":::); attr "i" is  :::"even":::  means :: ABIAN:def 1 (Bool (Num 2)  ($#r1_int_1 :::"divides"::: )  "i"); end; 




:: deftheorem    defines :::"even"::: ABIAN:def 1 :  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "i")) "is"   ($#v1_abian :::"even"::: )  ) "iff" (Bool (Num 2)  ($#r1_int_1 :::"divides"::: )  (Set (Var "i")))  ")" )); 
 notationlet "i" be   ($#m1_hidden :::"Integer":::); antonym  :::"odd"::: "i" for  :::"even"::: ; end; definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); redefine attr "n" is  :::"even":::  means :: ABIAN:def 2 (Bool  "ex" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool "n"  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "k"))))); end; 




:: deftheorem    defines :::"even"::: ABIAN:def 2 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "n")) "is"   ($#v1_abian :::"even"::: )  ) "iff" (Bool  "ex" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "k")))))  ")" )); 
 registration
cluster   ($#v1_xxreal_0 :::"ext-real"::: )   bbbadV1_ORDINAL1() bbbadV2_ORDINAL1() bbbadV3_ORDINAL1() bbbadV7_ORDINAL1()   ($#v1_xcmplx_0 :::"complex"::: )   bbbadV1_XREAL_0()   ($#v1_int_1 :::"integer"::: )   bbbadV1_RAT_1() bbbadV1_MEMBERED() bbbadV2_MEMBERED() bbbadV3_MEMBERED() bbbadV4_MEMBERED() bbbadV5_MEMBERED() bbbadV6_MEMBERED() bbbadV3_XXREAL_2()   ($#v1_abian :::"even"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 

cluster   ($#v1_xxreal_0 :::"ext-real"::: )   bbbadV1_ORDINAL1() bbbadV2_ORDINAL1() bbbadV3_ORDINAL1() bbbadV7_ORDINAL1()   ($#v1_xcmplx_0 :::"complex"::: )   bbbadV1_XREAL_0()   ($#v1_int_1 :::"integer"::: )   bbbadV1_RAT_1() bbbadV1_MEMBERED() bbbadV2_MEMBERED() bbbadV3_MEMBERED() bbbadV4_MEMBERED() bbbadV5_MEMBERED() bbbadV6_MEMBERED() bbbadV3_XXREAL_2()   ($#v1_abian :::"odd"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 

cluster   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v1_xcmplx_0 :::"complex"::: )   bbbadV1_XREAL_0()   ($#v1_int_1 :::"integer"::: )     ($#v1_abian :::"even"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v1_xcmplx_0 :::"complex"::: )   bbbadV1_XREAL_0()   ($#v1_int_1 :::"integer"::: )     ($#v1_abian :::"odd"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: ABIAN:1 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "i")) "is"   ($#v1_abian :::"odd"::: )  ) "iff" (Bool  "ex" (Set (Var "j")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "j")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))))  ")" )) ; 
 registrationlet "i" be   ($#m1_hidden :::"Integer":::); 
cluster (Set (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  "i") ->   ($#v1_abian :::"even"::: )   ; 
end; registrationlet "i" be   ($#v1_abian :::"even"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)) ->   ($#v1_abian :::"odd"::: )   ; 
end; registrationlet "i" be   ($#v1_abian :::"odd"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)) ->   ($#v1_abian :::"even"::: )   ; 
end; registrationlet "i" be   ($#v1_abian :::"even"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)) ->   ($#v1_abian :::"odd"::: )   ; 
end; registrationlet "i" be   ($#v1_abian :::"odd"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)) ->   ($#v1_abian :::"even"::: )   ; 
end; registrationlet "i" be   ($#v1_abian :::"even"::: )    ($#m1_hidden :::"Integer":::); let "j" be   ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k3_xcmplx_0 :::"*"::: )  "j") ->   ($#v1_abian :::"even"::: )   ; 

cluster (Set "j"  ($#k3_xcmplx_0 :::"*"::: )  "i") ->   ($#v1_abian :::"even"::: )   ; 
end; registrationlet "i", "j" be   ($#v1_abian :::"odd"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k3_xcmplx_0 :::"*"::: )  "j") ->   ($#v1_abian :::"odd"::: )   ; 
end; registrationlet "i", "j" be   ($#v1_abian :::"even"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k2_xcmplx_0 :::"+"::: )  "j") ->   ($#v1_abian :::"even"::: )   ; 
end; registrationlet "i" be   ($#v1_abian :::"even"::: )    ($#m1_hidden :::"Integer":::); let "j" be   ($#v1_abian :::"odd"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k2_xcmplx_0 :::"+"::: )  "j") ->   ($#v1_abian :::"odd"::: )   ; 

cluster (Set "j"  ($#k2_xcmplx_0 :::"+"::: )  "i") ->   ($#v1_abian :::"odd"::: )   ; 
end; registrationlet "i", "j" be   ($#v1_abian :::"odd"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k2_xcmplx_0 :::"+"::: )  "j") ->   ($#v1_abian :::"even"::: )   ; 
end; registrationlet "i" be   ($#v1_abian :::"even"::: )    ($#m1_hidden :::"Integer":::); let "j" be   ($#v1_abian :::"odd"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k6_xcmplx_0 :::"-"::: )  "j") ->   ($#v1_abian :::"odd"::: )   ; 

cluster (Set "j"  ($#k6_xcmplx_0 :::"-"::: )  "i") ->   ($#v1_abian :::"odd"::: )   ; 
end; registrationlet "i", "j" be   ($#v1_abian :::"odd"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k6_xcmplx_0 :::"-"::: )  "j") ->   ($#v1_abian :::"even"::: )   ; 
end; registrationlet "m" be   ($#v1_abian :::"even"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "m"  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) ->   ($#v1_abian :::"even"::: )   ; 
end; registrationlet "m" be   ($#v1_abian :::"odd"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "m"  ($#k2_xcmplx_0 :::"+"::: )  (Num 2)) ->   ($#v1_abian :::"odd"::: )   ; 
end; definitionlet "E" be    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "E")) "," (Set (Const "E")); let "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); :: original: :::"iter"::: redefine func  :::"iter":::  "(" "f" "," "n" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" "E" "," "E"; end; 
theorem :: ABIAN:2 (Bool  "for" (Set (Var "S")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) )  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set   ($#k6_seq_4 :::"min"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: ABIAN:3 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) "holds"  (Bool (Set (Set  "("  ($#k1_abian :::"iter"::: )   "(" (Set (Var "f")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))))) ; 
 definitionlet "x" be    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_hidden :::"Function":::); pred "x" :::"is_a_fixpoint_of"::: "f" means :: ABIAN:def 3 (Bool  "("  (Bool "x"  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "f")) & (Bool "x"  ($#r1_hidden :::"="::: )  (Set "f"  ($#k1_funct_1 :::"."::: )  "x"))  ")" ); end; 





:: deftheorem    defines :::"is_a_fixpoint_of"::: ABIAN:def 3 :  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))  ")" )  ")" ))); 
 definitionlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "a" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "A")); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set (Const "A")); :: original: :::"is_a_fixpoint_of"::: redefine pred "a" :::"is_a_fixpoint_of"::: "f" means :: ABIAN:def 4 (Bool "a"  ($#r1_hidden :::"="::: )  (Set "f"  ($#k3_funct_2 :::"."::: )  "a")); end; 






:: deftheorem    defines :::"is_a_fixpoint_of"::: ABIAN:def 4 :  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r2_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f"))) "iff" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a"))))  ")" )))); 
 definitionlet "f" be   ($#m1_hidden :::"Function":::); attr "f" is  :::"with_fixpoint":::  means :: ABIAN:def 5 (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set (Var "x"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  "f")); end; 




:: deftheorem    defines :::"with_fixpoint"::: ABIAN:def 5 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_abian :::"with_fixpoint"::: )  ) "iff" (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set (Var "x"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f"))))  ")" )); 
 notationlet "f" be   ($#m1_hidden :::"Function":::); antonym  :::"without_fixpoints"::: "f" for  :::"with_fixpoint"::: ; end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "X")); attr "x" is  :::"covering":::  means :: ABIAN:def 6 (Bool (Set   ($#k3_tarski :::"union"::: )  "x")  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  "X" ")" ))); end; 





:: deftheorem    defines :::"covering"::: ABIAN:def 6 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v3_abian :::"covering"::: )  ) "iff" (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "X")) ")" )))  ")" ))); 
 
theorem :: ABIAN:4 (Bool  "for" (Set (Var "E")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "sE")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "E")) "holds"   (Bool  "("  (Bool (Set (Var "sE")) "is"   ($#v3_abian :::"covering"::: )  ) "iff" (Bool (Set   ($#k5_setfam_1 :::"union"::: )  (Set (Var "sE")))  ($#r1_hidden :::"="::: )  (Set (Var "E")))  ")" ))) ; 
 registrationlet "E" be    ($#m1_hidden :::"set"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#v3_abian :::"covering"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  "E" ")" )); 
end; 
theorem :: ABIAN:5 (Bool  "for" (Set (Var "E")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "sE")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_abian :::"covering"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "E"))  "st" (Bool (Bool  "("   "for" (Set (Var "X")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Var "sE")) "holds"  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "X"))))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v2_abian :::"without_fixpoints"::: )  )))) ; 
 definitionlet "E" be    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "E")) "," (Set (Const "E")); func  :::"=_"::: "f" ->   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "E" means :: ABIAN:def 7 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "E") & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "E")) "holds"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "k")) "," (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Set  "("  ($#k1_abian :::"iter"::: )   "(" "f" "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_abian :::"iter"::: )   "(" "f" "," (Set (Var "l")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))))  ")" )); end; 






:: deftheorem    defines :::"=_"::: ABIAN:def 7 :  (Bool  "for" (Set (Var "E")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "E")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_abian :::"=_"::: )  (Set (Var "f")))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "E"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "E")))) "holds"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "ex" (Set (Var "k")) "," (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Set  "("  ($#k1_abian :::"iter"::: )   "(" (Set (Var "f")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_abian :::"iter"::: )   "(" (Set (Var "f")) "," (Set (Var "l")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))))  ")" ))  ")" )))); 
 
theorem :: ABIAN:6 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "c")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_eqrel_1 :::"Class"::: )  (Set  "("  ($#k2_abian :::"=_"::: )  (Set (Var "f")) ")" ))  (Bool  "for" (Set (Var "e")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Var "c")) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "e")))  ($#r2_hidden :::"in"::: )  (Set (Var "c"))))))) ; 
 
theorem :: ABIAN:7 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "c")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k8_eqrel_1 :::"Class"::: )  (Set  "("  ($#k2_abian :::"=_"::: )  (Set (Var "f")) ")" ))  (Bool  "for" (Set (Var "e")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Var "c"))  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k1_abian :::"iter"::: )   "(" (Set (Var "f")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "e")))  ($#r2_hidden :::"in"::: )  (Set (Var "c")))))))) ; 
 registration
cluster   ($#v2_setfam_1 :::"empty-membered"::: )    ->   ($#v1_zfmisc_1 :::"trivial"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "A" be    ($#m1_hidden :::"set"::: )  ; let "B" be   ($#v2_setfam_1 :::"with_non-empty_element"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v2_relat_1 :::"non-empty"::: )   "A"  ($#v4_relat_1 :::"-defined"::: )   "B"  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2("A" "," "B")  for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) )); 
end; registrationlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "B" be   ($#v2_setfam_1 :::"with_non-empty_element"::: )     ($#m1_hidden :::"set"::: )  ; let "f" be   ($#v2_relat_1 :::"non-empty"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set (Const "B")); let "a" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "A")); 
cluster (Set "f"  ($#k1_funct_1 :::"."::: )  "a") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_zfmisc_1 :::"bool"::: )  "X") ->   ($#v2_setfam_1 :::"with_non-empty_element"::: )   ; 
end; 
theorem :: ABIAN:8 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "E"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_abian :::"without_fixpoints"::: )  )) "holds"  (Bool  "ex" (Set (Var "E1")) "," (Set (Var "E2")) "," (Set (Var "E3")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "E1"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "E2")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "E3")))  ($#r1_hidden :::"="::: )  (Set (Var "E"))) & (Bool (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "E1")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "E1"))) & (Bool (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "E2")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "E2"))) & (Bool (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "E3")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "E3")))  ")" )))) ; 
 begin  
theorem :: ABIAN:9 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  ) "iff" (Bool  "ex" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "k")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))))  ")" )) ; 
 
theorem :: ABIAN:10 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "A"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) "holds"  (Bool (Set (Set  "("  ($#k1_abian :::"iter"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "("  ($#k1_abian :::"iter"::: )   "(" (Set (Var "f")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ))))))) ; 
 
theorem :: ABIAN:11 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "i")) "is"   ($#v1_abian :::"even"::: )  ) "iff" (Bool  "ex" (Set (Var "j")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "j")))))  ")" )) ; 
 registration
cluster   ($#v1_xxreal_0 :::"ext-real"::: )   bbbadV1_ORDINAL1() bbbadV2_ORDINAL1() bbbadV3_ORDINAL1() bbbadV7_ORDINAL1()   ($#v1_xcmplx_0 :::"complex"::: )   bbbadV1_XREAL_0()   ($#v1_int_1 :::"integer"::: )     ($#v1_abian :::"odd"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_xxreal_0 :::"ext-real"::: )   bbbadV1_ORDINAL1() bbbadV2_ORDINAL1() bbbadV3_ORDINAL1() bbbadV7_ORDINAL1()   ($#v1_xcmplx_0 :::"complex"::: )   bbbadV1_XREAL_0()   ($#v1_int_1 :::"integer"::: )     ($#v1_abian :::"even"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: ABIAN:12 (Bool  "for" (Set (Var "n")) "being"   ($#v1_abian :::"odd"::: )    ($#m1_hidden :::"Nat":::) "holds"  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) ; 
 registration
cluster   ($#v1_int_1 :::"integer"::: )     ($#v1_abian :::"odd"::: )    ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   for    ($#m1_hidden :::"set"::: )  ; 
end;