:: REAL_3  semantic presentation begin  
























registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "n"  ($#k5_int_1 :::"div"::: )  (Set  ($#k6_numbers :::"0"::: ) )) ->   ($#v1_xboole_0 :::"zero"::: )   ; 

cluster (Set "n"  ($#k6_int_1 :::"mod"::: )  (Set  ($#k6_numbers :::"0"::: ) )) ->   ($#v1_xboole_0 :::"zero"::: )   ; 

cluster (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k5_int_1 :::"div"::: )  "n") ->   ($#v1_xboole_0 :::"zero"::: )   ; 

cluster (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k6_int_1 :::"mod"::: )  "n") ->   ($#v1_xboole_0 :::"zero"::: )   ; 
end; registrationlet "c" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "c"  ($#k6_xcmplx_0 :::"-"::: )  "c") ->   ($#v1_xboole_0 :::"zero"::: )   ; 

cluster (Set "c"  ($#k7_xcmplx_0 :::"/"::: )  (Set  ($#k6_numbers :::"0"::: ) )) ->   ($#v1_xboole_0 :::"zero"::: )   ; 
end; registration
cluster (Set  ($#k1_int_1 :::"[\"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_int_1 :::"/]"::: ) ) ->   ($#v1_xboole_0 :::"zero"::: )   ; 
end; 
theorem :: REAL_3:1 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) "holds"  (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "r"))))) ; 
 
theorem :: REAL_3:2 (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"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "i"))  ($#k3_real_1 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set (Var "r")) ($#k1_int_1 :::"/]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "i"))))) ; 
 
theorem :: REAL_3:3 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set (Var "m"))  ($#k13_complex1 :::"/"::: )  (Set (Var "n")) ")" ) ($#k1_int_1 :::"/]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k3_nat_d :::"div"::: )  (Set (Var "n"))))) ; 
 
theorem :: REAL_3:4 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "m"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "m"))  ($#k13_complex1 :::"/"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k3_nat_d :::"div"::: )  (Set (Var "n"))))) ; 
 
theorem :: REAL_3:5 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "m"))  ($#k13_complex1 :::"/"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k3_nat_d :::"div"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set (Var "m"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: REAL_3:6 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k4_int_1 :::"frac"::: )  (Set  "(" (Set (Var "m"))  ($#k13_complex1 :::"/"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "m"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")) ")" )  ($#k13_complex1 :::"/"::: )  (Set (Var "n"))))) ; 
 
theorem :: REAL_3:7 (Bool  "for" (Set (Var "p")) "being"   ($#v1_rat_1 :::"rational"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k13_complex1 :::"/"::: )  (Set (Var "n"))))  ")" ))) ; 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k1_numbers :::"REAL"::: )  )  ($#v5_relat_1 :::"-valued"::: )   (Set   ($#k4_numbers :::"INT"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_PARTFUN1((Set   ($#k5_numbers :::"NAT"::: )  )) bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k1_numbers :::"REAL"::: )  )) bbbadV1_VALUED_0() bbbadV2_VALUED_0() bbbadV3_VALUED_0()  for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ))))); 
end; definitionmode Integer_Sequence is (Set   ($#k4_numbers :::"INT"::: )  )  ($#v5_relat_1 :::"-valued"::: )    ($#m1_subset_1 :::"Real_Sequence":::); end; 
theorem :: REAL_3:8 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Integer_Sequence":::)) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))) "is"   ($#v1_int_1 :::"integer"::: )  )  ")" )  ")" )  ")" )) ; 
 
theorem :: REAL_3:9 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k4_numbers :::"INT"::: ) )) "iff" (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Integer_Sequence":::))  ")" )) ; 
 
theorem :: REAL_3:10 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) )) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))) "is"   ($#v7_ordinal1 :::"natural"::: )  )  ")" )  ")" )  ")" )) ; 
 
theorem :: REAL_3:11 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) )) "iff" (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ))  ")" )) ; 
 begin  definitionlet "m", "n" be   ($#m1_hidden :::"Nat":::); func  :::"modSeq":::  "(" "m" "," "n" ")"  ->   ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) means :: REAL_3:def 1 (Bool  "("  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set "m"  ($#k4_nat_d :::"mod"::: )  "n")) & (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set "n"  ($#k4_nat_d :::"mod"::: )  (Set  "(" "m"  ($#k4_nat_d :::"mod"::: )  "n" ")" ))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" it  ($#k1_seq_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set  "(" it  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )  ")" ); end; 






:: deftheorem    defines :::"modSeq"::: REAL_3:def 1 :  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )) "iff" (Bool  "("  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")))) & (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set (Var "m"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")) ")" ))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b3"))  ($#k1_seq_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )  ")" )  ")" ))); 
 definitionlet "m", "n" be   ($#m1_hidden :::"Nat":::); func  :::"divSeq":::  "(" "m" "," "n" ")"  ->   ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) means :: REAL_3:def 2 (Bool  "("  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set "m"  ($#k3_nat_d :::"div"::: )  "n")) & (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set "n"  ($#k3_nat_d :::"div"::: )  (Set  "(" "m"  ($#k4_nat_d :::"mod"::: )  "n" ")" ))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" "m" "," "n" ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k3_nat_d :::"div"::: )  (Set  "(" (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" "m" "," "n" ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )  ")" ); end; 






:: deftheorem    defines :::"divSeq"::: REAL_3:def 2 :  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_real_3 :::"divSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )) "iff" (Bool  "("  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k3_nat_d :::"div"::: )  (Set (Var "n")))) & (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set  "(" (Set (Var "m"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n")) ")" ))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k3_nat_d :::"div"::: )  (Set  "(" (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )  ")" )  ")" ))); 
 
theorem :: REAL_3:12 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k2_real_3 :::"divSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set  "(" (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )))) ; 
 
theorem :: REAL_3:13 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )))) ; 
 
theorem :: REAL_3:14 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: REAL_3:15 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) "or" (Bool (Set (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::">"::: )  (Set (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "b")))) "or" (Bool (Set (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: REAL_3:16 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "a")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set  "("  ($#k2_real_3 :::"divSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "a"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: REAL_3:17 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Set  "("  ($#k2_real_3 :::"divSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k2_real_3 :::"divSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: REAL_3:18 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k2_real_3 :::"divSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: REAL_3:19 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k2_real_3 :::"divSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )))) ; 
 
theorem :: REAL_3:20 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "m"))  ($#k13_complex1 :::"/"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k2_real_3 :::"divSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k3_real_1 :::"+"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" )))) ; 
 
theorem :: REAL_3:21 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k2_real_3 :::"divSeq"::: )   "(" (Set (Var "m")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) )))) ; 
 
theorem :: REAL_3:22 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) )))) ; 
 
theorem :: REAL_3:23 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k2_real_3 :::"divSeq"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n")) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) )))) ; 
 
theorem :: REAL_3:24 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_real_3 :::"modSeq"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n")) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) )))) ; 
 
theorem :: REAL_3:25 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Set  "("  ($#k2_real_3 :::"divSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 begin  definitionlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"remainders_for_scf"::: "r" ->   ($#m1_subset_1 :::"Real_Sequence":::) means :: REAL_3:def 3 (Bool  "("  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  "r") & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k4_int_1 :::"frac"::: )  (Set  "(" it  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )))  ")" )  ")" ); end; 





:: deftheorem    defines :::"remainders_for_scf"::: REAL_3:def 3 :  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_real_3 :::"remainders_for_scf"::: )  (Set (Var "r")))) "iff" (Bool  "("  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "r"))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k4_int_1 :::"frac"::: )  (Set  "(" (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )))  ")" )  ")" )  ")" ))); 
 notationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; synonym  :::"rfs"::: "r" for  :::"remainders_for_scf"::: "r"; end; definitionlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"SimpleContinuedFraction"::: "r" ->   ($#m1_subset_1 :::"Integer_Sequence":::) means :: REAL_3:def 4 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "("  ($#k3_real_3 :::"rfs"::: )  "r" ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k1_int_1 :::"/]"::: ) ))); end; 





:: deftheorem    defines :::"SimpleContinuedFraction"::: REAL_3:def 4 :  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Integer_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_real_3 :::"SimpleContinuedFraction"::: )  (Set (Var "r")))) "iff" (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_int_1 :::"[\"::: ) (Set  "(" (Set  "("  ($#k3_real_3 :::"rfs"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k1_int_1 :::"/]"::: ) )))  ")" ))); 
 notationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; synonym  :::"scf"::: "r" for  :::"SimpleContinuedFraction"::: "r"; end; 
theorem :: REAL_3:26 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_real_3 :::"rfs"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_real_3 :::"rfs"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ))))) ; 
 
theorem :: REAL_3:27 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "("  ($#k3_real_3 :::"rfs"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set  "("  ($#k3_real_3 :::"rfs"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: REAL_3:28 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "("  ($#k3_real_3 :::"rfs"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: REAL_3:29 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set  "("  ($#k3_real_3 :::"rfs"::: )  (Set (Var "i")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: REAL_3:30 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "i")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "i"))) & (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "i")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 
theorem :: REAL_3:31 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k3_real_3 :::"rfs"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "i")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "i"))) & (Bool (Set (Set  "("  ($#k3_real_3 :::"rfs"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "i")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 
theorem :: REAL_3:32 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "i")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "i")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "i"))) & (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "i")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 
theorem :: REAL_3:33 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k3_real_3 :::"rfs"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: REAL_3:34 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: REAL_3:35 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k5_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )))) ; 
 
theorem :: REAL_3:36 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_real_3 :::"rfs"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_real_3 :::"rfs"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k4_int_1 :::"frac"::: )  (Set (Var "r")) ")" ) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))))) ; 
 
theorem :: REAL_3:37 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k4_int_1 :::"frac"::: )  (Set (Var "r")) ")" ) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))))) ; 
 
theorem :: REAL_3:38 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: REAL_3:39 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_numbers :::"NAT"::: )  )))) ; 
 
theorem :: REAL_3:40 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Num 1)))) ; 
 
theorem :: REAL_3:41 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set  "(" (Set (Var "m"))  ($#k13_complex1 :::"/"::: )  (Set (Var "n")) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_real_3 :::"divSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "k")))) & (Bool (Set (Set  "("  ($#k3_real_3 :::"rfs"::: )  (Set  "(" (Set (Var "m"))  ($#k13_complex1 :::"/"::: )  (Set (Var "n")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Set  "("  ($#k3_real_3 :::"rfs"::: )  (Set  "(" (Set (Var "m"))  ($#k13_complex1 :::"/"::: )  (Set (Var "n")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k1_real_3 :::"modSeq"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )) ; 
 
theorem :: REAL_3:42 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "r")) "is"   ($#v1_rat_1 :::"rational"::: )  ) "iff" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))))  ")" )) ; 
 
theorem :: REAL_3:43 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Var "r")) "is"   ($#v1_rat_1 :::"irrational"::: )  )) ; 
 begin  








definitionlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"convergent_numerators"::: "r" ->   ($#m1_subset_1 :::"Real_Sequence":::) means :: REAL_3:def 5 (Bool  "("  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  "r" ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  "r" ")" )  ($#k3_funct_2 :::"."::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  "r" ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  "r" ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" it  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" it  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )  ")" ); end; 





:: deftheorem    defines :::"convergent_numerators"::: REAL_3:def 5 :  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_real_3 :::"convergent_numerators"::: )  (Set (Var "r")))) "iff" (Bool  "("  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )  ")" )  ")" ))); 
 definitionlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"convergent_denominators"::: "r" ->   ($#m1_subset_1 :::"Real_Sequence":::) means :: REAL_3:def 6 (Bool  "("  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  "r" ")" )  ($#k3_funct_2 :::"."::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  "r" ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" it  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" it  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )  ")" ); end; 





:: deftheorem    defines :::"convergent_denominators"::: REAL_3:def 6 :  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_real_3 :::"convergent_denominators"::: )  (Set (Var "r")))) "iff" (Bool  "("  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )  ")" )  ")" ))); 
 notationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; synonym  :::"c_n"::: "r" for  :::"convergent_numerators"::: "r"; synonym  :::"c_d"::: "r" for  :::"convergent_denominators"::: "r"; end; 
theorem :: REAL_3:44 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_numbers :::"NAT"::: )  )))) ; 
 
theorem :: REAL_3:45 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: REAL_3:46 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))))) ; 
 
theorem :: REAL_3:47 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n1")) "," (Set (Var "n2")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n1"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))) & (Bool (Set (Var "n2"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set (Var "n1"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "n2")))  ($#r1_hidden :::"="::: )  (Num 1))))) ; 
 
theorem :: REAL_3:48 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: REAL_3:49 (Bool  "for" (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Set (Var "b"))  ($#k3_real_1 :::"+"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k3_real_1 :::"+"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k2_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )))))) ; 
 
theorem :: REAL_3:50 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_numbers :::"NAT"::: )  )))) ; 
 
theorem :: REAL_3:51 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: REAL_3:52 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: REAL_3:53 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))))) ; 
 
theorem :: REAL_3:54 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))))) ; 
 
theorem :: REAL_3:55 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ))))) ; 
 
theorem :: REAL_3:56 (Bool  "for" (Set (Var "b")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Set (Var "b"))  ($#k3_real_1 :::"+"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k3_real_1 :::"+"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k2_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )))))) ; 
 
theorem :: REAL_3:57 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n1")) "," (Set (Var "n2")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n1"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))) & (Bool (Set (Var "n2"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set (Var "n1"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "n2")))  ($#r1_hidden :::"="::: )  (Num 1))))) ; 
 
theorem :: REAL_3:58 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" ))))) ; 
 
theorem :: REAL_3:59 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))))) ; 
 
theorem :: REAL_3:60 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ))))) ; 
 
theorem :: REAL_3:61 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  ($#k1_fib_num :::"tau"::: ) )  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: REAL_3:62 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "a")))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_real_1 :::"+"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k3_real_1 :::"+"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k2_newton :::"|^"::: )  (Set (Var "n"))))))) ; 
 
theorem :: REAL_3:63 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ))))) ; 
 
theorem :: REAL_3:64 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" )  ($#k2_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: REAL_3:65 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" )  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ))))) ; 
 
theorem :: REAL_3:66 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" )  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" ))))) ; 
 
theorem :: REAL_3:67 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" )  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ))))) ; 
 
theorem :: REAL_3:68 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1) ")" ) ")" ) ")" ))))) ; 
 
theorem :: REAL_3:69 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ) ")" ))))) ; 
 
theorem :: REAL_3:70 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" ) ")" ))))) ; 
 definitionlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"convergents_of_continued_fractions"::: "r" ->   ($#m1_subset_1 :::"Real_Sequence":::) equals :: REAL_3:def 7 (Set (Set  "("  ($#k5_real_3 :::"c_n"::: )  "r" ")" )  ($#k52_valued_1 :::"/""::: )  (Set  "("  ($#k6_real_3 :::"c_d"::: )  "r" ")" )); end; 





:: deftheorem    defines :::"convergents_of_continued_fractions"::: REAL_3:def 7 :  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k7_real_3 :::"convergents_of_continued_fractions"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k52_valued_1 :::"/""::: )  (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )))); 
 notationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; synonym  :::"cocf"::: "r" for  :::"convergents_of_continued_fractions"::: "r"; end; 
theorem :: REAL_3:71 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k7_real_3 :::"cocf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )))) ; 
 
theorem :: REAL_3:72 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k7_real_3 :::"cocf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Num 1) ")" ) ")" )))) ; 
 
theorem :: REAL_3:73 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k7_real_3 :::"cocf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Num 1) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Num 2) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: REAL_3:74 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k7_real_3 :::"cocf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Num 1) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Num 2) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: REAL_3:75 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" ) ")" ))))) ; 
 
theorem :: REAL_3:76 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" ) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k9_real_1 :::"-"::: )  (Num 2) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k9_real_1 :::"-"::: )  (Num 2) ")" ) ")" ))))) ; 
 
theorem :: REAL_3:77 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_real_3 :::"c_d"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" ) ")" ))))) ; 
 definitionlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"backContinued_fraction"::: "r" ->   ($#m1_subset_1 :::"Real_Sequence":::) means :: REAL_3:def 8 (Bool  "("  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  "r" ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" it  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  "r" ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )  ")" ); end; 





:: deftheorem    defines :::"backContinued_fraction"::: REAL_3:def 8 :  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_real_3 :::"backContinued_fraction"::: )  (Set (Var "r")))) "iff" (Bool  "("  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )  ")" )  ")" ))); 
 notationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; synonym  :::"bcf"::: "r" for  :::"backContinued_fraction"::: "r"; end; 
theorem :: REAL_3:78 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "("  ($#k4_real_3 :::"scf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k8_real_3 :::"bcf"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k5_real_3 :::"c_n"::: )  (Set (Var "r")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))))) ;