:: FILEREC1 semantic presentation begin theorem :: FILEREC1:1 (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")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "q")) ")" ) ($#k1_finseq_8 :::"^"::: ) (Set (Var "r")) ")" ) ($#k1_finseq_8 :::"^"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_finseq_8 :::"^"::: ) (Set "(" (Set (Var "q")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "r")) ")" ) ")" ) ($#k1_finseq_8 :::"^"::: ) (Set (Var "s")))) & (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "q")) ")" ) ($#k1_finseq_8 :::"^"::: ) (Set (Var "r")) ")" ) ($#k1_finseq_8 :::"^"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "q")) ")" ) ($#k1_finseq_8 :::"^"::: ) (Set "(" (Set (Var "r")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k1_finseq_8 :::"^"::: ) (Set "(" (Set (Var "q")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "r")) ")" ) ")" ) ($#k1_finseq_8 :::"^"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "q")) ")" ) ($#k1_finseq_8 :::"^"::: ) (Set "(" (Set (Var "r")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "s")) ")" ))) ")" ))) ; theorem :: FILEREC1:2 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: FILEREC1:3 (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" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "q")))))) ; theorem :: FILEREC1: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 "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "m")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")) ")" )))))) ; theorem :: FILEREC1: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")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (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"))))) ; theorem :: FILEREC1:6 (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 "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 (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "g")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ))))) ; theorem :: FILEREC1: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 "i")) "," (Set (Var "j")) "," (Set (Var "n")) "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 (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" ))))) ; theorem :: FILEREC1:8 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (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 (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))))) ; theorem :: FILEREC1:9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (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 (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" )))) ; theorem :: FILEREC1:10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (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 (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k11_finseq_1 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" )))) ; theorem :: FILEREC1:11 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (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 (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ))))) ; theorem :: FILEREC1:12 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (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 (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ))))) ; theorem :: FILEREC1:13 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (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 (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k11_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ))))) ; theorem :: FILEREC1:14 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (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 (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k11_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ))))) ; theorem :: FILEREC1:15 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (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 (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k11_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ))))) ; theorem :: FILEREC1:16 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) (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 (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k11_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "c")) ($#k9_finseq_1 :::"*>"::: ) ))))) ; theorem :: FILEREC1:17 (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 (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: FILEREC1:18 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "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 "r"))))) "holds" (Bool (Set ($#k4_finseq_5 :::"Rev"::: ) (Set "(" (Set (Var "r")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "r")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "r")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" )))))) ; theorem :: FILEREC1:19 (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")) "st" (Bool (Bool (Bool "not" (Set (Var "CR")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Num 1))) & (Bool (Set (Var "CR")) ($#r1_finseq_8 :::"separates_uniquely"::: ) )) "holds" (Bool (Set ($#k8_finseq_8 :::"instr"::: ) "(" (Num 1) "," (Set "(" (Set (Var "f")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "CR")) ")" ) "," (Set (Var "CR")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: FILEREC1: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 "CR")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Bool "not" (Set (Var "CR")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Num 1))) & (Bool (Set (Var "CR")) ($#r1_finseq_8 :::"separates_uniquely"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "CR"))) ($#r5_finseq_8 :::"is_terminated_by"::: ) (Set (Var "CR"))))) ; notationlet "D" be ($#m1_hidden :::"set"::: ) ; synonym :::"File"::: "of" "D" for :::"FinSequence"::: "of" "D"; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "r", "f", "CR" be ($#m1_finseq_1 :::"File"::: ) "of" (Set (Const "D")); pred "r" :::"is_a_record_of"::: "f" "," "CR" means :: FILEREC1:def 1 (Bool "(" (Bool "(" (Bool (Set "CR" ($#k1_finseq_8 :::"^"::: ) "r") ($#r2_finseq_8 :::"is_substring_of"::: ) (Set ($#k9_finseq_8 :::"addcr"::: ) "(" "f" "," "CR" ")" ) "," (Num 1)) "or" (Bool (Set ($#k9_finseq_8 :::"addcr"::: ) "(" "f" "," "CR" ")" ) ($#r1_tarski :::"is_preposition_of"::: ) ) ")" ) & (Bool "r" ($#r5_finseq_8 :::"is_terminated_by"::: ) "CR") ")" ); end; :: deftheorem defines :::"is_a_record_of"::: FILEREC1:def 1 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "," (Set (Var "f")) "," (Set (Var "CR")) "being" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r1_filerec1 :::"is_a_record_of"::: ) (Set (Var "f")) "," (Set (Var "CR"))) "iff" (Bool "(" (Bool "(" (Bool (Set (Set (Var "CR")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "r"))) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set ($#k9_finseq_8 :::"addcr"::: ) "(" (Set (Var "f")) "," (Set (Var "CR")) ")" ) "," (Num 1)) "or" (Bool (Set ($#k9_finseq_8 :::"addcr"::: ) "(" (Set (Var "f")) "," (Set (Var "CR")) ")" ) ($#r1_tarski :::"is_preposition_of"::: ) ) ")" ) & (Bool (Set (Var "r")) ($#r5_finseq_8 :::"is_terminated_by"::: ) (Set (Var "CR"))) ")" ) ")" ))); theorem :: FILEREC1:21 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "D")) ")" ) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "D")))) & (Bool (Set ($#k4_finseq_8 :::"ovlpart"::: ) "(" (Set (Var "r")) "," (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "D")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "D")))) ")" ))) ; theorem :: FILEREC1:22 (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 (Set (Var "CR")) ($#r1_filerec1 :::"is_a_record_of"::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "D"))) "," (Set (Var "CR"))))) ; theorem :: FILEREC1:23 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "r")) "," (Set (Var "CR")) "being" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "CR")) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "b")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "CR")) ($#r1_filerec1 :::"is_a_record_of"::: ) (Set (Var "f")) "," (Set (Var "CR"))) & (Bool (Set (Var "r")) ($#r1_filerec1 :::"is_a_record_of"::: ) (Set (Var "f")) "," (Set (Var "CR"))) ")" )))) ; theorem :: FILEREC1: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 "CR")) "being" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "f")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "CR"))) ($#r1_tarski :::"is_preposition_of"::: ) ))) ; theorem :: FILEREC1: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 "CR")) "being" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k9_finseq_8 :::"addcr"::: ) "(" (Set (Var "f")) "," (Set (Var "CR")) ")" ) ($#r1_tarski :::"is_preposition_of"::: ) ))) ; theorem :: FILEREC1:26 (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" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "CR")) ($#r4_finseq_8 :::"is_postposition_of"::: ) (Set (Var "r")))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "r")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "CR")) ")" ))))) ; theorem :: FILEREC1:27 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "CR")) "," (Set (Var "r")) "being" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "CR")) ($#r4_finseq_8 :::"is_postposition_of"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_8 :::"addcr"::: ) "(" (Set (Var "r")) "," (Set (Var "CR")) ")" )))) ; theorem :: FILEREC1:28 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "CR")) "," (Set (Var "r")) "being" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "r")) ($#r5_finseq_8 :::"is_terminated_by"::: ) (Set (Var "CR")))) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_8 :::"addcr"::: ) "(" (Set (Var "r")) "," (Set (Var "CR")) ")" )))) ; theorem :: FILEREC1:29 (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" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "f")) ($#r5_finseq_8 :::"is_terminated_by"::: ) (Set (Var "g")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))))) ; theorem :: FILEREC1:30 (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" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k9_finseq_8 :::"addcr"::: ) "(" (Set (Var "f")) "," (Set (Var "CR")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k9_finseq_8 :::"addcr"::: ) "(" (Set (Var "f")) "," (Set (Var "CR")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "CR")))) ")" ))) ; theorem :: FILEREC1:31 (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 (Var "g")) ($#r1_hidden :::"="::: ) (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 :: FILEREC1:32 (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 "(" ($#k6_finseq_8 :::"ovlldiff"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_finseq_8 :::"^"::: ) (Set (Var "g")))))) ; theorem :: FILEREC1:33 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "CR")) "," (Set (Var "r")) "being" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k9_finseq_8 :::"addcr"::: ) "(" (Set (Var "r")) "," (Set (Var "CR")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_finseq_8 :::"ovlldiff"::: ) "(" (Set (Var "r")) "," (Set (Var "CR")) ")" ")" ) ($#k1_finseq_8 :::"^"::: ) (Set (Var "CR")))))) ; theorem :: FILEREC1:34 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "f")) "being" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "r2"))))) "holds" (Bool "(" (Bool (Set (Var "r1")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Num 1)) & (Bool (Set (Var "r2")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Num 1)) ")" ))) ; theorem :: FILEREC1:35 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "," (Set (Var "f")) "being" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r1")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "r2")) ")" ) ($#k1_finseq_8 :::"^"::: ) (Set (Var "r3"))))) "holds" (Bool "(" (Bool (Set (Var "r1")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Num 1)) & (Bool (Set (Var "r2")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Num 1)) & (Bool (Set (Var "r3")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Num 1)) ")" ))) ; theorem :: FILEREC1:36 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "CR")) "," (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "r1")) ($#r5_finseq_8 :::"is_terminated_by"::: ) (Set (Var "CR"))) & (Bool (Set (Var "r2")) ($#r5_finseq_8 :::"is_terminated_by"::: ) (Set (Var "CR")))) "holds" (Bool (Set (Set (Var "CR")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "r2"))) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set ($#k9_finseq_8 :::"addcr"::: ) "(" (Set "(" (Set (Var "r1")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "r2")) ")" ) "," (Set (Var "CR")) ")" ) "," (Num 1)))) ; theorem :: FILEREC1:37 (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" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k8_finseq_8 :::"instr"::: ) "(" (Set (Var "n")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "n")))))) ; theorem :: FILEREC1:38 (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" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k8_finseq_8 :::"instr"::: ) "(" (Set (Var "n")) "," (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))))) ; theorem :: FILEREC1:39 (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" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Var "CR")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set ($#k5_finseq_8 :::"ovlcon"::: ) "(" (Set (Var "f")) "," (Set (Var "CR")) ")" ) "," (Num 1)))) ; theorem :: FILEREC1:40 (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" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Var "CR")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set ($#k9_finseq_8 :::"addcr"::: ) "(" (Set (Var "f")) "," (Set (Var "CR")) ")" ) "," (Num 1)))) ; theorem :: FILEREC1:41 (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 (Set (Var "g")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n"))) "," (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "g")) ($#r2_finseq_8 :::"is_substring_of"::: ) (Set (Var "f")) "," (Num 1))))) ; theorem :: FILEREC1:42 (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" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) (Bool "ex" (Set (Var "r")) "being" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "st" (Bool (Set (Var "r")) ($#r1_filerec1 :::"is_a_record_of"::: ) (Set (Var "f")) "," (Set (Var "CR")))))) ; theorem :: FILEREC1:43 (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")) "," (Set (Var "r")) "being" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "r")) ($#r1_filerec1 :::"is_a_record_of"::: ) (Set (Var "f")) "," (Set (Var "CR")))) "holds" (Bool (Set (Var "r")) ($#r1_filerec1 :::"is_a_record_of"::: ) (Set (Var "r")) "," (Set (Var "CR"))))) ; theorem :: FILEREC1:44 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "CR")) "," (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "f")) "being" ($#m1_finseq_1 :::"File"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "r1")) ($#r5_finseq_8 :::"is_terminated_by"::: ) (Set (Var "CR"))) & (Bool (Set (Var "r2")) ($#r5_finseq_8 :::"is_terminated_by"::: ) (Set (Var "CR"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k1_finseq_8 :::"^"::: ) (Set (Var "r2"))))) "holds" (Bool "(" (Bool (Set (Var "r1")) ($#r1_filerec1 :::"is_a_record_of"::: ) (Set (Var "f")) "," (Set (Var "CR"))) & (Bool (Set (Var "r2")) ($#r1_filerec1 :::"is_a_record_of"::: ) (Set (Var "f")) "," (Set (Var "CR"))) ")" ))) ;