:: HELLY semantic presentation begin theorem :: HELLY:1 (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_graph_2 :::"^'"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p")))) ; definitionlet "p", "q" be ($#m1_hidden :::"FinSequence":::); func :::"maxPrefix"::: "(" "p" "," "q" ")" -> ($#m1_hidden :::"FinSequence":::) means :: HELLY:def 1 (Bool "(" (Bool it ($#r1_tarski :::"is_a_prefix_of"::: ) "p") & (Bool it ($#r1_tarski :::"is_a_prefix_of"::: ) "q") & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_tarski :::"is_a_prefix_of"::: ) "p") & (Bool (Set (Var "r")) ($#r1_tarski :::"is_a_prefix_of"::: ) "q")) "holds" (Bool (Set (Var "r")) ($#r1_tarski :::"is_a_prefix_of"::: ) it) ")" ) ")" ); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "b1")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "p"))) & (Bool (Set (Var "b1")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q"))) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "p"))) & (Bool (Set (Var "r")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "r")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "b1"))) ")" )) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q"))) & (Bool (Set (Var "b1")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "p"))) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q"))) & (Bool (Set (Var "r")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "r")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "b1"))) ")" ) ")" )) ; end; :: deftheorem defines :::"maxPrefix"::: HELLY:def 1 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) "iff" (Bool "(" (Bool (Set (Var "b3")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "p"))) & (Bool (Set (Var "b3")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q"))) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "p"))) & (Bool (Set (Var "r")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "r")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "b3"))) ")" ) ")" ) ")" )); theorem :: HELLY:2 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q"))) "iff" (Bool (Set ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p"))) ")" )) ; theorem :: HELLY:3 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) ; theorem :: HELLY:4 (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k9_finseq_1 :::"*>"::: ) ) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "p")))) ; theorem :: HELLY:5 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "holds" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )))) ; theorem :: HELLY:6 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))))) ; theorem :: HELLY:7 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))))) ; theorem :: HELLY:8 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q")))) "iff" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) ")" )) ; theorem :: HELLY:9 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) ; begin theorem :: HELLY:10 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))))) ; theorem :: HELLY:11 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Bool "not" (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) "is" ($#v3_glib_001 :::"trivial"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) ))))) ; theorem :: HELLY:12 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "i")) "being" ($#v1_abian :::"odd"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" )))) "holds" (Bool "ex" (Set (Var "j")) "being" ($#v1_abian :::"odd"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "i")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) ")" ))))) ; registrationlet "G" be ($#m1_hidden :::"_Graph":::); cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m3_glib_001 :::"Walk"::: ) "of" "G"; end; theorem :: HELLY:13 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "W2")) ($#k13_glib_001 :::".vertices()"::: ) )))) ; theorem :: HELLY:14 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "W2")) ($#k14_glib_001 :::".edges()"::: ) )))) ; theorem :: HELLY:15 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Var "W1")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")))))) ; theorem :: HELLY:16 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#v3_glib_001 :::"trivial"::: ) ) & (Bool (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) ))) "holds" (Bool (Set (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W2"))))) ; theorem :: HELLY:17 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Trail":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) )) & (Bool (Set (Set (Var "W1")) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "W2")) ($#k14_glib_001 :::".edges()"::: ) ))) "holds" (Bool (Set (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2"))) "is" ($#v4_glib_001 :::"Trail-like"::: ) ))) ; theorem :: HELLY:18 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "P1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P2")) ($#k3_glib_001 :::".first()"::: ) )) & (Bool (Set (Var "P1")) "is" ($#v1_glib_001 :::"open"::: ) ) & (Bool (Set (Var "P2")) "is" ($#v1_glib_001 :::"open"::: ) ) & (Bool (Set (Set (Var "P1")) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "P2")) ($#k14_glib_001 :::".edges()"::: ) )) & "(" (Bool (Bool (Set (Set (Var "P1")) ($#k3_glib_001 :::".first()"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P2")) ($#k13_glib_001 :::".vertices()"::: ) ))) "implies" (Bool (Set (Set (Var "P1")) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P2")) ($#k4_glib_001 :::".last()"::: ) )) ")" & (Bool (Set (Set "(" (Set (Var "P1")) ($#k13_glib_001 :::".vertices()"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "P2")) ($#k13_glib_001 :::".vertices()"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "P1")) ($#k3_glib_001 :::".first()"::: ) ")" ) "," (Set "(" (Set (Var "P1")) ($#k4_glib_001 :::".last()"::: ) ")" ) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set (Var "P1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "P2"))) "is" ($#v5_glib_001 :::"Path-like"::: ) ))) ; theorem :: HELLY:19 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "P1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P2")) ($#k3_glib_001 :::".first()"::: ) )) & (Bool (Set (Var "P1")) "is" ($#v1_glib_001 :::"open"::: ) ) & (Bool (Set (Var "P2")) "is" ($#v1_glib_001 :::"open"::: ) ) & (Bool (Set (Set "(" (Set (Var "P1")) ($#k13_glib_001 :::".vertices()"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "P2")) ($#k13_glib_001 :::".vertices()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "P1")) ($#k4_glib_001 :::".last()"::: ) ")" ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "P1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "P2"))) "is" ($#v1_glib_001 :::"open"::: ) ) & (Bool (Set (Set (Var "P1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "P2"))) "is" ($#v5_glib_001 :::"Path-like"::: ) ) ")" ))) ; theorem :: HELLY:20 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "P1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P2")) ($#k3_glib_001 :::".first()"::: ) )) & (Bool (Set (Set (Var "P2")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P1")) ($#k3_glib_001 :::".first()"::: ) )) & (Bool (Set (Var "P1")) "is" ($#v1_glib_001 :::"open"::: ) ) & (Bool (Set (Var "P2")) "is" ($#v1_glib_001 :::"open"::: ) ) & (Bool (Set (Set (Var "P1")) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "P2")) ($#k14_glib_001 :::".edges()"::: ) )) & (Bool (Set (Set "(" (Set (Var "P1")) ($#k13_glib_001 :::".vertices()"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "P2")) ($#k13_glib_001 :::".vertices()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "P1")) ($#k4_glib_001 :::".last()"::: ) ")" ) "," (Set "(" (Set (Var "P1")) ($#k3_glib_001 :::".first()"::: ) ")" ) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set (Var "P1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "P2"))) "is" ($#v8_glib_001 :::"Cycle-like"::: ) ))) ; theorem :: HELLY:21 (Bool "for" (Set (Var "G")) "being" ($#v7_glib_000 :::"simple"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "k")) "being" ($#v1_abian :::"odd"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W1")))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W2")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#v1_abian :::"odd"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "W1")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) ")" )) "holds" (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "W1")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))))))) ; theorem :: HELLY:22 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) ))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ")" )) "is" ($#v1_abian :::"odd"::: ) ))) ; theorem :: HELLY:23 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) )) & (Bool (Bool "not" (Set (Var "W1")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "W2"))))) "holds" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W1")))))) ; theorem :: HELLY:24 (Bool "for" (Set (Var "G")) "being" ($#v5_glib_000 :::"non-multi"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) )) & (Bool (Bool "not" (Set (Var "W1")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "W2")))) & (Bool (Bool "not" (Set (Var "W2")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "W1"))))) "holds" (Bool (Set (Set (Var "W1")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "W2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ))))) ; begin definitionmode _Tree is ($#v3_glib_002 :::"Tree-like"::: ) ($#m1_hidden :::"_Graph":::); let "G" be ($#m1_hidden :::"_Graph":::); mode _Subtree of "G" is ($#v3_glib_002 :::"Tree-like"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "T" be ($#m1_hidden :::"_Tree":::); cluster ($#v4_glib_001 :::"Trail-like"::: ) -> ($#v5_glib_001 :::"Path-like"::: ) for ($#m3_glib_001 :::"Walk"::: ) "of" "T"; end; theorem :: HELLY:25 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "P")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "T")) "st" (Bool (Bool (Bool "not" (Set (Var "P")) "is" ($#v3_glib_001 :::"trivial"::: ) ))) "holds" (Bool (Set (Var "P")) "is" ($#v1_glib_001 :::"open"::: ) ))) ; registrationlet "T" be ($#m1_hidden :::"_Tree":::); cluster ($#~v3_glib_001 "non" ($#v3_glib_001 :::"trivial"::: ) ) ($#v5_glib_001 :::"Path-like"::: ) -> ($#v1_glib_001 :::"open"::: ) for ($#m3_glib_001 :::"Walk"::: ) "of" "T"; end; theorem :: HELLY:26 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "P")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#v1_abian :::"odd"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P"))))) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))))) ; theorem :: HELLY:27 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P1")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "P2")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) (Set (Var "P2")))))) ; definitionlet "T" be ($#m1_hidden :::"_Tree":::); let "a", "b" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "T")); func "T" :::".pathBetween"::: "(" "a" "," "b" ")" -> ($#m3_glib_001 :::"Path":::) "of" "T" means :: HELLY:def 2 (Bool it ($#r1_glib_001 :::"is_Walk_from"::: ) "a" "," "b"); end; :: deftheorem defines :::".pathBetween"::: HELLY:def 2 : (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "b4")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool (Set (Var "b4")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" )))); theorem :: HELLY:28 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))) ; theorem :: HELLY:29 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) )) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) )) ")" ))) ; registrationlet "T" be ($#m1_hidden :::"_Tree":::); let "a" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "T")); cluster (Set "T" ($#k2_helly :::".pathBetween"::: ) "(" "a" "," "a" ")" ) -> ($#v1_glib_001 :::"closed"::: ) ; end; registrationlet "T" be ($#m1_hidden :::"_Tree":::); let "a" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "T")); cluster (Set "T" ($#k2_helly :::".pathBetween"::: ) "(" "a" "," "a" ")" ) -> ($#v3_glib_001 :::"trivial"::: ) ; end; theorem :: HELLY:30 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: HELLY:31 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k6_glib_001 :::".reverse()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" )))) ; theorem :: HELLY:32 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) )))) ; theorem :: HELLY:33 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "t")) "being" ($#m1_glib_000 :::"_Subtree":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "t")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a9"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9")))) "holds" (Bool (Set (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a9")) "," (Set (Var "b9")) ")" )))))) ; theorem :: HELLY:34 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "t")) "being" ($#m1_glib_000 :::"_Subtree":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "t")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "t"))))) "holds" (Bool (Set (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "t"))))))) ; theorem :: HELLY:35 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "P")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#v1_abian :::"odd"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")))) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )))))) ; theorem :: HELLY:36 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) )) "iff" (Bool (Set (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) ($#k7_glib_001 :::".append"::: ) (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "c")) "," (Set (Var "b")) ")" ")" ))) ")" ))) ; theorem :: HELLY:37 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) )) "iff" (Bool (Set (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ))) ; theorem :: HELLY:38 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "P1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P2")) ($#k3_glib_001 :::".first()"::: ) )) & (Bool (Set (Set "(" (Set (Var "P1")) ($#k13_glib_001 :::".vertices()"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "P2")) ($#k13_glib_001 :::".vertices()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "P1")) ($#k4_glib_001 :::".last()"::: ) ")" ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set (Var "P1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "P2"))) "is" ($#v5_glib_001 :::"Path-like"::: ) ))) ; theorem :: HELLY:39 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) )) "iff" (Bool (Set (Set "(" (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "c")) "," (Set (Var "b")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "c")) ($#k1_tarski :::"}"::: ) )) ")" ))) ; theorem :: HELLY:40 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "P2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" )) & (Bool (Bool "not" (Set (Var "P1")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "P2")))) & (Bool (Bool "not" (Set (Var "P2")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "P1")))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P1")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "P1")) "," (Set (Var "P2")) ")" ")" ) ")" )))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "d")) "," (Set (Var "b")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "d")) "," (Set (Var "c")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "d")) ($#k1_tarski :::"}"::: ) ))))) ; definitionlet "T" be ($#m1_hidden :::"_Tree":::); let "a", "b", "c" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "T")); func :::"MiddleVertex"::: "(" "a" "," "b" "," "c" ")" -> ($#m1_subset_1 :::"Vertex":::) "of" "T" means :: HELLY:def 3 (Bool (Set (Set "(" (Set "(" (Set "(" "T" ($#k2_helly :::".pathBetween"::: ) "(" "a" "," "b" ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" "T" ($#k2_helly :::".pathBetween"::: ) "(" "b" "," "c" ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" "T" ($#k2_helly :::".pathBetween"::: ) "(" "c" "," "a" ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) it ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"MiddleVertex"::: HELLY:def 3 : (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "b5")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )) "iff" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "c")) "," (Set (Var "a")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b5")) ($#k1_tarski :::"}"::: ) )) ")" ))); theorem :: HELLY:41 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) ")" )))) ; theorem :: HELLY:42 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) ")" )))) ; theorem :: HELLY:43 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) ")" )))) ; theorem :: HELLY:44 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )))) ; theorem :: HELLY:45 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) ")" )))) ; theorem :: HELLY:46 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ))) "holds" (Bool (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) ; theorem :: HELLY:47 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: HELLY:48 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: HELLY:49 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: HELLY:50 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: HELLY:51 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "P2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" )) & (Bool (Bool "not" (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P2")) ($#k13_glib_001 :::".vertices()"::: ) ))) & (Bool (Bool "not" (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P1")) ($#k13_glib_001 :::".vertices()"::: ) )))) "holds" (Bool (Set ($#k3_helly :::"MiddleVertex"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P1")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "P1")) "," (Set (Var "P2")) ")" ")" ) ")" )))))) ; theorem :: HELLY:52 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "," (Set (Var "P3")) "," (Set (Var "P4")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "P2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" )) & (Bool (Set (Var "P3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" )) & (Bool (Set (Var "P4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k2_helly :::".pathBetween"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" )) & (Bool (Bool "not" (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P2")) ($#k13_glib_001 :::".vertices()"::: ) ))) & (Bool (Bool "not" (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P1")) ($#k13_glib_001 :::".vertices()"::: ) ))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P4")) ($#k13_glib_001 :::".vertices()"::: ) )))) "holds" (Bool (Set (Set (Var "P1")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "P1")) "," (Set (Var "P2")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "P3")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_helly :::"maxPrefix"::: ) "(" (Set (Var "P3")) "," (Set (Var "P4")) ")" ")" ) ")" )))))) ; theorem :: HELLY:53 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "(" (Bool "ex" (Set (Var "t")) "being" ($#m1_glib_000 :::"_Subtree":::) "of" (Set (Var "T")) "st" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "t"))))) & (Bool "(" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "s"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "s"))) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "s"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "s"))) ")" ) "or" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "s"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "s"))) ")" ) ")" ) ")" ) ")" )) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "S"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; begin definitionlet "F" be ($#m1_hidden :::"set"::: ) ; attr "F" is :::"with_Helly_property"::: means :: HELLY:def 4 (Bool "for" (Set (Var "H")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "H")) ($#r1_tarski :::"c="::: ) "F") & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "H"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "x")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "y"))) ")" )) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "H"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))); end; :: deftheorem defines :::"with_Helly_property"::: HELLY:def 4 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_helly :::"with_Helly_property"::: ) ) "iff" (Bool "for" (Set (Var "H")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "H")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "H"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "x")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "y"))) ")" )) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "H"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" )); theorem :: HELLY:54 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"_Tree":::) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "t")) "being" ($#m1_glib_000 :::"_Subtree":::) "of" (Set (Var "T")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "t"))))) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#v1_helly :::"with_Helly_property"::: ) ))) ;