:: PYTHTRIP  semantic presentation begin  















definitionlet "m", "n" be   ($#m1_hidden :::"Nat":::); redefine pred "m" "," "n" :::"are_relative_prime":::  means :: PYTHTRIP:def 1 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_nat_d :::"divides"::: )  "m") & (Bool (Set (Var "k"))  ($#r1_nat_d :::"divides"::: )  "n")) "holds"  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Num 1))); end; 





:: deftheorem    defines :::"are_relative_prime"::: PYTHTRIP:def 1 :  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "m")) "," (Set (Var "n"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) "iff" (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "m"))) & (Bool (Set (Var "k"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Num 1)))  ")" )); 
 definitionlet "m", "n" be   ($#m1_hidden :::"Nat":::); redefine pred "m" "," "n" :::"are_relative_prime":::  means :: PYTHTRIP:def 2 (Bool  "for" (Set (Var "p")) "being"   ($#v1_int_2 :::"prime"::: )    ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "p"))  ($#r1_nat_d :::"divides"::: )  "m") "or"  "not" (Bool (Set (Var "p"))  ($#r1_nat_d :::"divides"::: )  "n")  ")" )); end; 





:: deftheorem    defines :::"are_relative_prime"::: PYTHTRIP:def 2 :  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "m")) "," (Set (Var "n"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#v1_int_2 :::"prime"::: )    ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "p"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "m"))) "or"  "not" (Bool (Set (Var "p"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n")))  ")" ))  ")" )); 
 begin  definitionlet "n" be    ($#m1_hidden :::"number"::: )  ; attr "n" is  :::"square":::  means :: PYTHTRIP:def 3 (Bool  "ex" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool "n"  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k1_pepin :::"^2"::: )  ))); end; 




:: deftheorem    defines :::"square"::: PYTHTRIP:def 3 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "n")) "is"   ($#v1_pythtrip :::"square"::: )  ) "iff" (Bool  "ex" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k1_pepin :::"^2"::: )  )))  ")" )); 
 registration
cluster   ($#v1_pythtrip :::"square"::: )    ->   ($#v7_ordinal1 :::"natural"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "n"  ($#k3_square_1 :::"^2"::: )  ) ->   ($#v1_pythtrip :::"square"::: )   ; 
end; registration
cluster   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )     ($#v3_ordinal1 :::"ordinal"::: )     ($#v7_ordinal1 :::"natural"::: )   bbbadV1_XCMPLX_0() bbbadV1_XREAL_0()   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_int_1 :::"integer"::: )     ($#v1_abian :::"even"::: )     ($#v1_pythtrip :::"square"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
end; registration
cluster   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )     ($#v3_ordinal1 :::"ordinal"::: )     ($#v7_ordinal1 :::"natural"::: )   bbbadV1_XCMPLX_0() bbbadV1_XREAL_0()   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_int_1 :::"integer"::: )     ($#v1_abian :::"odd"::: )     ($#v1_pythtrip :::"square"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
end; registration
cluster bbbadV1_XCMPLX_0() bbbadV1_XREAL_0()   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v1_int_1 :::"integer"::: )     ($#v1_abian :::"even"::: )     ($#v1_pythtrip :::"square"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster bbbadV1_XCMPLX_0() bbbadV1_XREAL_0()   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v1_int_1 :::"integer"::: )     ($#v1_abian :::"odd"::: )     ($#v1_pythtrip :::"square"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "m", "n" be   ($#v1_pythtrip :::"square"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "m"  ($#k3_xcmplx_0 :::"*"::: )  "n") ->   ($#v1_pythtrip :::"square"::: )   ; 
end; 
theorem :: PYTHTRIP:1 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "m"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "n"))) "is"   ($#v1_pythtrip :::"square"::: )  ) & (Bool (Set (Var "m")) "," (Set (Var "n"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "m")) "is"   ($#v1_pythtrip :::"square"::: )  ) & (Bool (Set (Var "n")) "is"   ($#v1_pythtrip :::"square"::: )  )  ")" )) ; 
 registrationlet "i" be   ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k3_square_1 :::"^2"::: )  ) ->   ($#v1_int_1 :::"integer"::: )   ; 
end; registrationlet "i" be   ($#v1_abian :::"even"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k3_square_1 :::"^2"::: )  ) ->   ($#v1_abian :::"even"::: )   ; 
end; registrationlet "i" be   ($#v1_abian :::"odd"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "i"  ($#k3_square_1 :::"^2"::: )  ) ->   ($#v1_abian :::"odd"::: )   ; 
end; 
theorem :: PYTHTRIP:2 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "i")) "is"   ($#v1_abian :::"even"::: )  ) "iff" (Bool (Set (Set (Var "i"))  ($#k1_pepin :::"^2"::: )  ) "is"   ($#v1_abian :::"even"::: )  )  ")" )) ; 
 
theorem :: PYTHTRIP:3 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i")) "is"   ($#v1_abian :::"even"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k1_pepin :::"^2"::: )  ")" )  ($#k4_nat_d :::"mod"::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: PYTHTRIP:4 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i")) "is"   ($#v1_abian :::"odd"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k1_pepin :::"^2"::: )  ")" )  ($#k4_nat_d :::"mod"::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 registrationlet "m", "n" be   ($#v1_abian :::"odd"::: )     ($#v1_pythtrip :::"square"::: )    ($#m1_hidden :::"Integer":::); 
cluster (Set "m"  ($#k2_xcmplx_0 :::"+"::: )  "n") ->  ($#~v1_pythtrip  "non"   ($#v1_pythtrip :::"square"::: )   )  ; 
end; 
theorem :: PYTHTRIP:5 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "m"))  ($#k1_pepin :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_pepin :::"^2"::: )  ))) "holds"  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) ; 
 
theorem :: PYTHTRIP:6 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "m"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n"))) "iff" (Bool (Set (Set (Var "m"))  ($#k1_pepin :::"^2"::: )  )  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "n"))  ($#k1_pepin :::"^2"::: )  ))  ")" )) ; 
 begin  
theorem :: PYTHTRIP:7 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n"))) "or" (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "iff" (Bool (Set (Set (Var "k"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "m")))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "k"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "n"))))  ")" )) ; 
 
theorem :: PYTHTRIP:8 (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "k"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "m")) ")" )  ($#k6_nat_d :::"gcd"::: )  (Set  "(" (Set (Var "k"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set (Var "m"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "n")) ")" )))) ; 
 begin  
theorem :: PYTHTRIP:9 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) (Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m"))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" ))  ")" )) "holds"  (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"infinite"::: )  )) ; 
 begin  
theorem :: PYTHTRIP:10 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) "or" (Bool (Set (Var "a")) "is"   ($#v1_abian :::"odd"::: )  ) "or" (Bool (Set (Var "b")) "is"   ($#v1_abian :::"odd"::: )  )  ")" )) ; 
 
theorem :: PYTHTRIP:11 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_pepin :::"^2"::: )  ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_pepin :::"^2"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k1_pepin :::"^2"::: )  )) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "a")) "is"   ($#v1_abian :::"odd"::: )  )) "holds"  (Bool  "ex" (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 (Var "n"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k1_pepin :::"^2"::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "m"))  ($#k1_pepin :::"^2"::: )  ")" ))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "m")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k1_pepin :::"^2"::: )  ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set (Var "m"))  ($#k1_pepin :::"^2"::: )  ")" )))  ")" ))) ; 
 
theorem :: PYTHTRIP:12 (Bool  "for" (Set (Var "a")) "," (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k1_pepin :::"^2"::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "m"))  ($#k1_pepin :::"^2"::: )  ")" ))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "m")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k1_pepin :::"^2"::: )  ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set (Var "m"))  ($#k1_pepin :::"^2"::: )  ")" )))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_pepin :::"^2"::: )  ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_pepin :::"^2"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k1_pepin :::"^2"::: )  ))) ; 
 definitionmode  :::"Pythagorean_triple":::  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) means :: PYTHTRIP:def 4 (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_pepin :::"^2"::: )  ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_pepin :::"^2"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k1_pepin :::"^2"::: )  )) & (Bool it  ($#r1_hidden :::"="::: )  (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k8_domain_1 :::"}"::: ) ))  ")" )); end; 




:: deftheorem    defines :::"Pythagorean_triple"::: PYTHTRIP:def 4 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b1")) "is"    ($#m1_pythtrip :::"Pythagorean_triple"::: )  ) "iff" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_pepin :::"^2"::: )  ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_pepin :::"^2"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k1_pepin :::"^2"::: )  )) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k8_domain_1 :::"}"::: ) ))  ")" ))  ")" )); 
 


registration
cluster   ->   ($#v1_finset_1 :::"finite"::: )    for    ($#m1_pythtrip :::"Pythagorean_triple"::: )  ; 
end; definitionredefine mode  :::"Pythagorean_triple":::  means :: PYTHTRIP:def 5 (Bool  "ex" (Set (Var "k")) "," (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 (Var "n"))) & (Bool it  ($#r1_hidden :::"="::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set  "(" (Set (Var "k"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k1_pepin :::"^2"::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "m"))  ($#k1_pepin :::"^2"::: )  ")" ) ")" ) ")" ) "," (Set  "(" (Set (Var "k"))  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "m")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" ) ")" ) "," (Set  "(" (Set (Var "k"))  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k1_pepin :::"^2"::: )  ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set (Var "m"))  ($#k1_pepin :::"^2"::: )  ")" ) ")" ) ")" ) ($#k1_enumset1 :::"}"::: ) ))  ")" )); end; 




:: deftheorem    defines :::"Pythagorean_triple"::: PYTHTRIP:def 5 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b1")) "is"    ($#m1_pythtrip :::"Pythagorean_triple"::: )  ) "iff" (Bool  "ex" (Set (Var "k")) "," (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 (Var "n"))) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set  "(" (Set (Var "k"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k1_pepin :::"^2"::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "m"))  ($#k1_pepin :::"^2"::: )  ")" ) ")" ) ")" ) "," (Set  "(" (Set (Var "k"))  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "m")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" ) ")" ) "," (Set  "(" (Set (Var "k"))  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k1_pepin :::"^2"::: )  ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set (Var "m"))  ($#k1_pepin :::"^2"::: )  ")" ) ")" ) ")" ) ($#k1_enumset1 :::"}"::: ) ))  ")" ))  ")" )); 
 definitionlet "X" be    ($#m1_pythtrip :::"Pythagorean_triple"::: )  ; attr "X" is  :::"degenerate":::  means :: PYTHTRIP:def 6 (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_hidden :::"in"::: )  "X"); end; 




:: deftheorem    defines :::"degenerate"::: PYTHTRIP:def 6 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_pythtrip :::"Pythagorean_triple"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v2_pythtrip :::"degenerate"::: )  ) "iff" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" )); 
 
theorem :: PYTHTRIP:13 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 2))) "holds"  (Bool  "ex" (Set (Var "X")) "being"    ($#m1_pythtrip :::"Pythagorean_triple"::: )   "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v2_pythtrip :::"degenerate"::: )  )) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" ))) ; 
 definitionlet "X" be    ($#m1_pythtrip :::"Pythagorean_triple"::: )  ; attr "X" is  :::"simplified":::  means :: PYTHTRIP:def 7 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool (Set (Var "k"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n")))  ")" )) "holds"  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Num 1))); end; 




:: deftheorem    defines :::"simplified"::: PYTHTRIP:def 7 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_pythtrip :::"Pythagorean_triple"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v3_pythtrip :::"simplified"::: )  ) "iff" (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "k"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n")))  ")" )) "holds"  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Num 1)))  ")" )); 
 definitionlet "X" be    ($#m1_pythtrip :::"Pythagorean_triple"::: )  ; redefine attr "X" is  :::"simplified":::  means :: PYTHTRIP:def 8 (Bool  "ex" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "m")) "," (Set (Var "n"))  ($#r1_int_2 :::"are_relative_prime"::: )  )  ")" )); end; 




:: deftheorem    defines :::"simplified"::: PYTHTRIP:def 8 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_pythtrip :::"Pythagorean_triple"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v3_pythtrip :::"simplified"::: )  ) "iff" (Bool  "ex" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "m")) "," (Set (Var "n"))  ($#r1_int_2 :::"are_relative_prime"::: )  )  ")" ))  ")" )); 
 
theorem :: PYTHTRIP:14 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "X")) "being"    ($#m1_pythtrip :::"Pythagorean_triple"::: )   "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v2_pythtrip :::"degenerate"::: )  )) & (Bool (Set (Var "X")) "is"   ($#v3_pythtrip :::"simplified"::: )  ) & (Bool (Set (Num 4)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" ))) ; 
 registration
cluster   ($#v1_finset_1 :::"finite"::: )    ($#~v2_pythtrip  "non"   ($#v2_pythtrip :::"degenerate"::: )   )    ($#v3_pythtrip :::"simplified"::: )    for    ($#m1_pythtrip :::"Pythagorean_triple"::: )  ; 
end; 
theorem :: PYTHTRIP:15 (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Num 3) "," (Num 4) "," (Num 5) ($#k8_domain_1 :::"}"::: ) ) "is"  ($#~v2_pythtrip  "non"   ($#v2_pythtrip :::"degenerate"::: )   )    ($#v3_pythtrip :::"simplified"::: )     ($#m1_pythtrip :::"Pythagorean_triple"::: )  ) ; 
 
theorem :: PYTHTRIP:16 (Bool  "{"  (Set (Var "X")) where X "is"    ($#m1_pythtrip :::"Pythagorean_triple"::: )   : (Bool  "("  (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v2_pythtrip :::"degenerate"::: )  )) & (Bool (Set (Var "X")) "is"   ($#v3_pythtrip :::"simplified"::: )  )  ")" )  "}"   "is"   ($#v1_finset_1 :::"infinite"::: )  ) ;