:: WSIERP_1  semantic presentation begin  




























theorem :: WSIERP_1:1 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x")))) & (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "x")) ")" )  ($#k1_newton :::"|^"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Num 2)))  ")" )) ; 
 
theorem :: WSIERP_1:2 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "x")) ")" )  ($#k1_newton :::"|^"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "a")) ")" ))) & (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "x")) ")" )  ($#k1_newton :::"|^"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" ))) ; 
 
theorem :: WSIERP_1:3 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "d")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "d"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k1_newton :::"|^"::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))) ; 
 registrationlet "k" be   ($#m1_hidden :::"Integer":::); let "a" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "k"  ($#k1_newton :::"|^"::: )  "a") ->   ($#v1_int_1 :::"integer"::: )   ; 
end; 
theorem :: WSIERP_1:4 (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_int_1 :::"divides"::: )  (Set (Var "m"))) & (Bool (Set (Var "k"))  ($#r1_int_1 :::"divides"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "k"))  ($#r1_int_1 :::"divides"::: )  (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "n"))))) ; 
 
theorem :: WSIERP_1:5 (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "m1")) "," (Set (Var "n1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_int_1 :::"divides"::: )  (Set (Var "m"))) & (Bool (Set (Var "k"))  ($#r1_int_1 :::"divides"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "k"))  ($#r1_int_1 :::"divides"::: )  (Set (Set  "(" (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "n"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n1")) ")" )))) ; 
 
theorem :: WSIERP_1:6 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Set (Var "m"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "k"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "k")) ")" )  ($#k3_int_2 :::"gcd"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: WSIERP_1:7 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "c"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: WSIERP_1:8 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k3_int_2 :::"gcd"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_int_2 :::"abs"::: )  (Set (Var "m")))) & (Bool (Set (Num 1)  ($#k3_int_2 :::"gcd"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 
theorem :: WSIERP_1:9 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Num 1) "," (Set (Var "k"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) ; 
 
theorem :: WSIERP_1:10 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "k")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "k")) "," (Set (Var "l"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set (Set (Var "k"))  ($#k1_newton :::"|^"::: )  (Set (Var "a"))) "," (Set (Var "l"))  ($#r1_int_2 :::"are_relative_prime"::: )  ))) ; 
 
theorem :: WSIERP_1:11 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "k")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "k")) "," (Set (Var "l"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set (Set (Var "k"))  ($#k1_newton :::"|^"::: )  (Set (Var "a"))) "," (Set (Set (Var "l"))  ($#k1_newton :::"|^"::: )  (Set (Var "b")))  ($#r1_int_2 :::"are_relative_prime"::: )  ))) ; 
 
theorem :: WSIERP_1:12 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "k")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Set (Var "k"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Set (Var "k"))  ($#k3_int_2 :::"gcd"::: )  (Set  "(" (Set (Var "l"))  ($#k1_newton :::"|^"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set  "(" (Set (Var "k"))  ($#k1_newton :::"|^"::: )  (Set (Var "a")) ")" )  ($#k3_int_2 :::"gcd"::: )  (Set  "(" (Set (Var "l"))  ($#k1_newton :::"|^"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))  ")" ))) ; 
 
theorem :: WSIERP_1:13 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set   ($#k1_int_2 :::"abs"::: )  (Set (Var "m")))  ($#r1_int_1 :::"divides"::: )  (Set (Var "k"))) "iff" (Bool (Set (Var "m"))  ($#r1_int_1 :::"divides"::: )  (Set (Var "k")))  ")" )) ; 
 
theorem :: WSIERP_1:14 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "c")))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Set (Var "c"))))) ; 
 
theorem :: WSIERP_1:15 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_nat_d :::"divides"::: )  (Num 1))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: WSIERP_1:16 (Bool  "for" (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "d"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "a"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "d"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: WSIERP_1:17 (Bool  "for" (Set (Var "k")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_int_1 :::"divides"::: )  (Set (Var "l"))) "iff" (Bool (Set (Set (Var "l"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "k"))) "is"   ($#m1_hidden :::"Integer":::))  ")" )) ; 
 
theorem :: WSIERP_1:18 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c"))))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))  ")" )) ; 
 





definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "D1" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "D")); let "f1", "f2" be    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set (Const "D1")); :: original: :::"^"::: redefine func "f1" :::"^"::: "f2" ->    ($#m1_trees_4 :::"FinSequence"::: )   "of" "D1"; end; 



















registrationlet "fr" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ); 
cluster (Set   ($#k19_rvsum_1 :::"Product"::: )  "fr") ->   ($#v1_int_1 :::"integer"::: )   ; 
end; definitionlet "fp" be    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); :: original: :::"Sum"::: redefine func  :::"Sum"::: "fp" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); end; definitionlet "fp" be    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); :: original: :::"Product"::: redefine func  :::"Product"::: "fp" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); end; definitionlet "a" be   ($#m1_hidden :::"Nat":::); let "fs" be   ($#m1_hidden :::"FinSequence":::); redefine func  :::"Del":::  "(" "fs" "," "a" ")"  means :: WSIERP_1:def 1 (Bool it  ($#r1_hidden :::"="::: )  "fs") if (Bool (Bool  "not" "a"  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  "fs")))  otherwise (Bool  "("  (Bool (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  it ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "fs")) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  "a")) "implies" (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set "fs"  ($#k1_funct_1 :::"."::: )  (Set (Var "b"))))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">="::: )  "a")) "implies" (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set "fs"  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "b"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )))  ")"   ")" )  ")" )  ")" ); end; 






:: deftheorem    defines :::"Del"::: WSIERP_1:def 1 :  (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "fs")) "being"   ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "fs")))))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_finseq_3 :::"Del"::: )   "(" (Set (Var "fs")) "," (Set (Var "a")) ")" )) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Var "fs")))  ")" )  ")"  &  "("  (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "fs"))))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_finseq_3 :::"Del"::: )   "(" (Set (Var "fs")) "," (Set (Var "a")) ")" )) "iff" (Bool  "("  (Bool (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "b3")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs")))) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) "implies" (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "fs"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b"))))  ")"  &  "("  (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "a")))) "implies" (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "fs"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "b"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )))  ")"   ")" )  ")" )  ")" )  ")" )  ")"   ")" )))); 
 definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "a" be   ($#m1_hidden :::"Nat":::); let "fs" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Const "D")); :: original: :::"Del"::: redefine func  :::"Del":::  "(" "fs" "," "a" ")"  ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" "D"; end; definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "D1" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "D")); let "a" be   ($#m1_hidden :::"Nat":::); let "fs" be    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set (Const "D1")); :: original: :::"Del"::: redefine func  :::"Del":::  "(" "fs" "," "a" ")"  ->    ($#m1_trees_4 :::"FinSequence"::: )   "of" "D1"; end; 
theorem :: WSIERP_1:19 (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k2_finseq_3 :::"Del"::: )   "(" (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "v1")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set   ($#k2_finseq_3 :::"Del"::: )   "(" (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "v2")) ($#k9_finseq_1 :::"*>"::: ) )) & (Bool (Set   ($#k2_finseq_3 :::"Del"::: )   "(" (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Num 2) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "v1")) ($#k9_finseq_1 :::"*>"::: ) )) & (Bool (Set   ($#k2_finseq_3 :::"Del"::: )   "(" (Set  ($#k11_finseq_1 :::"<*"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "v2")) "," (Set (Var "v3")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set   ($#k2_finseq_3 :::"Del"::: )   "(" (Set  ($#k11_finseq_1 :::"<*"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Num 2) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "v1")) "," (Set (Var "v3")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set   ($#k2_finseq_3 :::"Del"::: )   "(" (Set  ($#k11_finseq_1 :::"<*"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) ($#k11_finseq_1 :::"*>"::: ) ) "," (Num 3) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k10_finseq_1 :::"*>"::: ) ))  ")" )) ; 
 
theorem :: WSIERP_1:20 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "ft")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "ft"))))) "holds"  (Bool (Set (Set  "("  ($#k18_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k4_wsierp_1 :::"Del"::: )   "(" (Set (Var "ft")) "," (Set (Var "a")) ")"  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "ft"))  ($#k1_seq_1 :::"."::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set (Var "ft")))))) ; 
 
theorem :: WSIERP_1:21 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "fp")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "fp"))))) "holds"  (Bool (Set (Set  "("  ($#k3_wsierp_1 :::"Product"::: )  (Set (Var "fp")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "fp"))  ($#k1_seq_1 :::"."::: )  (Set (Var "a")) ")" )) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )))) ; 
 
theorem :: WSIERP_1:22 (Bool  "for" (Set (Var "q")) "being"   ($#m1_hidden :::"Rational":::) "holds"  (Bool (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "q"))) "," (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "q")))  ($#r1_int_2 :::"are_relative_prime"::: )  )) ; 
 
theorem :: WSIERP_1:23 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "q")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "k")) "," (Set (Var "a"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_rat_1 :::"numerator"::: )  (Set (Var "q")))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rat_1 :::"denominator"::: )  (Set (Var "q"))))  ")" )))) ; 
 
theorem :: WSIERP_1:24 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool  "ex" (Set (Var "q")) "being"   ($#m1_hidden :::"Rational":::) "st" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Set (Var "b")))))) "holds"  (Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k1_newton :::"|^"::: )  (Set (Var "b")))))) ; 
 
theorem :: WSIERP_1:25 (Bool  "for" (Set (Var "a")) "," (Set (Var "d")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool  "ex" (Set (Var "q")) "being"   ($#m1_hidden :::"Rational":::) "st" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Set (Var "d")))))) "holds"  (Bool  "ex" (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Set (Var "d")))))) ; 
 
theorem :: WSIERP_1:26 (Bool  "for" (Set (Var "e")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "e")))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Set (Var "e"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "b")))) ; 
 
theorem :: WSIERP_1:27 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Set (Var "a"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" ))))) ; 
 
theorem :: WSIERP_1:28 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) (Bool  "ex" (Set (Var "m1")) "," (Set (Var "n1")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Set (Var "m"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "n"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n1")) ")" ))))) ; 
 
theorem :: WSIERP_1:29 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_int_1 :::"divides"::: )  (Set (Set (Var "n"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "k")))) & (Bool (Set (Set (Var "m"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Var "m"))  ($#r1_int_1 :::"divides"::: )  (Set (Var "k")))) ; 
 
theorem :: WSIERP_1:30 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "a"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "c")))) ; 
 
theorem :: WSIERP_1:31 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Set (Var "a"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "d")) ")" ))))) ; 
 
theorem :: WSIERP_1:32 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "g"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "f"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Set (Var "g"))))) "holds"  (Bool  "ex" (Set (Var "e")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "e"))  ($#k1_newton :::"|^"::: )  (Set (Var "g")))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "e"))  ($#k1_newton :::"|^"::: )  (Set (Var "f"))))  ")" ))) ; 
 





theorem :: WSIERP_1:33 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Set  "(" (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "n"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "k")))) "iff" (Bool (Set (Set (Var "m"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "n")))  ($#r1_int_1 :::"divides"::: )  (Set (Var "k")))  ")" )) ; 
 
theorem :: WSIERP_1:34 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "m1")) "," (Set (Var "n1")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "n"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "k")))) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Set  "(" (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "n"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "k")))) "holds"  (Bool  "ex" (Set (Var "t")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "t"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "n"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "m"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "n")) ")" ) ")" ) ")" ))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "t"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "m"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set (Var "m"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "n")) ")" ) ")" ) ")" )))  ")" )))) ; 
 
theorem :: WSIERP_1:35 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "a"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k1_newton :::"|^"::: )  (Set (Var "d"))))) "holds"  (Bool  "ex" (Set (Var "e")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "e"))  ($#k1_newton :::"|^"::: )  (Set (Var "d")))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_newton :::"|^"::: )  (Set (Var "d"))))  ")" ))) ; 
 
theorem :: WSIERP_1:36 (Bool  "for" (Set (Var "fp")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "d")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "fp"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "fp"))  ($#k1_seq_1 :::"."::: )  (Set (Var "a")) ")" )  ($#k3_int_2 :::"gcd"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k3_wsierp_1 :::"Product"::: )  (Set (Var "fp")) ")" )  ($#k3_int_2 :::"gcd"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Num 1)))) ; 
 
theorem :: WSIERP_1:37 (Bool  "for" (Set (Var "fp")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fp")))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool  "("   "for" (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "fp")))) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "fp")))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c")))) "holds"  (Bool (Set (Set  "(" (Set (Var "fp"))  ($#k1_seq_1 :::"."::: )  (Set (Var "b")) ")" )  ($#k3_int_2 :::"gcd"::: )  (Set  "(" (Set (Var "fp"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) "holds"  (Bool  "for" (Set (Var "fr")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fr")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fp"))))) "holds"  (Bool  "ex" (Set (Var "fr1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fr1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "fp")))) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "fp"))))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "fp"))  ($#k1_seq_1 :::"."::: )  (Set (Var "b")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "fr1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "b")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "fr"))  ($#k1_seq_1 :::"."::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "fp"))  ($#k1_seq_1 :::"."::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "fr1"))  ($#k1_seq_1 :::"."::: )  (Num 1) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "fr"))  ($#k1_seq_1 :::"."::: )  (Num 1) ")" )))  ")" )  ")" )))) ; 
 
theorem :: WSIERP_1:38 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "a"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "ex" (Set (Var "b")) "," (Set (Var "e")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_hidden :::"<>"::: )  (Set (Var "e"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")))) & (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")))) & (Bool  "("  (Bool (Set (Var "a"))  ($#r1_int_1 :::"divides"::: )  (Set (Set  "(" (Set (Var "k"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "e")))) "or" (Bool (Set (Var "a"))  ($#r1_int_1 :::"divides"::: )  (Set (Set  "(" (Set (Var "k"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "e"))))  ")" )  ")" )))) ; 
 
theorem :: WSIERP_1:39 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "fs")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "("  ($#k2_finseq_3 :::"Del"::: )   "(" (Set (Var "fs")) "," (Set (Var "a")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "fs")))))) ; 
 
theorem :: WSIERP_1:40 (Bool  "for" (Set (Var "fs")) "being"   ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "v")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k2_finseq_3 :::"Del"::: )   "(" (Set  "(" (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "v")) ($#k9_finseq_1 :::"*>"::: ) )  ($#k7_finseq_1 :::"^"::: )  (Set (Var "fs")) ")" ) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "fs"))) & (Bool (Set   ($#k2_finseq_3 :::"Del"::: )   "(" (Set  "(" (Set (Var "fs"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "v")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "," (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "fs")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "fs")))  ")" ))) ; 
 begin  



theorem :: WSIERP_1:41 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "k"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "k"))  ($#k5_int_1 :::"div"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "k")) ")" )  ($#k5_int_1 :::"div"::: )  (Set (Var "n")) ")" )  ($#k3_real_1 :::"+"::: )  (Num 1))))) ; 
 
theorem :: WSIERP_1:42 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "k"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "k"))  ($#k5_int_1 :::"div"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "k")) ")" )  ($#k5_int_1 :::"div"::: )  (Set (Var "n")))))) ;