:: SEQM_3 semantic presentation begin definitionlet "f" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); redefine attr "f" is :::"increasing"::: means :: SEQM_3:def 1 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<"::: ) (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))); redefine attr "f" is :::"decreasing"::: means :: SEQM_3:def 2 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::">"::: ) (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))); redefine attr "f" is :::"non-decreasing"::: means :: SEQM_3:def 3 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))); redefine attr "f" is :::"non-increasing"::: means :: SEQM_3:def 4 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::">="::: ) (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))); end; :: deftheorem defines :::"increasing"::: SEQM_3:def 1 : (Bool "for" (Set (Var "f")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_valued_0 :::"increasing"::: ) ) "iff" (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))) ")" )); :: deftheorem defines :::"decreasing"::: SEQM_3:def 2 : (Bool "for" (Set (Var "f")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_valued_0 :::"decreasing"::: ) ) "iff" (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))) ")" )); :: deftheorem defines :::"non-decreasing"::: SEQM_3:def 3 : (Bool "for" (Set (Var "f")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) "iff" (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))) ")" )); :: deftheorem defines :::"non-increasing"::: SEQM_3:def 4 : (Bool "for" (Set (Var "f")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) "iff" (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))) ")" )); definitionlet "seq" be ($#m1_subset_1 :::"Real_Sequence":::); attr "seq" is :::"monotone"::: means :: SEQM_3:def 5 (Bool "(" (Bool "seq" "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) "or" (Bool "seq" "is" ($#v8_valued_0 :::"non-increasing"::: ) ) ")" ); end; :: deftheorem defines :::"monotone"::: SEQM_3:def 5 : (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_seqm_3 :::"monotone"::: ) ) "iff" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) "or" (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) ")" ) ")" )); theorem :: SEQM_3:1 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v5_valued_0 :::"increasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))))) ")" )) ; theorem :: SEQM_3:2 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v5_valued_0 :::"increasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" )))) ")" )) ; theorem :: SEQM_3:3 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v6_valued_0 :::"decreasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))) ")" )) ; theorem :: SEQM_3:4 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v6_valued_0 :::"decreasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))) ")" )) ; theorem :: SEQM_3:5 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" )))) ")" )) ; theorem :: SEQM_3:6 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))))) ")" )) ; theorem :: SEQM_3:7 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))) ")" )) ; theorem :: SEQM_3:8 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))) ")" )) ; theorem :: SEQM_3:9 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v5_valued_0 :::"increasing"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))))) ; theorem :: SEQM_3:10 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v6_valued_0 :::"decreasing"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: SEQM_3:11 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))))) ; theorem :: SEQM_3:12 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; registration cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) -> ($#v7_valued_0 :::"non-decreasing"::: ) ($#v8_valued_0 :::"non-increasing"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ))))); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v7_valued_0 :::"non-decreasing"::: ) ($#v8_valued_0 :::"non-increasing"::: ) -> ($#v3_funct_1 :::"constant"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ))))); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) )) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v4_valued_0 :::"natural-valued"::: ) ($#v5_valued_0 :::"increasing"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ))))); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) )) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v4_valued_0 :::"natural-valued"::: ) ($#v5_valued_0 :::"increasing"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ))))); end; theorem :: SEQM_3:13 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ))) ")" )) ; registrationlet "Nseq" be ($#v5_valued_0 :::"increasing"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "Nseq" ($#k9_nat_1 :::"^\"::: ) "k") -> ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v4_valued_0 :::"natural-valued"::: ) ($#v5_valued_0 :::"increasing"::: ) for ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::); end; definitionlet "f" be ($#m1_subset_1 :::"Real_Sequence":::); redefine attr "f" is :::"increasing"::: means :: SEQM_3:def 6 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "f" ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set "f" ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))); redefine attr "f" is :::"decreasing"::: means :: SEQM_3:def 7 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "f" ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">"::: ) (Set "f" ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))); redefine attr "f" is :::"non-decreasing"::: means :: SEQM_3:def 8 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "f" ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set "f" ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))); redefine attr "f" is :::"non-increasing"::: means :: SEQM_3:def 9 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "f" ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set "f" ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))); end; :: deftheorem defines :::"increasing"::: SEQM_3:def 6 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_valued_0 :::"increasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" )); :: deftheorem defines :::"decreasing"::: SEQM_3:def 7 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_valued_0 :::"decreasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" )); :: deftheorem defines :::"non-decreasing"::: SEQM_3:def 8 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" )); :: deftheorem defines :::"non-increasing"::: SEQM_3:def 9 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" )); theorem :: SEQM_3:14 (Bool "for" (Set (Var "Nseq")) "being" ($#v5_valued_0 :::"increasing"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "Nseq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))))) ; registrationlet "s" be ($#m1_subset_1 :::"Real_Sequence":::); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set "s" ($#k9_nat_1 :::"^\"::: ) "k") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; theorem :: SEQM_3:15 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool (Set (Set "(" (Set (Var "seq")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq1")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "seq1")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ))))) ; theorem :: SEQM_3:16 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool (Set (Set "(" ($#k32_valued_1 :::"-"::: ) (Set (Var "seq")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k32_valued_1 :::"-"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ))))) ; theorem :: SEQM_3:17 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool (Set (Set "(" (Set (Var "seq")) ($#k47_valued_1 :::"-"::: ) (Set (Var "seq1")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "seq1")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ))))) ; theorem :: SEQM_3:18 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool (Set (Set "(" (Set (Var "seq")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ) ($#k37_valued_1 :::"""::: ) )))) ; theorem :: SEQM_3:19 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool (Set (Set "(" (Set (Var "seq")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "seq1")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "seq1")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ))))) ; theorem :: SEQM_3:20 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool (Set (Set "(" (Set (Var "seq")) ($#k52_valued_1 :::"/""::: ) (Set (Var "seq1")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ) ($#k52_valued_1 :::"/""::: ) (Set "(" (Set (Var "seq1")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ))))) ; theorem :: SEQM_3:21 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" )))))) ; theorem :: SEQM_3:22 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq")))) "holds" (Bool (Set (Var "seq1")) "is" ($#v5_valued_0 :::"increasing"::: ) )) ; theorem :: SEQM_3:23 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v6_valued_0 :::"decreasing"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq")))) "holds" (Bool (Set (Var "seq1")) "is" ($#v6_valued_0 :::"decreasing"::: ) )) ; theorem :: SEQM_3:24 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq")))) "holds" (Bool (Set (Var "seq1")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) )) ; theorem :: SEQM_3:25 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq")))) "holds" (Bool (Set (Var "seq1")) "is" ($#v8_valued_0 :::"non-increasing"::: ) )) ; theorem :: SEQM_3:26 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_seqm_3 :::"monotone"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq")))) "holds" (Bool (Set (Var "seq1")) "is" ($#v1_seqm_3 :::"monotone"::: ) )) ; theorem :: SEQM_3:27 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq")))) "holds" (Bool (Set (Var "seq1")) "is" ($#v1_seq_2 :::"bounded_above"::: ) )) ; theorem :: SEQM_3:28 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_seq_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq")))) "holds" (Bool (Set (Var "seq1")) "is" ($#v2_seq_2 :::"bounded_below"::: ) )) ; theorem :: SEQM_3:29 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq")))) "holds" (Bool (Set (Var "seq1")) "is" ($#v1_comseq_2 :::"bounded"::: ) )) ; theorem :: SEQM_3:30 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq")) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v5_valued_0 :::"increasing"::: ) ) ")" & "(" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r")))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v3_funct_1 :::"constant"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ")" ")" ))) ; theorem :: SEQM_3:31 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq")) "is" ($#v6_valued_0 :::"decreasing"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v6_valued_0 :::"decreasing"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v5_valued_0 :::"increasing"::: ) ) ")" ")" ))) ; theorem :: SEQM_3:32 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) ")" ")" ))) ; theorem :: SEQM_3:33 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) ")" ")" ))) ; theorem :: SEQM_3:34 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq")) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#v5_valued_0 :::"increasing"::: ) )) "implies" (Bool (Set (Set (Var "seq")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq1"))) "is" ($#v5_valued_0 :::"increasing"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v6_valued_0 :::"decreasing"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#v6_valued_0 :::"decreasing"::: ) )) "implies" (Bool (Set (Set (Var "seq")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq1"))) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) )) "implies" (Bool (Set (Set (Var "seq")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq1"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#v8_valued_0 :::"non-increasing"::: ) )) "implies" (Bool (Set (Set (Var "seq")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq1"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) ")" ")" )) ; theorem :: SEQM_3:35 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq")) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#v3_funct_1 :::"constant"::: ) )) "implies" (Bool (Set (Set (Var "seq")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq1"))) "is" ($#v5_valued_0 :::"increasing"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v6_valued_0 :::"decreasing"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#v3_funct_1 :::"constant"::: ) )) "implies" (Bool (Set (Set (Var "seq")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq1"))) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#v3_funct_1 :::"constant"::: ) )) "implies" (Bool (Set (Set (Var "seq")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq1"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#v3_funct_1 :::"constant"::: ) )) "implies" (Bool (Set (Set (Var "seq")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq1"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) ")" ")" )) ; theorem :: SEQM_3:36 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq")) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) ")" & "(" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r")))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) ) ")" ")" ))) ; theorem :: SEQM_3:37 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq")) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "implies" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v1_comseq_2 :::"bounded"::: ) )) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "implies" (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set (Var "seq"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "implies" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "seq"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" & "(" (Bool (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "seq"))) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "implies" (Bool (Set (Var "seq")) "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" ")" )) ; theorem :: SEQM_3:38 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#v8_valued_0 :::"non-increasing"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq1"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) )) ; theorem :: SEQM_3:39 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_seq_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq1"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) )) ; theorem :: SEQM_3:40 (Bool "(" (Bool (Set ($#k6_funct_3 :::"incl"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set ($#k6_funct_3 :::"incl"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "is" ($#v4_valued_0 :::"natural-valued"::: ) ) ")" ) ; registration cluster -> ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; begin theorem :: SEQM_3:41 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "s"))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k7_real_1 :::"+"::: ) (Num 1))) ")" ) "or" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k7_real_1 :::"+"::: ) (Num 1))) ")" ) ")" ) ")" )) ; theorem :: SEQM_3:42 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Set (Var "j")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "n")) ($#k9_real_1 :::"-"::: ) (Set (Var "m")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool "(" (Bool "(" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Var "m"))) ")" ) "or" (Bool "(" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "n")) ($#k9_real_1 :::"-"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j"))) ")" ) ")" ) ")" )) ; theorem :: SEQM_3:43 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Num 1)) "iff" (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" )) ; theorem :: SEQM_3:44 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")))) & (Bool (Bool "not" (Set (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))))) "holds" (Bool (Set (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))) ; definitionlet "f" be ($#m1_hidden :::"FinSequence":::); redefine attr "f" is :::"constant"::: means :: SEQM_3:def 10 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "m"))))); end; :: deftheorem defines :::"constant"::: SEQM_3:def 10 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_funct_1 :::"constant"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))))) ")" )); registration cluster -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v5_valued_0 :::"increasing"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: SEQM_3:45 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "v"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "v")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Bool "not" (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)))) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Var "s")))) ")" ) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "v")))) & (Bool (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "v")))) & (Bool (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "i")))) "holds" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "v")))) & (Bool (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ))) ; theorem :: SEQM_3:46 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "v"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "v")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Bool "not" (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)))) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Var "s")))) ")" )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "v")))) & (Bool (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "v")))) & (Bool (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "v")))) & (Bool (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Var "i")))) "holds" (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) ")" ) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "v")))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) ")" ) ")" ))) ;