:: FINSEQ_8 semantic presentation begin definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); :: original: :::"^"::: redefine func "f" :::"^"::: "g" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D"; end; theorem :: FINSEQ_8:1 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "g")) ")" ) "," (Num 1) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: FINSEQ_8:2 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "D"))))))) ; theorem :: FINSEQ_8:3 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "D")) ")" ) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "D")))))) ; definitionlet "f" be ($#m1_hidden :::"FinSequence":::); let "k1", "k2" be ($#m1_hidden :::"Nat":::); func :::"smid"::: "(" "f" "," "k1" "," "k2" ")" -> ($#m1_hidden :::"FinSequence":::) equals :: FINSEQ_8:def 1 (Set (Set "(" "f" ($#k1_rfinseq :::"/^"::: ) (Set "(" "k1" ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k16_finseq_1 :::"|"::: ) (Set "(" (Set "(" "k2" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) "k1" ")" )); end; :: deftheorem defines :::"smid"::: FINSEQ_8:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_finseq_8 :::"smid"::: ) "(" (Set (Var "f")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_rfinseq :::"/^"::: ) (Set "(" (Set (Var "k1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k16_finseq_1 :::"|"::: ) (Set "(" (Set "(" (Set (Var "k2")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "k1")) ")" ))))); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "k1", "k2" be ($#m1_hidden :::"Nat":::); :: original: :::"smid"::: redefine func :::"smid"::: "(" "f" "," "k1" "," "k2" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D"; end; theorem :: FINSEQ_8:4 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k2")))) "holds" (Bool (Set ($#k2_finseq_8 :::"smid"::: ) "(" (Set (Var "f")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" )))) ; theorem :: FINSEQ_8: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 "k2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set (Var "f")) "," (Num 1) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "k2"))))))) ; theorem :: FINSEQ_8: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 "k2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k2")))) "holds" (Bool (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set (Var "f")) "," (Num 1) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: FINSEQ_8:7 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k1")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "k2")))) "holds" (Bool (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set (Var "f")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: FINSEQ_8:8 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "k2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set (Var "f")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set (Var "f")) "," (Num 1) "," (Set "(" (Set (Var "k2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: FINSEQ_8:9 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "g"))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); func :::"ovlpart"::: "(" "f" "," "g" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" means :: FINSEQ_8:def 2 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "g")) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_8 :::"smid"::: ) "(" "g" "," (Num 1) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ")" )) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_8 :::"smid"::: ) "(" "f" "," (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "f" ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) "f" ")" ) ")" )) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "g")) & (Bool (Set ($#k3_finseq_8 :::"smid"::: ) "(" "g" "," (Num 1) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_8 :::"smid"::: ) "(" "f" "," (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "f" ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "j")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) "f" ")" ) ")" ))) "holds" (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) it)) ")" ) ")" ); end; :: deftheorem defines :::"ovlpart"::: FINSEQ_8:def 2 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set (Var "g")) "," (Num 1) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4")) ")" ) ")" )) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" )) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")))) & (Bool (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set (Var "g")) "," (Num 1) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "j")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ))) "holds" (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4")))) ")" ) ")" ) ")" ))); theorem :: FINSEQ_8:10 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); func :::"ovlcon"::: "(" "f" "," "g" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" equals :: FINSEQ_8:def 3 (Set "f" ($#k1_finseq_8 :::"^"::: ) (Set "(" "g" ($#k2_rfinseq :::"/^"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" "f" "," "g" ")" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"ovlcon"::: FINSEQ_8:def 3 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k5_finseq_8 :::"ovlcon"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_finseq_8 :::"^"::: ) (Set "(" (Set (Var "g")) ($#k2_rfinseq :::"/^"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ")" ))))); theorem :: FINSEQ_8:11 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k5_finseq_8 :::"ovlcon"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ")" ) ")" ) ($#k1_finseq_8 :::"^"::: ) (Set (Var "g")))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); func :::"ovlldiff"::: "(" "f" "," "g" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" equals :: FINSEQ_8:def 4 (Set "f" ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "f" ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" "f" "," "g" ")" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"ovlldiff"::: FINSEQ_8:def 4 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k6_finseq_8 :::"ovlldiff"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ")" ))))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); func :::"ovlrdiff"::: "(" "f" "," "g" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" equals :: FINSEQ_8:def 5 (Set "g" ($#k2_rfinseq :::"/^"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" "f" "," "g" ")" ")" ) ")" )); end; :: deftheorem defines :::"ovlrdiff"::: FINSEQ_8:def 5 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k7_finseq_8 :::"ovlrdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k2_rfinseq :::"/^"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ))))); theorem :: FINSEQ_8:12 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set ($#k5_finseq_8 :::"ovlcon"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_finseq_8 :::"ovlldiff"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_finseq_8 :::"^"::: ) (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ($#k1_finseq_8 :::"^"::: ) (Set "(" ($#k7_finseq_8 :::"ovlrdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ))) & (Bool (Set ($#k5_finseq_8 :::"ovlcon"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_finseq_8 :::"ovlldiff"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_finseq_8 :::"^"::: ) (Set "(" (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_finseq_8 :::"^"::: ) (Set "(" ($#k7_finseq_8 :::"ovlrdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ))) ")" ))) ; theorem :: FINSEQ_8:13 (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")) "holds" (Bool "(" (Bool (Set ($#k5_finseq_8 :::"ovlcon"::: ) "(" (Set (Var "f")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "f")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k6_finseq_8 :::"ovlldiff"::: ) "(" (Set (Var "f")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k7_finseq_8 :::"ovlrdiff"::: ) "(" (Set (Var "f")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: FINSEQ_8:14 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "g")) ")" ) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "f")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "g")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ))) ; theorem :: FINSEQ_8:15 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k5_finseq_8 :::"ovlcon"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k5_finseq_8 :::"ovlcon"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k5_finseq_8 :::"ovlcon"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ")" ))) ")" ))) ; theorem :: FINSEQ_8:16 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")))) ")" ))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "CR" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); pred "CR" :::"separates_uniquely"::: means :: FINSEQ_8:def 6 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "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 (Var "j"))) & (Bool (Set (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "CR" ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "CR" ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set (Var "f")) "," (Set (Var "j")) "," (Set "(" (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "CR" ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) & (Bool (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "CR" ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) "CR")) "holds" (Bool (Set (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "CR")))); end; :: deftheorem defines :::"separates_uniquely"::: FINSEQ_8:def 6 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "CR")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "CR")) ($#r1_finseq_8 :::"separates_uniquely"::: ) ) "iff" (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "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 (Var "j"))) & (Bool (Set (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "CR")) ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "CR")) ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set (Var "f")) "," (Set (Var "j")) "," (Set "(" (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "CR")) ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) & (Bool (Set ($#k3_finseq_8 :::"smid"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "CR")) ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "CR")))) "holds" (Bool (Set (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "CR")))))) ")" ))); theorem :: FINSEQ_8:17 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "CR")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "CR")) ($#r1_finseq_8 :::"separates_uniquely"::: ) ) "iff" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set "(" (Set (Var "CR")) ($#k2_rfinseq :::"/^"::: ) (Num 1) ")" ) "," (Set (Var "CR")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); pred "g" :::"is_substring_of"::: "f" "," "n" means :: FINSEQ_8:def 7 "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) "g") ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool "n" ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f")) & (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" "f" "," (Set (Var "i")) "," (Set "(" (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "g" ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) "g") ")" )) ")" ; end; :: deftheorem defines :::"is_substring_of"::: FINSEQ_8:def 7 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Set (Var "n"))) "iff" "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set "(" (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" )) ")" ")" )))); theorem :: FINSEQ_8:18 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n"))) & (Bool (Set (Var "g")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Set (Var "m")))) "holds" (Bool (Set (Var "g")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Set (Var "n")))))) ; theorem :: FINSEQ_8: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")) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "f")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Num 1)))) ; theorem :: FINSEQ_8:20 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "g")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "g")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Num 1)))) ; notationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "g", "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); synonym "g" :::"is_preposition_of"::: "f" for "D" :::"c="::: "g"; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "g", "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); :: original: :::"is_preposition_of"::: redefine pred "g" :::"c="::: "f" means :: FINSEQ_8:def 8 "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) "g") ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f")) & (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" "f" "," (Num 1) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) "g" ")" ) ")" ) ($#r1_hidden :::"="::: ) "g") ")" ) ")" ; end; :: deftheorem defines :::"c="::: FINSEQ_8:def 8 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r3_finseq_8 :::"c="::: ) (Set (Var "f"))) "iff" "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Num 1) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ) ")" ")" ))); theorem :: FINSEQ_8:21 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "f")) ($#r1_tarski :::"is_preposition_of"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); pred "g" :::"is_postposition_of"::: "f" means :: FINSEQ_8:def 9 (Bool (Set ($#k4_finseq_5 :::"Rev"::: ) "f") ($#r1_tarski :::"is_preposition_of"::: ) ); end; :: deftheorem defines :::"is_postposition_of"::: FINSEQ_8:def 9 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r4_finseq_8 :::"is_postposition_of"::: ) (Set (Var "f"))) "iff" (Bool (Set ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "f"))) ($#r1_tarski :::"is_preposition_of"::: ) ) ")" ))); theorem :: FINSEQ_8:22 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "g")) ($#r4_finseq_8 :::"is_postposition_of"::: ) (Set (Var "f"))))) ; theorem :: FINSEQ_8:23 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "g")) ($#r4_finseq_8 :::"is_postposition_of"::: ) (Set (Var "f")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))))) ; theorem :: FINSEQ_8:24 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "g")) ($#r4_finseq_8 :::"is_postposition_of"::: ) (Set (Var "f"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ))) ; theorem :: FINSEQ_8:25 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ) ")" ) "holds" (Bool (Set (Var "g")) ($#r4_finseq_8 :::"is_postposition_of"::: ) (Set (Var "f"))))) ; theorem :: FINSEQ_8:26 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_tarski :::"is_preposition_of"::: ) )) "holds" (Bool (Set (Var "g")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Num 1)))) ; theorem :: FINSEQ_8:27 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Bool "not" (Set (Var "g")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Set (Var "n"))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i")))) "holds" (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set "(" (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set (Var "g"))))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"instr"::: "(" "n" "," "f" "," "g" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: FINSEQ_8:def 10 (Bool "(" "(" (Bool (Bool it ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool "n" ($#r1_xxreal_0 :::"<="::: ) it) & (Bool (Set "f" ($#k2_rfinseq :::"/^"::: ) (Set "(" it ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_tarski :::"is_preposition_of"::: ) ) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">="::: ) "n") & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "f" ($#k2_rfinseq :::"/^"::: ) (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_tarski :::"is_preposition_of"::: ) )) "holds" (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">="::: ) it) ")" ) ")" ) ")" & "(" (Bool (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "not" (Bool "g" ($#r2_finseq_8 :::"is_substring_of"::: ) "f" "," "n")) ")" ")" ); end; :: deftheorem defines :::"instr"::: FINSEQ_8:def 10 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "," (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k8_finseq_8 :::"instr"::: ) "(" (Set (Var "n")) "," (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (Bool "(" "(" (Bool (Bool (Set (Var "b5")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b5"))) & (Bool (Set (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set "(" (Set (Var "b5")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_tarski :::"is_preposition_of"::: ) ) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_tarski :::"is_preposition_of"::: ) )) "holds" (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "b5"))) ")" ) ")" ) ")" & "(" (Bool (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "g")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Set (Var "n")))) ")" ")" ) ")" )))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "CR" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); func :::"addcr"::: "(" "f" "," "CR" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" equals :: FINSEQ_8:def 11 (Set ($#k5_finseq_8 :::"ovlcon"::: ) "(" "f" "," "CR" ")" ); end; :: deftheorem defines :::"addcr"::: FINSEQ_8:def 11 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "CR")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k9_finseq_8 :::"addcr"::: ) "(" (Set (Var "f")) "," (Set (Var "CR")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_finseq_8 :::"ovlcon"::: ) "(" (Set (Var "f")) "," (Set (Var "CR")) ")" )))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "r", "CR" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); pred "r" :::"is_terminated_by"::: "CR" means :: FINSEQ_8:def 12 "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) "CR") ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "r") ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "CR")) & (Bool (Set ($#k8_finseq_8 :::"instr"::: ) "(" (Num 1) "," "r" "," "CR" ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "r" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "CR" ")" ))) ")" ) ")" ; end; :: deftheorem defines :::"is_terminated_by"::: FINSEQ_8:def 12 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "," (Set (Var "CR")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r5_finseq_8 :::"is_terminated_by"::: ) (Set (Var "CR"))) "iff" "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "CR"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "CR")))) & (Bool (Set ($#k8_finseq_8 :::"instr"::: ) "(" (Num 1) "," (Set (Var "r")) "," (Set (Var "CR")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "r")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "CR")) ")" ))) ")" ) ")" ")" ))); theorem :: FINSEQ_8: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")) "holds" (Bool (Set (Var "f")) ($#r5_finseq_8 :::"is_terminated_by"::: ) (Set (Var "f"))))) ;