:: INT_1  semantic presentation begin  













definitionredefine func  :::"INT":::  means :: INT_1:def 1 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "k"))) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set (Var "k"))))  ")" ))  ")" )); end; 




:: deftheorem    defines :::"INT"::: INT_1:def 1 :  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_numbers :::"INT"::: )  )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) "iff" (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "k"))) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set (Var "k"))))  ")" ))  ")" ))  ")" )); 
 definitionlet "i" be    ($#m1_hidden :::"number"::: )  ; attr "i" is  :::"integer":::  means :: INT_1:def 2 (Bool "i"  ($#r2_hidden :::"in"::: )  (Set   ($#k4_numbers :::"INT"::: )  )); end; 




:: deftheorem    defines :::"integer"::: INT_1:def 2 :  (Bool  "for" (Set (Var "i")) "being"    ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "i")) "is"   ($#v1_int_1 :::"integer"::: )  ) "iff" (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_numbers :::"INT"::: )  ))  ")" )); 
 registration
cluster   ($#v1_xxreal_0 :::"ext-real"::: )   bbbadV1_XCMPLX_0()   ($#v1_xreal_0 :::"real"::: )     ($#v1_int_1 :::"integer"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); 

cluster   ($#v1_int_1 :::"integer"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ->   ($#v1_int_1 :::"integer"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ); 
end; definitionmode Integer is   ($#v1_int_1 :::"integer"::: )     ($#m1_hidden :::"number"::: )  ; end; 
theorem :: INT_1:1 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool  "("  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Var "k"))) "or" (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "k"))))  ")" )) "holds"  (Bool (Set (Var "r")) "is"   ($#m1_hidden :::"Integer":::)))) ; 
 
theorem :: INT_1:2 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r")) "is"   ($#m1_hidden :::"Integer":::))) "holds"  (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Var "k"))) "or" (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set (Var "k"))))  ")" ))) ; 
 registration
cluster   ($#v7_ordinal1 :::"natural"::: )    ->   ($#v1_int_1 :::"integer"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster   ($#v1_int_1 :::"integer"::: )    ->   ($#v1_xreal_0 :::"real"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 











registrationlet "i1", "i2" be   ($#m1_hidden :::"Integer":::); 
cluster (Set "i1"  ($#k2_xcmplx_0 :::"+"::: )  "i2") ->   ($#v1_int_1 :::"integer"::: )   ; 

cluster (Set "i1"  ($#k3_xcmplx_0 :::"*"::: )  "i2") ->   ($#v1_int_1 :::"integer"::: )   ; 
end; registrationlet "i0" be   ($#m1_hidden :::"Integer":::); 
cluster (Set   ($#k4_xcmplx_0 :::"-"::: )  "i0") ->   ($#v1_int_1 :::"integer"::: )   ; 
end; registrationlet "i1", "i2" be   ($#m1_hidden :::"Integer":::); 
cluster (Set "i1"  ($#k6_xcmplx_0 :::"-"::: )  "i2") ->   ($#v1_int_1 :::"integer"::: )   ; 
end; 
theorem :: INT_1:3 (Bool  "for" (Set (Var "i0")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i0")))) "holds"  (Bool (Set (Var "i0"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))) ; 
 
theorem :: INT_1:4 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r")) "is"   ($#m1_hidden :::"Integer":::))) "holds"  (Bool  "("  (Bool (Set (Set (Var "r"))  ($#k3_real_1 :::"+"::: )  (Num 1)) "is"   ($#m1_hidden :::"Integer":::)) & (Bool (Set (Set (Var "r"))  ($#k5_real_1 :::"-"::: )  (Num 1)) "is"   ($#m1_hidden :::"Integer":::))  ")" )) ; 
 
theorem :: INT_1:5 (Bool  "for" (Set (Var "i2")) "," (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1")))) "holds"  (Bool (Set (Set (Var "i1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "i2")))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))) ; 
 
theorem :: INT_1:6 (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Set (Var "i1"))  ($#k3_real_1 :::"+"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Var "i2")))) "holds"  (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))))) ; 
 
theorem :: INT_1:7 (Bool  "for" (Set (Var "i0")) "," (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i0"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i1")))) "holds"  (Bool (Set (Set (Var "i0"))  ($#k3_real_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1")))) ; 
 
theorem :: INT_1:8 (Bool  "for" (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))) ; 
 
theorem :: INT_1:9 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "i1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i2")))  ($#r1_hidden :::"="::: )  (Num 1)) "iff" (Bool  "("  (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "i2"))  ($#r1_hidden :::"="::: )  (Num 1))  ")" ) "or" (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Var "i2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))  ")" )  ")" )  ")" )) ; 
 
theorem :: INT_1:10 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "i1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i2")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) "iff" (Bool  "("  (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Var "i2"))  ($#r1_hidden :::"="::: )  (Num 1))  ")" ) "or" (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "i2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))  ")" )  ")" )  ")" )) ; 
 scheme  :: INT_1:sch 1 SepInt{ P1[  ($#m1_hidden :::"Integer":::)] } : 
(Bool  "ex" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k4_numbers :::"INT"::: ) ) "st"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "iff" (Bool P1[(Set (Var "x"))])  ")" )))
 proof 


end; scheme  :: INT_1:sch 2 IntIndUp{ F1() ->   ($#m1_hidden :::"Integer":::), P1[  ($#m1_hidden :::"Integer":::)] } : 
(Bool  "for" (Set (Var "i0")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set F1 "("  ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i0")))) "holds"  (Bool P1[(Set (Var "i0"))]))
 provided
(Bool P1[(Set F1 "("  ")" )])
 and  
(Bool  "for" (Set (Var "i2")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set F1 "("  ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool P1[(Set (Var "i2"))])) "holds"  (Bool P1[(Set (Set (Var "i2"))  ($#k3_real_1 :::"+"::: )  (Num 1))]))
 proof 


end; scheme  :: INT_1:sch 3 IntIndDown{ F1() ->   ($#m1_hidden :::"Integer":::), P1[  ($#m1_hidden :::"Integer":::)] } : 
(Bool  "for" (Set (Var "i0")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i0"))  ($#r1_xxreal_0 :::"<="::: )  (Set F1 "("  ")" ))) "holds"  (Bool P1[(Set (Var "i0"))]))
 provided
(Bool P1[(Set F1 "("  ")" )])
 and  
(Bool  "for" (Set (Var "i2")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set F1 "("  ")" )) & (Bool P1[(Set (Var "i2"))])) "holds"  (Bool P1[(Set (Set (Var "i2"))  ($#k5_real_1 :::"-"::: )  (Num 1))]))
 proof 


end; scheme  :: INT_1:sch 4 IntIndFull{ F1() ->   ($#m1_hidden :::"Integer":::), P1[  ($#m1_hidden :::"Integer":::)] } : 
(Bool  "for" (Set (Var "i0")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool P1[(Set (Var "i0"))]))
 provided
(Bool P1[(Set F1 "("  ")" )])
 and  
(Bool  "for" (Set (Var "i2")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool P1[(Set (Var "i2"))])) "holds"  (Bool  "("  (Bool P1[(Set (Set (Var "i2"))  ($#k5_real_1 :::"-"::: )  (Num 1))]) & (Bool P1[(Set (Set (Var "i2"))  ($#k3_real_1 :::"+"::: )  (Num 1))])  ")" ))
 proof 


end; scheme  :: INT_1:sch 5 IntMin{ F1() ->   ($#m1_hidden :::"Integer":::), P1[  ($#m1_hidden :::"Integer":::)] } : 
(Bool  "ex" (Set (Var "i0")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool P1[(Set (Var "i0"))]) & (Bool  "("   "for" (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool P1[(Set (Var "i1"))])) "holds"  (Bool (Set (Var "i0"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1")))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool P1[(Set (Var "i1"))])) "holds"  (Bool (Set F1 "("  ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))))
 and  
(Bool  "ex" (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool P1[(Set (Var "i1"))]))
 proof 


end; scheme  :: INT_1:sch 6 IntMax{ F1() ->   ($#m1_hidden :::"Integer":::), P1[  ($#m1_hidden :::"Integer":::)] } : 
(Bool  "ex" (Set (Var "i0")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool P1[(Set (Var "i0"))]) & (Bool  "("   "for" (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool P1[(Set (Var "i1"))])) "holds"  (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i0")))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool P1[(Set (Var "i1"))])) "holds"  (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set F1 "("  ")" )))
 and  
(Bool  "ex" (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool P1[(Set (Var "i1"))]))
 proof 


end; definitionlet "i1", "i2" be   ($#m1_hidden :::"Integer":::); pred "i1" :::"divides"::: "i2" means :: INT_1:def 3 (Bool  "ex" (Set (Var "i3")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool "i2"  ($#r1_hidden :::"="::: )  (Set "i1"  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i3"))))); reflexivity  
(Bool  "for" (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::) (Bool  "ex" (Set (Var "i3")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i3"))))))
 ; end; 





:: deftheorem    defines :::"divides"::: INT_1:def 3 :  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_int_1 :::"divides"::: )  (Set (Var "i2"))) "iff" (Bool  "ex" (Set (Var "i3")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "i2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i3")))))  ")" )); 
 definitionlet "i1", "i2", "i3" be   ($#m1_hidden :::"Integer":::); pred "i1" "," "i2" :::"are_congruent_mod"::: "i3" means :: INT_1:def 4 (Bool "i3"  ($#r1_int_1 :::"divides"::: )  (Set "i1"  ($#k6_xcmplx_0 :::"-"::: )  "i2")); end; 






:: deftheorem    defines :::"are_congruent_mod"::: INT_1:def 4 :  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "i1")) "," (Set (Var "i2"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i3"))) "iff" (Bool (Set (Var "i3"))  ($#r1_int_1 :::"divides"::: )  (Set (Set (Var "i1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "i2"))))  ")" )); 
 definitionlet "i1", "i2", "i3" be   ($#m1_hidden :::"Integer":::); redefine pred "i1" "," "i2" :::"are_congruent_mod"::: "i3" means :: INT_1:def 5 (Bool  "ex" (Set (Var "i4")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set "i3"  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i4")))  ($#r1_hidden :::"="::: )  (Set "i1"  ($#k6_xcmplx_0 :::"-"::: )  "i2"))); end; 






:: deftheorem    defines :::"are_congruent_mod"::: INT_1:def 5 :  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "i1")) "," (Set (Var "i2"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i3"))) "iff" (Bool  "ex" (Set (Var "i4")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Set (Var "i3"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i4")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "i2")))))  ")" )); 
 
theorem :: INT_1:11 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Var "i1")) "," (Set (Var "i1"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i2")))) ; 
 
theorem :: INT_1:12 (Bool  "for" (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "i1")) "," (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i1"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  ) "," (Set (Var "i1"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i1")))  ")" )) ; 
 
theorem :: INT_1:13 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Var "i1")) "," (Set (Var "i2"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Num 1))) ; 
 
theorem :: INT_1:14 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i1")) "," (Set (Var "i2"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i3")))) "holds"  (Bool (Set (Var "i2")) "," (Set (Var "i1"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i3")))) ; 
 
theorem :: INT_1:15 (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 "i2")) "," (Set (Var "i3"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5")))) "holds"  (Bool (Set (Var "i1")) "," (Set (Var "i3"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5")))) ; 
 
theorem :: INT_1:16 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i5")) "," (Set (Var "i3")) "," (Set (Var "i4")) "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 "i3")) "," (Set (Var "i4"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5")))) "holds"  (Bool (Set (Set (Var "i1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i3"))) "," (Set (Set (Var "i2"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i4")))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5")))) ; 
 
theorem :: INT_1:17 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i5")) "," (Set (Var "i3")) "," (Set (Var "i4")) "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 "i3")) "," (Set (Var "i4"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5")))) "holds"  (Bool (Set (Set (Var "i1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "i3"))) "," (Set (Set (Var "i2"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "i4")))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5")))) ; 
 
theorem :: INT_1:18 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i5")) "," (Set (Var "i3")) "," (Set (Var "i4")) "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 "i3")) "," (Set (Var "i4"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5")))) "holds"  (Bool (Set (Set (Var "i1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i3"))) "," (Set (Set (Var "i2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i4")))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5")))) ; 
 
theorem :: INT_1:19 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i5")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "i1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i2"))) "," (Set (Var "i3"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5"))) "iff" (Bool (Set (Var "i1")) "," (Set (Set (Var "i3"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "i2")))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5")))  ")" )) ; 
 
theorem :: INT_1:20 (Bool  "for" (Set (Var "i4")) "," (Set (Var "i5")) "," (Set (Var "i3")) "," (Set (Var "i1")) "," (Set (Var "i2")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Set (Var "i4"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i5")))  ($#r1_hidden :::"="::: )  (Set (Var "i3"))) & (Bool (Set (Var "i1")) "," (Set (Var "i2"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i3")))) "holds"  (Bool (Set (Var "i1")) "," (Set (Var "i2"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i4")))) ; 
 
theorem :: INT_1:21 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i5")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "i1")) "," (Set (Var "i2"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5"))) "iff" (Bool (Set (Set (Var "i1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i5"))) "," (Set (Var "i2"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5")))  ")" )) ; 
 
theorem :: INT_1:22 (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i5")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "i1")) "," (Set (Var "i2"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5"))) "iff" (Bool (Set (Set (Var "i1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "i5"))) "," (Set (Var "i2"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "i5")))  ")" )) ; 
 
theorem :: INT_1:23 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Set (Var "r"))  ($#k5_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i1"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Set (Var "r"))  ($#k5_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i2")))) "holds"  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))))) ; 
 
theorem :: INT_1:24 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i1"))) & (Bool (Set (Var "i1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "r"))  ($#k3_real_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i2"))) & (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "r"))  ($#k3_real_1 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))))) ; 
 










definitionlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func :::"[\":::"r":::"/]"::: ->   ($#m1_hidden :::"Integer":::) means :: INT_1:def 6 (Bool  "("  (Bool it  ($#r1_xxreal_0 :::"<="::: )  "r") & (Bool (Set "r"  ($#k5_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  it)  ")" ); projectivity  
(Bool  "for" (Set (Var "b1")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b2"))) & (Bool (Set (Set (Var "b2"))  ($#k5_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b1")))) "holds"  (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b1"))) & (Bool (Set (Set (Var "b1"))  ($#k5_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b1")))  ")" )))
 ; end; 





:: deftheorem    defines :::"[\"::: INT_1:def 6 :  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )) "iff" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Set (Var "r"))  ($#k5_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b2")))  ")" )  ")" ))); 
 
theorem :: INT_1:25 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "r"))) "iff" (Bool (Set (Var "r")) "is"   ($#v1_int_1 :::"integer"::: )  )  ")" )) ; 
 
theorem :: INT_1:26 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) "iff" (Bool  "not" (Bool (Set (Var "r")) "is"   ($#v1_int_1 :::"integer"::: )  ))  ")" )) ; 
 
theorem :: INT_1:27 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#k5_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "r"))  ($#k3_real_1 :::"+"::: )  (Num 1)))  ")" )) ; 
 
theorem :: INT_1:28 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i0")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i0")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set (Var "r"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i0")) ")" ) ($#k1_int_1 :::"/]"::: ) )))) ; 
 
theorem :: INT_1:29 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "holds" (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#k3_real_1 :::"+"::: )  (Num 1)))) ; 
 definitionlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func :::"[/":::"r":::"\]"::: ->   ($#m1_hidden :::"Integer":::) means :: INT_1:def 7 (Bool  "("  (Bool "r"  ($#r1_xxreal_0 :::"<="::: )  it) & (Bool it  ($#r1_xxreal_0 :::"<"::: )  (Set "r"  ($#k3_real_1 :::"+"::: )  (Num 1)))  ")" ); projectivity  
(Bool  "for" (Set (Var "b1")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b2"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b1"))) & (Bool (Set (Var "b1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "b2"))  ($#k3_real_1 :::"+"::: )  (Num 1)))) "holds"  (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b1"))) & (Bool (Set (Var "b1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "b1"))  ($#k3_real_1 :::"+"::: )  (Num 1)))  ")" )))
 ; end; 





:: deftheorem    defines :::"[/"::: INT_1:def 7 :  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) )) "iff" (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b2"))) & (Bool (Set (Var "b2"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "r"))  ($#k3_real_1 :::"+"::: )  (Num 1)))  ")" )  ")" ))); 
 
theorem :: INT_1:30 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "r"))) "iff" (Bool (Set (Var "r")) "is"   ($#v1_int_1 :::"integer"::: )  )  ")" )) ; 
 
theorem :: INT_1:31 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) )) "iff" (Bool  "not" (Bool (Set (Var "r")) "is"   ($#v1_int_1 :::"integer"::: )  ))  ")" )) ; 
 
theorem :: INT_1:32 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Set (Var "r"))  ($#k5_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) )) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) )  ($#k3_real_1 :::"+"::: )  (Num 1)))  ")" )) ; 
 
theorem :: INT_1:33 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i0")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i0")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_int_1 :::"[/"::: ) (Set  "(" (Set (Var "r"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i0")) ")" ) ($#k2_int_1 :::"\]"::: ) )))) ; 
 
theorem :: INT_1:34 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) )) "iff" (Bool (Set (Var "r")) "is"   ($#v1_int_1 :::"integer"::: )  )  ")" )) ; 
 
theorem :: INT_1:35 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) )) "iff" (Bool  "not" (Bool (Set (Var "r")) "is"   ($#v1_int_1 :::"integer"::: )  ))  ")" )) ; 
 
theorem :: INT_1:36 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) ))) ; 
 
theorem :: INT_1:37 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) ) ($#k1_int_1 :::"/]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) ))) ; 
 
theorem :: INT_1:38 canceled; 
 
theorem :: INT_1:39 canceled; 
 
theorem :: INT_1:40 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k2_int_1 :::"[/"::: ) (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) ) ($#k2_int_1 :::"\]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) ))) ; 
 
theorem :: INT_1:41 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) )) "iff" (Bool (Bool  "not" (Set (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#k3_real_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) )))  ")" )) ; 
 definitionlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"frac"::: "r" ->    ($#m1_hidden :::"set"::: )   equals :: INT_1:def 8 (Set "r"  ($#k6_xcmplx_0 :::"-"::: )  (Set  ($#k1_int_1 :::"[\"::: ) "r" ($#k1_int_1 :::"/]"::: ) )); end; 





:: deftheorem    defines :::"frac"::: INT_1:def 8 :  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_int_1 :::"frac"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )))); 
 registrationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k3_int_1 :::"frac"::: )  "r") ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; definitionlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"frac"::: redefine func  :::"frac"::: "r" ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: INT_1:42 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#k3_real_1 :::"+"::: )  (Set  "("  ($#k4_int_1 :::"frac"::: )  (Set (Var "r")) ")" )))) ; 
 
theorem :: INT_1:43 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "r"))))  ")" )) ; 
 
theorem :: INT_1:44 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set  "("  ($#k4_int_1 :::"frac"::: )  (Set (Var "r")) ")" ) ($#k1_int_1 :::"/]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: INT_1:45 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set (Var "r")) "is"   ($#v1_int_1 :::"integer"::: )  )  ")" )) ; 
 
theorem :: INT_1:46 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "r")))) "iff" (Bool  "not" (Bool (Set (Var "r")) "is"   ($#v1_int_1 :::"integer"::: )  ))  ")" )) ; 
 definitionlet "i1", "i2" be   ($#m1_hidden :::"Integer":::); func "i1" :::"div"::: "i2" ->   ($#m1_hidden :::"Integer":::) equals :: INT_1:def 9 (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" "i1"  ($#k7_xcmplx_0 :::"/"::: )  "i2" ")" ) ($#k1_int_1 :::"/]"::: ) ); end; 






:: deftheorem    defines :::"div"::: INT_1:def 9 :  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set (Var "i1"))  ($#k5_int_1 :::"div"::: )  (Set (Var "i2")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set (Var "i1"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "i2")) ")" ) ($#k1_int_1 :::"/]"::: ) ))); 
 definitionlet "i1", "i2" be   ($#m1_hidden :::"Integer":::); func "i1" :::"mod"::: "i2" ->   ($#m1_hidden :::"Integer":::) equals :: INT_1:def 10 (Set "i1"  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" "i1"  ($#k5_int_1 :::"div"::: )  "i2" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "i2" ")" )) if (Bool "i2"  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  otherwise (Set   ($#k6_numbers :::"0"::: )  ); end; 






:: deftheorem    defines :::"mod"::: INT_1:def 10 :  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "i2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Set (Var "i1"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "i2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "i1"))  ($#k5_int_1 :::"div"::: )  (Set (Var "i2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i2")) ")" )))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "i2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool (Set (Set (Var "i1"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "i2")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" )); 
 
theorem :: INT_1:47 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set (Var "r"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "r")) ")" ) ($#k1_int_1 :::"/]"::: ) )  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: INT_1:48 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set (Var "i"))  ($#k5_int_1 :::"div"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: INT_1:49 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "i"))  ($#k5_int_1 :::"div"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: INT_1:50 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set (Var "i"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 begin  
theorem :: INT_1:51 (Bool  "for" (Set (Var "k")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i")))) "holds"  (Bool  "ex" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "j"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "k")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j")))  ")" ))) ; 
 
theorem :: INT_1:52 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "b"))  ($#k5_real_1 :::"-"::: )  (Num 1)))) ; 
 
theorem :: INT_1:53 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) ) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )) & (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) ) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ))  ")" )) ; 
 
theorem :: INT_1:54 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))) "holds"  (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )))) ; 
 
theorem :: INT_1:55 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "m"))  ($#k5_int_1 :::"div"::: )  (Set (Var "n"))))) ; 
 
theorem :: INT_1:56 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j")))) "holds"  (Bool (Set (Set (Var "i"))  ($#k5_int_1 :::"div"::: )  (Set (Var "j")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i")))) ; 
 
theorem :: INT_1:57 (Bool  "for" (Set (Var "i2")) "," (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "i1"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "i2")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: INT_1:58 (Bool  "for" (Set (Var "i2")) "," (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "i1"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "i2")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i2")))) ; 
 
theorem :: INT_1:59 (Bool  "for" (Set (Var "i2")) "," (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "i1"))  ($#k5_int_1 :::"div"::: )  (Set (Var "i2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "i1"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "i2")) ")" )))) ; 
 
theorem :: INT_1:60 (Bool  "for" (Set (Var "m")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "j"))) "," (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "m")))) ; 
 
theorem :: INT_1:61 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "i"))  ($#k5_int_1 :::"div"::: )  (Set (Var "j")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: INT_1:62 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set (Var "n"))  ($#r1_int_1 :::"divides"::: )  (Set (Var "a")))  ")" ))) ; 
 




theorem :: INT_1:63 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "r"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "s"))) "is" (Bool  "not"   ($#m1_hidden :::"Integer":::)))) "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set (Var "r"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "s")) ")" ) ($#k1_int_1 :::"/]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "s")) ")" ) ($#k1_int_1 :::"/]"::: ) )  ($#k3_real_1 :::"+"::: )  (Num 1)))) ; 
 
theorem :: INT_1:64 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "r"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "s"))) "is"   ($#m1_hidden :::"Integer":::))) "holds"  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set (Var "r"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "s")) ")" ) ($#k1_int_1 :::"/]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "s")) ")" ) ($#k1_int_1 :::"/]"::: ) ))) ; 
 
theorem :: INT_1:65 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))) "holds"  (Bool (Set  ($#k2_int_1 :::"[/"::: ) (Set (Var "r")) ($#k2_int_1 :::"\]"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))))) ; 
 scheme  :: INT_1:sch 7 FinInd{ F1() ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ), F2() ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ), P1[  ($#m1_hidden :::"Nat":::)] } : 
(Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set F1 "("  ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set F2 "("  ")" ))) "holds"  (Bool P1[(Set (Var "i"))]))
 provided
(Bool P1[(Set F1 "("  ")" )])
 and  
(Bool  "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set F1 "("  ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set F2 "("  ")" )) & (Bool P1[(Set (Var "j"))])) "holds"  (Bool P1[(Set (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1))]))
 proof 


end; scheme  :: INT_1:sch 8 FinInd2{ F1() ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ), F2() ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ), P1[  ($#m1_hidden :::"Nat":::)] } : 
(Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set F1 "("  ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set F2 "("  ")" ))) "holds"  (Bool P1[(Set (Var "i"))]))
 provided
(Bool P1[(Set F1 "("  ")" )])
 and  
(Bool  "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set F1 "("  ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "j9")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set F1 "("  ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j9"))) & (Bool (Set (Var "j9"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j")))) "holds"  (Bool P1[(Set (Var "j9"))])  ")" )) "holds"  (Bool P1[(Set (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1))]))
 proof 


end; 









theorem :: INT_1:66 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_int_1 :::"frac"::: )  (Set  "(" (Set (Var "r"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "r")))))) ; 
 
theorem :: INT_1:67 (Bool  "for" (Set (Var "r")) "," (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#k3_real_1 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "a")) ($#k1_int_1 :::"/]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) ))) ; 
 
theorem :: INT_1:68 (Bool  "for" (Set (Var "r")) "," (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#k3_real_1 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "a"))))) ; 
 
theorem :: INT_1:69 (Bool  "for" (Set (Var "r")) "," (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#k3_real_1 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "a"))))) ; 
 
theorem :: INT_1:70 (Bool  "for" (Set (Var "a")) "," (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#k3_real_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "r"))  ($#k3_real_1 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "a")) ($#k1_int_1 :::"/]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#k3_real_1 :::"+"::: )  (Num 1)))) ; 
 
theorem :: INT_1:71 (Bool  "for" (Set (Var "a")) "," (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#k3_real_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "r"))  ($#k3_real_1 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "r"))))) ; 
 
theorem :: INT_1:72 (Bool  "for" (Set (Var "r")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "r"))  ($#k3_real_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "r"))  ($#k3_real_1 :::"+"::: )  (Num 1))) & (Bool (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "b"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ;