Impressum cycle_deg.prf
Sprache: Lisp
(cycle_degnil 3312297543"" (skosimp*)"" (typepred "vert(G!1)" )"" (lemma "finite_subset[T]" )"" "vert(G!1)" "{y: T | AND ") "" (bddsimp)"" (hide 2)"" (expand "subset?" )"" (expand "member" ) (("" (skosimp*) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil cycle_deg nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"bool" walks nil )nil walks nil )"bool" walks nil )"bool" sets nil )"bool" sets nil )nil finite_sets nil ))nil )nil 3312285093 ("" (subtype-tcc) nil nil ) nil nil ))nil 3312297501 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil cycle_deg nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil graphs nil )nil graphs nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"finite_set[T]" cycle_deg nil )"bool" sets nil )"bool" sets nil )nil application-judgement "finite_set[T]" cycle_deg nil ))nil 3559571065"" (skosimp*)"" (lemma "conn_eq_path" )"" (inst -1 "subgraph(G!1, reachable(G!1, x!1))" )"" (iff -1)"" (bddsimp)"" (hide 1)"" (expand "path_connected?" )"" (bddsimp)"1" (install-rewrites "subgraphs" )"1" (assert )"1" (inst -1 "x!1" )"1" (bddsimp)"1" "(#length := 1, seq :=(LAMBDA (i:below(1)): x!1)#)" )"1" (assert ) nil nil )) nil )"2" (typepred "x!1" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "x!2" )"2" (typepred "y!1" )"2" (expand "subgraph" -)"2" (flatten)"2" (expand "reachable" -)"2" "2" "2" "walk?_reverse" )"2" "G!1" "x!1" "y!1" "w!1" )"2" "G!1" "x!1" "x!2" "w!2" )"2" "2" "2" "walk_merge" )"2" "G!1" "w!4" "w!3" "x!2" "y!1" "x!1" )"2" "2" "2" "p!1" )"1" "walks" )"1" assert )"1" nil nil ))nil ))nil )"2" assert )"2" "walks" )"2" assert )"2" "2" "1" "1" "1" "p!1" )"1" "n!1" )"1" nil nil ))nil ))nil )"2" "2" "n!1" )"1" "1+n!1" )"1" "1" "1" "1" "1" "1" "walk?_caret" )"1" "G!1" "0" "n!1" "p!1" )"1" "1" assert )"1" case "walk?(G!1,p!1)" )"1" "1" "G!1" "x!2" "x!3" "p!1 ^ (0, n!1)" )"1" expand "walk_from?" "1" expand "^" "1" "1" "1" "G!1" "w!5" "w!2" "x!1" "x!3" "x!2" )"1" expand "walk_from?" "1" "w!2" )"1" case "walk?(G!1,w!2)" )"1" "1" "1" "p!2" )"1" expand "walk_from?" "1" "1" expand "walk?" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "walks" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand min )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" "walk?_caret" )"3" "G!1" "0" "1+n!1" "p!1" )"3" "G!1" "x!2" "x!3" "p!1 ^ (0, 1 + n!1)" )"1" "n!1" )"1" "1" "1" "G!1" "w!5" "w!2" "x!1" "x!3" "x!2" )"1" "1" "w!2" )"1" case "walk_from?(G!1, w!2, x!1, x!2)" )"1" "1" "1" "p!2" )"1" "1" assert )"1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil )"3" "3" "3" assert )"3" "3" "p!1" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "4" "4" assert )"4" nil nil ))nil ))nil ))nil ))nil )"5" assert )nil nil )"6" assert )nil nil )"7" assert )nil nil )"8" assert )nil nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" assert nil nil ))nil ))nil )"2" assert nil nil ))nil )"2" assert nil nil ))nil ))nil )"3" "n!1" )"3" assert )nil nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" "2" "walk?_caret" )"2" "G!1" "0" "i!1" "p!1" )"2" "i!1" )"2" "2" "G!1" "x!2" "seq(p!1)(i!1)" "p!1 ^ (0, i!1)" )"1" case "walk?(G!1,p!1)" )"1" "1" expand "walk_from?" "1" expand "^" "1" expand "^" "1" "1" "1" "1" "G!1" "w!5" "w!2" "x!1" "seq(p!1)(i!1)" "x!2" )"1" case "walk_from?(G!1, w!2, x!1, x!2)" )"1" "1" "1" "p!2" )"1" "1" nil nil ))nil )"2" "p!2" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "walk_from?" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand min )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "^" "2" assert )"2" expand min )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cycle_deg nil )nil graph_connected nil )nil application-judgement "finite_set[T]" cycle_deg nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"bool" sets nil )"bool" sets nil )"bool" graphs nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil walks nil )"bool" walks nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil walks nil )"graph[T]" cycle_deg nil )"(vert(G!1))" cycle_deg nil )"prewalk[T]" cycle_deg nil )nil application-judgement "finite_set[T]" graph_conn_piece nil )"int" integers nil )"prewalk[T]" cycle_deg nil )"below(length(p!1))" cycle_deg nil )"posint" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil walks nil )"finseq" finite_sequences nil )"{k: nat | k <= i AND k <= j}" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"int" integers nil )"(total_order?[real])" nil )"{k: int | k <= i AND k <= j}" nil )"prewalk[T]" cycle_deg nil )"(total_order?[real])" nil )"prewalk[T]" cycle_deg nil )"nat" cycle_deg nil )"(strict_total_order?[real])" real_props nil )nil walks nil )nil walks nil )"bool" graph_conn_defs nil )"finite_set[T]" cycle_deg nil )"bool" finite_sets nil )"Subgraph(G)" subgraphs nil )nil subgraphs nil )"bool" subgraphs nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil ))nil )nil 3559570741"" (skosimp*)"" (lemma "conn_eq_path" )"" (inst -1 "subgraph(G!1, reachable(G!1, x!1))" )"" (iff -1)"" (bddsimp)"" (hide 1)"" (expand "path_connected?" )"" (bddsimp)"1" (install-rewrites "subgraphs" )"1" (assert )"1" (inst -1 "x!1" )"1" (bddsimp)"1" "(#l := 1, seq :=(LAMBDA (i:below(1)): x!1)#)" )"1" (assert ) nil )))"2" (typepred "x!1" )"2" (propax) nil )))))))))))"2" (skosimp*)"2" (typepred "x!2" )"2" (typepred "y!1" )"2" (expand "subgraph" -)"2" (flatten)"2" (expand "reachable" -)"2" "2" "2" "walk?_reverse" )"2" "G!1" "x!1" "y!1" "w!1" )"2" "G!1" "x!1" "x!2" "w!2" )"2" "2" "2" "walk_merge" )"2" "G!1" "w!4" "w!3" "x!2" "y!1" "x!1" )"2" "2" "2" "p!1" )"1" "walks" )"1" assert )"1" nil )))))"2" assert )"2" "walks" )"2" assert )"2" "2" "1" "1" "1" "p!1" )"1" "n!1" )"1" nil )))))"2" "2" "n!1" )"1" "1+n!1" )"1" "1" "1" "1" "1" "1" "walk?_caret" )"1" "G!1" "0" "n!1" "p!1" )"1" "1" assert )"1" case "walk?(G!1,p!1)" )"1" "1" "G!1" "x!2" "x!3" "p!1 ^ (0, n!1)" )"1" expand "walk_from?" "1" expand "^" "1" "1" "1" "G!1" "w!5" "w!2" "x!1" "x!3" "x!2" )"1" expand "walk_from?" "1" "w!2" )"1" case "walk?(G!1,w!2)" )"1" "1" "1" "p!2" )"1" expand "walk_from?" "1" "1" expand "walk?" "1" "1" "1" nil )))))))))))"2" "2" nil )))))))))"2" "2" "2" "walks" )"2" assert )nil )))))))))))))))))))))))))))"2" "2" "2" "2" "2" assert )"2" nil )))))))))))))))))))))))))))"2" "2" assert )nil )))"3" "3" "walk?_caret" )"3" "G!1" "0" "1+n!1" "p!1" )"3" "G!1" "x!2" "x!3" "p!1 ^ (0, 1 + n!1)" )"1" "n!1" )"1" "1" "1" "G!1" "w!5" "w!2" "x!1" "x!3" "x!2" )"1" "1" "w!2" )"1" case "walk_from?(G!1, w!2, x!1, x!2)" )"1" "1" "1" "p!2" )"1" "1" assert )"1" nil )))))"2" "2" nil )))))))))"2" "2" "2" assert )"2" nil )))))))))))))))))"2" "2" "2" assert )"2" "1" nil )"2" nil )))))))))"3" "3" "3" assert )"3" "3" "p!1" )"3" "3" nil )))))))))))))"4" "4" "4" "4" assert )"4" nil )))))))))"5" assert )nil )"6" assert )nil )"7" assert )nil )"8" assert )nil )))))"2" "2" "2" nil )))))))))))))"4" assert nil )))))"2" assert nil )))"2" assert nil )))))"3" "n!1" )"3" assert )nil )))))))"2" "2" "i!1" )"2" "2" "walk?_caret" )"2" "G!1" "0" "i!1" "p!1" )"2" "i!1" )"2" "2" "G!1" "x!2" "seq(p!1)(i!1)" "p!1 ^ (0, i!1)" )"1" case "walk?(G!1,p!1)" )"1" "1" expand "walk_from?" "1" expand "^" "1" expand "^" "1" "1" "1" "1" "G!1" "w!5" "w!2" "x!1" "seq(p!1)(i!1)" "x!2" )"1" case "walk_from?(G!1, w!2, x!1, x!2)" )"1" "1" "1" "p!2" )"1" "1" nil )))"2" "p!2" )"2" "2" nil )))))))))))"2" expand "walk_from?" "2" "2" "2" nil )))))))))))))))))))))))"2" nil )))"2" "2" "2" "2" nil )))))))))"2" "2" expand "^" "2" assert )nil ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))nil )nil nil )nil 3559570524"" (skosimp*)"" (lemma "conn_eq_path" )"" (inst -1 "subgraph(G!1, reachable(G!1, x!1))" )"" (iff -1)"" (bddsimp)"" (hide 1)"" (expand "path_connected?" )"" (bddsimp)"1" (install-rewrites "subgraphs" )"1" (assert )"1" (inst -1 "x!1" )"1" (bddsimp)"1" "(#l := 1, seq :=(LAMBDA (i:below(1)): x!1)#)" )"1" (assert ) nil )))"2" (typepred "x!1" )"2" (propax) nil )))))))))))"2" (skosimp*)"2" (typepred "x!2" )"2" (typepred "y!1" )"2" (expand "subgraph" -)"2" (flatten)"2" (expand "reachable" -)"2" "2" "2" "walk?_reverse" )"2" "G!1" "x!1" "y!1" "w!1" )"2" "G!1" "x!1" "x!2" "w!2" )"2" "2" "2" "walk_merge" )"2" "G!1" "w!4" "w!3" "x!2" "y!1" "x!1" )"2" "2" "2" "p!1" )"1" "walks" )"1" assert )"1" nil )))))"2" assert )"2" "walks" )"2" assert )"2" "2" "1" "1" "1" "p!1" )"1" "n!1" )"1" nil )))))"2" "2" "n!1" )"1" "1+n!1" )"1" "1" "1" "1" "1" "1" "walk?_caret" )"1" "G!1" "0" "n!1" "p!1" )"1" "1" assert )"1" case "walk?(G!1,p!1)" )"1" "1" "G!1" "x!2" "x!3" "p!1 ^ (0, n!1)" )"1" expand "walk_from?" "1" expand "^" "1" expand *min "1" "1" "1" "G!1" "w!5" "w!2" "x!1" "x!3" "x!2" )"1" expand "walk_from?" "1" "w!2" )"1" case "walk?(G!1,w!2)" )"1" "1" "1" "p!2" )"1" expand "walk_from?" "1" "1" expand "walk?" "1" "1" "1" nil )))))))))))"2" "2" nil )))))))))"2" "2" "2" "walks" )"2" assert )nil )))))))))))))))))))))))))))))"2" "2" "2" "2" "2" assert )"2" nil )))))))))))))))))))))))))))"2" "2" assert )nil )))"3" "3" "walk?_caret" )"3" "G!1" "0" "1+n!1" "p!1" )"3" "G!1" "x!2" "x!3" "p!1 ^ (0, 1 + n!1)" )"1" "n!1" )"1" "1" "1" "G!1" "w!5" "w!2" "x!1" "x!3" "x!2" )"1" "1" "w!2" )"1" case "walk_from?(G!1, w!2, x!1, x!2)" )"1" "1" "1" "p!2" )"1" "1" assert )"1" nil )))))"2" "2" nil )))))))))"2" "2" "2" assert )"2" nil )))))))))))))))))"2" "2" "2" assert )"2" "1" nil )"2" nil )))))))))"3" "3" "3" assert )"3" "3" "p!1" )"3" "3" nil )))))))))))))"4" "4" "4" "4" assert )"4" nil )))))))))"5" assert )nil )"6" assert )nil )"7" assert )nil )"8" assert )nil )))))"2" "2" "2" nil )))))))))))))"4" assert nil )))))"2" assert nil )))"2" assert nil )))))"3" "n!1" )"3" assert )nil )))))))"2" "2" "i!1" )"2" "2" "walk?_caret" )"2" "G!1" "0" "i!1" "p!1" )"2" "i!1" )"2" "2" "G!1" "x!2" "seq(p!1)(i!1)" "p!1 ^ (0, i!1)" )"1" case "walk?(G!1,p!1)" )"1" "1" expand "walk_from?" "1" expand "^" "1" expand *min "1" expand "^" "1" expand *min "1" "1" "1" "1" "G!1" "w!5" "w!2" "x!1" "seq(p!1)(i!1)" "x!2" )"1" case "walk_from?(G!1, w!2, x!1, x!2)" )"1" "1" "1" "p!2" )"1" "1" nil )))"2" "p!2" )"2" "2" nil )))))))))))"2" expand "walk_from?" "2" "2" "2" nil )))))))))))))))))))))))))))"2" nil )))"2" "2" "2" "2" nil )))))))))"2" "2" expand "^" "2" assert )nil ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))nil )nil nil )nil 3559570298"" (skosimp*)"" (lemma "conn_eq_path" )"" (inst -1 "subgraph(G!1, reachable(G!1, x!1))" )"" (iff -1)"" (bddsimp)"" (hide 1)"" (expand "path_connected?" )"" (bddsimp)"1" (install-rewrites "subgraphs" )"1" (assert )"1" (inst -1 "x!1" )"1" (bddsimp)"1" "(#l := 1, seq :=(LAMBDA (i:below(1)): x!1)#)" )"1" (assert ) nil )))"2" (typepred "x!1" )"2" (propax) nil )))))))))))"2" (skosimp*)"2" (typepred "x!2" )"2" (typepred "y!1" )"2" (expand "subgraph" -)"2" (flatten)"2" (expand "reachable" -)"2" "2" "2" "walk?_reverse" )"2" "G!1" "x!1" "y!1" "w!1" )"2" "G!1" "x!1" "x!2" "w!2" )"2" "2" "2" "walk_merge" )"2" "G!1" "w!4" "w!3" "x!2" "y!1" "x!1" )"2" "2" "2" "p!1" )"1" "walks" )"1" assert )"1" nil )))))"2" assert )"2" "walks" )"2" assert )"2" "2" "1" "1" "1" "p!1" )"1" "n!1" )"1" nil )))))"2" "2" "n!1" )"1" "1+n!1" )"1" "1" "1" "1" "1" "1" "walk?_caret" )"1" "G!1" "0" "n!1" "p!1" )"1" "1" assert )"1" case "walk?(G!1,p!1)" )"1" "1" "G!1" "x!2" "x!3" "p!1 ^ (0, n!1)" )"1" expand "walk_from?" "1" expand "^" "1" expand *min "1" "1" "1" "G!1" "w!5" "w!2" "x!1" "x!3" "x!2" )"1" expand "walk_from?" "1" "w!2" )"1" case "walk?(G!1,w!2)" )"1" "1" "1" "p!2" )"1" expand "walk_from?" "1" "1" expand "walk?" "1" "1" "1" nil )))))))))))"2" "2" nil )))))))))"2" "2" "2" "walks" )"2" assert )nil )))))))))))))))))))))))))))))"2" "2" "2" "2" "2" assert )"2" nil )))))))))))))))))))))))))))"2" "2" assert )nil )))"3" "3" "walk?_caret" )"3" "G!1" "0" "1+n!1" "p!1" )"3" "G!1" "x!2" "x!3" "p!1 ^ (0, 1 + n!1)" )"1" "n!1" )"1" "1" "1" "G!1" "w!5" "w!2" "x!1" "x!3" "x!2" )"1" "1" "w!2" )"1" case "walk_from?(G!1, w!2, x!1, x!2)" )"1" "1" "1" "p!2" )"1" "1" assert )"1" nil )))))"2" "2" nil )))))))))"2" "2" "2" assert )"2" nil )))))))))))))))))"2" "2" "2" assert )"2" "1" nil )"2" nil )))))))))"3" "3" "3" assert )"3" "3" "p!1" )"3" "3" nil )))))))))))))"4" "4" "4" "4" assert )"4" nil )))))))))"5" assert )nil )"6" assert )nil )"7" assert )nil )"8" assert )nil )))))"2" "2" "2" nil )))))))))))))"4" assert nil )))))"2" assert nil )))"2" assert nil )))))"3" "n!1" )"3" assert )nil )))))))"2" "2" "i!1" )"2" "2" "walk?_caret" )"2" "G!1" "0" "i!1" "p!1" )"2" "i!1" )"2" "2" "G!1" "x!2" "seq(p!1)(i!1)" "p!1 ^ (0, i!1)" )"1" case "walk?(G!1,p!1)" )"1" "1" expand "walk_from?" "1" expand "^" "1" expand *min "1" expand "^" "1" expand *min "1" "1" "1" "1" "G!1" "w!5" "w!2" "x!1" "seq(p!1)(i!1)" "x!2" )"1" case "walk_from?(G!1, w!2, x!1, x!2)" )"1" "1" "1" "p!2" )"1" "1" nil )))"2" "p!2" )"2" "2" nil )))))))))))"2" expand "walk_from?" "2" "2" "2" nil )))))))))))))))))))))))))))"2" nil )))"2" "2" "2" "2" nil )))))))))"2" "2" expand "^" "2" expand *min "2" assert )nil ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))nil )nil nil )nil 3312285132"" (skosimp*)"" (lemma "conn_eq_path" )"" (inst -1 "subgraph(G!1, reachable(G!1, x!1))" )"" (iff -1)"" (bddsimp)"" (hide 1)"" (expand "path_connected?" )"" (bddsimp)"1" (install-rewrites "subgraphs" )"1" (assert )"1" (inst -1 "x!1" )"1" (bddsimp)"1" "(#l := 1, seq :=(LAMBDA (i:below(1)): x!1)#)" )"1" (assert ) nil nil )) nil )"2" (typepred "x!1" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "x!2" )"2" (typepred "y!1" )"2" (expand "subgraph" -)"2" (flatten)"2" (expand "reachable" -)"2" "2" "2" "walk?_reverse" )"2" "G!1" "x!1" "y!1" "w!1" )"2" "G!1" "x!1" "x!2" "w!2" )"2" "2" "2" "walk_merge" )"2" "G!1" "w!4" "w!3" "x!2" "y!1" "x!1" )"2" "2" "2" "p!1" )"1" "walks" )"1" assert )"1" nil nil ))nil ))nil )"2" assert )"2" "walks" )"2" assert )"2" "2" "1" "1" "1" "p!1" )"1" "n!1" )"1" nil nil ))nil ))nil )"2" "2" "n!1" )"1" "1+n!1" )"1" "1" "1" "1" "1" "1" "walk?_caret" )"1" "G!1" "0" "n!1" "p!1" )"1" "1" assert )"1" case "walk?(G!1,p!1)" )"1" "1" "G!1" "x!2" "x!3" "p!1 ^ (0, n!1)" )"1" expand "walk_from?" "1" expand "^" "1" "1" "1" "G!1" "w!5" "w!2" "x!1" "x!3" "x!2" )"1" expand "walk_from?" "1" "w!2" )"1" case "walk?(G!1,w!2)" )"1" "1" "1" "p!2" )"1" expand "walk_from?" "1" "1" expand "walk?" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "walks" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" "walk?_caret" )"3" "G!1" "0" "1+n!1" "p!1" )"3" "G!1" "x!2" "x!3" "p!1 ^ (0, 1 + n!1)" )"1" "n!1" )"1" "1" "1" "G!1" "w!5" "w!2" "x!1" "x!3" "x!2" )"1" "1" "w!2" )"1" case "walk_from?(G!1, w!2, x!1, x!2)" )"1" "1" "1" "p!2" )"1" "1" assert )"1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil )"3" "3" "3" assert )"3" "3" "p!1" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "4" "4" assert )"4" nil nil ))nil ))nil ))nil ))nil )"5" assert )nil nil )"6" assert )nil nil )"7" assert )nil nil )"8" assert )nil nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" assert nil nil ))nil ))nil )"2" assert nil nil ))nil )"2" assert nil nil ))nil ))nil )"3" "n!1" )"3" assert )nil nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" "2" "walk?_caret" )"2" "G!1" "0" "i!1" "p!1" )"2" "i!1" )"2" "2" "G!1" "x!2" "seq(p!1)(i!1)" "p!1 ^ (0, i!1)" )"1" case "walk?(G!1,p!1)" )"1" "1" expand "walk_from?" "1" expand "^" "1" expand "^" "1" "1" "1" "1" "G!1" "w!5" "w!2" "x!1" "seq(p!1)(i!1)" "x!2" )"1" case "walk_from?(G!1, w!2, x!1, x!2)" )"1" "1" "1" "p!2" )"1" "1" nil nil ))nil )"2" "p!2" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "walk_from?" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "^" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil graph_connected nil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"bool" graphs nil )nil walks nil )"bool" walks nil )nil walks nil )nil walks nil )nil application-judgement "finite_set[T]" graph_conn_piece nil )nil walks nil )nil walks nil )nil walks nil )"bool" graph_conn_defs nil )"Subgraph(G)" subgraphs nil )nil subgraphs nil )"bool" subgraphs nil )nil graphs nil )nil graphs nil )nil doubletons nil )"set[T]" doubletons nil ))nil ))nil 3312284893"" (skosimp*)"" (inst 1 "subgraph(G!1,reachable(G!1,x!1))" )"" (bddsimp)"1" (skosimp*)"1" (typepred "y!1" )"1" (expand "deg" )"1" case "incident_edges(y!1, G!1) = ") "1" "finite_sets[doubleton[T]]" )"1" (replace -1 1) (("1" (propax) nil nil )) nil ))nil )"2" (hide 2)"2" (expand "incident_edges" )"2" (apply-extensionality 1 :hide? t)"2" (iff 1)"2" (bddsimp)"1" (expand "reachable" )"1" (expand "subgraph" )"1" "1" "1" "1" case "y!1=x!3" )"1" replace -1 1 rl)"1" (inst 1 "w!1" ) nil nil ))nil )"2" "add1(w!1,x!3)" )"1" expand "walk_from?" )"1" assert )"1" "1" "walk?_add1" )"1" "G!1" "w!1" "x!3" )"1" "1" replace -7 1)"1" "1" "1" "edge_has_2_verts" )"1" "x!2" "x!3" "y!1" )"1" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "G!1" )"2" "x!2" )"2" "2" "x!3" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "walks" )"2" assert )nil nil ))nil ))nil )"3" assert )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "walk_from?" )"2" "2" expand "walk?" )"2" expand "verts_in?" )"2" "2" "i!1" )"2" expand "add1" "2" case "i!1=length(w!1)" )"1" replace "1" case "seq(add1[T](w!1, x!3))(length(w!1))=x!3" )"1" replace "1" "G!1" )"1" "x!2" )"1" "1" "x!3" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" "i!1-1" )"1" "1" assert "1" "1" "G!1" )"1" expand "add1" )"1" "1" "w!1" )"1" expand "verts_in?" )"1" nil nil ))nil ))nil )"2" "2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" case "i!1=0" )"1" replace "1" expand "add1" )"1" "w!1" )"1" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "G!1" )"2" "2" "2" "x!3" )"2" (prop) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (install-rewrites "subgraphs[T]" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "x!1" )"2" (assert )"2" (expand "reachable" )"2" (assert )"2" (expand "subgraph" )"2" (inst 1 "gen_seq1(G!1,x!1)" )"2" (install-rewrites "walks[T]" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "reachable_conn" ) (("3" (inst? -1) nil nil )) nil )"4" (install-rewrites "subgraphs[T]" )"4" (stop-rewrite)"4" (auto-rewrite-theory "subgraphs[T]" )"4" (typepred "x!1" )"4" (assert )"4" (bddsimp)"1" "finite_sets[doubleton[T]]" )"1" (assert ) (("1" (grind) nil nil )) nil )) nil )"2" (assert )"2" (install-rewrites "finite_sets[T]" )"2" (assert ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cycle_deg nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"bool" subgraphs nil )nil subgraphs nil )"Subgraph(G)" subgraphs nil )"bool" finite_sets nil )"finite_set[T]" cycle_deg nil )"(partial_order?[set[T]])" nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"bool" sets nil )nil cycle_deg nil )"Seq(G)" walks nil )"nat" graph_deg nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"bool" walks nil )nil walks nil )"bool" walks nil )"(total_order?[real])" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"below(length(add1[T](w!1, x!3)))" cycle_degnil )"int" integers nil )"posint" nil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )"bool" walks nil )"int" integers nil )"bool" graphs nil )nil application-judgement "finite_set[T]" cycle_deg nil )nil graphs nil )nil walks nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"graph[T]" cycle_deg nil )"prewalk" walks nil )"Seq[T](G!1)" cycle_deg nil )"T" cycle_deg nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finite_set[doubleton[T]]" graph_degnil )NOT const-decl "[bool -> bool]" booleans nil ))nil )nil 3312284858"" (skosimp*)"" (inst 1 "subgraph(G!1,reachable(G!1,x!1))" )"" (bddsimp)"1" (skosimp*)"1" (typepred "y!1" )"1" (expand "deg" )"1" case "incident_edges(y!1, G!1) = ") "1" "finite_sets[doubleton[T]]" )"1" (replace -1 1) (("1" (propax) nil )))))"2" (hide 2)"2" (expand "incident_edges" )"2" (apply-extensionality 1 :hide? t)"2" (iff 1)"2" (bddsimp)"1" (expand "reachable" )"1" (expand "subgraph" )"1" "1" "1" "1" case "y!1=x!3" )"1" replace -1 1 rl)"1" (inst 1 "w!1" ) nil )))"2" "add1(w!1,x!3)" )"1" expand "walk_from?" )"1" assert )"1" "1" "walk?_add1" )"1" "G!1" "w!1" "x!3" )"1" "1" replace -7 1)"1" "1" "1" "edge_has_2_verts" )"1" "x!2" "x!3" "y!1" )"1" "1" assert )nil )"2" assert )nil )))))))))))))"2" "G!1" )"2" "x!2" )"2" "2" "x!3" )"2" assert )nil )))))))))))))))"2" assert )"2" "walks" )"2" assert )nil )))))"3" assert )"3" "3" nil )))))))))))"2" expand "walk_from?" )"2" "2" expand "walk?" )"2" expand "verts_in?" )"2" "2" "i!1" )"2" expand "add1" "2" case "i!1=length(w!1)" )"1" replace "1" case "seq(add1[T](w!1, x!3))(length(w!1))=x!3" )"1" replace "1" "G!1" )"1" "x!2" )"1" "1" "x!3" )"1" nil )))))))))))"2" "2" nil )))))))"2" "i!1-1" )"1" "1" assert "1" "1" "G!1" )"1" expand "add1" )"1" "1" "w!1" )"1" expand "verts_in?" )"1" nil )))))"2" "2" "x!2" )"2" assert )nil )))))))))))))))"2" assert )nil )))"2" case "i!1=0" )"1" replace "1" expand "add1" )"1" "w!1" )"1" nil )))))))"2" assert )nil )))))))))))))))))))))))))"2" "G!1" )"2" "2" "2" "x!3" )"2" nil )))))))))))))))))))"2" (install-rewrites "subgraphs[T]" )"2" (assert ) nil )))))))))))))))))))))"2" (typepred "x!1" )"2" (assert )"2" (expand "reachable" )"2" (assert )"2" (expand "subgraph" )"2" (inst 1 "gen_seq1(G!1,x!1)" )"2" (install-rewrites "walks[T]" )"2" (assert ) nil )))))))))))))))"3" (lemma "reachable_conn" ) (("3" (inst? -1) nil )))"4" (install-rewrites "subgraphs[T]" )"4" (stop-rewrite)"4" (auto-rewrite-theory "subgraphs[T]" )"4" (typepred "x!1" )"4" (assert )"4" (bddsimp)"1" "finite_sets[doubleton[T]]" )"1" (assert ) (("1" (grind) nil )))))"2" (assert )"2" (install-rewrites "finite_sets[T]" )"2" (assert )"2" (grind) nil ))))))))))))))))))))))))nil )nil nil )nil 3312283698"" (skosimp*)"" (inst 1 "subgraph(G!1,reachable(G!1,x!1))" )"" (bddsimp)"1" (skosimp*)"1" (typepred "y!1" )"1" (expand "deg" )"1" case "incident_edges(y!1, G!1) = ") "1" "finite_sets[doubleton[T]]" )"1" (replace -1 1) (("1" (propax) nil )))))"2" (hide 2)"2" (expand "incident_edges" )"2" (apply-extensionality 1 :hide? t)"2" (iff 1)"2" (bddsimp)"1" (expand "reachable" )"1" (expand "subgraph" )"1" "1" "1" "1" case "y!1=x!3" )"1" replace -1 1 rl)"1" (inst 1 "w!1" ) nil )))"2" "add1(w!1,x!3)" )"1" expand "walk_from?" )"1" assert )"1" "1" "walk?_add1" )"1" "G!1" "w!1" "x!3" )"1" "1" replace -7 1)"1" "1" "1" "edge_has_2_verts" )"1" "x!2" "x!3" "y!1" )"1" "1" assert )nil )"2" assert )nil )))))))))))))"2" "G!1" )"2" "x!2" )"2" "2" "x!3" )"2" assert )nil )))))))))))))))"2" assert )"2" "walks" )"2" assert )nil )))))"3" assert )"3" "3" nil )))))))))))"2" expand "walk_from?" )"2" "2" expand "walk?" )"2" expand "finseq_appl" )"2" expand "verts_in?" )"2" "2" "i!1" )"2" expand "add1" "2" case "i!1=length(w!1)" )"1" replace "1" case "seq(add1[T](w!1, x!3))(length(w!1))=x!3" )"1" replace "1" "G!1" )"1" "x!2" )"1" "1" "x!3" )"1" nil )))))))))))"2" "2" nil )))"3" "3" nil )))))))"2" "i!1-1" )"1" "1" assert "1" "1" "G!1" )"1" "dbl[T](seq(w!1)(i!1 - 1), seq(w!1)(i!1))" )"1" "1" "seq(add1[T](w!1, x!3))(i!1)" )"1" assert )"1" expand "add1" )"1" assert )"1" "1" nil )))))))))))"2" "2" nil )))))"2" "seq(w!1)(i!1 - 1)" "seq(w!1)(i!1)" )"1" "1" nil )"2" expand "edge?" )"2" assert )nil )))))"2" assert )nil )"3" assert )"3" "3" case "i!1=0" )"1" replace "1" expand "add1" )"1" "w!1" )"1" "1" nil )))))))))"2" assert )nil )))))))))"3" assert )nil )"4" assert )"4" case "i!1=0" )"1" replace "1" expand "add1" )"1" "w!1" )"1" "1" nil )))))))))"2" assert )nil )))))))))))))"2" assert )nil )))"2" case "i!1=0" )"1" replace "1" expand "add1" )"1" "w!1" )"1" nil )))))))"2" assert )nil )))))))))))))))))))))))))))"2" "G!1" )"2" "2" "2" "x!3" )"2" nil )))))))))))))))))))"2" (install-rewrites "subgraphs[T]" )"2" (assert ) nil )))))))))))))))))))))"2" (typepred "x!1" )"2" (assert )"2" (expand "reachable" )"2" (assert )"2" (expand "subgraph" )"2" (inst 1 "gen_seq1(G!1,x!1)" )"2" (install-rewrites "walks[T]" )"2" (assert ) nil )))))))))))))))"3" (lemma "reachable_conn" ) (("3" (inst? -1) nil )))"4" (install-rewrites "subgraphs[T]" )"4" (stop-rewrite)"4" (auto-rewrite-theory "subgraphs[T]" )"4" (typepred "x!1" )"4" (assert )"4" (bddsimp)"1" "finite_sets[doubleton[T]]" )"1" (assert ) (("1" (grind) nil )))))"2" (assert )"2" (install-rewrites "finite_sets[T]" )"2" (assert )"2" (grind) nil ))))))))))))))))))))))))nil )nil nil ))nil 3312297570"" (skosimp*)"" (typepred "w!1" )"" (expand "verts_in?" )"" (skosimp*)"" (expand "subgraph?" )"" (flatten)"" (hide -5)"" (expand "subset?" )"" (expand "member" )"" (assert )"" (inst?)"" (inst?) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil walks nil )"bool" walks nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil walks nil )nil finite_sequences nil )nil cycle_deg nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sets nil )"bool" subgraphs nil ))nil )nil 3312285654 ("" (subtype-tcc) nil nil ) nil nil ))nil 3393153710"" (skosimp*)"" (expand "cycle?" )"" (flatten)"" (bddsimp)"1" (assert ) nil nil )"2" (inst -4 "1" "length(w!1)-2" )"1" (bddsimp)"1" (expand "pre_circuit?" )"1" (flatten)"1" (bddsimp)"1" (lemma "walk?_subgraph[T]" )"1" (inst -1 "G!1" "H!1" "w!1" )"1" (bddsimp (-1 -2 -3))"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" cycles nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil subgraph_paths nil )"bool" walks nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )nil nat_types nil )nil cycle_deg nil )nil finite_sequences nil )"bool" reals nil )nil walks nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"bool" walks nil )"graph[T]" cycle_deg nil )nil walks nil )"Seq[T](H!1)" cycle_deg nil )"(total_order?[real])" nil ))nil )nil 3312297681"" (skosimp*)"" (expand "cycle?" )"" (flatten)"" (bddsimp)"1" (assert ) nil nil )"2" (inst -4 "1" "length(w!1)-2" )"1" (bddsimp)"1" (expand "pre_circuit?" )"1" (flatten)"1" (bddsimp)"1" (lemma "meng_scaff_defs[T].walk?_subgraph" )"1" (inst -1 "G!1" "H!1" "w!1" )"1" (bddsimp (-1 -2 -3))"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" walks nil )nil walks nil )"set[T]" doubletons nil )nil doubletons nil )nil graphs nil )nil graphs nil )"bool" walks nil )nil walks nil ))nil ))nil 3312297467"" (skosimp*)"" (expand "uniq_paths?" 1)"" (skosimp*)"" (lemma "path_ops[T].path?_del_vert" )"" (inst -1 "G!1" "v!1" "p!1" )"" (reveal -1)"" (inst -1 "G!1" "v!1" "q!1" )"" (expand "path_from?" -)"" (flatten)"" (bddsimp)"" (expand "uniq_paths?" -)"" (inst -5 "s!1" "t!1" "p!1" "q!1" )"" (expand "path_from?" -)"" (bddsimp) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" cycle_deg nil )nil cycle_deg nil )nil path_ops nil )"bool" paths nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil ))nil ))nil 3312297438"" (skosimp*)"" (lemma "graph_connected[T].conn_eq_path" )"" (inst -1 "del_edge(G!1, e!1)" )"" (iff -1)"" (bddsimp)"" (hide -1)"" (typepred "e!1" )"" (skosimp*)"" (expand "path_connected?" -3)"" (bddsimp)"" (inst -3 "x!1" "y!1" )"1" (lemma "path_ops[T].walk_to_path_from" )"1" (skosimp*)"1" "del_edge(G!1, e!1)" "x!1" "y!1" "w!1" )"1" "w!1" )"1" expand "walk_from?" -3)"1" "1" "1" "walks[T].edge_to_walk" )"1" "G!1" "x!1" "y!1" )"1" "1" case "path_from?(G!1,gen_seq2(G!1, x!1, y!1),x!1,y!1)" )"1" case "path_from?(G!1, p!1, x!1, y!1)" )"1" expand "uniq_paths?" "1" "x!1" "y!1" "p!1" "gen_seq2(G!1, x!1, y!1)" )"1" "1" "1" "p!1" )"1" "1" expand "path_from?" "1" "1" expand "path?" "1" "1" "1" expand "walk?" "1" "1" "0" )"1" replace "1" assert )"1" "walks[T]" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "paths[T]" )"2" nil nil ))nil ))nil ))nil )"2" "2" expand "path_from?" "2" expand "path?" 1)"2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace -7 -1)"2" "2" (grind) nil nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -3)"2" (grind)"2" (typepred "G!1" )"2" "2" "2" "y!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "graph_ops[T].vert_del_edge" )"3" (inst? -1)"3" (typepred "G!1" )"3" "e!1" )"3" "3" "x!1" )"3" assert )"3" replace -3 1)"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cycle_deg nil )nil graph_connected nil )nil graph_ops nil )nil path_ops nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"bool" walks nil )nil walks nil )"bool" walks nil )"doubleton[T]" graphs nil )"bool" paths nil )"bool" walks nil )nil walks nil )"Seq(G)" walks nil )nil naturalnumbers nil )"bool" reals nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil )"bool" cycle_deg nil )"bool" paths nil )"finite_set" finite_sets nil )nil application-judgement "finite_set[T]" graph_conn_piece nil )"bool" graphs nil )"set" sets nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" graphs nil )"bool" sets nil )"bool" sets nil )"bool" walks nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set[T]" cycle_deg nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil walks nil )"T" cycle_deg nil )"graph[T]" cycle_deg nil )"(edges(G!1))" cycle_deg nil )"T" cycle_deg nil )"bool" graph_conn_defs nil )NOT const-decl "[bool -> bool]" booleans nil )"graph[T]" graph_ops nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil ))nil ))nil 3312297339"" (lemma "size_prep" )"" "LAMBDA G:(connected?(G) AND uniq_paths?(G) IMPLIES tree?(G))" )"" (bddsimp)"" (hide 1)"" (induct "n" 1 "nat_induction" )"1" (skosimp*)"1" (hide -3 1)"1" (lemma "graph_complected[T].connected_not_empty" )"1" (inst -1 "G!1" )"1" (bddsimp)"1" (hide -1)"1" (grind)"1" (lemma "finite_sets[T].nonempty_card" )"1" (inst -1 "vert(G!1)" )"1" "1" (grind) nil nil )"2" expand "nonempty?" 1)"2" expand "empty?" -1)"2" "x!1" )"2" expand "member" 1)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "graph_complected[T].conn_lem3" )"2" (inst -1 "G!1" )"2" (bddsimp)"1" (lemma "graph_complected[T].conn_eq_compl" )"1" (inst? -1)"1" (bddsimp)"1" (expand "tree?" )"1" (flatten)"1" expand "singleton?" )"1" expand "size" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "v!1" )"2" (lemma "graph_complected[T].rev_lem2" )"2" (inst? -1)"2" (bddsimp)"2" "graph_ops[T].size_del_vert" )"2" "2" "uniq_del_vert" )"2" "2" "2" "del_vert(G!1, v!1)" )"2" replace -9 -3)"2" assert -3)"2" "2" expand "tree?" 1)"2" "2" "v!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "del_edge_uniq" )"3" (inst? -1)"3" (skolem! -3)"3" (inst? -1) (("3" (bddsimp) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil defined_types nil )"bool" graph_conn_defs nil )"bool" cycle_deg nil )"bool" trees nil )nil cycle_deg nil )nil graph_complected nil )"graph[T]" graph_ops nil )"posint" nil )"int" integers nil )nil cycle_deg nil )nil graph_ops nil )NOT const-decl "[bool -> bool]" booleans nil )nil graph_complected nil )"bool" graphs nil )nil graph_complected nil )nil graph_complected nil )"bool" graphs nil )"bool" sets nil )"bool" sets nil )"bool" finite_sets nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )nil finite_sets nil )nil naturalnumbers nil )"nat" graphs nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil graph_inductions nil )nil cycle_deg nil ))nil ))nil 3312285692"" (skosimp*)"" (expand "XOR" )"" (flatten)"" (iff)"" (bddsimp)"1" (skosimp*)"1" (lemma "tree_no_circuits" )"1" (inst? -1)"1" (inst -1 "w!1" )"1" (bddsimp)"1" (hide -1 -2)"1" (expand "cycle?" )"1" (flatten)"1" (install-rewrites "circuits[T]" )"1" assert )"1" "1" "1" "k!1" )"1" "k!1-1" "k!1+1" )"1" assert )"1" "1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" case "length(w!1)=2" )"1" replace -1 * lr)"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2)"2" (expand "cycle?" )"2" (flatten)"2" (expand "pre_circuit?" )"2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "uniq_paths?(G!1)" )"1" (lemma "charact_tree" )"1" (inst? -1) (("1" (bddsimp) nil nil )) nil )) nil )"2" (expand "uniq_paths?" )"2" (skosimp*)"2" (hide 2)"2" case "tree_paths[T].dual_paths?(G!1,p!1,q!1)" )"1" (lemma "min_dual_exists" )"1" (inst? -1)"1" (bddsimp (-1 -2))"1" (hide -1)"1" "1" "min_dual_distin" )"1" "G!1" "p!2" "q!2" )"1" "dual_cycle" )"1" "G!1" "p!2" "q!2" )"1" "1" expand "is_min_dual?" )"1" "1" "1" "trunc1(p!2) o rev(q!2)" )nil nil ))nil ))nil ))nil ))nil )"2" "graph_complected[T].connected_not_empty" )"2" "G!1" )"2" "2" expand "empty?" )"2" expand "nonempty?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "graph_complected[T].connected_not_empty" )"2" "G!1" )"2" "2" expand "empty?" )"2" expand "nonempty?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "q!1" )"2" (expand "path_from?" )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" expand "path?" -6)"2" "2" expand "walk?" )"2" "2" expand "verts_in?" )"2" "0" )"2" "seq(q!1)(0)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "dual_paths?" )"2" (hide -3 3)"2" (install-rewrites "paths[T]" )"2" (assert )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "path_from?" )"3" (flatten) nil nil )) nil )"4" (expand "path_from?" )"4" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" xor_def nil )"bool" cycle_deg nil )nil cycle_deg nil )"bool" tree_paths nil )nil paths nil )"bool" paths nil )"bool" sets nil )nil graphs nil )nil tree_paths nil )nil tree_paths nil )nil graph_complected nil )"bool" graphs nil )"finseq[T]" doubletons nil )"prewalk" walks nil )nil walks nil )"finseq" finite_sequences nil )"bool" tree_paths nil )"bool" paths nil )"bool" sets nil )"bool" sets nil )nil tree_paths nil )"bool" walks nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"bool" cycles nil )NOT const-decl "[bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )"posnat" cycle_deg nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"even_int" integersnil )"odd_int" integersnil )"bool" paths nil )"bool" circuits nil )"bool" walks nil )"bool" graphs nil )"bool" circuits nil )"bool" circuits nil )"bool" circuits nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil application-judgement "finite_set[T]" graph_conn_piece nil )nil application-judgement "finite_set[T]" cycle_deg nil )nil walks nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"bool" walks nil )"graph[T]" cycle_deg nil )"bool" walks nil )nil walks nil )"Seq[T](G!1)" cycle_deg nil )nil tree_circ nil )nil cycle_deg nil ))nil ))"RWB NEW" 3312544218"" (lemma "size_prep[T]" )"" "LAMBDA G: (connected?(G) and num_edges(G)<size(G) IMPLIES tree?(G))" )"" (assert )"" (ground)"" (hide 2 3)"" (induct "n" 1 "nat_induction" )"1" (skosimp*)"1" (hide -3 1)"1" "graph_complected[T].connected_not_empty" )"1" (inst -1 "G!1" )"1" (bddsimp)"1" (hide -1)"1" (grind)"1" "finite_sets[T].nonempty_card" )"1" "vert(G!1)" )"1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "graph_complected[T].connect_deg_0" )"2" (case "forall (v:(vert(G!1))):deg(v,G!1)>1" )"1" (lemma "graph_deg_sum[T].deg_gt_one" )"1" (inst -1 "G!1" )"1" (bddsimp (-1 -2))"1" (assert (-2 -7)) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (case "deg(v!1,G!1)=0" )"1" (typepred "v!1" )"1" (inst -3 "G!1" "v!1" )"1" (bddsimp (-1 -2 -3 -6))"1" expand "tree?" 2)"1" "1" "1" "1" "1" expand "singleton" 1)"1" "1" "1" "finite_sets[T].card_one" )"1" "{y: T | y = v!1}" )"1" "1" "v!1" )"1" "1" "1" expand "singleton" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "1" "LAMBDA (y:T): 0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "deg(v!1,G!1)=1" )"1" (hide -2)"1" "graph_complected[T].rev_lem2" )"1" "G!1" "v!1" )"1" "1" "del_vert(G!1, v!1)" )"1" "graph_ops[T].size_del_vert" )"1" "1" replace -6 -1)"1" assert -1)"1" "1" "1" expand "tree?" 3)"1" "1" "v!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "graph_ops" )"2" assert )"2" case "card[T](remove[T](v!1, vert(G!1)))=card[T](vert(G!1))-1" )"1" "{e: doubleton[T] | edges(G!1)(e) AND NOT e(v!1)} = edges(del_vert(G!1,v!1))" )"1" case "card(edges(del_vert(G!1,v!1)))=card(edges(G!1))-1" )"1" expand "del_vert" )"1" assert )nil nil ))nil )"2" "2" "is_finite" )"2" "finite_sets[doubleton[T]].card_one" )"2" "incident_edges(v!1, G!1)" )"2" "1" "1" expand "incident_edges" "1" "finite_sets[doubleton[T]].card_disj_union" )"1" "{e: doubleton[T] | edges(G!1)(e) AND e(v!1)}" "{e: doubleton[T] | edges(G!1)(e) AND NOT e(v!1)}" )"1" "1" expand "union" "1" expand "member" "1" case "{x: doubleton[T] | AND x(v!1) OR edges(G!1)(x) AND NOT x(v!1)}=edges(G!1)") "1" replace "1" "1" expand "incident_edges" "1" replace "1" assert nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "finite_sets[doubleton[T]]" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "finite_subset[doubleton[T]]" )"2" "edges(G!1)" "{e: doubleton[T] | edges(G!1)(e) AND NOT e(v!1)}" )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "finite_subset[doubleton[T]]" )"3" "edges(G!1)" "{e: doubleton[T] | edges(G!1)(e) AND e(v!1)}" )"3" assert )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "del_vert" )"2" nil nil ))nil ))nil ))nil )"2" "2" "finite_sets[T].card_remove" )"2" "vert(G!1)" "v!1" )"2" "v!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2 -3 -4 -5 4)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil defined_types nil )"bool" graph_conn_defs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"nat" graph_ops nil )"nat" graphs nil )"bool" trees nil )nil naturalnumbers nil )nil finite_sets nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"bool" finite_sets nil )"bool" sets nil )"bool" sets nil )"bool" graphs nil )nil graph_complected nil )nil graph_complected nil )nil graph_complected nil )nil graph_ops nil )"finite_set[T]" cycle_deg nil )nil finite_sets nil )"set" sets nil )"bool" sets nil )"set" sets nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil finite_sets nil )"(partial_order?[set[T]])" nil )"bool" sets nil )nil finite_sets nil )"finite_set[doubleton[T]]" graph_degnil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"set" sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"int" integers nil )"posint" nil )"graph[T]" graph_ops nil )NOT const-decl "[bool -> bool]" booleans nil )"(singleton?)" graphs nil )"non_empty_finite_set[T]" cycle_deg nil )"finite_set" finite_sets nil )"(singleton?)" sets nil )"graph[T]" cycle_deg nil )"(vert(G!1))" cycle_deg nil )nil nat_types nil )"bool" booleans nil )"bool" functions nil )"R" restrict nil )nil finite_sets nil )nil graph_deg_sum nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nat" graph_deg nil )"bool" reals nil )nil graph_inductions nil )nil cycle_deg nil ))nil 3312286644"" (lemma "size_prep[T]" )"" "LAMBDA G: (connected?(G) and num_edges(G)<size(G) IMPLIES tree?(G))" )"" (bddsimp)"1" (assert ) nil )"2" (hide 1 3)"2" (induct "n" 1 "nat_induction" )"1" (skosimp*)"1" (hide -3 1)"1" (lemma "graph_complected[T].connected_not_empty" )"1" (inst -1 "G!1" )"1" (bddsimp)"1" (hide -1)"1" (grind)"1" (lemma "finite_sets[T].nonempty_card" )"1" (inst -1 "vert(G!1)" )"1" "1" (grind) nil )"2" expand "nonempty?" 1)"2" expand "empty?" -1)"2" "x!1" )"2" expand "member" 1)"2" nil )))))))))))))))))))))))))))))"2" (skosimp*)"2" (lemma "graph_complected[T].connect_deg_0" )"2" (case "forall (v:(vert(G!1))):deg(v,G!1)>1" )"1" (lemma "graph_deg_sum[T].deg_gt_one" )"1" (inst -1 "G!1" )"1" (bddsimp (-1 -2))"1" (assert (-2 -7)) nil )))))))"2" (skosimp*)"2" (case "deg(v!1,G!1)=0" )"1" (typepred "v!1" )"1" (inst -3 "G!1" "v!1" )"1" (bddsimp (-1 -2 -3 -6))"1" (expand "tree?" 2)"1" "1" "1" "1" "1" expand "singleton" 1)"1" "1" "1" "finite_sets[T].card_one" )"1" "{y: T | y = v!1}" )"1" "1" "v!1" )"1" "1" "1" expand "singleton" "1" nil )))))))))))"2" "finite_sets[T].card_one" )"2" "2" "2" "1" "LAMBDA (y:T): 0" )"2" nil )))))))))))))))))))))))))))))))))))"2" (case "deg(v!1,G!1)=1" )"1" (hide -2)"1" (lemma "graph_complected[T].rev_lem2" )"1" (inst -1 "G!1" "v!1" )"1" "1" "del_vert(G!1, v!1)" )"1" "graph_ops[T].size_del_vert" )"1" "1" replace -6 -1)"1" assert -1)"1" "1" "1" expand "tree?" 3)"1" "1" "v!1" )"1" assert )nil )))))))))"2" "2" "2" "graph_ops" )"2" assert )"2" case "card[T](remove[T](v!1, vert(G!1)))=card[T](vert(G!1))-1" )"1" case "card({e: doubleton[T] | edges(G!1)(e) AND NOT e(v!1)})=card(edges(G!1))-1" )"1" assert )nil )"2" "2" "2" "finite_sets[doubleton[T]].card_one" )"2" "incident_edges(v!1, G!1)" )"2" "2" "2" expand "incident_edges" "2" "finite_sets[doubleton[T]].card_disj_union" )"2" "{e: doubleton[T] | edges(G!1)(e) AND e(v!1)}" "{e: doubleton[T] | edges(G!1)(e) AND NOT e(v!1)}" )"1" "1" expand "union" "1" expand "member" "1" case "{x: doubleton[T] | AND x(v!1) OR edges(G!1)(x) AND NOT x(v!1)}=edges(G!1)") "1" replace "1" "1" expand "incident_edges" "1" replace "1" assert nil )))))))))"2" "2" "2" "2" "2" "2" nil )))))))))))))))))"2" "2" "finite_sets[doubleton[T]]" )"2" assert )"2" nil )))))))))"2" "graph_deg[T].incident_edges_TCC1" )"2"
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.915Bemerkung:
(vorverarbeitet am 2026-04-27)
¤ *Bot Zugriff
2026-05-26
