:: LEXBFS semantic presentation begin theorem :: LEXBFS:1 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) "{" (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "A")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "w"))) & (Bool (Set (Var "w")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "A")) ($#k2_nat_1 :::"+"::: ) (Set (Var "B")))) ")" ) "}" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k2_nat_1 :::"+"::: ) (Num 1)))))) ; theorem :: LEXBFS:2 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n"))))) ; notationlet "S" be ($#m1_hidden :::"set"::: ) ; synonym :::"with_finite-elements"::: "S" for :::"finite-membered"::: ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v5_finset_1 :::"with_finite-elements"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" )); end; definitioncanceled; let "f", "g" be ($#m1_hidden :::"Function":::); func "f" :::".\/"::: "g" -> ($#m1_hidden :::"Function":::) means :: LEXBFS:def 2 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" )))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" "g" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem LEXBFS:def 1 : canceled; :: deftheorem defines :::".\/"::: LEXBFS:def 2 : (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_lexbfs :::".\/"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" )); theorem :: LEXBFS:3 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "k")) ")" ) ($#k2_finsub_1 :::"\"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" ))) "iff" (Bool "(" (Bool (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) ")" ) ")" )) ; theorem :: LEXBFS:4 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "k")) ")" ) ($#k2_finsub_1 :::"\"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "k")) ")" ) ($#k2_finsub_1 :::"\"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set (Var "m")) ")" ) ")" )))) ; theorem :: LEXBFS:5 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "k")) ")" ) ($#k2_finsub_1 :::"\"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k1_finsub_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "k")) ")" ) ($#k2_finsub_1 :::"\"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))) ; definitionlet "f" be ($#m1_hidden :::"Relation":::); attr "f" is :::"natsubset-yielding"::: means :: LEXBFS:def 3 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "f") ($#r1_tarski :::"c="::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))); end; :: deftheorem defines :::"natsubset-yielding"::: LEXBFS:def 3 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_lexbfs :::"natsubset-yielding"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_finset_1 :::"finite-yielding"::: ) ($#v1_lexbfs :::"natsubset-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "f" be ($#v2_finset_1 :::"finite-yielding"::: ) ($#v1_lexbfs :::"natsubset-yielding"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; :: original: :::"."::: redefine func "f" :::"."::: "x" -> ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: LEXBFS:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set "(" (Set (Var "a")) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ) ($#r1_hidden :::"<>"::: ) (Set "(" (Set (Var "b")) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) )))) ; definitionlet "F" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::); let "S" be ($#m1_hidden :::"set"::: ) ; let "k" be ($#m1_hidden :::"Nat":::); func "F" :::".incSubset"::: "(" "S" "," "k" ")" -> ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::) means :: LEXBFS:def 4 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F")) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "S") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F"))) "implies" (Bool (Set it ($#k1_recdef_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k2_nat_1 :::"+"::: ) "k")) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) "S"))) "implies" (Bool (Set it ($#k1_recdef_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "y")))) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::".incSubset"::: LEXBFS:def 4 : (Bool "for" (Set (Var "F")) "being" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b4")) "being" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_lexbfs :::".incSubset"::: ) "(" (Set (Var "S")) "," (Set (Var "k")) ")" )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_recdef_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_recdef_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "y")))) ")" ")" ) ")" ) ")" ) ")" ))))); definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Const "n")) ")" ); func :::"max"::: "(" "B" "," "T" ")" -> ($#m1_hidden :::"bag":::) "of" "n" means :: LEXBFS:def 5 (Bool "(" (Bool it ($#r2_hidden :::"in"::: ) "B") & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"bag":::) "of" "n" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "B")) "holds" (Bool (Set (Var "x")) ($#r1_termord :::"<="::: ) it "," "T") ")" ) ")" ); end; :: deftheorem defines :::"max"::: LEXBFS:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_lexbfs :::"max"::: ) "(" (Set (Var "B")) "," (Set (Var "T")) ")" )) "iff" (Bool "(" (Bool (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "x")) ($#r1_termord :::"<="::: ) (Set (Var "b4")) "," (Set (Var "T"))) ")" ) ")" ) ")" ))))); registrationlet "O" be ($#m1_hidden :::"Ordinal":::); cluster (Set ($#k4_bagorder :::"InvLexOrder"::: ) "O") -> ($#v6_relat_2 :::"connected"::: ) ; end; begin definitionlet "s" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); attr "s" is :::"iterative"::: means :: LEXBFS:def 6 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set "s" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set "s" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set "s" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "s" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))); end; :: deftheorem defines :::"iterative"::: LEXBFS:def 6 : (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v2_lexbfs :::"iterative"::: ) ) "iff" (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" )); definitionlet "S" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); attr "S" is :::"eventually-constant"::: means :: LEXBFS:def 7 (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set "S" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "S" ($#k1_funct_1 :::"."::: ) (Set (Var "m")))))); end; :: deftheorem defines :::"eventually-constant"::: LEXBFS:def 7 : (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_lexbfs :::"eventually-constant"::: ) ) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v13_glib_000 :::"halting"::: ) ($#v2_lexbfs :::"iterative"::: ) ($#v3_lexbfs :::"eventually-constant"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: LEXBFS:7 (Bool "for" (Set (Var "Gs")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "Gs")) "is" ($#v13_glib_000 :::"halting"::: ) ) & (Bool (Set (Var "Gs")) "is" ($#v2_lexbfs :::"iterative"::: ) )) "holds" (Bool (Set (Var "Gs")) "is" ($#v3_lexbfs :::"eventually-constant"::: ) )) ; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v13_glib_000 :::"halting"::: ) ($#v2_lexbfs :::"iterative"::: ) -> ($#v3_lexbfs :::"eventually-constant"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: LEXBFS:8 (Bool "for" (Set (Var "Gs")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "Gs")) "is" ($#v3_lexbfs :::"eventually-constant"::: ) )) "holds" (Bool (Set (Var "Gs")) "is" ($#v13_glib_000 :::"halting"::: ) )) ; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v3_lexbfs :::"eventually-constant"::: ) -> ($#v13_glib_000 :::"halting"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: LEXBFS:9 (Bool "for" (Set (Var "Gs")) "being" ($#v2_lexbfs :::"iterative"::: ) ($#v3_lexbfs :::"eventually-constant"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "Gs")) ($#k39_glib_000 :::".Lifespan()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "Gs")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "Gs")) ($#k39_glib_000 :::".Lifespan()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "Gs")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))))) ; theorem :: LEXBFS:10 (Bool "for" (Set (Var "Gs")) "being" ($#v2_lexbfs :::"iterative"::: ) ($#v3_lexbfs :::"eventually-constant"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "Gs")) ($#k39_glib_000 :::".Lifespan()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "Gs")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Gs")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))))) ; begin definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); mode :::"preVNumberingSeq"::: "of" "G" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: LEXBFS:def 8 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ))); end; :: deftheorem defines :::"preVNumberingSeq"::: LEXBFS:def 8 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_lexbfs :::"preVNumberingSeq"::: ) "of" (Set (Var "G"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ))) ")" ))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "S" be ($#m1_lexbfs :::"preVNumberingSeq"::: ) "of" (Set (Const "G")); let "n" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "S" :::"."::: "n" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "S" be ($#m1_lexbfs :::"preVNumberingSeq"::: ) "of" (Set (Const "G")); attr "S" is :::"vertex-numbering"::: means :: LEXBFS:def 9 (Bool "(" (Bool (Set "S" ($#k5_lexbfs :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "S" "is" ($#v2_lexbfs :::"iterative"::: ) ) & (Bool "S" "is" ($#v13_glib_000 :::"halting"::: ) ) & (Bool (Set "S" ($#k39_glib_000 :::".Lifespan()"::: ) ) ($#r1_hidden :::"="::: ) (Set "G" ($#k15_glib_000 :::".order()"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set "S" ($#k39_glib_000 :::".Lifespan()"::: ) ))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "G" "st" (Bool "(" (Bool (Bool "not" (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "S" ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" )))) & (Bool (Set "S" ($#k5_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "S" ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "w")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "(" "S" ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" ))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"vertex-numbering"::: LEXBFS:def 9 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"preVNumberingSeq"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v4_lexbfs :::"vertex-numbering"::: ) ) "iff" (Bool "(" (Bool (Set (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "S")) "is" ($#v2_lexbfs :::"iterative"::: ) ) & (Bool (Set (Var "S")) "is" ($#v13_glib_000 :::"halting"::: ) ) & (Bool (Set (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" )))) & (Bool (Set (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "w")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" ))) ")" )) ")" ) ")" ) ")" ))); registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v4_lexbfs :::"vertex-numbering"::: ) for ($#m1_lexbfs :::"preVNumberingSeq"::: ) "of" "G"; end; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); cluster ($#v4_lexbfs :::"vertex-numbering"::: ) -> ($#v13_glib_000 :::"halting"::: ) ($#v2_lexbfs :::"iterative"::: ) for ($#m1_lexbfs :::"preVNumberingSeq"::: ) "of" "G"; end; definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); mode VNumberingSeq of "G" is ($#v4_lexbfs :::"vertex-numbering"::: ) ($#m1_lexbfs :::"preVNumberingSeq"::: ) "of" "G"; end; definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "S" be ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Const "G")); let "n" be ($#m1_hidden :::"Nat":::); func "S" :::".PickedAt"::: "n" -> ($#m1_hidden :::"set"::: ) means :: LEXBFS:def 10 (Bool it ($#r1_hidden :::"="::: ) (Set ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ))) if (Bool "n" ($#r1_xxreal_0 :::">="::: ) (Set "S" ($#k39_glib_000 :::".Lifespan()"::: ) )) otherwise (Bool "(" (Bool (Bool "not" it ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "S" ($#k5_lexbfs :::"."::: ) "n" ")" )))) & (Bool (Set "S" ($#k5_lexbfs :::"."::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "S" ($#k5_lexbfs :::"."::: ) "n" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" it ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "(" "S" ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) "n" ")" ) ")" ))) ")" ); end; :: deftheorem defines :::".PickedAt"::: LEXBFS:def 10 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k6_lexbfs :::".PickedAt"::: ) (Set (Var "n")))) "iff" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k6_lexbfs :::".PickedAt"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" )))) & (Bool (Set (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "b4")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" ))) ")" ) ")" ) ")" ")" ))))); theorem :: LEXBFS:11 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "S")) ($#k6_lexbfs :::".PickedAt"::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "S")) ($#k6_lexbfs :::".PickedAt"::: ) (Set (Var "n")) ")" ) ($#k1_tarski :::"}"::: ) ))) ")" )))) ; theorem :: LEXBFS:12 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "S")) ($#k6_lexbfs :::".PickedAt"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n"))))))) ; theorem :: LEXBFS:13 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))))) ; theorem :: LEXBFS:14 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ")" ) ($#k2_finsub_1 :::"\"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" )))))) ; theorem :: LEXBFS:15 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) )) & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" )))) "implies" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "x")))) ")" ")" ))))) ; theorem :: LEXBFS:16 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))) ")" ))))) ; theorem :: LEXBFS:17 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "m"))) ($#r1_relset_1 :::"c="::: ) (Set (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n"))))))) ; theorem :: LEXBFS:18 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) )))) ; theorem :: LEXBFS:19 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "m")) ")" ))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "m")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "v")))))))) ; theorem :: LEXBFS:20 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "m")) ")" ))) & (Bool (Set (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "m")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "S")) ($#k6_lexbfs :::".PickedAt"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))))))) ; theorem :: LEXBFS:21 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool "(" (Bool (Set (Set (Var "S")) ($#k6_lexbfs :::".PickedAt"::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "m")) ")" ))) & (Bool (Set (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "m")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "S")) ($#k6_lexbfs :::".PickedAt"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")))) ")" )))) ; theorem :: LEXBFS:22 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "m")) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "m")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "v")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) & (Bool (Set (Set "(" (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "m")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "v")))) ")" ))))) ; theorem :: LEXBFS:23 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "a")) ")" ) ")" ) ")" ))))))) ; theorem :: LEXBFS:24 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m1_lexbfs :::"VNumberingSeq":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "b"))))) "holds" (Bool "not" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k39_glib_000 :::".Lifespan()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k5_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")) ")" ) ")" ) ")" )))))))) ; begin definitionlet "X1", "X3" be ($#m1_hidden :::"set"::: ) ; let "X2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Const "X1")) "," (Set (Const "X3")) ")" ")" ) "," (Set (Const "X2")) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"`1"::: redefine func "x" :::"`1"::: -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "X1" "," "X3" ")" ); end; definitionlet "X1", "X3" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X2" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X1")) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Const "X2")) "," (Set (Const "X3")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"`2"::: redefine func "x" :::"`2"::: -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "X2" "," "X3" ")" ); end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode LexBFS:Labeling of "G" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); end; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "L" be ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" (Set (Const "G")); cluster (Set "L" ($#k1_xtuple_0 :::"`1"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set "L" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); func :::"LexBFS:Init"::: "G" -> ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" "G" equals :: LEXBFS:def 11 (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"LexBFS:Init"::: LEXBFS:def 11 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set ($#k9_lexbfs :::"LexBFS:Init"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "L" be ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" (Set (Const "G")); func :::"LexBFS:PickUnnumbered"::: "L" -> ($#m1_subset_1 :::"Vertex":::) "of" "G" means :: LEXBFS:def 12 (Bool it ($#r1_hidden :::"="::: ) (Set ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ))) if (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "L" ($#k7_lexbfs :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G")) otherwise (Bool "ex" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" )(Bool "ex" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" )(Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")))) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set "(" "L" ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" "L" ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set "(" (Set (Var "x")) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "y")) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) )) ")" )) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k10_subset_1 :::"choose"::: ) (Set "(" (Set (Var "F")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set "(" ($#k4_lexbfs :::"max"::: ) "(" (Set (Var "B")) "," (Set "(" ($#k4_bagorder :::"InvLexOrder"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) ")" ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) ")" )))); end; :: deftheorem defines :::"LexBFS:PickUnnumbered"::: LEXBFS:def 12 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_lexbfs :::"LexBFS:PickUnnumbered"::: ) (Set (Var "L")))) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_lexbfs :::"LexBFS:PickUnnumbered"::: ) (Set (Var "L")))) "iff" (Bool "ex" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" )(Bool "ex" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" )(Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")))) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set "(" (Set (Var "x")) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "y")) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) )) ")" )) ")" ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_subset_1 :::"choose"::: ) (Set "(" (Set (Var "F")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set "(" ($#k4_lexbfs :::"max"::: ) "(" (Set (Var "B")) "," (Set "(" ($#k4_bagorder :::"InvLexOrder"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) ")" ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) ")" )))) ")" ) ")" ")" )))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "L" be ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" (Set (Const "G")); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "n" be ($#m1_hidden :::"Nat":::); func :::"LexBFS:Update"::: "(" "L" "," "v" "," "n" ")" -> ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" "G" equals :: LEXBFS:def 13 (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" "L" ($#k7_lexbfs :::"`1"::: ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "v" ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "(" "G" ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) "n" ")" ) ")" ) ")" ) "," (Set "(" (Set "(" "L" ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_lexbfs :::".\/"::: ) (Set "(" (Set "(" (Set "(" "G" ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k6_domain_1 :::"{"::: ) "v" ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k2_finsub_1 :::"\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" "L" ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ) ")" ) ($#k4_rfunct_3 :::"-->"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set "(" "G" ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) "n" ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"LexBFS:Update"::: LEXBFS:def 13 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k11_lexbfs :::"LexBFS:Update"::: ) "(" (Set (Var "L")) "," (Set (Var "v")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "v")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_lexbfs :::".\/"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "G")) ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k2_finsub_1 :::"\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ) ")" ) ($#k4_rfunct_3 :::"-->"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) )))))); theorem :: LEXBFS:25 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))))) "holds" (Bool (Set (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k11_lexbfs :::"LexBFS:Update"::: ) "(" (Set (Var "L")) "," (Set (Var "v")) "," (Set (Var "k")) ")" ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))))))) ; theorem :: LEXBFS:26 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" )))) "holds" (Bool (Set (Set "(" (Set "(" ($#k11_lexbfs :::"LexBFS:Update"::: ) "(" (Set (Var "L")) "," (Set (Var "v")) "," (Set (Var "k")) ")" ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))))))) ; theorem :: LEXBFS:27 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" ))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k11_lexbfs :::"LexBFS:Update"::: ) "(" (Set (Var "L")) "," (Set (Var "v")) "," (Set (Var "k")) ")" ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ($#k6_domain_1 :::"}"::: ) )))))))) ; definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "L" be ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" (Set (Const "G")); func :::"LexBFS:Step"::: "L" -> ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" "G" equals :: LEXBFS:def 14 "L" if (Bool (Set "G" ($#k15_glib_000 :::".order()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" "L" ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ))) otherwise (Set ($#k11_lexbfs :::"LexBFS:Update"::: ) "(" "L" "," (Set "(" ($#k10_lexbfs :::"LexBFS:PickUnnumbered"::: ) "L" ")" ) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" "L" ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"LexBFS:Step"::: LEXBFS:def 14 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" (Set (Var "G")) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" )))) "implies" (Bool (Set ($#k12_lexbfs :::"LexBFS:Step"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Var "L"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ))))) "implies" (Bool (Set ($#k12_lexbfs :::"LexBFS:Step"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k11_lexbfs :::"LexBFS:Update"::: ) "(" (Set (Var "L")) "," (Set "(" ($#k10_lexbfs :::"LexBFS:PickUnnumbered"::: ) (Set (Var "L")) ")" ) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ) ")" ) ")" )) ")" ")" ))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode :::"LexBFS:LabelingSeq"::: "of" "G" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: LEXBFS:def 15 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" "G")); end; :: deftheorem defines :::"LexBFS:LabelingSeq"::: LEXBFS:def 15 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_lexbfs :::"LexBFS:LabelingSeq"::: ) "of" (Set (Var "G"))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" (Set (Var "G")))) ")" ))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "S" be ($#m2_lexbfs :::"LexBFS:LabelingSeq"::: ) "of" (Set (Const "G")); let "n" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "S" :::"."::: "n" -> ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "S" be ($#m2_lexbfs :::"LexBFS:LabelingSeq"::: ) "of" (Set (Const "G")); :: original: :::".Result()"::: redefine func "S" :::".Result()"::: -> ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" "G"; end; definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "S" be ($#m2_lexbfs :::"LexBFS:LabelingSeq"::: ) "of" (Set (Const "G")); func "S" :::"``1"::: -> ($#m1_lexbfs :::"preVNumberingSeq"::: ) "of" "G" means :: LEXBFS:def 16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k5_lexbfs :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" "S" ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ))); end; :: deftheorem defines :::"``1"::: LEXBFS:def 16 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m2_lexbfs :::"LexBFS:LabelingSeq"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m1_lexbfs :::"preVNumberingSeq"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k15_lexbfs :::"``1"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k5_lexbfs :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "S")) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ))) ")" )))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); func :::"LexBFS:CSeq"::: "G" -> ($#m2_lexbfs :::"LexBFS:LabelingSeq"::: ) "of" "G" means :: LEXBFS:def 17 (Bool "(" (Bool (Set it ($#k13_lexbfs :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_lexbfs :::"LexBFS:Init"::: ) "G")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k13_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_lexbfs :::"LexBFS:Step"::: ) (Set "(" it ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"LexBFS:CSeq"::: LEXBFS:def 17 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "b2")) "being" ($#m2_lexbfs :::"LexBFS:LabelingSeq"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")))) "iff" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k13_lexbfs :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_lexbfs :::"LexBFS:Init"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b2")) ($#k13_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_lexbfs :::"LexBFS:Step"::: ) (Set "(" (Set (Var "b2")) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) ")" ))); theorem :: LEXBFS:28 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G"))) "is" ($#v2_lexbfs :::"iterative"::: ) )) ; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); cluster (Set ($#k16_lexbfs :::"LexBFS:CSeq"::: ) "G") -> ($#v2_lexbfs :::"iterative"::: ) ; end; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Const "Y")) ")" ); let "x" be ($#m1_hidden :::"set"::: ) ; :: original: :::"."::: redefine func "f" :::"."::: "x" -> ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "Y"; end; theorem :: LEXBFS:29 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" )))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) "holds" (Bool (Set "(" (Set "(" (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "x")) ")" ) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ) ($#r1_termord :::"<="::: ) (Set "(" (Set "(" (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set "(" ($#k10_lexbfs :::"LexBFS:PickUnnumbered"::: ) (Set (Var "L")) ")" ) ")" ) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ) "," (Set ($#k4_bagorder :::"InvLexOrder"::: ) (Set ($#k5_numbers :::"NAT"::: ) )))))) ; theorem :: LEXBFS:30 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"LexBFS:Labeling":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) "holds" (Bool "not" (Bool (Set ($#k10_lexbfs :::"LexBFS:PickUnnumbered"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" )))))) ; theorem :: LEXBFS:31 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k7_lexbfs :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" ($#k10_lexbfs :::"LexBFS:PickUnnumbered"::: ) (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ) ")" ) ")" ) ")" ))))) ; theorem :: LEXBFS:32 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))))) ; theorem :: LEXBFS:33 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")))))) ; theorem :: LEXBFS:34 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")))))) ; theorem :: LEXBFS:35 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G"))) "is" ($#v3_lexbfs :::"eventually-constant"::: ) )) ; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); cluster (Set ($#k16_lexbfs :::"LexBFS:CSeq"::: ) "G") -> ($#v3_lexbfs :::"eventually-constant"::: ) ; end; theorem :: LEXBFS:36 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))) "iff" (Bool (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ))) ; theorem :: LEXBFS:37 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k39_glib_000 :::".Lifespan()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ))) ; theorem :: LEXBFS:38 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k15_lexbfs :::"``1"::: ) ) "is" ($#v3_lexbfs :::"eventually-constant"::: ) )) ; theorem :: LEXBFS:39 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k15_lexbfs :::"``1"::: ) ")" ) ($#k39_glib_000 :::".Lifespan()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k39_glib_000 :::".Lifespan()"::: ) ))) ; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); cluster (Set (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) "G" ")" ) ($#k15_lexbfs :::"``1"::: ) ) -> ($#v4_lexbfs :::"vertex-numbering"::: ) ; end; theorem :: LEXBFS:40 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k15_lexbfs :::"``1"::: ) ")" ) ($#k40_glib_000 :::".Result()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k14_lexbfs :::".Result()"::: ) ")" ) ($#k7_lexbfs :::"`1"::: ) ))) ; theorem :: LEXBFS:41 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k15_lexbfs :::"``1"::: ) ")" ) ($#k6_lexbfs :::".PickedAt"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k10_lexbfs :::"LexBFS:PickUnnumbered"::: ) (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ))))) ; theorem :: LEXBFS:42 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set ($#k10_lexbfs :::"LexBFS:PickUnnumbered"::: ) (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ))))) "implies" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "v")) ")" ) ($#k1_finsub_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) ))) "or" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ))) ")" )) "implies" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "v")))) ")" ")" ) ")" ) ")" )))) ; theorem :: LEXBFS:43 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "v"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ")" ) ($#k2_finsub_1 :::"\"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" ) ")" )))))) ; theorem :: LEXBFS:44 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "j")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "x"))))))) ; theorem :: LEXBFS:45 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k10_lexbfs :::"LexBFS:PickUnnumbered"::: ) (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" )))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "m")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "x"))))))) ; theorem :: LEXBFS:46 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "m"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set "(" (Set (Var "m")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "x")))))) "holds" (Bool "not" (Bool (Set (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "m"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "x")))))))) ; theorem :: LEXBFS:47 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "x")))))) "holds" (Bool "not" (Bool (Set (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "m")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "x")))))))) ; theorem :: LEXBFS:48 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "m")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "x"))))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set ($#k10_lexbfs :::"LexBFS:PickUnnumbered"::: ) (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" )))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ))) ")" ))))) ; theorem :: LEXBFS:49 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k14_lexbfs :::".Result()"::: ) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) ; theorem :: LEXBFS:50 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k14_lexbfs :::".Result()"::: ) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ) ($#k2_funct_1 :::"""::: ) ) "is" ($#m3_chord :::"VertexScheme"::: ) "of" (Set (Var "G")))) ; theorem :: LEXBFS:51 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ))) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")) ")" )))) "holds" (Bool (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "j")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "a")) ")" ) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ) ($#r1_termord :::"<="::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "j")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "b")) ")" ) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ) "," (Set ($#k4_bagorder :::"InvLexOrder"::: ) (Set ($#k5_numbers :::"NAT"::: ) )))))) ; theorem :: LEXBFS:52 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k17_lexbfs :::"."::: ) (Set (Var "v"))))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ))) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "i")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) ))) ")" ))))) ; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "F" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Const "G")) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ); attr "F" is :::"with_property_L3"::: means :: LEXBFS:def 18 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "G" "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F")) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F")) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F")) & (Bool (Set "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "b")))) & (Bool (Set "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<"::: ) (Set "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_chord :::"are_adjacent"::: ) ) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "c")) ($#r1_chord :::"are_adjacent"::: ) ))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "G" "st" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F")) & (Bool (Set "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "c"))) ($#r1_xxreal_0 :::"<"::: ) (Set "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "d")))) & (Bool (Set (Var "b")) "," (Set (Var "d")) ($#r1_chord :::"are_adjacent"::: ) ) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "d")) ($#r1_chord :::"are_adjacent"::: ) )) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "G" "st" (Bool (Bool (Set (Var "e")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool (Set (Var "e")) "," (Set (Var "b")) ($#r1_chord :::"are_adjacent"::: ) ) & (Bool (Bool "not" (Set (Var "e")) "," (Set (Var "a")) ($#r1_chord :::"are_adjacent"::: ) ))) "holds" (Bool (Set "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "e"))) ($#r1_xxreal_0 :::"<"::: ) (Set "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" ))); end; :: deftheorem defines :::"with_property_L3"::: LEXBFS:def 18 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v5_lexbfs :::"with_property_L3"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")))) & (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_chord :::"are_adjacent"::: ) ) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "c")) ($#r1_chord :::"are_adjacent"::: ) ))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "c"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "d")))) & (Bool (Set (Var "b")) "," (Set (Var "d")) ($#r1_chord :::"are_adjacent"::: ) ) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "d")) ($#r1_chord :::"are_adjacent"::: ) )) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "e")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool (Set (Var "e")) "," (Set (Var "b")) ($#r1_chord :::"are_adjacent"::: ) ) & (Bool (Bool "not" (Set (Var "e")) "," (Set (Var "a")) ($#r1_chord :::"are_adjacent"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "e"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" ))) ")" ))); theorem :: LEXBFS:53 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k13_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ) "is" ($#v5_lexbfs :::"with_property_L3"::: ) ))) ; theorem :: LEXBFS:54 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v6_chord :::"chordal"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "L")) "is" ($#v5_lexbfs :::"with_property_L3"::: ) ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) "holds" (Bool "for" (Set (Var "V")) "being" ($#m3_chord :::"VertexScheme"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "V")) ($#k2_funct_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "L")))) "holds" (Bool (Set (Var "V")) "is" ($#v7_chord :::"perfect"::: ) )))) ; theorem :: LEXBFS:55 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v6_chord :::"chordal"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k14_lexbfs :::".Result()"::: ) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ) ($#k2_funct_1 :::"""::: ) ) "is" ($#v7_chord :::"perfect"::: ) ($#m3_chord :::"VertexScheme"::: ) "of" (Set (Var "G")))) ; begin definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode MCS:Labeling of "G" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); end; definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); func :::"MCS:Init"::: "G" -> ($#m1_subset_1 :::"MCS:Labeling":::) "of" "G" equals :: LEXBFS:def 19 (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"MCS:Init"::: LEXBFS:def 19 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set ($#k18_lexbfs :::"MCS:Init"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_tarski :::"]"::: ) ))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "L" be ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Const "G")); func :::"MCS:PickUnnumbered"::: "L" -> ($#m1_subset_1 :::"Vertex":::) "of" "G" means :: LEXBFS:def 20 (Bool it ($#r1_hidden :::"="::: ) (Set ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ))) if (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "L" ($#k7_lexbfs :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G")) otherwise (Bool "ex" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_membered :::"natural-membered"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")))) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set "(" "L" ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" "L" ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ) ")" ))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k10_subset_1 :::"choose"::: ) (Set "(" (Set (Var "F")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k1_xxreal_2 :::"max"::: ) (Set (Var "S")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) ")" ))); end; :: deftheorem defines :::"MCS:PickUnnumbered"::: LEXBFS:def 20 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k19_lexbfs :::"MCS:PickUnnumbered"::: ) (Set (Var "L")))) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k19_lexbfs :::"MCS:PickUnnumbered"::: ) (Set (Var "L")))) "iff" (Bool "ex" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_membered :::"natural-membered"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")))) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ) ")" ))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_subset_1 :::"choose"::: ) (Set "(" (Set (Var "F")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k1_xxreal_2 :::"max"::: ) (Set (Var "S")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) ")" ))) ")" ) ")" ")" )))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "L" be ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Const "G")); let "v" be ($#m1_hidden :::"set"::: ) ; func :::"MCS:LabelAdjacent"::: "(" "L" "," "v" ")" -> ($#m1_subset_1 :::"MCS:Labeling":::) "of" "G" equals :: LEXBFS:def 21 (Set ($#k4_tarski :::"["::: ) (Set "(" "L" ($#k7_lexbfs :::"`1"::: ) ")" ) "," (Set "(" (Set "(" "L" ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k3_lexbfs :::".incSubset"::: ) "(" (Set "(" (Set "(" "G" ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k1_tarski :::"{"::: ) "v" ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_finsub_1 :::"\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" "L" ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ) ")" ) "," (Num 1) ")" ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"MCS:LabelAdjacent"::: LEXBFS:def 21 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k20_lexbfs :::"MCS:LabelAdjacent"::: ) "(" (Set (Var "L")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k3_lexbfs :::".incSubset"::: ) "(" (Set "(" (Set "(" (Set (Var "G")) ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_finsub_1 :::"\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ) ")" ) "," (Num 1) ")" ")" ) ($#k4_tarski :::"]"::: ) ))))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "L" be ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Const "G")); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "n" be ($#m1_hidden :::"Nat":::); func :::"MCS:Update"::: "(" "L" "," "v" "," "n" ")" -> ($#m1_subset_1 :::"MCS:Labeling":::) "of" "G" means :: LEXBFS:def 22 (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"MCS:Labeling":::) "of" "G" "st" (Bool "(" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" "L" ($#k7_lexbfs :::"`1"::: ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "v" ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "(" "G" ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) "n" ")" ) ")" ) ")" ) "," (Set "(" "L" ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k20_lexbfs :::"MCS:LabelAdjacent"::: ) "(" (Set (Var "M")) "," "v" ")" )) ")" )); end; :: deftheorem defines :::"MCS:Update"::: LEXBFS:def 22 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k21_lexbfs :::"MCS:Update"::: ) "(" (Set (Var "L")) "," (Set (Var "v")) "," (Set (Var "n")) ")" )) "iff" (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "v")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k20_lexbfs :::"MCS:LabelAdjacent"::: ) "(" (Set (Var "M")) "," (Set (Var "v")) ")" )) ")" )) ")" )))))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "L" be ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Const "G")); func :::"MCS:Step"::: "L" -> ($#m1_subset_1 :::"MCS:Labeling":::) "of" "G" equals :: LEXBFS:def 23 "L" if (Bool (Set "G" ($#k15_glib_000 :::".order()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" "L" ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ))) otherwise (Set ($#k21_lexbfs :::"MCS:Update"::: ) "(" "L" "," (Set "(" ($#k19_lexbfs :::"MCS:PickUnnumbered"::: ) "L" ")" ) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" "L" ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"MCS:Step"::: LEXBFS:def 23 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Var "G")) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" )))) "implies" (Bool (Set ($#k22_lexbfs :::"MCS:Step"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Var "L"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ))))) "implies" (Bool (Set ($#k22_lexbfs :::"MCS:Step"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k21_lexbfs :::"MCS:Update"::: ) "(" (Set (Var "L")) "," (Set "(" ($#k19_lexbfs :::"MCS:PickUnnumbered"::: ) (Set (Var "L")) ")" ) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ) ")" ) ")" )) ")" ")" ))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode :::"MCS:LabelingSeq"::: "of" "G" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: LEXBFS:def 24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"MCS:Labeling":::) "of" "G")); end; :: deftheorem defines :::"MCS:LabelingSeq"::: LEXBFS:def 24 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m3_lexbfs :::"MCS:LabelingSeq"::: ) "of" (Set (Var "G"))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Var "G")))) ")" ))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "S" be ($#m3_lexbfs :::"MCS:LabelingSeq"::: ) "of" (Set (Const "G")); let "n" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "S" :::"."::: "n" -> ($#m1_subset_1 :::"MCS:Labeling":::) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "S" be ($#m3_lexbfs :::"MCS:LabelingSeq"::: ) "of" (Set (Const "G")); :: original: :::".Result()"::: redefine func "S" :::".Result()"::: -> ($#m1_subset_1 :::"MCS:Labeling":::) "of" "G"; end; definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "S" be ($#m3_lexbfs :::"MCS:LabelingSeq"::: ) "of" (Set (Const "G")); func "S" :::"``1"::: -> ($#m1_lexbfs :::"preVNumberingSeq"::: ) "of" "G" means :: LEXBFS:def 25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k5_lexbfs :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" "S" ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ))); end; :: deftheorem defines :::"``1"::: LEXBFS:def 25 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "S")) "being" ($#m3_lexbfs :::"MCS:LabelingSeq"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m1_lexbfs :::"preVNumberingSeq"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k25_lexbfs :::"``1"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k5_lexbfs :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "S")) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ))) ")" )))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); func :::"MCS:CSeq"::: "G" -> ($#m3_lexbfs :::"MCS:LabelingSeq"::: ) "of" "G" means :: LEXBFS:def 26 (Bool "(" (Bool (Set it ($#k23_lexbfs :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k18_lexbfs :::"MCS:Init"::: ) "G")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k23_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k22_lexbfs :::"MCS:Step"::: ) (Set "(" it ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"MCS:CSeq"::: LEXBFS:def 26 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "b2")) "being" ($#m3_lexbfs :::"MCS:LabelingSeq"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")))) "iff" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k23_lexbfs :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k18_lexbfs :::"MCS:Init"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b2")) ($#k23_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k22_lexbfs :::"MCS:Step"::: ) (Set "(" (Set (Var "b2")) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) ")" ))); theorem :: LEXBFS:56 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G"))) "is" ($#v2_lexbfs :::"iterative"::: ) )) ; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); cluster (Set ($#k26_lexbfs :::"MCS:CSeq"::: ) "G") -> ($#v2_lexbfs :::"iterative"::: ) ; end; theorem :: LEXBFS:57 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set "(" ($#k18_lexbfs :::"MCS:Init"::: ) (Set (Var "G")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: LEXBFS:58 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" )))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k19_lexbfs :::"MCS:PickUnnumbered"::: ) (Set (Var "L")) ")" )))))) ; theorem :: LEXBFS:59 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) "holds" (Bool "not" (Bool (Set ($#k19_lexbfs :::"MCS:PickUnnumbered"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" )))))) ; theorem :: LEXBFS:60 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "v")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v")) ($#k1_tarski :::"}"::: ) ))))) "holds" (Bool (Set (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k20_lexbfs :::"MCS:LabelAdjacent"::: ) "(" (Set (Var "L")) "," (Set (Var "v")) ")" ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "x"))))))) ; theorem :: LEXBFS:61 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "v")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k20_lexbfs :::"MCS:LabelAdjacent"::: ) "(" (Set (Var "L")) "," (Set (Var "v")) ")" ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "x"))))))) ; theorem :: LEXBFS:62 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "v")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v")) ($#k1_tarski :::"}"::: ) ))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k7_lexbfs :::"`1"::: ) ")" ))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k20_lexbfs :::"MCS:LabelAdjacent"::: ) "(" (Set (Var "L")) "," (Set (Var "v")) ")" ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))))) ; theorem :: LEXBFS:63 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"MCS:Labeling":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "L")) ($#k8_lexbfs :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k20_lexbfs :::"MCS:LabelAdjacent"::: ) "(" (Set (Var "L")) "," (Set (Var "v")) ")" ")" ) ($#k8_lexbfs :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))))) ; theorem :: LEXBFS:64 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k7_lexbfs :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" ($#k19_lexbfs :::"MCS:PickUnnumbered"::: ) (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ) ")" ) ")" ) ")" ))))) ; theorem :: LEXBFS:65 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))))) ; theorem :: LEXBFS:66 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")))))) ; theorem :: LEXBFS:67 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")))))) ; theorem :: LEXBFS:68 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G"))) "is" ($#v3_lexbfs :::"eventually-constant"::: ) )) ; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); cluster (Set ($#k26_lexbfs :::"MCS:CSeq"::: ) "G") -> ($#v3_lexbfs :::"eventually-constant"::: ) ; end; theorem :: LEXBFS:69 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))) "iff" (Bool (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ))) ; theorem :: LEXBFS:70 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k39_glib_000 :::".Lifespan()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ))) ; theorem :: LEXBFS:71 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k25_lexbfs :::"``1"::: ) ) "is" ($#v3_lexbfs :::"eventually-constant"::: ) )) ; theorem :: LEXBFS:72 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k25_lexbfs :::"``1"::: ) ")" ) ($#k39_glib_000 :::".Lifespan()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k39_glib_000 :::".Lifespan()"::: ) ))) ; theorem :: LEXBFS:73 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k25_lexbfs :::"``1"::: ) ) "is" ($#v4_lexbfs :::"vertex-numbering"::: ) )) ; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); cluster (Set (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) "G" ")" ) ($#k25_lexbfs :::"``1"::: ) ) -> ($#v4_lexbfs :::"vertex-numbering"::: ) ; end; theorem :: LEXBFS:74 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k25_lexbfs :::"``1"::: ) ")" ) ($#k6_lexbfs :::".PickedAt"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k19_lexbfs :::"MCS:PickUnnumbered"::: ) (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ))))) ; theorem :: LEXBFS:75 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set ($#k19_lexbfs :::"MCS:PickUnnumbered"::: ) (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ))))) "implies" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "v")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) ))) "or" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ))) ")" )) "implies" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "v")))) ")" ")" ) ")" ) ")" )))) ; theorem :: LEXBFS:76 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ))))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k8_lexbfs :::"`2"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k2_chord :::".AdjacentSet"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k3_finsub_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ")" ) ")" ) ")" )))))) ; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "F" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Const "G")) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ); attr "F" is :::"with_property_T"::: means :: LEXBFS:def 27 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "G" "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F")) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F")) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F")) & (Bool (Set "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "b")))) & (Bool (Set "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<"::: ) (Set "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_chord :::"are_adjacent"::: ) ) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "c")) ($#r1_chord :::"are_adjacent"::: ) ))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "G" "st" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F")) & (Bool (Set "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<"::: ) (Set "F" ($#k1_recdef_1 :::"."::: ) (Set (Var "d")))) & (Bool (Set (Var "b")) "," (Set (Var "d")) ($#r1_chord :::"are_adjacent"::: ) ) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "d")) ($#r1_chord :::"are_adjacent"::: ) )) ")" ))); end; :: deftheorem defines :::"with_property_T"::: LEXBFS:def 27 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v6_lexbfs :::"with_property_T"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")))) & (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_chord :::"are_adjacent"::: ) ) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "c")) ($#r1_chord :::"are_adjacent"::: ) ))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "F")) ($#k1_recdef_1 :::"."::: ) (Set (Var "d")))) & (Bool (Set (Var "b")) "," (Set (Var "d")) ($#r1_chord :::"are_adjacent"::: ) ) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "d")) ($#r1_chord :::"are_adjacent"::: ) )) ")" ))) ")" ))); theorem :: LEXBFS:77 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k26_lexbfs :::"MCS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k23_lexbfs :::"."::: ) (Set (Var "n")) ")" ) ($#k7_lexbfs :::"`1"::: ) ) "is" ($#v6_lexbfs :::"with_property_T"::: ) ))) ; theorem :: LEXBFS:78 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k16_lexbfs :::"LexBFS:CSeq"::: ) (Set (Var "G")) ")" ) ($#k14_lexbfs :::".Result()"::: ) ")" ) ($#k7_lexbfs :::"`1"::: ) ) "is" ($#v6_lexbfs :::"with_property_T"::: ) )) ; theorem :: LEXBFS:79 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v6_chord :::"chordal"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "L")) "is" ($#v6_lexbfs :::"with_property_T"::: ) ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) "holds" (Bool "for" (Set (Var "V")) "being" ($#m3_chord :::"VertexScheme"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "V")) ($#k2_funct_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "L")))) "holds" (Bool (Set (Var "V")) "is" ($#v7_chord :::"perfect"::: ) )))) ;