:: PRGCOR_1  semantic presentation begin  
theorem :: PRGCOR_1:1 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" )  ($#k7_nat_d :::"-'"::: )  (Set  "(" (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "m"))))) ; 
 
theorem :: PRGCOR_1:2 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "k")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k")))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "k")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "k")))) & (Bool (Set (Set  "(" (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "k")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "k")) ")" )))  ")" )) ; 
 
theorem :: PRGCOR_1:3 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "k")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k")))) "holds"  (Bool (Set (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "k")) ")" ) ")" )  ($#k4_nat_1 :::"*"::: )  (Num 2) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)))) ; 
 
theorem :: PRGCOR_1:4 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "k")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k")))) "holds"  (Bool (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "k"))))) ; 
 
theorem :: PRGCOR_1:5 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "k")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k")))) "holds"  (Bool (Set (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "k")) ")" ) ")" )  ($#k4_nat_1 :::"*"::: )  (Num 2)))) ; 
 
theorem :: PRGCOR_1:6 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "k2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k2"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i")))) "holds"  (Bool (Set (Set (Var "m"))  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Num 2)  ($#k13_newton :::"|^"::: )  (Set (Var "k2")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" ) & (Bool (Set (Set (Var "m"))  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Num 2)  ($#k13_newton :::"|^"::: )  (Set (Var "i")) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n")))  ")" ))) ; 
 
theorem :: PRGCOR_1:7 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))))) ; 
 definitionlet "n", "m" be   ($#m1_hidden :::"Integer":::); assume that  
(Bool (Set (Const "n"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))
 and  
(Bool (Set (Const "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))
 ; func  :::"idiv1_prg":::  "(" "n" "," "m" ")"  ->   ($#m1_hidden :::"Integer":::) means :: PRGCOR_1:def 1 (Bool  "ex" (Set (Var "sm")) "," (Set (Var "sn")) "," (Set (Var "pn")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "sm")))  ($#r1_hidden :::"="::: )  (Set "n"  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "sn")))  ($#r1_hidden :::"="::: )  (Set "n"  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "pn")))  ($#r1_hidden :::"="::: )  (Set "n"  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))) &  "("  (Bool (Bool "n"  ($#r1_xxreal_0 :::"<"::: )  "m")) "implies" (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" "n"  ($#r1_xxreal_0 :::"<"::: )  "m"))) "implies" (Bool  "("  (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  "m") & (Bool  "ex" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  "n") & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2))) & (Bool (Bool  "not" (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::">"::: )  "n"))  ")" )  ")" ) & (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2))) & (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::">"::: )  "n") & (Bool (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  "n") & (Bool  "("   "for" (Set (Var "j")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" )))) "implies" (Bool  "("  (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ) ")" ))) & (Bool (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))))) "implies" (Bool  "("  (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ))) & (Bool (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2)))  ")" )  ")"   ")" )  ")" ) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Num 1)))  ")" ))  ")" )  ")"   ")" )); end; 







:: deftheorem    defines :::"idiv1_prg"::: PRGCOR_1:def 1 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_prgcor_1 :::"idiv1_prg"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )) "iff" (Bool  "ex" (Set (Var "sm")) "," (Set (Var "sn")) "," (Set (Var "pn")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "sm")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "sn")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "pn")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))) &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "implies" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m"))))) "implies" (Bool  "("  (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool  "ex" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2))) & (Bool (Bool  "not" (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n"))))  ")" )  ")" ) & (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2))) & (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool  "("   "for" (Set (Var "j")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" )))) "implies" (Bool  "("  (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ) ")" ))) & (Bool (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))))) "implies" (Bool  "("  (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ))) & (Bool (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2)))  ")" )  ")"   ")" )  ")" ) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Num 1)))  ")" ))  ")" )  ")"   ")" ))  ")" ))); 
 
theorem :: PRGCOR_1:8 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "sm")) "," (Set (Var "sn")) "," (Set (Var "pn")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  )  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "sm")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "sn")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "pn")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))) &  "("  (Bool (Bool (Bool  "not" (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m"))))) "implies" (Bool  "("  (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2))) & (Bool (Bool  "not" (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n"))))  ")" )  ")" ) & (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2))) & (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool  "("   "for" (Set (Var "j")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" )))) "implies" (Bool  "("  (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ) ")" ))) & (Bool (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))))) "implies" (Bool  "("  (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ))) & (Bool (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2)))  ")" )  ")"   ")" )  ")" ) & (Bool (Set   ($#k1_prgcor_1 :::"idiv1_prg"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Num 1)))  ")" )  ")" ) "holds"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "sm")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "sn")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "pn")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))) &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "implies" (Bool (Set   ($#k1_prgcor_1 :::"idiv1_prg"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m"))))) "implies" (Bool  "("  (Bool (Num 1)  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "sm")))) & (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "sm")))) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "sm")))) & (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2))) & (Bool (Bool  "not" (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n"))))  ")" )  ")" ) & (Bool (Set (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "sm")))) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "sm")))) & (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2))) & (Bool (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "pn")))) & (Bool (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "sn")))) & (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool  "("   "for" (Set (Var "j")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "sn")))) & (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "sm")))) &  "("  (Bool (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" )))) "implies" (Bool  "("  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "sn")))) & (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "sm")))) & (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ) ")" ))) & (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "pn")))) & (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "pn")))) & (Bool (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1)))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "sm"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))))) "implies" (Bool  "("  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "sn")))) & (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "sn")))) & (Bool (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "sn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ))) & (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "pn")))) & (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "pn")))) & (Bool (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "j"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Num 2)))  ")" )  ")"   ")" )  ")" ) & (Bool (Num 1)  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "pn")))) & (Bool (Set   ($#k1_prgcor_1 :::"idiv1_prg"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "pn"))  ($#k1_funct_1 :::"."::: )  (Num 1)))  ")" )  ")"   ")" )))) ; 
 
theorem :: PRGCOR_1:9 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k1_prgcor_1 :::"idiv1_prg"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set (Var "m"))))) ; 
 
theorem :: PRGCOR_1:10 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k1_prgcor_1 :::"idiv1_prg"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_int_1 :::"div"::: )  (Set (Var "m"))))) ; 
 
theorem :: PRGCOR_1:11 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "n2")) "," (Set (Var "m2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n2"))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Var "m2"))  ($#r1_hidden :::"="::: )  (Set (Var "m")))) "implies" (Bool  "("  (Bool (Set (Set (Var "n"))  ($#k5_int_1 :::"div"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "n2"))  ($#k3_nat_d :::"div"::: )  (Set (Var "m2")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")"  &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n2"))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Var "m2"))  ($#r1_hidden :::"="::: )  (Set (Var "m")))) "implies" (Bool (Set (Set (Var "n"))  ($#k5_int_1 :::"div"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n2"))  ($#k3_nat_d :::"div"::: )  (Set (Var "m2"))))  ")"  &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n2"))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Var "m2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "m"))))) "implies" (Bool  "("   "("  (Bool (Bool (Set (Set (Var "m2"))  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set (Var "n2"))  ($#k3_nat_d :::"div"::: )  (Set (Var "m2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n2")))) "implies" (Bool (Set (Set (Var "n"))  ($#k5_int_1 :::"div"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "n2"))  ($#k3_nat_d :::"div"::: )  (Set (Var "m2")) ")" )))  ")"  &  "("  (Bool (Bool (Set (Set (Var "m2"))  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set (Var "n2"))  ($#k3_nat_d :::"div"::: )  (Set (Var "m2")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set (Var "n2")))) "implies" (Bool (Set (Set (Var "n"))  ($#k5_int_1 :::"div"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "n2"))  ($#k3_nat_d :::"div"::: )  (Set (Var "m2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))  ")"   ")" )  ")"  &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "n")))) & (Bool (Set (Var "m2"))  ($#r1_hidden :::"="::: )  (Set (Var "m")))) "implies" (Bool  "("   "("  (Bool (Bool (Set (Set (Var "m2"))  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set (Var "n2"))  ($#k3_nat_d :::"div"::: )  (Set (Var "m2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n2")))) "implies" (Bool (Set (Set (Var "n"))  ($#k5_int_1 :::"div"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "n2"))  ($#k3_nat_d :::"div"::: )  (Set (Var "m2")) ")" )))  ")"  &  "("  (Bool (Bool (Set (Set (Var "m2"))  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set (Var "n2"))  ($#k3_nat_d :::"div"::: )  (Set (Var "m2")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set (Var "n2")))) "implies" (Bool (Set (Set (Var "n"))  ($#k5_int_1 :::"div"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "n2"))  ($#k3_nat_d :::"div"::: )  (Set (Var "m2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))  ")"   ")" )  ")"  &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "n")))) & (Bool (Set (Var "m2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "m"))))) "implies" (Bool (Set (Set (Var "n"))  ($#k5_int_1 :::"div"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n2"))  ($#k3_nat_d :::"div"::: )  (Set (Var "m2"))))  ")"   ")" ))) ; 
 definitionlet "n", "m" be   ($#m1_hidden :::"Integer":::); func  :::"idiv_prg":::  "(" "n" "," "m" ")"  ->   ($#m1_hidden :::"Integer":::) means :: PRGCOR_1:def 2 (Bool  "ex" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("   "("  (Bool (Bool "m"  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" "m"  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool  "("   "("  (Bool (Bool "n"  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool "m"  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_prgcor_1 :::"idiv1_prg"::: )   "(" "n" "," "m" ")" ))  ")"  &  "("  (Bool (Bool  "("   "not" (Bool "n"  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or"  "not" (Bool "m"  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "implies" (Bool  "("   "("  (Bool (Bool "n"  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool "m"  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_prgcor_1 :::"idiv1_prg"::: )   "(" "n" "," (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  "m" ")" ) ")" )) &  "("  (Bool (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  "m" ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  "n")) "implies" (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "i"))))  ")"  &  "("  (Bool (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  "m" ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i")))  ($#r1_hidden :::"<>"::: )  "n")) "implies" (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "i")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))  ")"   ")" )  ")"  &  "("  (Bool (Bool  "("   "not" (Bool "n"  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or"  "not" (Bool "m"  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "implies" (Bool  "("   "("  (Bool (Bool "n"  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool "m"  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_prgcor_1 :::"idiv1_prg"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  "n" ")" ) "," "m" ")" )) &  "("  (Bool (Bool (Set "m"  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  "n"))) "implies" (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "i"))))  ")"  &  "("  (Bool (Bool (Set "m"  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  "n"))) "implies" (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "i")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))  ")"   ")" )  ")"  &  "("  (Bool (Bool  "("   "not" (Bool "n"  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or"  "not" (Bool "m"  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "implies" (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_prgcor_1 :::"idiv1_prg"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  "n" ")" ) "," (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  "m" ")" ) ")" ))  ")"   ")" )  ")"   ")" )  ")"   ")" )  ")"   ")" )); end; 






:: deftheorem    defines :::"idiv_prg"::: PRGCOR_1:def 2 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "b3")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_prgcor_1 :::"idiv_prg"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )) "iff" (Bool  "ex" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("   "("  (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool  "("   "("  (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_prgcor_1 :::"idiv1_prg"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" ))  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or"  "not" (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "implies" (Bool  "("   "("  (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_prgcor_1 :::"idiv1_prg"::: )   "(" (Set (Var "n")) "," (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "m")) ")" ) ")" )) &  "("  (Bool (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "m")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "implies" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "i"))))  ")"  &  "("  (Bool (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "m")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i")))  ($#r1_hidden :::"<>"::: )  (Set (Var "n")))) "implies" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "i")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))  ")"   ")" )  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or"  "not" (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "implies" (Bool  "("   "("  (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_prgcor_1 :::"idiv1_prg"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "n")) ")" ) "," (Set (Var "m")) ")" )) &  "("  (Bool (Bool (Set (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "n"))))) "implies" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "i"))))  ")"  &  "("  (Bool (Bool (Set (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "n"))))) "implies" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "i")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))  ")"   ")" )  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or"  "not" (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "implies" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_prgcor_1 :::"idiv1_prg"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "m")) ")" ) ")" ))  ")"   ")" )  ")"   ")" )  ")"   ")" )  ")"   ")" ))  ")" )); 
 
theorem :: PRGCOR_1:12 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k2_prgcor_1 :::"idiv_prg"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_int_1 :::"div"::: )  (Set (Var "m"))))) ;