:: YELLOW15 semantic presentation begin scheme :: YELLOW15:sch 1 SeqLambda1C{ F1() -> ($#m1_hidden :::"Nat":::), F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set F1 "(" ")" )))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "i"))])) "implies" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "i")) ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "i"))])) "implies" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "i")) ")" )) ")" ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set F1 "(" ")" )))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "i"))])) "implies" (Bool (Set F3 "(" (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "i"))])) "implies" (Bool (Set F4 "(" (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) ")" ")" )) proof end; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Const "X"))); let "q" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); func :::"MergeSequence"::: "(" "p" "," "q" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) "X") means :: YELLOW15:def 1 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "p")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k14_funcop_1 :::"IFEQ"::: ) "(" (Set "(" "q" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set ($#k8_margrel1 :::"TRUE"::: ) ) "," (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" "X" ($#k6_subset_1 :::"\"::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"MergeSequence"::: YELLOW15:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k14_funcop_1 :::"IFEQ"::: ) "(" (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set ($#k8_margrel1 :::"TRUE"::: ) ) "," (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ) ")" )) ")" ) ")" ) ")" ))))); theorem :: YELLOW15:1 canceled; theorem :: YELLOW15:2 canceled; theorem :: YELLOW15:3 canceled; theorem :: YELLOW15:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))))) ; theorem :: YELLOW15:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))))) ; theorem :: YELLOW15:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))))))) ; theorem :: YELLOW15:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) ")" ) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: YELLOW15:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ) ")" ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ))))) ; theorem :: YELLOW15:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 1))))) ; theorem :: YELLOW15:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "implies" (Bool (Set (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) "implies" (Bool (Set (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "x")))) ")" ")" )))) ; theorem :: YELLOW15:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_finseq_4 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 2))))) ; theorem :: YELLOW15:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "implies" (Bool (Set (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_finseq_4 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) "implies" (Bool (Set (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_finseq_4 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "x")))) ")" & "(" (Bool (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "implies" (Bool (Set (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_finseq_4 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" & "(" (Bool (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) "implies" (Bool (Set (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_finseq_4 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "y")))) ")" ")" )))) ; theorem :: YELLOW15:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 3))))) ; theorem :: YELLOW15:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "implies" (Bool (Set (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) "implies" (Bool (Set (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "x")))) ")" & "(" (Bool (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "implies" (Bool (Set (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" & "(" (Bool (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) "implies" (Bool (Set (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "y")))) ")" & "(" (Bool (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "implies" (Bool (Set (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" & "(" (Bool (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) "implies" (Bool (Set (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "z")))) ")" ")" )))) ; theorem :: YELLOW15:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "holds" (Bool "{" (Set "(" ($#k8_setfam_1 :::"Intersect"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ")" ) ")" ) where q "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) : (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) "}" "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))))) ; registration cluster -> ($#v1_margrel1 :::"boolean-valued"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); func :::"Components"::: "Y" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "X" means :: YELLOW15:def 2 (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) "X") "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) "Y")) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) "Y") & (Bool it ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k8_setfam_1 :::"Intersect"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ")" ) ")" ) where q "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) : (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) "}" ) ")" )); end; :: deftheorem defines :::"Components"::: YELLOW15:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow15 :::"Components"::: ) (Set (Var "Y")))) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Y")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k8_setfam_1 :::"Intersect"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k1_yellow15 :::"MergeSequence"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ")" ) ")" ) where q "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) : (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) "}" ) ")" )) ")" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); cluster (Set ($#k2_yellow15 :::"Components"::: ) "Y") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: YELLOW15:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_yellow15 :::"Components"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: YELLOW15:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k2_yellow15 :::"Components"::: ) (Set (Var "Y"))) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set ($#k2_yellow15 :::"Components"::: ) (Set (Var "Z")))))) ; theorem :: YELLOW15:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_yellow15 :::"Components"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: YELLOW15:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k2_yellow15 :::"Components"::: ) (Set (Var "Y")))) & (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k2_yellow15 :::"Components"::: ) (Set (Var "Y")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); attr "Y" is :::"in_general_position"::: means :: YELLOW15:def 3 (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_yellow15 :::"Components"::: ) "Y"))); end; :: deftheorem defines :::"in_general_position"::: YELLOW15:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v1_yellow15 :::"in_general_position"::: ) ) "iff" (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_yellow15 :::"Components"::: ) (Set (Var "Y"))))) ")" ))); theorem :: YELLOW15:20 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Z")) "is" ($#v1_yellow15 :::"in_general_position"::: ) ) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "Y")) "is" ($#v1_yellow15 :::"in_general_position"::: ) ))) ; theorem :: YELLOW15:21 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "Y")) "is" ($#v1_yellow15 :::"in_general_position"::: ) ))) ; theorem :: YELLOW15:22 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) "is" ($#v1_yellow15 :::"in_general_position"::: ) )) "holds" (Bool (Set ($#k2_yellow15 :::"Components"::: ) (Set (Var "Y"))) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X"))))) ; begin theorem :: YELLOW15:23 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "L"))) "is" ($#v3_waybel23 :::"infs-closed"::: ) ) & (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "L"))) "is" ($#v4_waybel23 :::"sups-closed"::: ) ) ")" )) ; theorem :: YELLOW15:24 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "L"))) "is" ($#v6_waybel23 :::"with_bottom"::: ) ) & (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "L"))) "is" ($#v7_waybel23 :::"with_top"::: ) ) ")" )) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_struct_0 :::"[#]"::: ) "L") -> ($#v3_waybel23 :::"infs-closed"::: ) ($#v4_waybel23 :::"sups-closed"::: ) ($#v6_waybel23 :::"with_bottom"::: ) ($#v7_waybel23 :::"with_top"::: ) ; end; theorem :: YELLOW15:25 (Bool "for" (Set (Var "L")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "holds" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "L"))) "is" ($#m1_waybel23 :::"CLbasis"::: ) "of" (Set (Var "L")))) ; theorem :: YELLOW15:26 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v8_struct_0 :::"finite"::: ) )) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel_8 :::"CompactSublatt"::: ) (Set (Var "L")) ")" )))) ; theorem :: YELLOW15:27 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v1_finset_1 :::"infinite"::: ) )) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "B")) ")" ))))) ; theorem :: YELLOW15:28 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_pre_topc :::"T_0"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T")))))) ; theorem :: YELLOW15:29 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "for" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B")) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")))) "holds" (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_yellow15 :::"Components"::: ) (Set (Var "B")))) "or" (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y"))) "or" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" ))))) ; theorem :: YELLOW15:30 (Bool "for" (Set (Var "T")) "being" ($#v6_pre_topc :::"T_0"::: ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v8_struct_0 :::"infinite"::: ) )) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) "holds" (Bool (Set (Var "B")) "is" ($#v1_finset_1 :::"infinite"::: ) ))) ; theorem :: YELLOW15:31 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v8_struct_0 :::"finite"::: ) )) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "A")) where A "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" ) ($#r2_hidden :::"in"::: ) (Set (Var "B")))))) ;