:: FINSEQ_7 semantic presentation begin theorem :: FINSEQ_7:1 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "i")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "j")) ")" )))))) ; theorem :: FINSEQ_7:2 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "g")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))) ; theorem :: FINSEQ_7:3 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"FinSequence":::) "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 (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ))))) ; theorem :: FINSEQ_7:4 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "i")) ")" )))))) ; begin notationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "i" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); synonym :::"Replace"::: "(" "f" "," "i" "," "p" ")" for "D" :::"+*"::: "(" "f" "," "i" ")" ; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "i" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"Replace"::: redefine func :::"Replace"::: "(" "f" "," "i" "," "p" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" equals :: FINSEQ_7:def 1 (Set (Set "(" (Set "(" "f" ($#k17_finseq_1 :::"|"::: ) (Set "(" "i" ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) "p" ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" "f" ($#k2_rfinseq :::"/^"::: ) "i" ")" )) if (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) "i") & (Bool "i" ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f")) ")" ) otherwise "f"; end; :: deftheorem defines :::"Replace"::: FINSEQ_7:def 1 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" "(" (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"))))) "implies" (Bool (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "i")) ")" ))) ")" & "(" (Bool (Bool "(" "not" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) "or" "not" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) ")" )) "implies" (Bool (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ")" ))))); theorem :: FINSEQ_7:5 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_finseq_7 :::"Replace"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))))))) ; theorem :: FINSEQ_7:6 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_finseq_7 :::"Replace"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "p")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "p")) ($#k1_tarski :::"}"::: ) ))))))) ; theorem :: FINSEQ_7:7 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"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 (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_finseq_7 :::"Replace"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "p")) ")" ")" ))))))) ; theorem :: FINSEQ_7:8 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"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 (Set (Set "(" ($#k1_finseq_7 :::"Replace"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "p")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))))))) ; theorem :: FINSEQ_7:9 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"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 "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set "(" ($#k1_finseq_7 :::"Replace"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "p")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))))))) ; theorem :: FINSEQ_7:10 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set "(" ($#k1_finseq_7 :::"Replace"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "p")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")))))))) ; theorem :: FINSEQ_7:11 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set "(" ($#k1_finseq_7 :::"Replace"::: ) "(" (Set (Var "f")) "," (Set (Var "j")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "i")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "i")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "j")) ")" ))))))) ; theorem :: FINSEQ_7:12 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Num 1) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) )))) ; theorem :: FINSEQ_7:13 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_finseq_4 :::"*>"::: ) ) "," (Num 1) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "q")) "," (Set (Var "p2")) ($#k2_finseq_4 :::"*>"::: ) )))) ; theorem :: FINSEQ_7:14 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_finseq_4 :::"*>"::: ) ) "," (Num 2) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "p1")) "," (Set (Var "q")) ($#k2_finseq_4 :::"*>"::: ) )))) ; theorem :: FINSEQ_7:15 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Num 1) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "q")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#k3_finseq_4 :::"*>"::: ) )))) ; theorem :: FINSEQ_7:16 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Num 2) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p1")) "," (Set (Var "q")) "," (Set (Var "p3")) ($#k3_finseq_4 :::"*>"::: ) )))) ; theorem :: FINSEQ_7:17 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Num 3) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) ($#k3_finseq_4 :::"*>"::: ) )))) ; begin registrationlet "f" be ($#m1_hidden :::"FinSequence":::); let "i", "j" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k10_funct_7 :::"Swap"::: ) "(" "f" "," "i" "," "j" ")" ) -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "i", "j" be ($#m1_hidden :::"Nat":::); :: original: :::"Swap"::: redefine func :::"Swap"::: "(" "f" "," "i" "," "j" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" equals :: FINSEQ_7:def 2 (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set "(" ($#k1_finseq_7 :::"Replace"::: ) "(" "f" "," "i" "," (Set "(" "f" ($#k7_partfun1 :::"/."::: ) "j" ")" ) ")" ")" ) "," "j" "," (Set "(" "f" ($#k7_partfun1 :::"/."::: ) "i" ")" ) ")" ) if (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) "i") & (Bool "i" ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f")) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) "j") & (Bool "j" ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f")) ")" ) otherwise "f"; end; :: deftheorem defines :::"Swap"::: FINSEQ_7:def 2 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "(" (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")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "implies" (Bool (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set "(" ($#k1_finseq_7 :::"Replace"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ) ")" ")" ) "," (Set (Var "j")) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" )) ")" & "(" (Bool (Bool "(" "not" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) "or" "not" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) "or" "not" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) "or" "not" (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) ")" )) "implies" (Bool (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ")" )))); theorem :: FINSEQ_7:18 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))))) ; theorem :: FINSEQ_7:19 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: FINSEQ_7:20 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set "(" ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) "," (Set (Var "j")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: FINSEQ_7:21 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "j")) "," (Set (Var "i")) ")" ))))) ; theorem :: FINSEQ_7:22 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))))) ; theorem :: FINSEQ_7:23 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_finseq_4 :::"*>"::: ) ) "," (Num 1) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "p2")) "," (Set (Var "p1")) ($#k2_finseq_4 :::"*>"::: ) )))) ; theorem :: FINSEQ_7:24 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Num 1) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "p3")) ($#k3_finseq_4 :::"*>"::: ) )))) ; theorem :: FINSEQ_7:25 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Num 1) "," (Num 3) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p3")) "," (Set (Var "p2")) "," (Set (Var "p1")) ($#k3_finseq_4 :::"*>"::: ) )))) ; theorem :: FINSEQ_7:26 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Num 2) "," (Num 3) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "p2")) ($#k3_finseq_4 :::"*>"::: ) )))) ; theorem :: FINSEQ_7:27 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "i")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "j")) ")" )))))) ; theorem :: FINSEQ_7:28 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"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 (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Num 1) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Num 1) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "i")) ")" )))))) ; theorem :: FINSEQ_7:29 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"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 (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "i")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )))))) ; theorem :: FINSEQ_7:30 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "k"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "k"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))))))) ; theorem :: FINSEQ_7:31 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"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")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")))) & (Bool (Set (Set "(" ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")))) ")" )))) ; begin theorem :: FINSEQ_7:32 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"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")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set "(" ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) "," (Set (Var "i")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set "(" ($#k1_finseq_7 :::"Replace"::: ) "(" (Set (Var "f")) "," (Set (Var "j")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" )))))) ; theorem :: FINSEQ_7:33 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "k"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "k"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set "(" ($#k1_finseq_7 :::"Replace"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set "(" ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) "," (Set (Var "k")) "," (Set (Var "p")) ")" )))))) ; theorem :: FINSEQ_7:34 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "k"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "k"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set "(" ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) "," (Set (Var "j")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set "(" ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "k")) ")" ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" ))))) ; theorem :: FINSEQ_7:35 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "j")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "k"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "k"))) & (Bool (Set (Var "l")) ($#r1_hidden :::"<>"::: ) (Set (Var "i"))) & (Bool (Set (Var "l")) ($#r1_hidden :::"<>"::: ) (Set (Var "j"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l"))) & (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set "(" ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) "," (Set (Var "k")) "," (Set (Var "l")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set "(" ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "k")) "," (Set (Var "l")) ")" ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" ))))) ;