:: RFINSEQ2 semantic presentation begin definitionlet "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"max_p"::: "f" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: RFINSEQ2:def 1 (Bool "(" "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) "f") ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) "f") ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool it ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_seq_1 :::"."::: ) it))) "holds" (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2")))) ")" ) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_seq_1 :::"."::: ) it))) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) ")" ) ")" ) ")" ")" ); end; :: deftheorem defines :::"max_p"::: RFINSEQ2:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_rfinseq2 :::"max_p"::: ) (Set (Var "f")))) "iff" (Bool "(" "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2")))) ")" ) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Var "b2")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) ")" ) ")" ) ")" ")" ) ")" ))); definitionlet "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"min_p"::: "f" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: RFINSEQ2:def 2 (Bool "(" "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) "f") ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) "f") ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool it ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_seq_1 :::"."::: ) it))) "holds" (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r2")))) ")" ) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_seq_1 :::"."::: ) it))) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) ")" ) ")" ) ")" ")" ); end; :: deftheorem defines :::"min_p"::: RFINSEQ2:def 2 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_rfinseq2 :::"min_p"::: ) (Set (Var "f")))) "iff" (Bool "(" "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r2")))) ")" ) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Var "b2")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) ")" ) ")" ) ")" ")" ) ")" ))); definitionlet "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"max"::: "f" -> ($#m1_subset_1 :::"Real":::) equals :: RFINSEQ2:def 3 (Set "f" ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_rfinseq2 :::"max_p"::: ) "f" ")" )); func :::"min"::: "f" -> ($#m1_subset_1 :::"Real":::) equals :: RFINSEQ2:def 4 (Set "f" ($#k1_seq_1 :::"."::: ) (Set "(" ($#k2_rfinseq2 :::"min_p"::: ) "f" ")" )); end; :: deftheorem defines :::"max"::: RFINSEQ2:def 3 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k3_rfinseq2 :::"max"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_rfinseq2 :::"max_p"::: ) (Set (Var "f")) ")" )))); :: deftheorem defines :::"min"::: RFINSEQ2:def 4 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k4_rfinseq2 :::"min"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k2_rfinseq2 :::"min_p"::: ) (Set (Var "f")) ")" )))); theorem :: RFINSEQ2:1 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_rfinseq2 :::"max_p"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_rfinseq2 :::"max"::: ) (Set (Var "f")))) ")" ))) ; theorem :: RFINSEQ2:2 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k2_rfinseq2 :::"min_p"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k4_rfinseq2 :::"min"::: ) (Set (Var "f")))) ")" ))) ; theorem :: RFINSEQ2:3 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k12_finseq_1 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k1_rfinseq2 :::"max_p"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k3_rfinseq2 :::"max"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" ))) ; theorem :: RFINSEQ2:4 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k12_finseq_1 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k2_rfinseq2 :::"min_p"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k4_rfinseq2 :::"min"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" ))) ; theorem :: RFINSEQ2:5 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "r1")) "," (Set (Var "r2")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_rfinseq2 :::"max"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) ")" )) & (Bool (Set ($#k1_rfinseq2 :::"max_p"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k15_funcop_1 :::"IFEQ"::: ) "(" (Set (Var "r1")) "," (Set "(" ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) ")" ")" ) "," (Num 1) "," (Num 2) ")" )) ")" ))) ; theorem :: RFINSEQ2:6 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "r1")) "," (Set (Var "r2")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k4_rfinseq2 :::"min"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) ")" )) & (Bool (Set ($#k2_rfinseq2 :::"min_p"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k15_funcop_1 :::"IFEQ"::: ) "(" (Set (Var "r1")) "," (Set "(" ($#k3_xxreal_0 :::"min"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) ")" ")" ) "," (Num 1) "," (Num 2) ")" )) ")" ))) ; theorem :: RFINSEQ2:7 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_rfinseq2 :::"max"::: ) (Set "(" (Set (Var "f1")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "f2")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_rfinseq2 :::"max"::: ) (Set (Var "f1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k3_rfinseq2 :::"max"::: ) (Set (Var "f2")) ")" )))) ; theorem :: RFINSEQ2:8 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_rfinseq2 :::"min"::: ) (Set "(" (Set (Var "f1")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "f2")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" ($#k4_rfinseq2 :::"min"::: ) (Set (Var "f1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_rfinseq2 :::"min"::: ) (Set (Var "f2")) ")" )))) ; theorem :: RFINSEQ2:9 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_rfinseq2 :::"max"::: ) (Set "(" (Set (Var "a")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_rfinseq2 :::"max"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k1_rfinseq2 :::"max_p"::: ) (Set "(" (Set (Var "a")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rfinseq2 :::"max_p"::: ) (Set (Var "f")))) ")" ))) ; theorem :: RFINSEQ2:10 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k4_rfinseq2 :::"min"::: ) (Set "(" (Set (Var "a")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_rfinseq2 :::"min"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k2_rfinseq2 :::"min_p"::: ) (Set "(" (Set (Var "a")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_rfinseq2 :::"min_p"::: ) (Set (Var "f")))) ")" ))) ; theorem :: RFINSEQ2:11 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_rfinseq2 :::"max"::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k4_rfinseq2 :::"min"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k1_rfinseq2 :::"max_p"::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_rfinseq2 :::"min_p"::: ) (Set (Var "f")))) ")" )) ; theorem :: RFINSEQ2:12 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k4_rfinseq2 :::"min"::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k3_rfinseq2 :::"max"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k2_rfinseq2 :::"min_p"::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rfinseq2 :::"max_p"::: ) (Set (Var "f")))) ")" )) ; theorem :: RFINSEQ2:13 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set ($#k3_rfinseq2 :::"max"::: ) (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_rfinseq2 :::"max"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_rfinseq2 :::"min"::: ) (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k4_rfinseq2 :::"min"::: ) (Set (Var "f")))) ")" ))) ; theorem :: RFINSEQ2:14 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set ($#k3_rfinseq2 :::"max"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rfinseq2 :::"max"::: ) (Set (Var "g"))))) ; theorem :: RFINSEQ2:15 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set ($#k4_rfinseq2 :::"min"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rfinseq2 :::"min"::: ) (Set (Var "g"))))) ; definitionlet "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"sort_d"::: "f" -> ($#v8_valued_0 :::"non-increasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: RFINSEQ2:def 5 (Bool "f" "," it ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ); projectivity (Bool "for" (Set (Var "b1")) "being" ($#v8_valued_0 :::"non-increasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "b2")) "," (Set (Var "b1")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set (Var "b1")) "," (Set (Var "b1")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ))) ; end; :: deftheorem defines :::"sort_d"::: RFINSEQ2:def 5 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#v8_valued_0 :::"non-increasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_rfinseq2 :::"sort_d"::: ) (Set (Var "f")))) "iff" (Bool (Set (Var "f")) "," (Set (Var "b2")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) ")" ))); theorem :: RFINSEQ2:16 (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) "holds" (Bool (Set (Var "R")) "is" ($#v1_integra2 :::"non-decreasing"::: ) )) ; theorem :: RFINSEQ2:17 (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_integra2 :::"non-decreasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))))) ")" )) ; theorem :: RFINSEQ2:18 (Bool "for" (Set (Var "R")) "being" ($#v1_integra2 :::"non-decreasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "R")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n"))) "is" ($#v1_integra2 :::"non-decreasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) )))) ; theorem :: RFINSEQ2:19 (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#v1_integra2 :::"non-decreasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "R1")) "," (Set (Var "R2")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set (Var "R1")) ($#r1_hidden :::"="::: ) (Set (Var "R2")))) ; definitionlet "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"sort_a"::: "f" -> ($#v1_integra2 :::"non-decreasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: RFINSEQ2:def 6 (Bool "f" "," it ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ); projectivity (Bool "for" (Set (Var "b1")) "being" ($#v1_integra2 :::"non-decreasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "b2")) "," (Set (Var "b1")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set (Var "b1")) "," (Set (Var "b1")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ))) ; end; :: deftheorem defines :::"sort_a"::: RFINSEQ2:def 6 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#v1_integra2 :::"non-decreasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_rfinseq2 :::"sort_a"::: ) (Set (Var "f")))) "iff" (Bool (Set (Var "f")) "," (Set (Var "b2")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) ")" ))); theorem :: RFINSEQ2:20 (Bool "for" (Set (Var "f")) "being" ($#v8_valued_0 :::"non-increasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k5_rfinseq2 :::"sort_d"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ; theorem :: RFINSEQ2:21 (Bool "for" (Set (Var "f")) "being" ($#v1_integra2 :::"non-decreasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k6_rfinseq2 :::"sort_a"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ; theorem :: RFINSEQ2:22 canceled; theorem :: RFINSEQ2:23 canceled; theorem :: RFINSEQ2:24 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v8_valued_0 :::"non-increasing"::: ) )) "holds" (Bool (Set ($#k6_rvsum_1 :::"-"::: ) (Set (Var "f"))) "is" ($#v1_integra2 :::"non-decreasing"::: ) )) ; theorem :: RFINSEQ2:25 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_integra2 :::"non-decreasing"::: ) )) "holds" (Bool (Set ($#k6_rvsum_1 :::"-"::: ) (Set (Var "f"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) )) ; theorem :: RFINSEQ2:26 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "g")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "P")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k6_rvsum_1 :::"-"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "P")))))) ; theorem :: RFINSEQ2:27 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set ($#k6_rvsum_1 :::"-"::: ) (Set (Var "f"))) "," (Set ($#k6_rvsum_1 :::"-"::: ) (Set (Var "g"))) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) ; theorem :: RFINSEQ2:28 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k5_rfinseq2 :::"sort_d"::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_rvsum_1 :::"-"::: ) (Set "(" ($#k6_rfinseq2 :::"sort_a"::: ) (Set (Var "f")) ")" )))) ; theorem :: RFINSEQ2:29 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k6_rfinseq2 :::"sort_a"::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_rvsum_1 :::"-"::: ) (Set "(" ($#k5_rfinseq2 :::"sort_d"::: ) (Set (Var "f")) ")" )))) ; theorem :: RFINSEQ2:30 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k5_rfinseq2 :::"sort_d"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k5_rfinseq2 :::"sort_d"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) ")" )) ; theorem :: RFINSEQ2:31 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k6_rfinseq2 :::"sort_a"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k6_rfinseq2 :::"sort_a"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) ")" )) ; theorem :: RFINSEQ2:32 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set ($#k1_rfinseq2 :::"max_p"::: ) (Set "(" ($#k5_rfinseq2 :::"sort_d"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k2_rfinseq2 :::"min_p"::: ) (Set "(" ($#k6_rfinseq2 :::"sort_a"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "(" ($#k5_rfinseq2 :::"sort_d"::: ) (Set (Var "f")) ")" ) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_rfinseq2 :::"max"::: ) (Set (Var "f")))) & (Bool (Set (Set "(" ($#k6_rfinseq2 :::"sort_a"::: ) (Set (Var "f")) ")" ) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k4_rfinseq2 :::"min"::: ) (Set (Var "f")))) ")" )) ;