Impressum complem.prf
Sprache: Lisp
(complem"from-prelude" 3349377711"" (use "finite_sets_of_sets[T].powerset_natfun_inj" )"" (skosimp)"" (expand "is_finite" )"" (inst 1 "exp2(card(A!1))" "powerset_natfun(A!1)" )"" (expand "injective?" ) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" exp2 nil ) (set type-eq-decl nil sets nil )nil finite_sets nil )"[T, T -> boolean]" equalities nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )nil defined_types nil )nil sets nil )"setofsets" sets nil )"bool" reals nil )nil nat_types nil )nil naturalnumbers nil )"below(exp2(card(A)))" nil )"bool" functions nil )"bool" finite_sets nil )nil complem nil )nil finite_sets_of_sets nil ))nil 3349377681"" (use "powerset_natfun_inj" )"" (skosimp)"" (expand "is_finite" )"" (inst 1 "exp2(card(A!1))" "powerset_natfun(A!1)" )"" (expand "injective?" ) (("" (grind) nil ))))))))))nil )nil nil ))nil 3349381067 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil complem nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil application-judgement "finite_set[T]" graph_ops nil )"bool" functions nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"boolean" notequal nil )"set[doubleton[T]]" complem nil )"bool" sets nil )"bool" sets nil )"setofsets" sets nil )"R" restrict nil ))"revis all_edge" 3349528703"" (skosimp*)"" (use all_edges_power)"" (lemma "finite_sets[set[T]].finite_subset" )"" (inst -1 "powerset(V!1)" "all_edges(V!1)" )"" (bddsimp)"1" (hide -2)"1" (expand "extend" )"1" (ground)"1" (expand "is_finite" )"1" (skosimp*)"1" (inst + "N!1" "f!1" )"1" (expand "injective?" )"1" (skosimp*)"1" (inst?) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (hide 2)"2" (expand "restrict" ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil complem nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil complem nil )"finite_set[set[T]]" nil )"(nonempty?[set[T]])" nil )nil defined_types nil )nil sets nil )"setofsets" 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 )"bool" booleans nil )"R" extend nil )"set[doubleton[T]]" complem nil )"finite_set[S]" nil )"(partial_order?[set[T]])" nil )"R" restrict nil )NOT const-decl "[bool -> bool]" booleans nil )nil application-judgement "finite_set[T]" graph_ops nil )"bool" sets nil )"bool" sets nil )"bool" functions nil )nil nat_types nil )"bool" reals 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 )"finite_set[T]" complem nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil ))nil 3349381260"" (skosimp*)"" (use all_edges_power)"" (lemma "finite_sets[set[T]].finite_subset" )"" (inst -1 "powerset(V!1)" "all_edges(V!1)" )"" (bddsimp)"1" (hide -2)"1" (expand "extend" )"1" (grind)"1" (reveal -1)"1" "dbl[T](x!3, y!3)" "dbl[T](x!4, y!4)" )"1" (assert ) nil nil )) nil ))nil )"2" (reveal -1)"2" "dbl[T](x!3, y!3)" "dbl[T](x!4, y!4)" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (hide 2)"2" (expand "restrict" ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"set[T]" doubletons nil )nil doubletons nil ))nil 3349204238"" (use "all_edges_finite" )"" (skosimp*) (("" (inst?) nil nil )) nil )) nil )nil complem nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_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 graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil complem nil ))nil ))nil 3349381053 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil complem 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 )nil application-judgement "finite_set[T]" graph_ops nil )"boolean" notequal nil )"set[doubleton[T]]" complem nil ))nil ))"works" 3349205027"" (grind)"1" (lemma "graphs[T].edges_vert_in" ) (("1" (grind) nil nil ))nil )"2" (lemma "graphs[T].edges_vert_in" ) (("2" (grind) nil nil ))nil )"3" (lemma "graphs[T].edges_vert_in" ) (("3" (grind) nil nil ))nil )"4" (lemma "graphs[T].edges_vert_in" ) (("4" (grind) nil nil ))nil )"5" (lemma "graphs[T].edges_vert_in" ) (("5" (grind) nil nil ))nil )"6" (lemma "graphs[T].edges_vert_in" ) (("6" (grind) nil nil ))nil ))nil )nil graphs nil )nil application-judgement "finite_set[T]" graph_ops nil )"graph[T]" complem nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil complem 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 )"bool" subgraphs nil )"set[doubleton[T]]" complem nil )"bool" sets nil )"bool" sets nil )"graph[T]" complem nil )"boolean" notequal nil ))nil 3349204238"" (skosimp*)"" case "subset?(difference[doubleton[T]](all_edges(vert(G!1)), edges(G!1)),all_edges(vert(G!1)))" )"1" (lemma "finite_sets[doubleton[T]].finite_subset" )"1" "all_edges(vert(G!1))" "difference[doubleton[T]](all_edges(vert(G!1)), edges(G!1))" )"1" (bddsimp) nil nil )"2" (lemma "all_edges_finite" )"2" (inst -1 "vert(G!1)" ) nil nil )) nil ))nil ))nil )"2" (lemma "sets_lemmas[doubleton[T]].difference_subset" )"2" (inst -1 "all_edges(vert(G!1))" "edges(G!1)" ) nil nil ))nil ))nil ))nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"set[doubleton[T]]" complem nil )nil finite_sets nil )"bool" finite_sets nil )"set" sets nil )"bool" 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 complem nil )"graph[T]" complem nil )nil complem nil )nil finite_sets nil )nil sets_lemmas nil ))nil ))nil 3349381053 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil complem 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 )nil application-judgement "finite_set[T]" graph_ops nil )"boolean" notequal nil )"set[doubleton[T]]" complem nil )"bool" sets nil )"set" sets nil ))nil ))nil 3349285188"" (skosimp*)"" (expand "complement" )"" (apply-extensionality 1 :hide? t)"" (apply-extensionality 1 :hide? t)"" (expand "difference" )"" (expand "member" )"" (iff 1)"" (bddsimp)"" (expand "all_edges" )"" (typepred "G!1" )"" (typepred "x!1" )"" (skosimp*)"" (inst 2 "x!2" "y!1" )"" (bddsimp)"1" "x!1" )"1" "1" (grind) nil nil ))nil ))nil )"2" "x!1" )"2" "2" (grind) nil nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"graph[T]" complem nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil application-judgement "finite_set[T]" graph_ops nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"set" sets nil )"set[doubleton[T]]" complem nil )nil finite_sets nil )"bool" 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 complem nil ))nil 3349204238 ("" (subtype-tcc) nil nil )"set" sets nil )) nil ))"Do not use vert_in" 3358451058"" (skosimp*)"" (expand "path_connected?" )"" (bddsimp)"1" (expand "empty?" )"1" (expand "empty?" )"1" (hide 2) (("1" (grind) nil nil )) nil )) nil ))nil )"2" (skosimp*)"2" (case "x!1=y!1" )"1" (inst 2 "gen_seq1(G!1,x!1)" )"1" (hide 3)"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil ))nil )"2" (lemma "walks[T].gen_seq1_is_walk" )"2" (inst -1 "G!1" "x!1" )"2" (typepred "x!1" ) (("2" (bddsimp) nil nil ))nil ))nil ))nil ))nil )"2" (case "x!2=y!2" )"1" (inst 4 "gen_seq1(complement(G!1),x!2)" )"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil )"2" (lemma "walks[T].gen_seq1_is_walk" )"2" (inst -1 "complement(G!1)" "x!2" )"2" (typepred "x!2" ) (("2" (bddsimp) nil nil ))nil ))nil ))nil ))nil )"2" (case "edge?(G!1)(x!2,y!2)" )"1" (case "x!1=x!2" )"1" (case "y!1=y!2" )"1" (inst 4 "gen_seq2(G!1,x!1,y!1)" )"1" (hide 5)"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil ))nil )"2" (lemma "walks[T].edge_to_walk" )"2" (inst -1 "G!1" "x!1" "y!1" )"2" (bddsimp)"1" (expand "edge?" )"1" "1" assert )"1" replace -1 1 lr)"1" replace -2 1 lr)"1" assert )"1" "1" "walks" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (case "edge?(G!1)(x!1, y!1)" )"1" (inst 5 "gen_seq2(G!1,x!1,y!1)" )"1" (hide -3 6)"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil ))nil )"2" (lemma "walks[T].edge_to_walk" )"2" (inst? -1)"2" (assert )"2" expand "edge?" )"2" "2" assert )"2" "walks" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "edge?(G!1)(y!2,y!1)" )"1" "add1(gen_seq2(G!1,x!2,y!2),y!1)" )"1" (hide 7)"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil ))nil )"2" (lemma "walks[T].walk?_add1" )"2" (inst? -1)"2" "1" "1" "walks" )"1" (assert ) nil nil ))nil ))nil )"2" "graphs[T].edges_vert_in" )"2" "G!1" "dbl[T](y!2,y!1)" "y!2" "y!1" )"1" expand "edge?" )"1" (assert ) nil nil ))nil )"2" "y!2" "y!1" )"2" (assert ) nil nil ))nil ))nil ))nil )"3" "walks[T].edge_to_walk" )"3" "G!1" "x!2" "y!2" )"3" expand "edge?" )"3" assert )"3" "3" "walks" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "graphs[T].edges_vert_in" )"3" "G!1" "dbl[T](y!2,y!1)" "y!2" "y!1" )"1" expand "edge?" )"1" (assert ) nil nil ))nil )"2" "y!2" "y!1" )"2" (assert ) nil nil ))nil ))nil ))nil )"4" (lemma "graphs[T].edges_vert_in" )"4" "G!1" "dbl[T](x!2,y!2)" "x!2" "y!2" )"1" "1" expand "edge?" )"1" (assert ) nil nil ))nil ))nil )"2" "x!2" "y!2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "add1(gen_seq2(complement(G!1),x!2,y!1),y!2)" )"1" (hide 7)"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil ))nil )"2" (lemma "walks[T].walk?_add1" )"2" (hide 8)"2" "complement(G!1)" "gen_seq2[T](complement(G!1), x!2, y!1)" "y!2" )"2" assert )"2" "walks" )"2" "2" "1" assert )"1" "1" assert )"1" "graphs[T].edge?_comm" )"1" "G!1" "y!2" "y!1" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "y!1" "y!2" )"2" assert )"2" "graphs[T].edges_vert_in" )"2" "G!1" "dbl[T](x!2,y!2)" "x!2" "y!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "walks[T].edge_to_walk" )"2" "complement(G!1)" "x!2" "y!1" )"2" "1" "1" replace -1 * lr)"1" "1" "walks" )"1" assert )"1" "1" "x!2" "y!1" )"1" "1" "y!1" )"1" nil nil ))nil )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "walks[T].edge_to_walk" )"2" "complement(G!1)" "x!2" "y!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "y!1" )"3" (hide-all-but (-1 1))"3" "walks" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case-replace "edge?(G!1)(x!1,y!1)" )"1" (inst 5 "gen_seq2(G!1,x!1,y!1)" )"1" (hide 6)"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil ))nil )"2" (lemma "walks[T].edge_to_walk" )"2" (inst? -1)"2" (assert )"2" (hide-all-but (-1 1))"2" "walks" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case-replace "edge?(G!1)(x!1,x!2)" )"1" (case-replace "edge?(G!1)(y!2,y!1)" )"1" case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!1 AND seq(w)(length(w) - 1) = y!1 and walk?(G!1,w)" )"1" (skosimp*)"1" (hide 7)"1" "walks" )"1" "w!1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 7 8)"2" (install-rewrites "walks" )"2" "walks[T].list2prewalk((:x!1,x!2,y!2,y!1:))" )"1" "walks" )"1" assert )"1" "1" "1" "1" case "n!1=0" )"1" replace -1 -3 lr)"1" expand "nth" )"1" nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 -3 lr)"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "n!1=2" )"1" replace -1 -3 lr)"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" case "n!1=0" )"1" expand "nth" )"1" (assert ) nil nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace -1 2 lr)"1" assert )nil nil ))nil ))nil )"2" case "n!1=2" )"1" replace -1 3 lr)"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" "graphs[T].edges_vert_in" )"2" "graphs[T].edges_vert_in" )"2" "graphs[T].edges_vert_in" )"2" "G!1" "dbl[T](y!2,y!1)" "y!2" "y!1" )"2" "G!1" "dbl[T](x!1,x!2)" "x!1" "x!2" )"2" "G!1" "dbl[T](x!2,y!2)" "x!2" "y!2" )"2" "2" case "i!1=0" )"1" expand "nth" )"1" replace "1" nil nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=3" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "edge?(G!1)(x!2,y!1)" )"1" (hide 8)"1" case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!1 AND seq(w)(length(w) - 1) = y!1 and walk?(G!1,w)" )"1" "1" "w!1" )"1" (bddsimp) nil nil ))nil ))nil )"2" "2" "walks[T].list2prewalk((:x!1,x!2,y!1:))" )"1" "walks" )"1" assert )"1" "1" "1" "1" case "n!1=0" )"1" replace -1 -3 lr)"1" expand "nth" )"1" nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 -3 lr)"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "n!1=0" )"1" expand "nth" )"1" assert )nil nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace -1 2 lr)"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "1" case "n!1=0" )"1" expand "nth" )"1" assert )nil nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace -1 -3 lr)"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "n!1=0" )"1" expand "nth" )"1" assert )nil nil ))nil )"2" case "n!1=1" )"1" replace -1 2 lr)"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "i!1" )"3" case "i!1=0" )"1" expand "nth" )"1" replace -1 1 lr)"1" "x!1" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace -1 2 lr)"1" expand "nth" )"1" expand "nth" )"1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace -1 3 lr)"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" assert )"4" "4" "i!1" )"4" case "i!1=0" )"1" expand "nth" )"1" replace -1 1 lr)"1" "x!1" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace -1 2 lr)"1" expand "nth" )"1" expand "nth" )"1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace -1 3 lr)"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 3 8))"2" (lemma "graphs[T].edge?_comm" )"2" "G!1" "y!2" "y!1" )"2" "2" case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!2 AND seq(w)(length(w) - 1) = y!2 and walk?(complement(G!1),w)" )"1" "1" "w!1" )"1" "walks" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "walks[T].list2prewalk((:x!2,y!1,y!2:))" )"1" "walks" )"1" assert )"1" "1" "1" "1" case "n!1=0" )"1" replace "1" expand "nth" )"1" assert )nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil )"3" case "n!1=0" )"1" expand "nth" )"1" replace "1" "x!2" "y!1" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace "1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "nth" )"2" "2" case "n!1=0" )"1" replace -1 1 lr)"1" assert )"1" "x!2" "y!1" )"1" "1" assert )nil nil )"2" assert )nil nil )"3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace "1" assert )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" case "n!1=0" )"1" replace -1 1 lr)"1" expand "nth" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace "1" assert )nil nil ))nil ))nil )"2" "1" assert )nil nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "4" case "n!1=0" )"1" replace -1 1 lr)"1" assert )"1" "x!2" "y!1" )"1" "1" assert )nil nil )"2" "2" replace "2" expand "edge?" )"2" nil nil ))nil ))nil ))nil )"3" "3" replace "3" expand "edge?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace "1" assert )"1" "1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"5" (assert ) nil nil )"6" "6" assert )"6" "1" case "n!1=0" )"1" replace "1" expand "nth" )"1" assert )nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "n!1=0" )"1" replace "1" expand "nth" )"1" nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"3" case "n!1=0" )"1" expand "nth" )"1" assert )"1" "x!2" "y!1" )"1" assert )"1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace "1" assert )"1" replace "1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"7" "7" assert )"7" "1" case "n!1=0" )"1" replace "1" expand "nth" )"1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "n!1=0" )"1" replace "1" expand "nth" )"1" "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"3" case "n!1=0" )"1" replace "1" expand "nth" )"1" "x!2" "y!1" )"1" assert )"1" "1" "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace "1" assert )"1" "y!1" "y!2" )"1" "1" assert )nil nil )"2" assert )"2" "2" expand "edge?" )"2" nil nil ))nil ))nil ))nil )"3" "3" replace "3" expand "edge?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"8" assert )"8" "8" case "n!1=0" )"1" expand "nth" )"1" assert )"1" "1" "1" expand "edge?" )"1" replace "1" nil nil ))nil ))nil ))nil )"2" "x!2" "y!1" )"2" "1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil )"2" "2" "y!1" )"2" nil nil ))nil ))nil )"3" "3" "x!2" )"3" expand "complement" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace "1" assert )"1" "1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil )"2" "y!1" "y!2" )"2" "1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil )"2" "y!2" )"2" expand "complement" )"2" nil nil ))nil ))nil )"3" "y!1" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"9" (assert ) nil nil )"10" "10" replace -4 * lr)"10" expand "edge?" )"10" assert )nil nil ))nil ))nil ))nil )"11" "11" "i!1" )"11" case "i!1=0" )"1" expand "nth" )"1" replace "1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"12" "12" "i!1" )"12" case "i!1=0" )"1" expand "nth" )"1" replace "1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"13" "13" "i!1" )"13" case "i!1=0" )"1" expand "nth" )"1" replace "1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"14" "14" "i!1" )"14" case "i!1=0" )"1" expand "nth" )"1" replace "1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"15" "15" "i!1" )"15" case "i!1=0" )"1" expand "nth" )"1" replace "1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"16" "16" "i!1" )"16" case "i!1=0" )"1" expand "nth" )"1" replace "1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "edge?(G!1)(y!1,y!2)" )"1" (case "y!1=y!2" )"1" case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!2 AND seq(w)(length(w) - 1) = y!2 and walk?(complement(G!1),w)" )"1" (skosimp*)"1" "w!1" )"1" "walks" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 8 9)"2" "walks[T].list2prewalk((:x!2,x!1,y!2:))" )"1" "walks" )"1" (assert ) nil nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil )"2" (case "edge?(G!1)(x!1,y!2)" )"1" case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!1 AND seq(w)(length(w) - 1) = y!1 and walk?(G!1,w)" )"1" "1" "w!1" )"1" "walks" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "walks[T].list2prewalk((:x!1,y!2,y!1:))" )"1" "walks" )"1" assert )"1" "1" "1" "1" case "n!1=0" )"1" replace -1 -3 lr)"1" expand "nth" )"1" nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 -3 lr)"1" expand "nth" )"1" expand "nth" )"1" replace "1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "n!1=0" )"1" expand "nth" )"1" assert )nil nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace -1 2 lr)"1" assert )"1" "graphs[T].edge?_comm" )"1" "G!1" "y!2" "y!1" )"1" "1" expand "edge?" )"1" nil nil ))nil )"2" expand "edge?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" case "i!1=0" )"1" expand "nth" )"1" replace -1 1 lr)"1" "x!1" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace -1 2 lr)"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" case "i!1=2" )"1" replace -1 3 lr)"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil )"2" case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!2 AND seq(w)(length(w) - 1) = y!2 and walk?(complement(G!1),w)" )"1" "1" "w!1" )"1" "1" "walks" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "walks[T].list2prewalk((:x!2,x!1,y!2:))" )"1" "walks" )"1" assert )"1" "1" "1" "1" case "n!1=0" )"1" replace -1 -3 lr)"1" expand "nth" )"1" replace -4 + lr)"1" "graphs[T].edge?_comm" )"1" "G!1" "y!2" "y!1" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 -3 lr)"1" expand "nth" )"1" expand "nth" )"1" replace "1" "graphs[T].edge?_comm" )"1" "G!1" "x!1" "x!2" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "graphs[T].edge?_comm" )"2" "G!1" "x!1" "x!2" )"2" replace -4 + rl)"2" replace -4 -6 rl)"2" expand "edge?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" case "n!1=0" )"1" expand "nth" )"1" assert )"1" "x!2" "x!1" )"1" assert )"1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace -1 2 lr)"1" assert )"1" "x!1" "y!2" )"1" assert )"1" replace "1" "graphs[T].edge?_comm" )"1" "G!1" "x!1" "x!2" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "1" case "n!1=0" )"1" replace -1 -3 lr)"1" expand "nth" )"1" replace -3 * lr)"1" nil nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 -3 lr)"1" expand "nth" )"1" expand "nth" )"1" replace "1" "graphs[T].edge?_comm" )"1" "G!1" "y!2" "x!2" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "n!1=0" )"1" expand "nth" )"1" assert )"1" "graphs[T].edge?_comm" )"1" "G!1" "x!1" "x!2" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace -1 -3 lr)"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" expand "nth" )"2" assert )nil nil ))nil ))nil ))nil )"3" case "n!1=0" )"1" expand "nth" )"1" assert )"1" "x!2" "x!1" )"1" assert )"1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace -1 2 lr)"1" assert )"1" "x!1" "y!2" )"1" assert )"1" "1" replace "1" "graphs[T].edge?_comm" )"1" "G!1" "y!2" "x!2" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "y!2" )"2" expand "complement" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" case "i!1=0" )"1" expand "nth" )"1" replace -1 1 lr)"1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace -1 2 lr)"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace -1 3 lr)"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "i!1" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" case "i!1=0" )"1" expand "nth" )"1" replace -1 1 lr)"1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace -1 2 lr)"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace -1 3 lr)"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!2 AND seq(w)(length(w) - 1) = y!2 and walk?(complement(G!1),w)" )"1" (skosimp*)"1" (inst 9 "w!1" )"1" "walks" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 10)"2" (hide 9)"2" case "y!1=y!2" )"1" "walks[T].list2prewalk((:x!2,x!1,y!2:))" )"1" "walks" )"1" assert )"1" "1" assert )"1" "1" assert )"1" "1" "1" "1" case "n!1=0" )"1" replace "1" expand "nth" )"1" assert )nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "n!1=0" )"1" replace "1" expand "nth" )"1" "1" "1" "graphs[T].edge?_comm" )"1" "G!1" "x!1" "x!2" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"3" assert )"3" case "n!1=0" )"1" replace "1" expand "nth" )"1" "x!2" "x!1" )"1" "x!1" )"1" "x!2" )"1" expand "complement" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" "x!1" "y!2" )"1" "x!1" )"1" "y!2" )"1" expand "complement" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "x!2" )"2" "x!1" )"2" "y!2" )"2" expand "complement" )"2" "2" "i!1" )"2" case "i!1=0" )"1" replace "1" expand "nth" )"1" nil nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" "walks[T].list2prewalk((:x!2,x!1,y!1,y!2:))" )"1" "walks" )"1" assert )"1" "1" "1" case "n!1=0" )"1" expand "nth" )"1" assert )"1" "1" "graphs[T].edge?_comm" )"1" "G!1" "x!1" "x!2" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil )"2" "x!2" "x!1" )"2" "x!2" )"2" "x!1" )"2" expand "complement" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 3 lr)"1" expand "nth" )"1" expand "nth" )"1" "1" "x!1" "y!1" )"1" "x!1" )"1" "y!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=2" )"1" replace -1 4 lr)"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!1" "y!2" )"1" assert )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "x!2" )"2" "x!1" )"2" "y!1" )"2" "y!2" )"2" expand "complement" )"2" "2" case "i!1=0" )"1" assert )nil nil )"2" case "i!1=1" )"1" assert )nil nil )"2" case "i!1=2" )"1" assert )nil nil )"2" case "i!1=3" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 5)"2" (inst 5 "gen_seq2(G!1,x!2,y!2)" )"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil )"2" (lemma "walks[T].edge_to_walk" )"2" (inst -1 "complement(G!1)" "x!2" "y!2" )"2" (assert )"2" (bddsimp)"1" (expand "complement" -1 2)"1" expand "gen_seq2" )"1" (propax) nil nil ))nil ))nil )"2" (hide 2)"2" "1" "y!2" )"1" expand "complement" )"1" (propax) nil nil ))nil ))nil )"2" "x!2" )"2" expand "complement" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "y!2" )"3" (expand "complement" )"3" (propax) nil nil )) nil ))nil )"4" (typepred "x!2" )"4" (expand "complement" )"4" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" graph_conn_defs nil )"(vert(complement(G!1)))" complem nil )"set[doubleton[T]]" complem nil )"set" sets nil )nil graphs nil )"(vert(complement(G!1)))" complem nil )"prewalk" walks nil )"(strict_total_order?[real])" real_props nil )nil graphs nil )"int" integers nil )nil walks nil )"(vert(G!1))" complem nil )"Seq(G)" walks nil )nil application-judgement "finite_set[T]" graph_conn_defs nil )"doubleton[T]" graphs nil )nil walks nil )"walks[T].prewalk" complem nil )"walks[T].prewalk" complem nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil ) (>= const-decl "bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"walks[T].prewalk" complem nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[below[length(fs)] -> T]" finite_sequencesnil )"even_int" integersnil )"T" list_props nil )"posint" nil )"prewalk" walks nil )nil walks nil )nil list_adt nil )"nat" list_props nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )nil defined_types nil )"boolean" list_adt nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"(strict_total_order?[real])" real_props nil )"walks[T].prewalk" complem nil )"walks[T].prewalk" complem nil )"walks[T].prewalk" complem nil )"walks[T].prewalk" complem nil )"bool" graphs nil )"(vert(G!1))" complem nil )"Seq(G)" walks nil )nil walks nil )"bool" walks nil )"graph[T]" complem 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 )nil walks nil )NOT const-decl "[bool -> bool]" booleans nil )nil walks nil )nil complem nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"bool" graphs nil )"graph[T]" complem nil )"bool" sets nil )"bool" sets nil ))"paul" 3358096826"" (skosimp*)"" (expand "path_connected?" )"" (bddsimp)"1" (expand "empty?" )"1" (expand "empty?" )"1" (hide 2) (("1" (grind) nil nil )) nil )) nil ))nil )"2" (skosimp*)"2" (case "x!1=y!1" )"1" (inst 2 "gen_seq1(G!1,x!1)" )"1" (hide 3)"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil ))nil )"2" (lemma "walks[T].gen_seq1_is_walk" )"2" (inst -1 "G!1" "x!1" )"2" (typepred "x!1" ) (("2" (bddsimp) nil nil ))nil ))nil ))nil ))nil )"2" (case "x!2=y!2" )"1" (inst 4 "gen_seq1(complement(G!1),x!2)" )"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil )"2" (lemma "walks[T].gen_seq1_is_walk" )"2" (inst -1 "complement(G!1)" "x!2" )"2" (typepred "x!2" ) (("2" (bddsimp) nil nil ))nil ))nil ))nil ))nil )"2" (case "edge?(G!1)(x!2,y!2)" )"1" (case "x!1=x!2" )"1" (case "y!1=y!2" )"1" (inst 4 "gen_seq2(G!1,x!1,y!1)" )"1" (hide 5)"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil ))nil )"2" (lemma "walks[T].edge_to_walk" )"2" (inst -1 "G!1" "x!1" "y!1" )"2" (bddsimp)"1" (expand "edge?" )"1" "1" assert )"1" replace -1 1 lr)"1" replace -2 1 lr)"1" assert )"1" "1" "walks" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (case "edge?(G!1)(x!1, y!1)" )"1" (inst 5 "gen_seq2(G!1,x!1,y!1)" )"1" (hide -3 6)"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil ))nil )"2" (lemma "walks[T].edge_to_walk" )"2" (inst? -1)"2" (assert )"2" expand "edge?" )"2" "2" assert )"2" "walks" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "edge?(G!1)(y!2,y!1)" )"1" "add1(gen_seq2(G!1,x!2,y!2),y!1)" )"1" (hide 7)"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil ))nil )"2" (lemma "walks[T].walk?_add1" )"2" (inst? -1)"2" "1" "1" "walks" )"1" (assert ) nil nil ))nil ))nil )"2" "graphs[T].edges_vert_in" )"2" "G!1" "dbl[T](y!2,y!1)" "y!2" "y!1" )"1" expand "edge?" )"1" (assert ) nil nil ))nil )"2" "y!2" "y!1" )"2" (assert ) nil nil ))nil ))nil ))nil )"3" "walks[T].edge_to_walk" )"3" "G!1" "x!2" "y!2" )"3" expand "edge?" )"3" assert )"3" "3" "walks" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "graphs[T].edges_vert_in" )"3" "G!1" "dbl[T](y!2,y!1)" "y!2" "y!1" )"1" expand "edge?" )"1" (assert ) nil nil ))nil )"2" "y!2" "y!1" )"2" (assert ) nil nil ))nil ))nil ))nil )"4" (lemma "graphs[T].edges_vert_in" )"4" "G!1" "dbl[T](x!2,y!2)" "x!2" "y!2" )"1" "1" expand "edge?" )"1" (assert ) nil nil ))nil ))nil )"2" "x!2" "y!2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "add1(gen_seq2(complement(G!1),x!2,y!1),y!2)" )"1" (hide 7)"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil ))nil )"2" (lemma "walks[T].walk?_add1" )"2" (hide 8)"2" "complement(G!1)" "gen_seq2[T](complement(G!1), x!2, y!1)" "y!2" )"2" assert )"2" "walks" )"2" "2" "1" assert )"1" "1" assert )"1" "graphs[T].edge?_comm" )"1" "G!1" "y!2" "y!1" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "y!1" "y!2" )"2" assert )"2" "graphs[T].edges_vert_in" )"2" "G!1" "dbl[T](x!2,y!2)" "x!2" "y!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "walks[T].edge_to_walk" )"2" "complement(G!1)" "x!2" "y!1" )"2" "1" "1" replace -1 * lr)"1" "1" "walks" )"1" assert )"1" "1" "x!2" "y!1" )"1" "1" "y!1" )"1" nil nil ))nil )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "walks[T].edge_to_walk" )"2" "complement(G!1)" "x!2" "y!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "y!1" )"3" (hide-all-but (-1 1))"3" "walks" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case-replace "edge?(G!1)(x!1,y!1)" )"1" (inst 5 "gen_seq2(G!1,x!1,y!1)" )"1" (hide 6)"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil ))nil )"2" (lemma "walks[T].edge_to_walk" )"2" (inst? -1)"2" (assert )"2" (hide-all-but (-1 1))"2" "walks" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case-replace "edge?(G!1)(x!1,x!2)" )"1" (case-replace "edge?(G!1)(y!2,y!1)" )"1" case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!1 AND seq(w)(length(w) - 1) = y!1 and walk?(G!1,w)" )"1" (skosimp*)"1" (hide 7)"1" "walks" )"1" "w!1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 7 8)"2" (install-rewrites "walks" )"2" "walks[T].list2prewalk((:x!1,x!2,y!2,y!1:))" )"1" "walks" )"1" assert )"1" "1" "1" "1" case "n!1=0" )"1" replace -1 -3 lr)"1" expand "nth" )"1" nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 -3 lr)"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "n!1=2" )"1" replace -1 -3 lr)"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" case "n!1=0" )"1" expand "nth" )"1" (assert ) nil nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace -1 2 lr)"1" assert )nil nil ))nil ))nil )"2" case "n!1=2" )"1" replace -1 3 lr)"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" "graphs[T].edges_vert_in" )"2" "graphs[T].edges_vert_in" )"2" "graphs[T].edges_vert_in" )"2" "G!1" "dbl[T](y!2,y!1)" "y!2" "y!1" )"2" "G!1" "dbl[T](x!1,x!2)" "x!1" "x!2" )"2" "G!1" "dbl[T](x!2,y!2)" "x!2" "y!2" )"2" "2" case "i!1=0" )"1" expand "nth" )"1" replace "1" nil nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=3" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "edge?(G!1)(x!2,y!1)" )"1" (hide 8)"1" case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!1 AND seq(w)(length(w) - 1) = y!1 and walk?(G!1,w)" )"1" "1" "w!1" )"1" (bddsimp) nil nil ))nil ))nil )"2" "2" "walks[T].list2prewalk((:x!1,x!2,y!1:))" )"1" "walks" )"1" assert )"1" "1" "1" "1" case "n!1=0" )"1" replace -1 -3 lr)"1" expand "nth" )"1" nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 -3 lr)"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "n!1=0" )"1" expand "nth" )"1" assert )nil nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace -1 2 lr)"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "1" case "n!1=0" )"1" expand "nth" )"1" assert )nil nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace -1 -3 lr)"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "n!1=0" )"1" expand "nth" )"1" assert )nil nil ))nil )"2" case "n!1=1" )"1" replace -1 2 lr)"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "i!1" )"3" "graphs[T].vert_in" )"3" "graphs[T].vert_in" )"3" "graphs[T].vert_in" )"3" "G!1" "x!1" "x!2" )"3" "G!1" "x!2" "y!1" )"3" "3" "3" case "i!1=0" )"1" expand "nth" )"1" replace "1" nil nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "i!1" )"4" "graphs[T].vert_in" )"4" "graphs[T].vert_in" )"4" "graphs[T].vert_in" )"4" "G!1" "x!2" "y!1" )"4" "G!1" "x!1" "x!2" )"4" "4" "4" case "i!1=0" )"1" expand "nth" )"1" replace "1" nil nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 3 8))"2" (lemma "graphs[T].edge?_comm" )"2" "G!1" "y!2" "y!1" )"2" "2" case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!2 AND seq(w)(length(w) - 1) = y!2 and walk?(complement(G!1),w)" )"1" "1" "w!1" )"1" "walks" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "walks[T].list2prewalk((:x!2,y!1,y!2:))" )"1" "walks" )"1" assert )"1" "1" "1" "1" case "n!1=0" )"1" replace "1" expand "nth" )"1" assert )nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil )"3" case "n!1=0" )"1" expand "nth" )"1" replace "1" "x!2" "y!1" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace "1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "nth" )"2" "2" case "n!1=0" )"1" replace -1 1 lr)"1" assert )"1" "x!2" "y!1" )"1" "1" assert )nil nil )"2" assert )nil nil )"3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace "1" assert )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" case "n!1=0" )"1" replace -1 1 lr)"1" expand "nth" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace "1" assert )nil nil ))nil ))nil )"2" "1" assert )nil nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "4" case "n!1=0" )"1" replace -1 1 lr)"1" assert )"1" "x!2" "y!1" )"1" "1" assert )nil nil )"2" "2" replace "2" expand "edge?" )"2" nil nil ))nil ))nil ))nil )"3" "3" replace "3" expand "edge?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace "1" assert )"1" "1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"5" (assert ) nil nil )"6" "6" assert )"6" "1" case "n!1=0" )"1" replace "1" expand "nth" )"1" assert )nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "n!1=0" )"1" replace "1" expand "nth" )"1" nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"3" case "n!1=0" )"1" expand "nth" )"1" assert )"1" "x!2" "y!1" )"1" assert )"1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace "1" assert )"1" replace "1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"7" "7" assert )"7" "1" case "n!1=0" )"1" replace "1" expand "nth" )"1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "n!1=0" )"1" replace "1" expand "nth" )"1" "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"3" case "n!1=0" )"1" replace "1" expand "nth" )"1" "x!2" "y!1" )"1" assert )"1" "1" "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace "1" assert )"1" "y!1" "y!2" )"1" "1" assert )nil nil )"2" assert )"2" "2" expand "edge?" )"2" nil nil ))nil ))nil ))nil )"3" "3" replace "3" expand "edge?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"8" assert )"8" "8" case "n!1=0" )"1" expand "nth" )"1" assert )"1" "1" "1" expand "edge?" )"1" replace "1" nil nil ))nil ))nil ))nil )"2" "x!2" "y!1" )"2" "1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil )"2" "2" "y!1" )"2" nil nil ))nil ))nil )"3" "3" "x!2" )"3" expand "complement" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace "1" assert )"1" "1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil )"2" "y!1" "y!2" )"2" "1" "1" replace "1" expand "edge?" )"1" nil nil ))nil ))nil ))nil )"2" "y!2" )"2" expand "complement" )"2" nil nil ))nil ))nil )"3" "y!1" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"9" (assert ) nil nil )"10" "10" replace -4 * lr)"10" expand "edge?" )"10" assert )nil nil ))nil ))nil ))nil )"11" "11" "i!1" )"11" case "i!1=0" )"1" expand "nth" )"1" replace "1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"12" "12" "i!1" )"12" case "i!1=0" )"1" expand "nth" )"1" replace "1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"13" "13" "i!1" )"13" case "i!1=0" )"1" expand "nth" )"1" replace "1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"14" "14" "i!1" )"14" case "i!1=0" )"1" expand "nth" )"1" replace "1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"15" "15" "i!1" )"15" case "i!1=0" )"1" expand "nth" )"1" replace "1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"16" "16" "i!1" )"16" case "i!1=0" )"1" expand "nth" )"1" replace "1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "edge?(G!1)(y!1,y!2)" )"1" (case "y!1=y!2" )"1" case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!2 AND seq(w)(length(w) - 1) = y!2 and walk?(complement(G!1),w)" )"1" (skosimp*)"1" "w!1" )"1" "walks" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 8 9)"2" "walks[T].list2prewalk((:x!2,x!1,y!2:))" )"1" "walks" )"1" (assert ) nil nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil )"2" (case "edge?(G!1)(x!1,y!2)" )"1" case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!1 AND seq(w)(length(w) - 1) = y!1 and walk?(G!1,w)" )"1" "1" "w!1" )"1" "walks" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "walks[T].list2prewalk((:x!1,y!2,y!1:))" )"1" "walks" )"1" assert )"1" "1" "1" "1" case "n!1=0" )"1" replace -1 -3 lr)"1" expand "nth" )"1" nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 -3 lr)"1" expand "nth" )"1" expand "nth" )"1" replace "1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "n!1=0" )"1" expand "nth" )"1" assert )nil nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace -1 2 lr)"1" assert )"1" "graphs[T].edge?_comm" )"1" "G!1" "y!2" "y!1" )"1" "1" expand "edge?" )"1" nil nil ))nil )"2" expand "edge?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" case "i!1=0" )"1" expand "nth" )"1" replace -1 1 lr)"1" "x!1" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace -1 2 lr)"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" case "i!1=2" )"1" replace -1 3 lr)"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil )"2" case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!2 AND seq(w)(length(w) - 1) = y!2 and walk?(complement(G!1),w)" )"1" "1" "w!1" )"1" "1" "walks" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "walks[T].list2prewalk((:x!2,x!1,y!2:))" )"1" "walks" )"1" assert )"1" "1" "1" "1" case "n!1=0" )"1" replace -1 -3 lr)"1" expand "nth" )"1" replace -4 + lr)"1" "graphs[T].edge?_comm" )"1" "G!1" "y!2" "y!1" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 -3 lr)"1" expand "nth" )"1" expand "nth" )"1" replace "1" "graphs[T].edge?_comm" )"1" "G!1" "x!1" "x!2" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "graphs[T].edge?_comm" )"2" "G!1" "x!1" "x!2" )"2" replace -4 + rl)"2" replace -4 -6 rl)"2" expand "edge?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" case "n!1=0" )"1" expand "nth" )"1" assert )"1" "x!2" "x!1" )"1" assert )"1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace -1 2 lr)"1" assert )"1" "x!1" "y!2" )"1" assert )"1" replace "1" "graphs[T].edge?_comm" )"1" "G!1" "x!1" "x!2" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "1" case "n!1=0" )"1" replace -1 -3 lr)"1" expand "nth" )"1" replace -3 * lr)"1" nil nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 -3 lr)"1" expand "nth" )"1" expand "nth" )"1" replace "1" "graphs[T].edge?_comm" )"1" "G!1" "y!2" "x!2" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "n!1=0" )"1" expand "nth" )"1" assert )"1" "graphs[T].edge?_comm" )"1" "G!1" "x!1" "x!2" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace -1 -3 lr)"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" expand "nth" )"2" assert )nil nil ))nil ))nil ))nil )"3" case "n!1=0" )"1" expand "nth" )"1" assert )"1" "x!2" "x!1" )"1" assert )"1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" expand "nth" )"1" replace -1 2 lr)"1" assert )"1" "x!1" "y!2" )"1" assert )"1" "1" replace "1" "graphs[T].edge?_comm" )"1" "G!1" "y!2" "x!2" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "y!2" )"2" expand "complement" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" case "i!1=0" )"1" expand "nth" )"1" replace -1 1 lr)"1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace -1 2 lr)"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace -1 3 lr)"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "i!1" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" case "i!1=0" )"1" expand "nth" )"1" replace -1 1 lr)"1" "x!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace -1 2 lr)"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace -1 3 lr)"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!2 AND seq(w)(length(w) - 1) = y!2 and walk?(complement(G!1),w)" )"1" (skosimp*)"1" (inst 9 "w!1" )"1" "walks" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 10)"2" (hide 9)"2" case "y!1=y!2" )"1" "walks[T].list2prewalk((:x!2,x!1,y!2:))" )"1" "walks" )"1" assert )"1" "1" assert )"1" "1" assert )"1" "1" "1" "1" case "n!1=0" )"1" replace "1" expand "nth" )"1" assert )nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" case "n!1=0" )"1" replace "1" expand "nth" )"1" "1" "1" "graphs[T].edge?_comm" )"1" "G!1" "x!1" "x!2" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"3" assert )"3" case "n!1=0" )"1" replace "1" expand "nth" )"1" "x!2" "x!1" )"1" "x!1" )"1" "x!2" )"1" expand "complement" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" "x!1" "y!2" )"1" "x!1" )"1" "y!2" )"1" expand "complement" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "x!2" )"2" "x!1" )"2" "y!2" )"2" expand "complement" )"2" "2" "i!1" )"2" case "i!1=0" )"1" replace "1" expand "nth" )"1" nil nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace "1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" "walks[T].list2prewalk((:x!2,x!1,y!1,y!2:))" )"1" "walks" )"1" assert )"1" "1" "1" case "n!1=0" )"1" expand "nth" )"1" assert )"1" "1" "graphs[T].edge?_comm" )"1" "G!1" "x!1" "x!2" )"1" expand "edge?" )"1" nil nil ))nil ))nil ))nil )"2" "x!2" "x!1" )"2" "x!2" )"2" "x!1" )"2" expand "complement" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 3 lr)"1" expand "nth" )"1" expand "nth" )"1" "1" "x!1" "y!1" )"1" "x!1" )"1" "y!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=2" )"1" replace -1 4 lr)"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" "y!1" "y!2" )"1" assert )"1" "y!2" )"1" expand "complement" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "x!2" )"2" "x!1" )"2" "y!1" )"2" "y!2" )"2" expand "complement" )"2" "2" case "i!1=0" )"1" assert )nil nil )"2" case "i!1=1" )"1" assert )nil nil )"2" case "i!1=2" )"1" assert )nil nil )"2" case "i!1=3" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 5)"2" (inst 5 "gen_seq2(G!1,x!2,y!2)" )"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil )"2" (lemma "walks[T].edge_to_walk" )"2" (inst -1 "complement(G!1)" "x!2" "y!2" )"2" (assert )"2" (bddsimp)"1" (expand "complement" -1 2)"1" expand "gen_seq2" )"1" (propax) nil nil ))nil ))nil )"2" (hide 2)"2" "1" "y!2" )"1" expand "complement" )"1" (propax) nil nil ))nil ))nil )"2" "x!2" )"2" expand "complement" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "y!2" )"3" (expand "complement" )"3" (propax) nil nil )) nil ))nil )"4" (typepred "x!2" )"4" (expand "complement" )"4" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" graph_conn_defs nil )nil graphs nil )"prewalk" walks nil )nil graphs nil )nil walks nil )"Seq(G)" walks nil )"doubleton[T]" graphs nil )nil walks nil )"prewalk" walks nil )nil walks nil )"bool" graphs nil )"Seq(G)" walks nil )nil walks nil )"bool" walks nil )"bool" walks nil )nil walks nil )nil walks nil )nil walks nil )"set[T]" doubletons nil )nil doubletons nil )nil graphs nil )nil graphs nil )"bool" graphs nil ))nil 3358001425"" (skosimp*)"" (expand "path_connected?" )"" (bddsimp)"1" (expand "empty?" )"1" (expand "empty?" )"1" (hide 2) (("1" (grind) nil nil )) nil )) nil ))nil )"2" (skosimp*)"2" case "NOT edge?(G!1)(x!1,x!2) OR NOT edge?(G!1)(x!2,y!1)" )"1" (bddsimp)"1" case "NOT edge?(G!1)(x!1,y!2) OR NOT edge?(G!1)(y!2,y!1)" )"1" (bddsimp)"1" (hide 4)"1" "add1(gen_seq2(complement(G!1),x!2,y!1),y!2)" )"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil )"2" (lemma "walks[T].walk?_add1" )"2" "complement(G!1)" "gen_seq2[T](complement(G!1), x!2, y!1)" "y!2" )"2" (lemma "walks[T].edge_to_walk" )"2" "complement(G!1)" "x!2" "y!1" )"2" "1" "1" "walks" )"1" assert )"1" "1" "1" assert )"1" "0" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "0" )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" (postpone) nil nil )"4" (postpone) nil nil )"5" (postpone) nil nil )"6" (postpone) nil nil )"7" (postpone) nil nil )"8" (postpone) nil nil )"9" (postpone) nil nil )"10" (postpone) nil nil )"11" (postpone) nil nil )"12" (postpone) nil nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil )"3" (postpone) nil nil )"4" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil )"2" (postpone) nil nil ))nil )"2" (postpone) nil nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil )nil shostak))"not-final" 3361205662"" (skosimp*)"" (case "edge?(G!1)(x!1,y!1)" )"1" (inst 2 "gen_seq2(G!1,x!1,y!1)" )"1" (hide 4)"1" (lemma "walks[T].edge_to_walk" )"1" (inst -1 "G!1" "x!1" "y!1" )"1" (bddsimp)"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil )"2" (install-rewrites "walks" )"2" (assert ) nil nil )) nil )"3" (expand "edge?" )"3" (assert )"3" (expand "edg" ) (("3" (propax) nil nil )) nil ))nil ))nil )"4" (expand "edge?" )"4" (expand "edg" ) (("4" (assert ) nil nil )) nil ))nil )"5" (assert ) nil nil ) ("6" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (case "NOT edge?(G!1)(x!2,y!2)" )"1" (inst 6 "gen_seq2(complement(G!1),x!2,y!2)" )"1" (bddsimp)"1" (hide (2 3 4))"1" (install-rewrites "walks" ) (("1" (assert ) nil nil ))nil ))nil )"2" (hide 2 4)"2" (lemma "walks[T].edge_to_walk" )"2" (inst -1 "complement(G!1)" "x!2" "y!2" )"2" (install-rewrites "walks" )"2" (bddsimp)"1" (expand "walk_from?" )"1" (bddsimp)"1" (hide -1 1) (("1" (assert ) nil nil ))nil )"2" (hide -1 1) (("2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 5)"2" (assert )"2" (bddsimp)"2" (inst 1 "x!2" "y!2" )"2" "x!2" )"2" "y!2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "y!2" )"2" (hide-all-but (-1 1))"2" (assert )"2" (expand "complement" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (-1 1))"3" (typepred "x!2" )"3" (expand "complement" ) (("3" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (case "x!1=x!2" )"1" (case "y!1=y!2" )"1" (hide 3 5) (("1" (grind) nil nil )) nil )"2" (case "edge?(G!1)(y!1,y!2)" )"1" (lemma "graphs[T].edge?_comm" )"1" (inst -1 "G!1" "y!2" "y!1" )"1" (prop)"1" (replace -3 -4 rl)"1" (hide 6)"1" "walks[T].list2prewalk((:x!1,y!2,y!1:))" )"1" (install-rewrites "walks" )"1" (assert )"1" "1" "1" "1" "n!1" )"1" case "n!1=0" )"1" replace -1 -8 lr)"1" expand "nth" )"1" (propax) nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 -8 lr)"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" "n!1" )"2" case "n!1=0" )"1" replace -1 6 lr)"1" expand "nth" )"1" (propax) nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 7 lr)"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" )"2" "y!2" )"2" "y!1" )"2" "2" "2" case "i!1=0" )"1" replace -1 5 lr)"1" expand "nth" )"1" nil nil ))nil ))nil )"2" case "i!1=1" )"1" replace -1 6 lr)"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" case "i!1=2" )"1" replace -1 7 lr)"1" expand "nth" )"1" expand "nth" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 -4 3))"2" (install-rewrites "walks" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 3 lr)"2" (hide 5)"2" "walks[T].list2prewalk((:x!2,y!1,y!2:))" )"1" (bddsimp)"1" (install-rewrites "walks" )"1" (assert ) nil nil )) nil )"2" (expand "walk_from?" )"2" (bddsimp)"1" (expand "complement" )"1" (expand "walk?" )"1" "1" "1" case "n!1=0" )"1" replace -1 -6 lr)"1" expand "nth" )"1" (propax) nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 -6 lr)"1" expand "nth" )"1" expand "nth" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" case "n!1=0" )"1" replace -1 -6 lr)"1" expand "nth" )"1" (propax) nil nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 -6 lr)"1" expand "nth" )"1" expand "nth" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"3" "3" case "n!1=0" )"1" replace -1 1 lr)"1" expand "nth" )"1" "x!2" "y!1" )"1" "x!2" )"1" "y!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "n!1=1" )"1" replace -1 2 lr)"1" expand "nth" )"1" expand "nth" )"1" "y!1" "y!2" )"1"
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.1.170Bemerkung:
(vorverarbeitet am 2026-05-06)
¤ *Bot Zugriff
2026-05-26
