Impressum mappings.prf
Sprache: Lisp
(mappings (reachable_TCC1 0nil 3318087528"" (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 mappings 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]" nil )nil number_fieldsnil )"[number_field -> boolean]" realsnil )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 3318087528 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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]" nil )"boolean" notequal nil )nil mappings nil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"finite_set[T]" mappings nil )"bool" sets nil )"bool" sets nil )nil application-judgement "finite_set[T]" mappings nil ))nil ))"Valid3.2" 3318377422"" (skosimp*)"" (split)"1" (flatten)"1" (expand "path_connected?" -1)"1" (skosimp*)"1" (expand "empty?" 1)"1" (expand "empty?" 1)"1" (skosimp*)"1" (inst 1 "x!1" )"1" (expand "member" -1)"1" expand "reachable" 1)"1" "1" (propax) nil nil )"2" "2" "2" "2" "1" (bddsimp) nil nil )"2" "2" "1" (propax) nil nil )"2" "x!1" "x!2" )"2" "2" "w!1" )"1" expand "walk_from?" "1" assert )nil nil ))nil )"2" "2" "w!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "path_connected?" )"2" (skosimp*)"2" (split)"1" (expand "empty?" )"1" (expand "empty?" )"1" (inst -1 "x!1" )"1" (expand "member" )"1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "reachable" )"2" (typepred "y!1" )"2" (typepred "x!2" )"2" "extensionality_postulate[T,bool]" )"2" "({y: T | vert(G!1)(y) AND (EXISTS (w: Seq(G!1)):walk_from?(G!1, w, x!1, y))})" "vert(G!1)" )"2" "2" "1" "1" "1" "x!2" )"1" "1" "1" "y!1" )"1" "1" "1" "1" "walk?_reverse" )"1" "G!1" "x!1" "y!1" "w!2" )"1" "G!1" "x!1" "x!2" "w!1" )"1" "1" "1" "1" "1" "walk_merge" )"1" "G!1" "w!4" "w!3" "x!2" "y!1" "x!1" )"1" "1" "1" expand "walk_from?" "1" assert )"1" "1" expand "walk?" "1" expand "finseq_appl" )"1" "p!1" )"1" assert )"1" "1" assert )nil nil ))nil ))nil )"2" expand "walk?" "2" assert )"2" 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 )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" graph_conn_defs nil )"bool" graphs nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )"[real -> boolean]" rationalsnil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set[T]" mappings nil )"(strict_total_order?[real])" real_props nil )"[below[length(fs)] -> T]" nil )"bool" graphs nil )"int" integersnil )"Walk[T](G!1)" mappings nil )nil walks nil )"bool" walks nil )"T" mappings nil )"graph[T]" mappings nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets 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 naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" nil )nil number_fieldsnil )"[number_field -> boolean]" realsnil )nil reals nil )"bool" reals nil )nil walks nil )"bool" walks nil )nil walks nil )"bool" walks nil )nil booleans nil )"finite_set[T]" mappings nil )nil mappings nil )"bool" sets nil )nil walks nil )"prewalk[T]" mappings nil )nil application-judgement "finite_set[T]" graphs nil )nil walks nil )nil functions nil ))nil 3318087528"" (skosimp*)"" (split)"1" (flatten)"1" (expand "path_connected?" -1)"1" (skosimp*)"1" (expand "empty?" 1)"1" (expand "empty?" 1)"1" (skosimp*)"1" (inst 1 "x!1" )"1" (expand "member" -1)"1" expand "reachable" 1)"1" "1" (propax) nil nil )"2" "2" "2" "2" "1" (bddsimp) nil nil )"2" "2" "1" (propax) nil nil )"2" "x!1" "x!2" )"2" "2" "w!1" )"1" expand "walk_from?" "1" assert )nil nil ))nil )"2" "2" "w!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "path_connected?" )"2" (skosimp*)"2" (split)"1" (expand "empty?" )"1" (expand "empty?" )"1" (inst -1 "x!1" )"1" (expand "member" )"1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "reachable" )"2" (typepred "y!1" )"2" (typepred "x!2" )"2" "extensionality_postulate[T,bool]" )"2" "({y: T | vert(G!1)(y) AND (EXISTS (w: Seq(G!1)):walk_from?(G!1, w, x!1, y))})" "vert(G!1)" )"2" "2" "1" "1" "1" "x!2" )"1" "1" "1" "1" "1" "y!1" )"1" "1" "1" "1" "walk?_reverse" )"1" "G!1" "x!1" "y!1" "w!2" )"1" "G!1" "x!1" "x!2" "w!1" )"1" "1" "1" "1" "1" "walk_merge" )"1" "G!1" "w!4" "w!3" "x!2" "y!1" "x!1" )"1" "1" "1" expand "walk_from?" "1" assert )"1" "1" expand "walk?" "1" expand "finseq_appl" )"1" "p!1" )"1" assert )"1" "1" assert )nil nil ))nil ))nil )"2" expand "walk?" "2" assert )"2" 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 )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" graph_conn_defs nil )"bool" graphs nil )"bool" graphs nil )nil walks nil )"bool" walks nil )"set[T]" doubletons nil )nil doubletons nil )nil graphs nil )nil graphs nil )nil walks nil )"bool" walks nil )nil walks nil )"bool" walks nil )nil walks nil )nil walks nil ))nil ))nil 3318087528"" (skosimp*)"" (split)"1" (flatten)"1" (expand "path_connected?" -1)"1" (skosimp*)"1" (expand "empty?" 1)"1" (expand "empty?" 1)"1" (expand "member" 1)"1" (skosimp*)"1" (expand "reachable" 1)"1" "1" "1" "1" "1" "1" "1" (bddsimp) nil nil )"2" "2" "x!2" "x!3" )"2" expand "walk_from?" "2" "2" "w!1" )"2" expand "walk?" "2" "2" expand "verts_in?" "2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (lemma "path_reach1" )"2" (inst -1 "G!1" )"2" (flatten)"2" (hide -1)"2" (copy 2)"2" (expand "path_connected?" 1)"2" (split)"1" (propax) nil nil )"2" expand "empty?" 2)"2" expand "empty?" 2)"2" "2" "2" expand "member" -)"2" "x!1" )"2" "2" "x!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" graph_conn_defs nil )"bool" graphs nil )"bool" sets nil )"finite_set[T]" mappings nil )"graph[T]" mappings nil )"T" mappings nil )"bool" walks nil )"bool" graphs nil )"[below[length(fs)] -> T]" nil )nil application-judgement "finite_set[T]" mappings nil )"posint" integers nil )NOT const-decl "[bool -> bool]" booleans nil )nil walks nil )"(strict_total_order?[real])" real_props nil )"int" integersnil )"[real -> boolean]" rationalsnil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"bool" reals nil )"bool" reals nil )nil naturalnumbers nil )"odd_int" nil )"(strict_total_order?[real])" real_props nil )"Walk[T](G!1)" mappings nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets 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 naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" nil )nil number_fieldsnil )"[number_field -> boolean]" realsnil )nil reals nil )"bool" reals nil )nil walks nil )"bool" walks nil )nil walks nil )"bool" walks nil )nil mappings nil )nil booleans nil )"bool" sets nil )nil mappings nil ))nil ))"V3.2 ran" 3319386050"" (skosimp*)"" (lemma "conn_eq_path[T]" )"" (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" "x!1" )"1" "1" "(#length := 1, seq :=(LAMBDA (i:below(1)): x!1)#)" )"1" (assert ) nil nil ))nil )"2" "x!1" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "x!2" )"2" "y!1" )"2" expand "subgraph" -)"2" "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" "2" expand "min" )"2" assert )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 )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "^" "2" expand "min" "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 mappings nil )nil graph_connected nil )nil application-judgement "finite_set[T]" mappings nil )"[below[length(fs)] -> T]" nil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"bool" sets nil )"bool" sets nil )"bool" graphs nil )nil naturalnumbers nil )"bool" reals nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationalsnil )nil walks nil )"bool" walks nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" realsnil )nil number_fieldsnil )"[number -> boolean]" nil )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]" mappings nil )"(vert(G!1))" mappings nil )"prewalk[T]" mappings nil )nil application-judgement "finite_set[T]" graphs nil )"int" integersnil )"prewalk[T]" mappings nil )"below(length(p!1))" mappings nil )"posint" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )nil walks nil )"finseq" finite_sequences nil )"{k: nat | k <= i AND k <= j}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defsnil )"int" integersnil )"(total_order?[real])" real_props nil )"{k: int | k <= i AND k <= j}" real_defs nil )"prewalk[T]" mappings nil )"(total_order?[real])" real_props nil )"prewalk[T]" mappings nil )"nat" mappings nil )"(strict_total_order?[real])" real_props nil )nil walks nil )nil walks nil )"bool" graph_conn_defs nil )"finite_set[T]" mappings 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 3318087528"" (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" "x!1" )"1" "1" "(#l := 1, seq :=(LAMBDA (i:below(1)): x!1)#)" )"1" (assert ) nil nil ))nil )"2" "x!1" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "x!2" )"2" "y!1" )"2" expand "subgraph" -)"2" "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 )"2" "2" "2" assert )"2" 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 )"3" assert 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 )"set[T]" doubletons nil )nil doubletons nil )nil graphs nil )nil graphs nil )"bool" subgraphs nil )nil subgraphs nil )"Subgraph(G)" subgraphs nil )"bool" graph_conn_defs nil )nil walks nil )nil walks nil )nil walks nil )nil walks nil )nil walks nil )"bool" walks nil )nil walks nil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"bool" graphs nil )nil graph_connected nil ))nil ))nil 3318087528"" (skosimp*)"" (inst -1 "size(G!1)-size(H!1)" "H!1" "G!1" )"1" (assert ) nil nil )"2" (lemma "subgraph_smaller" )"2" (inst -1 "G!1" "H!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"(total_order?[real])" real_props nil )"int" integersnil )"graph[T]" mappings nil )"graph[T]" mappings nil )"nat" graphs nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationalsnil )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 mappings nil )"[numfield, numfield -> numfield]" nil )nil number_fields nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" realsnil )nil number_fieldsnil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"int" integersnil )nil subgraphs nil ))nil ))"trial" 3393153877"" (skosimp*)"" (apply-extensionality 1)"1" (apply-extensionality 1)"1" (hide 2 3)"1" (iff)"1" (split)"1" (expand "subgraph?" -)"1" (flatten)"1" (hide -3)"1" (expand "subset?" -)"1" "x!1" )"1" assert )"1" expand "member" -)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "graph_connected[T].conn_eq_path" )"2" (inst -1 "H!1" )"2" (flatten)"2" (iff -1)"2" "2" "2" "2" "2" "tree_paths[T].tree_one_path" )"2" "path?_subgraph[T]" )"2" "x!1" )"2" "2" "pp" "(# length:= 2, seq:= (LAMBDA (ii:below(2)): IF ii=0 THEN x!2 ELSE y!1 ENDIF) #)" )"2" case "path_from?(G!1,pp,x!2,y!1)" )"1" "1" expand "path_connected?" "1" "1" "x!2" "y!1" )"1" "1" "path_ops[T].walk_to_path_from" )"1" "H!1" "x!2" "y!1" "w!1" )"1" "w!1" )"1" expand "walk_from?" "1" "1" "1" "1" "1" expand "path_from?" "1" expand "from?" "1" "1" "G!1" "H!1" "p!1" )"1" "1" "G!1" "pp" "p!1" "x!2" "y!1" )"1" case "path_from?(H!1, p!1, x!2, y!1) AND path?(G!1,p!1) IMPLIES path_from?(G!1, p!1, x!2, y!1)" )"1" "1" replace "1" expand "path?" "1" "1" "1" "1" expand "walk?" "1" "1" "0" )"1" case "length(pp)=2" )"1" nil nil )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "subgraph?" "2" "finite_sets" )"2" "2" expand "size" "2" assert )"2" case "vert(G!1)(y!1)" )"1" assert )"1" "finite_sets[T].card_diff_subset" )"1" "vert(H!1)" "vert(G!1)" )"1" expand "subset?" "1" expand "member" "1" "1" expand "difference" "1" replace "1" case "card(vert(G!1))=card[T](vert(G!1))" )"1" assert )"1" "finite_sets[T].empty_card" )"1" "{x: T | vert(G!1)(x) AND NOT vert(H!1)(x)}" )"1" "1" "1" "1" "1" expand "empty?" "1" "y!1" )"1" expand "member" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_difference[T]" )"2" "vert(G!1)" "vert(H!1)" )"2" "2" "2" "2" expand "is_finite" )"2" "2" "N!1" "f!1" )"2" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "finite_sets[T].card_diff_subset" )"2" "vert(H!1)" "vert(G!1)" )"2" expand "subset?" "2" expand "member" "2" "2" case "card[T](vert(H!1))=card(vert(H!1))" )"1" case "card[T](vert(G!1))=card(vert(G!1))" )"1" assert )"1" replace "1" replace "1" replace "1" replace "1" assert )"1" "finite_sets[T].empty_card" )"1" "difference(vert(G!1), vert(H!1))" )"1" "1" expand "empty?" "1" "y!1" )"1" expand "member" "1" expand "difference" "1" case "edges(G!1)(x!1)" )"1" assert )"1" "G!1" )"1" "x!1" )"1" "1" "y!1" )"1" assert )"1" "1" "1" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "size" "3" "finite_sets[T].card_diff_subset" )"3" "vert(H!1)" "vert(G!1)" )"3" expand "subset?" "3" expand "member" "3" "1" case "card[T](vert(H!1))=card(vert(H!1))" )"1" case "card[T](vert(G!1))=card(vert(G!1))" )"1" assert )"1" replace "1" replace "1" replace "1" assert )"1" "finite_sets[T].empty_card" )"1" "difference(vert(G!1), vert(H!1))" )"1" "1" expand "empty?" "1" "x!2" )"1" expand "member" "1" expand "difference" "1" case "edges(G!1)(x!1)" )"1" assert )"1" "G!1" )"1" "x!1" )"1" "1" "x!2" )"1" expand "member" "1" "1" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "path_from?" "2" expand "path?" "2" expand "from?" "2" expand "walk?" "2" expand "verts_in?" "2" expand "finseq_appl" )"2" case "edges(G!1)(x!1)" )"1" "1" "1" case "length(pp)=2" )"1" replace "1" assert )"1" case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)" )"1" "1" nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)" )"1" "1" assert )"1" nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"3" case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)" )"1" case "length(pp)=2" )"1" "1" nil nil ))nil )"2" "2" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"4" case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)" )"1" case "length(pp)=2" )"1" "1" expand "edge?" "1" replace "1" assert )"1" "1" "n!1" )"1" case "n!1=0" )"1" replace "1" assert )"1" replace "1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"5" case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)" )"1" case "length(pp)=2" )"1" "G!1" )"1" "x!1" )"1" "1" "x!2" )"1" "y!1" )"1" "1" "1" "i!1" )"1" replace "1" replace "1" case "i!1=0 OR i!1=1" )"1" "1" replace "1" "1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "1" "1" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "vert(H!1)=vert(G!1)" )"1" (propax) nil nil )"2" (hide 2 3)"2" (hide -1 -4)"2" (expand "size" )"2" (expand "subgraph?" -)"2" (flatten)"2" "finite_sets[T].card_diff_subset" )"2" (inst -1 "vert(H!1)" "vert(G!1)" )"2" "1" "1" case "card[T](vert(H!1))=card(vert(H!1))" )"1" case "card[T](vert(G!1))=card(vert(G!1))" )"1" replace -1 -3 rl)"1" replace -2 -3 rl)"1" assert -3 -4)"1" replace -4 -3)"1" assert -3)"1" "finite_sets[T].empty_card" )"1" "difference(vert(G!1), vert(H!1))" )"1" "1" expand "empty?" "1" "1" "1" "x!1" )"1" expand "member" "1" expand "difference" "1" "1" "1" expand "member" "1" "1" expand "subset?" "1" "x!1" )"1" expand "member" "1" "1" "1" 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 )"2" (propax) nil nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil mappings 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 )nil graphs nil )"[bool, bool -> bool]" booleans nil )"bool" sets nil )"bool" sets nil )"bool" subgraphs nil )nil subgraph_paths nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )"bool" paths nil )"(strict_total_order?[real])" real_props nil )"[bool, bool -> bool]" booleans nil )"bool" graph_conn_defs nil )"graph[T]" mappings nil )"T" mappings nil )"T" mappings nil )nil path_ops nil )"bool" paths nil )"(strict_total_order?[real])" real_props nil )"(partial_order?[set[T]])" graph_deg_sum nil )"(partial_order?[set[T]])" sets_lemmas nil )nil application-judgement "finite_set[T]" mappings nil )"odd_int" nil )"posint" integers nil )"int" integersnil )"bool" walks nil )"[below[length(fs)] -> T]" nil )"bool" graphs nil )"bool" sets nil )"bool" graphs nil )nil application-judgement "finite_set[T]" graphs nil )"bool" walks nil )"bool" walks nil )"bool" walks nil )nil walks nil )"finite_set[T]" nil )"odd_int" integersnil )"bool" finite_sets nil )"set" sets nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )nil finite_sets nil )nil finite_sets nil )"bool" functions nil )"graph[T]" mappings nil )nil finite_sets nil )"nat" graphs nil )OR const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" real_props nil )"odd_int" nil )nil numbers nil )"[number -> boolean]" nil )nil number_fieldsnil )"[number_field -> boolean]" realsnil )nil reals nil )"[real -> boolean]" rationalsnil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )IF const-decl "[boolean, T, T -> T]" if_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil tree_paths nil )nil graph_connected nil ))nil )"trial" 3319141305"" (skosimp*)"" (apply-extensionality 1)"1" (apply-extensionality 1)"1" (hide 2 3)"1" (iff)"1" (split)"1" (expand "subgraph?" -)"1" (flatten)"1" (hide -3)"1" (expand "subset?" -)"1" "x!1" )"1" assert )"1" expand "member" -)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "graph_connected[T].conn_eq_path" )"2" (inst -1 "H!1" )"2" (flatten)"2" (iff -1)"2" "2" "2" "2" "2" "tree_paths[T].tree_one_path" )"2" "meng_scaff_defs[T].path?_subgraph" )"2" "x!1" )"2" "2" "pp" "(# l:= 2, seq:= (LAMBDA (ii:below(2)): IF ii=0 THEN x!2 ELSE y!1 ENDIF) #)" )"2" case "path_from?(G!1,pp,x!2,y!1)" )"1" "1" expand "path_connected?" "1" "1" "x!2" "y!1" )"1" "1" "path_ops[T].walk_to_path_from" )"1" "H!1" "x!2" "y!1" "w!1" )"1" "w!1" )"1" expand "walk_from?" "1" "1" "1" "1" "1" expand "path_from?" "1" expand "from?" "1" "1" "G!1" "H!1" "p!1" )"1" "1" "G!1" "pp" "p!1" "x!2" "y!1" )"1" case "path_from?(H!1, p!1, x!2, y!1) AND path?(G!1,p!1) IMPLIES path_from?(G!1, p!1, x!2, y!1)" )"1" "1" replace "1" expand "path?" "1" "1" "1" "1" expand "walk?" "1" "1" "0" )"1" case "length(pp)=2" )"1" nil nil )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil )"2" "2" "1" "1" "1" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" "1" "1" assert )nil nil ))nil ))nil )"2" expand "pp" )"2" nil nil ))nil )"3" expand "pp" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "subgraph?" "2" "finite_sets" )"2" "2" expand "size" "2" assert )"2" case "vert(G!1)(y!1)" )"1" assert )"1" "finite_sets[T].card_diff_subset" )"1" "vert(H!1)" "vert(G!1)" )"1" expand "subset?" "1" expand "member" "1" "1" expand "difference" "1" replace "1" case "card(vert(G!1))=card[T](vert(G!1))" )"1" assert )"1" "finite_sets[T].empty_card" )"1" "{x: T | vert(G!1)(x) AND NOT vert(H!1)(x)}" )"1" "1" "1" "1" "1" expand "empty?" "1" "y!1" )"1" expand "member" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_difference[T]" )"2" "vert(G!1)" "vert(H!1)" )"2" "2" "2" "2" expand "is_finite" )"2" "2" "N!1" "f!1" )"2" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "finite_sets[T].card_diff_subset" )"2" "vert(H!1)" "vert(G!1)" )"2" expand "subset?" "2" expand "member" "2" "2" case "card[T](vert(H!1))=card(vert(H!1))" )"1" case "card[T](vert(G!1))=card(vert(G!1))" )"1" assert )"1" replace "1" replace "1" replace "1" replace "1" assert )"1" "finite_sets[T].empty_card" )"1" "difference(vert(G!1), vert(H!1))" )"1" "1" expand "empty?" "1" "y!1" )"1" expand "member" "1" expand "difference" "1" case "edges(G!1)(x!1)" )"1" assert )"1" "G!1" )"1" "x!1" )"1" "1" "y!1" )"1" assert )"1" "1" "1" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "size" "3" "finite_sets[T].card_diff_subset" )"3" "vert(H!1)" "vert(G!1)" )"3" expand "subset?" "3" expand "member" "3" "1" case "card[T](vert(H!1))=card(vert(H!1))" )"1" case "card[T](vert(G!1))=card(vert(G!1))" )"1" assert )"1" replace "1" replace "1" replace "1" assert )"1" "finite_sets[T].empty_card" )"1" "difference(vert(G!1), vert(H!1))" )"1" "1" expand "empty?" "1" "x!2" )"1" expand "member" "1" expand "difference" "1" case "edges(G!1)(x!1)" )"1" assert )"1" "G!1" )"1" "x!1" )"1" "1" "x!2" )"1" expand "member" "1" "1" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "path_from?" "2" expand "path?" "2" expand "from?" "2" expand "walk?" "2" expand "verts_in?" "2" case "edges(G!1)(x!1)" )"1" "1" "1" case "length(pp)=2" )"1" replace "1" assert )"1" case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)" )"1" "1" nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)" )"1" "1" assert )"1" nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"3" case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)" )"1" case "length(pp)=2" )"1" "1" nil nil ))nil )"2" "2" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"4" case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)" )"1" case "length(pp)=2" )"1" "1" expand "edge?" "1" replace "1" assert )"1" "1" "n!1" )"1" case "n!1=0" )"1" replace "1" assert )"1" replace "1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"5" case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)" )"1" case "length(pp)=2" )"1" "G!1" )"1" "x!1" )"1" "1" "x!2" )"1" "y!1" )"1" "1" "1" "i!1" )"1" replace "1" replace "1" case "i!1=0 OR i!1=1" )"1" "1" replace "1" "1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "1" "1" nil nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil )"4" "4" nil nil ))nil )"5" "5" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "vert(H!1)=vert(G!1)" )"1" (propax) nil nil )"2" (hide 2 3)"2" (hide -1 -4)"2" (expand "size" )"2" (expand "subgraph?" -)"2" (flatten)"2" "finite_sets[T].card_diff_subset" )"2" (inst -1 "vert(H!1)" "vert(G!1)" )"2" "1" "1" case "card[T](vert(H!1))=card(vert(H!1))" )"1" case "card[T](vert(G!1))=card(vert(G!1))" )"1" replace -1 -3 rl)"1" replace -2 -3 rl)"1" assert -3 -4)"1" replace -4 -3)"1" assert -3)"1" "finite_sets[T].empty_card" )"1" "difference(vert(G!1), vert(H!1))" )"1" "1" expand "empty?" "1" "1" "1" "x!1" )"1" expand "member" "1" expand "difference" "1" "1" "1" expand "member" "1" "1" expand "subset?" "1" "x!1" )"1" expand "member" "1" "1" "1" 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 )"2" (propax) nil nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil graph_connected nil )nil tree_paths nil )"nat" graphs nil )"finite_set[T]" nil )nil walks nil )"bool" walks nil )"bool" walks nil )"bool" walks nil )nil application-judgement "finite_set[T]" graphs nil )"bool" graphs nil )"bool" graphs nil )"bool" walks nil )"(partial_order?[set[T]])" graph_deg_sum nil )"bool" paths nil )nil path_ops nil )"bool" graph_conn_defs nil )nil walks nil )"bool" paths nil )"bool" subgraphs nil )nil graphs nil )nil graphs nil )nil doubletons nil )"set[T]" doubletons nil ))nil )"trial" 3319140197"" (skosimp*)"" (apply-extensionality 1)"1" (apply-extensionality 1)"1" (hide 2 3)"1" (iff)"1" (split)"1" (expand "subgraph?" -)"1" (flatten)"1" (hide -3)"1" (expand "subset?" -)"1" "x!1" )"1" assert )"1" expand "member" -)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "graph_connected[T].conn_eq_path" )"2" (inst -1 "H!1" )"2" (flatten)"2" (iff -1)"2" "2" "2" "2" "2" "tree_paths[T].tree_one_path" )"2" "meng_scaff_defs[T].path?_subgraph" )"2" "x!1" )"2" "2" "pp" "(# l:= 2, seq:= (LAMBDA (ii:below(2)): IF ii=0 THEN x!2 ELSE y!1 ENDIF) #)" )"2" case "path_from?(G!1,pp,x!2,y!1)" )"1" "1" expand "path_connected?" "1" "1" "x!2" "y!1" )"1" "1" "path_ops[T].walk_to_path_from" )"1" "H!1" "x!2" "y!1" "w!1" )"1" "w!1" )"1" expand "walk_from?" "1" "1" "1" "1" "1" expand "path_from?" "1" expand "from?" "1" "1" "G!1" "H!1" "p!1" )"1" "1" "G!1" "pp" "p!1" "x!2" "y!1" )"1" case "path_from?(H!1, p!1, x!2, y!1) AND path?(G!1,p!1) IMPLIES path_from?(G!1, p!1, x!2, y!1)" )"1" "1" replace "1" expand "path?" "1" "1" "1" "1" expand "walk?" "1" "1" "0" )"1" expand "finseq_appl" )"1" case "length(pp)=2" )"1" nil nil )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil )"2" "2" "1" "1" "1" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" "1" "1" assert )nil nil ))nil ))nil )"2" expand "pp" )"2" nil nil ))nil )"3" expand "pp" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "subgraph?" "2" "finite_sets" )"2" "2" expand "size" "2" assert )"2" case "vert(G!1)(y!1)" )"1" assert )"1" "finite_sets[T].card_diff_subset" )"1" "vert(H!1)" "vert(G!1)" )"1" expand "subset?" "1" expand "member" "1" "1" expand "difference" "1" replace "1" case "card(vert(G!1))=card[T](vert(G!1))" )"1" assert )"1" "finite_sets[T].empty_card" )"1" "{x: T | vert(G!1)(x) AND NOT vert(H!1)(x)}" )"1" "1"
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.673 Sekunden
(vorverarbeitet am 2026-04-30)
¤ *© Formatika GbR, Deutschland
2026-05-26
