:: PEPIN  semantic presentation begin  





















theorem :: PEPIN:1 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Var "i")) "," (Set (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_int_2 :::"are_relative_prime"::: )  )) ; 
 
theorem :: PEPIN:2 (Bool  "for" (Set (Var "m")) "," (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  ) "or" (Bool (Set (Var "m")) "," (Set (Var "p"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) "or" (Bool (Set (Set (Var "m"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "p")))  ")" )) ; 
 
theorem :: PEPIN:3 (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "n"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m")))) & (Bool (Set (Var "n")) "," (Set (Var "k"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set (Var "k"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "m")))) ; 
 
theorem :: PEPIN:4 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "m"))) & (Bool (Set (Var "k"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "m"))) & (Bool (Set (Var "n")) "," (Set (Var "k"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set (Set (Var "n"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "k")))  ($#r1_nat_d :::"divides"::: )  (Set (Var "m")))) ; 
 registrationlet "i" be   ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k3_square_1 :::"^2"::: )  ) ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; 
theorem :: PEPIN:5 (Bool  "for" (Set (Var "c")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set (Num 1)  ($#k6_int_1 :::"mod"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: PEPIN:6 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "i"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n"))) "iff" (Bool (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: PEPIN:7 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "m"))))) "holds"  (Bool (Set (Var "m"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n")))) ; 
 
theorem :: PEPIN:8 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "m"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "k")))) "holds"  (Bool (Set (Var "n"))  ($#r1_int_1 :::"divides"::: )  (Set (Set (Var "m"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "k"))))) ; 
 
theorem :: PEPIN:9 (Bool  "for" (Set (Var "i")) "," (Set (Var "p")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "i"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "k"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set (Var "i"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p")))) "holds"  (Bool (Set (Set (Var "k"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set (Var "i"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "p"))))) ; 
 
theorem :: PEPIN:10 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k6_int_1 :::"mod"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k4_nat_d :::"mod"::: )  (Set (Var "p")))))) ; 
 
theorem :: PEPIN:11 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m"))) & (Bool (Set (Set  "(" (Set (Var "n"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "k")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "m")))) & (Bool (Set (Var "k")) "," (Set (Var "m"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: PEPIN:12 (Bool  "for" (Set (Var "p")) "," (Set (Var "k")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "m")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "k")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "m"))))) ; 
 
theorem :: PEPIN:13 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: PEPIN:14 (Bool  "for" (Set (Var "k")) "," (Set (Var "j")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "k"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Set (Var "i"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Var "k")))) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k3_square_1 :::"^2"::: )  ))) ; 
 
theorem :: PEPIN:15 (Bool  "for" (Set (Var "p")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Set (Var "i"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: PEPIN:16 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n")) "is"   ($#v1_abian :::"even"::: )  )) "holds"  (Bool (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1)) "is"   ($#v1_abian :::"odd"::: )  )) ; 
 
theorem :: PEPIN:17 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 2)) & (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  )) "holds"  (Bool (Set (Var "p")) "is"   ($#v1_abian :::"odd"::: )  )) ; 
 
theorem :: PEPIN:18 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Num 2)  ($#k3_power :::"to_power"::: )  (Set (Var "n"))) "is"   ($#v1_abian :::"even"::: )  )) ; 
 
theorem :: PEPIN:19 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i")) "is"   ($#v1_abian :::"odd"::: )  ) & (Bool (Set (Var "j")) "is"   ($#v1_abian :::"odd"::: )  )) "holds"  (Bool (Set (Set (Var "i"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "j"))) "is"   ($#v1_abian :::"odd"::: )  )) ; 
 
theorem :: PEPIN:20 (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i")) "is"   ($#v1_abian :::"odd"::: )  )) "holds"  (Bool (Set (Set (Var "i"))  ($#k1_newton :::"|^"::: )  (Set (Var "k"))) "is"   ($#v1_abian :::"odd"::: )  )) ; 
 
theorem :: PEPIN:21 (Bool  "for" (Set (Var "k")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "i")) "is"   ($#v1_abian :::"even"::: )  )) "holds"  (Bool (Set (Set (Var "i"))  ($#k1_newton :::"|^"::: )  (Set (Var "k"))) "is"   ($#v1_abian :::"even"::: )  )) ; 
 
theorem :: PEPIN:22 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Num 2)  ($#r1_nat_d :::"divides"::: )  (Set (Var "n"))) "iff" (Bool (Set (Var "n")) "is"   ($#v1_abian :::"even"::: )  )  ")" )) ; 
 
theorem :: PEPIN:23 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n"))) "is"   ($#v1_abian :::"even"::: )  ) "or" (Bool (Set (Var "m")) "is"   ($#v1_abian :::"even"::: )  ) "or" (Bool (Set (Var "n")) "is"   ($#v1_abian :::"even"::: )  )  ")" )) ; 
 
theorem :: PEPIN:24 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "n"))  ($#k1_newton :::"|^"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k3_square_1 :::"^2"::: )  ))) ; 
 
theorem :: PEPIN:25 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "m"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) ; 
 
theorem :: PEPIN:26 (Bool  "for" (Set (Var "n")) "," (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "n"))  ($#k1_newton :::"|^"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "n"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "p"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )))) ; 
 
theorem :: PEPIN:27 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "m"))  ($#k4_nat_d :::"mod"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "m"))  ($#k3_nat_d :::"div"::: )  (Num 2) ")" ) ")" )  ($#k3_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_newton :::"|^"::: )  (Set (Var "m"))))) ; 
 
theorem :: PEPIN:28 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")) ")" )  ($#k3_nat_d :::"div"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "k"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )))) ; 
 
theorem :: PEPIN:29 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Num 2)  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" )))) ; 
 
theorem :: PEPIN:30 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Set (Var "k"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k1_newton :::"|^"::: )  (Set (Var "m"))))) "holds"  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Var "m")))) ; 
 
theorem :: PEPIN:31 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) "iff" (Bool (Set (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "m")))  ($#r1_nat_d :::"divides"::: )  (Set (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "n"))))  ")" )) ; 
 
theorem :: PEPIN:32 (Bool  "for" (Set (Var "p")) "," (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "i"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))) & (Bool (Bool  "not" (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Num 1)))) "holds"  (Bool  "ex" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k3_nat_1 :::"*"::: )  (Set (Var "k")))))) ; 
 
theorem :: PEPIN:33 (Bool  "for" (Set (Var "p")) "," (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )))) "holds"  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))) "iff" (Bool (Set (Var "n"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "k"))))  ")" )) ; 
 
theorem :: PEPIN:34 (Bool  "for" (Set (Var "p")) "," (Set (Var "d")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "d"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "k"))))) "holds"  (Bool  "ex" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "t")))) & (Bool (Set (Var "t"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))  ")" ))) ; 
 
theorem :: PEPIN:35 (Bool  "for" (Set (Var "p")) "," (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Set (Var "i"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: PEPIN:36 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k1_newton :::"|^"::: )  (Set (Var "m")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: PEPIN:37 (Bool  "for" (Set (Var "n")) "," (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "n")) "," (Set (Var "p"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "p"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: PEPIN:38 (Bool  "for" (Set (Var "p")) "," (Set (Var "d")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "d"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "d"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")))) & (Bool (Bool  "not" (Set (Var "d"))  ($#r1_nat_d :::"divides"::: )  (Set (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")) ")" )  ($#k3_nat_d :::"div"::: )  (Set (Var "p")))))) "holds"  (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Set (Var "k"))))) ; 
 definitionlet "i" be   ($#m1_hidden :::"Integer":::); :: original: :::"^2"::: redefine func "i" :::"^2":::  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); end; 
theorem :: PEPIN:39 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Set (Var "m"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Num 1)) "iff" (Bool (Set (Var "m")) "," (Num 1)  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "n")))  ")" )) ; 
 
theorem :: PEPIN:40 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i5")) "," (Set (Var "i3")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i1")) "," (Set (Var "i2"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5"))) & (Bool (Set (Var "i1")) "," (Set (Var "i3"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5")))) "holds"  (Bool (Set (Var "i2")) "," (Set (Var "i3"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5")))) ; 
 
theorem :: PEPIN:41 (Bool (Num 3) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: PEPIN:42 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k1_euler_1 :::"Euler"::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: PEPIN:43 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) ; 
 
theorem :: PEPIN:44 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 begin  definitionlet "k", "m", "n" be   ($#m1_hidden :::"Nat":::); func  :::"Crypto":::  "(" "m" "," "n" "," "k" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) equals :: PEPIN:def 1 (Set (Set  "(" "m"  ($#k1_newton :::"|^"::: )  "k" ")" )  ($#k4_nat_d :::"mod"::: )  "n"); end; 







:: deftheorem    defines :::"Crypto"::: PEPIN:def 1 :  (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k2_pepin :::"Crypto"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "m"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "n"))))); 
 
theorem :: PEPIN:45 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "n")) "," (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "q")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "q")))) & (Bool (Set (Var "k1")) "," (Set   ($#k1_euler_1 :::"Euler"::: )  (Set (Var "n")))  ($#r1_int_2 :::"are_relative_prime"::: )  ) & (Bool (Set (Set  "(" (Set (Var "k1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "k2")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set  "("  ($#k1_euler_1 :::"Euler"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k2_pepin :::"Crypto"::: )   "(" (Set  "("  ($#k2_pepin :::"Crypto"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k1")) ")"  ")" ) "," (Set (Var "n")) "," (Set (Var "k2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "m"))))) ; 
 begin  definitionlet "i", "p" be   ($#m1_hidden :::"Nat":::); assume that  
(Bool (Set (Const "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))
 and  
(Bool (Set (Const "i")) "," (Set (Const "p"))  ($#r1_int_2 :::"are_relative_prime"::: )  )
 ; func  :::"order":::  "(" "i" "," "p" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: PEPIN:def 2 (Bool  "("  (Bool it  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" "i"  ($#k1_newton :::"|^"::: )  it ")" )  ($#k4_nat_d :::"mod"::: )  "p")  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" "i"  ($#k1_newton :::"|^"::: )  (Set (Var "k")) ")" )  ($#k4_nat_d :::"mod"::: )  "p")  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  it) & (Bool it  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))  ")" )  ")" )  ")" ); end; 







:: deftheorem    defines :::"order"::: PEPIN:def 2 :  (Bool  "for" (Set (Var "i")) "," (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "i")) "," (Set (Var "p"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_pepin :::"order"::: )   "(" (Set (Var "i")) "," (Set (Var "p")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set (Var "i"))  ($#k1_newton :::"|^"::: )  (Set (Var "b3")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set (Var "i"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b3"))) & (Bool (Set (Var "b3"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))  ")" )  ")" )  ")" )  ")" ))); 
 
theorem :: PEPIN:46 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set   ($#k3_pepin :::"order"::: )   "(" (Num 1) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: PEPIN:47 (Bool  "for" (Set (Var "p")) "," (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Set  "(" (Set (Var "i"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "i")) "," (Set (Var "p"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set   ($#k3_pepin :::"order"::: )   "(" (Set (Var "i")) "," (Set (Var "p")) ")" )  ($#r1_nat_d :::"divides"::: )  (Set (Var "n")))) ; 
 
theorem :: PEPIN:48 (Bool  "for" (Set (Var "p")) "," (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "i")) "," (Set (Var "p"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) & (Bool (Set   ($#k3_pepin :::"order"::: )   "(" (Set (Var "i")) "," (Set (Var "p")) ")" )  ($#r1_nat_d :::"divides"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: PEPIN:49 (Bool  "for" (Set (Var "p")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "i")) "," (Set (Var "p"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool (Set   ($#k3_pepin :::"order"::: )   "(" (Set (Var "i")) "," (Set (Var "p")) ")" )  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "p"))  ($#k7_nat_d :::"-'"::: )  (Num 1)))) ; 
 begin  definitionlet "n" be   ($#m1_hidden :::"Nat":::); func  :::"Fermat"::: "n" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) equals :: PEPIN:def 3 (Set (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  "n" ")" ) ")" )  ($#k1_nat_1 :::"+"::: )  (Num 1)); end; 





:: deftheorem    defines :::"Fermat"::: PEPIN:def 3 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k4_pepin :::"Fermat"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" ) ")" )  ($#k1_nat_1 :::"+"::: )  (Num 1)))); 
 
theorem :: PEPIN:50 (Bool (Set   ($#k4_pepin :::"Fermat"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Num 3)) ; 
 
theorem :: PEPIN:51 (Bool (Set   ($#k4_pepin :::"Fermat"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Num 5)) ; 
 
theorem :: PEPIN:52 (Bool (Set   ($#k4_pepin :::"Fermat"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Num 17)) ; 
 
theorem :: PEPIN:53 (Bool (Set   ($#k4_pepin :::"Fermat"::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Num 257)) ; 
 
theorem :: PEPIN:54 (Bool (Set   ($#k4_pepin :::"Fermat"::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 256)  ($#k4_nat_1 :::"*"::: )  (Num 256) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))) ; 
 
theorem :: PEPIN:55 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set   ($#k4_pepin :::"Fermat"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Num 2))) ; 
 
theorem :: PEPIN:56 (Bool  "for" (Set (Var "p")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 2)) & (Bool (Set (Var "p"))  ($#r1_nat_d :::"divides"::: )  (Set   ($#k4_pepin :::"Fermat"::: )  (Set (Var "n"))))) "holds"  (Bool  "ex" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "k"))  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Num 2)  ($#k13_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))))) ; 
 
theorem :: PEPIN:57 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Num 3) "," (Set   ($#k4_pepin :::"Fermat"::: )  (Set (Var "n")))  ($#r1_int_2 :::"are_relative_prime"::: )  )) ; 
 begin  
theorem :: PEPIN:58 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Num 3)  ($#k13_newton :::"|^"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_pepin :::"Fermat"::: )  (Set (Var "n")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )  ($#k3_nat_d :::"div"::: )  (Num 2) ")" )) "," (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set   ($#k4_pepin :::"Fermat"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k4_pepin :::"Fermat"::: )  (Set (Var "n"))) "is"   ($#v1_int_2 :::"prime"::: )  )) ; 
 
theorem :: PEPIN:59 (Bool (Num 5) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: PEPIN:60 (Bool (Num 17) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: PEPIN:61 (Bool (Num 257) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: PEPIN:62 (Bool (Set (Set  "(" (Num 256)  ($#k4_nat_1 :::"*"::: )  (Num 256) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)) "is"   ($#v1_int_2 :::"prime"::: )  ) ; 
 
theorem :: PEPIN:63 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "i"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "i"))  ($#k3_nat_d :::"div"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "j"))))) ; 
 
theorem :: PEPIN:64 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k3_nat_d :::"div"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "i"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "i"))))) ; 
 



theorem :: PEPIN:65 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "holds"  (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: PEPIN:66 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::">"::: )  (Set (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ;