Quelle tree_paths.prf
Sprache: Lisp
(tree_pathsnil 3253637114 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3253637114 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3253637114 ("" (subtype-tcc) nil nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil ))nil ))nil 3253637114 ("" (subtype-tcc) nil nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil ))nil ))nil 3253637114"" (skolem-typepred) (("" (inst + "(r!1,s!1)" ) nil nil )) nil )"bool" tree_paths nil )nil paths nil )"bool" paths nil )nil walks nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil graphs nil )"bool" sets nil )nil graphs nil )nil graphs nil )nil finite_sets nil )"[bool, bool -> bool]" booleans 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 tree_paths nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3253637114"" (skolem-typepred)"" "min[[Path(G!1), Path(G!1)], LAMBDA (r: Path(G!1), s: Path(G!1)): length(r) + length(s),LAMBDA (r: Path(G!1), s: Path(G!1)):") "1" (assert )"1" (expand "minimal?" ) (("1" (propax) nil nil )) nil )) nil )"2" (hide 2) (("2" (inst + "(r!1,s!1)" ) nil nil )) nil ))nil ))nil )min const-decl "{S: T | minimal?(S)}" abstract_min nil )"bool" abstract_min nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil )"bool" tree_paths nil )nil paths nil )"bool" paths nil )nil walks nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil graphs nil )"bool" sets nil )nil graphs nil )nil graphs nil )nil finite_sets nil )"[bool, bool -> bool]" booleans 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 tree_paths nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3253637114"" (skolem-typepred)"" (flatten)"" (assert )"" (typepred "min_dual_paths(G!1, r!1, s!1)" )"" (assert )"" (expand "is_min_dual?" )"" (skosimp*)"" (expand "min_dual_paths" )"" "min[[Path(G!1), Path(G!1)], LAMBDA (r: Path(G!1), s_2847: Path(G!1)):LAMBDA (r: Path(G!1), s_2848: Path(G!1)):") "1" "min[[Path(G!1), Path(G!1)], LAMBDA (r: Path(G!1), s_2847: Path(G!1)):LAMBDA (r: Path(G!1), s_2848: Path(G!1)):") "1" (expand "minimal?" )"1" (assert )"1" (inst - "(r!2,s!2)" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide-all-but (-8 1))"2" (inst + "(r!1,s!1)" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Dual_paths(G)" tree_paths nil )nil tree_paths nil )"bool" tree_paths nil )"bool" tree_paths nil )"(total_order?[real])" nil )min const-decl "{S: T | minimal?(S)}" abstract_min nil )"bool" abstract_min nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil )nil paths nil )"bool" paths nil )nil walks nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil graphs nil )"bool" sets nil )nil graphs nil )nil graphs nil )nil finite_sets nil )"[bool, bool -> bool]" booleans 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 tree_paths nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3312299029"" (skosimp*)"" "proj_1(min_dual_paths(G!1,r!1,s!1))" "proj_2(min_dual_paths(G!1,r!1,s!1))" )"" (lemma "min_dual_def" )"" (inst -1 "G!1" "r!1" "s!1" ) (("" (bddsimp) nil nil )) nil ))nil ))nil ))nil )"Path[T](G!1)" tree_paths nil )"Path[T](G!1)" tree_paths nil )"Graph[T]" tree_paths nil )nil graphs nil )"bool" sets nil )"bool" tree_paths nil )nil paths nil )"bool" paths nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil tree_paths nil )nil tree_paths nil )"Dual_paths(G)" tree_paths nil )nil tree_paths nil ))nil ))nil 3312299267"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3312299267 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil tree_paths 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" sets nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )"bool" paths nil )nil paths nil )"bool" sets nil )"bool" sets nil )"bool" walks nil )"bool" graphs nil )"bool" walks nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )"(total_order?[real])" nil )"int" integers nil )nil application-judgement "finite_set[T]" tree_paths nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" tree_paths nil )"posint" nil ))nil ))nil 3312299267 ("" (subtype-tcc) 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 )"bool" sets nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )nil paths nil )"bool" sets nil )"bool" sets nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil tree_paths nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" tree_paths nil )"posint" nil )nil application-judgement "finite_set[T]" tree_paths nil ))nil ))nil 3312299267 ("" (subtype-tcc) 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 )"bool" sets nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )nil paths nil )"bool" sets nil )"bool" sets nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil tree_paths nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" tree_paths nil )"posint" nil )nil application-judgement "finite_set[T]" tree_paths nil ))nil ))nil 3312299267 ("" (subtype-tcc) nil nil )nil tree_paths nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" tree_paths nil )nil application-judgement "finite_set[T]" tree_paths nil )"posint" nil ))nil ))nil 3312299267 ("" (subtype-tcc) 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 )"bool" sets nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )nil paths nil )"bool" sets nil )"bool" sets nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil tree_paths nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" tree_paths nil )"posint" nil )nil application-judgement "finite_set[T]" tree_paths nil ))nil ))nil 3312299267 ("" (subtype-tcc) nil nil )nil tree_paths nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" tree_paths nil )nil application-judgement "finite_set[T]" tree_paths nil )"posint" nil ))nil ))nil 3312299267 ("" (subtype-tcc) 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 )"bool" sets nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )nil paths nil )"bool" sets nil )"bool" sets nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil tree_paths nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" tree_paths nil )"posint" nil )nil application-judgement "finite_set[T]" tree_paths nil ))nil ))nil 3312299311"" (skosimp*)"" (case "length(p!1)>1" )"1" (case "length(q!1)>1" )"1" (bddsimp)"1" (typepred "q!1" )"1" (lemma "path?_caret" )"1" (inst? -1)"1" (bddsimp (-1 -3 -4))"1" (propax) nil ) ("2" (assert ) nil )"3" (assert ) nil )))))))))"2" (lemma "path?_caret" )"2" (inst? -1)"2" (typepred "p!1" )"2" (bddsimp (-2 -3 -5))"1" (propax) nil ) ("2" (assert ) nil )"3" (assert ) nil )))))))))"3" (typepred "q!1" )"3" (lemma "path?_caret" )"3" (inst? -1)"1" (bddsimp (-1 -3 -4))"1" (propax) nil ) ("2" (assert ) nil )"3" (assert ) nil )))"2" (assert ) nil )))))))"4" (typepred "p!1" )"4" (lemma "path?_caret" )"4" (inst? -1)"1" (bddsimp (-1 -3 -5))"1" (propax) nil ) ("2" (assert ) nil )"3" (assert ) nil )))"2" (assert ) nil )))))))))"2" (hide 2)"2" (expand "dual_paths?" )"2" (bddsimp)"2" (flatten)"2" (case "length(q!1)=1" )"1" (replace -1 * lr)"1" (assert )"1" (replace -4 -3 rl)"1" (typepred "p!1" )"1" (expand "path?" )"1" (flatten)"1" "0" "length(p!1)-1" )"1" (assert ) nil )))))))))))))))"2" (assert ) nil )))))))))))))"2" (hide 2)"2" (case "length(p!1)=1" )"1" (expand "dual_paths?" )"1" (flatten)"1" (replace -1 * lr)"1" (assert )"1" (replace -3 -2 lr)"1" (typepred "q!1" )"1" (expand "path?" )"1" (flatten)"1" (inst -3 "0" "length(q!1)-1" )"1" (assert )"1" "1" case "length(q!1)=1" )"1" "1" "1" (grind) nil )))))"2" assert )nil )))))))))))))))))))))))))"2" (assert ) nil ))))))))nil )nil paths nil )nil graphs nil )"bool" sets nil )"bool" paths nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil walks nil )nil finite_sequences nil )nil tree_paths nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"even_int" integersnil )nil naturalnumbers nil )"bool" reals nil )"bool" tree_paths nil )nil paths nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"int" integers nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"Graph[T]" tree_paths nil )"Path[T](G!1)" tree_paths nil )"Path[T](G!1)" tree_paths nil )nil application-judgement "finite_set[T]" tree_paths nil )"bool" walks nil )"bool" graphs nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" walks nil ))nil )nil 3312299283"" (skosimp*)"" (lemma " dual_path_trunc" )"" (inst -1 "G!1" "p!1" "q!1" )"" (bddsimp)"" (delete -4 -5 -6 -7)"" (expand "dual_paths?" )"" (flatten)"" (expand "finseq_appl" )"" (lemma "plus_up" )"" (inst? -1)"" "seq(p!1)(0)" "seq(p!1)(length(p!1)-1)" )"" (assert )"" (bddsimp)"1" (install-rewrites "walks[T]" )"1" assert )"1" case "length(p!1)=2" )"1" replace -1 * lr)"1" assert )"1" case "length(q!1)=2" )"1" replace -1 * lr)"1" assert )"1" "1" "1" "1" replace -1 * lr)"1" replace -2 * lr)"1" assert )nil )))))))))))))))"2" (assert ) nil )))))))"2" (assert ) nil )))))))"2" (install-rewrites "walks[T]" )"2" (assert ) nil )))"3" (install-rewrites "walks[T]" )"3" (assert ) nil )))"4" (assert )"4" "path_one" )"4" "G!1" "p!1" "seq(p!1)(0)" "seq(p!1)(length(p!1)-1)" )"4" assert )"4" expand "path_from?" )"4" expand "from?" )"4" nil ))))))))))))))))))))))))))))))))))))))nil )nil nil ))nil 3312300679"" (auto-rewrite "finseq_appl" )"" (skosimp*)"" (lemma " dual_path_trunc" )"" (inst -1 "G!1" "p!1" "q!1" )"" (prop)"" (hide -3 -4 -5 -6)"" (case "length(p!1)=2 AND length(q!1)=2" )"1" (hide -2 -3 1 2)"1" (flatten)"1" (expand "dual_paths?" )"1" (flatten)"1" (lemma "plus_up" )"1" (assert )"1" "p!1" "q!1" "seq(p!1)(0)" "seq(p!1)(length(p!1)-1)" )"1" assert )"1" "1" expand "trunc1" )"1" "1" expand * "^" "min" )"1" (assert ) nil nil ))nil )"2" "2" "x!1" )"2" expand * "^" "min" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "path_one" )"2" "G!1" "q!1" "seq(q!1)(0)" "seq(q!1)(length(q!1)-1)" )"2" assert )"2" expand *"path_from?" "from?" )"2" expand "circuit?" )"2" "2" expand "cyclically_reduced?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "from?" )"3" (propax) nil nil ))nil )"4" expand "from?" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil tree_paths nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"bool" sets nil )nil graphs nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"bool" paths nil )nil paths nil )"(strict_total_order?[real])" real_props nil )"bool" tree_paths nil )nil path_circ nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"finseq" finite_sequences nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"posint" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"prewalk" walks nil )"bool" walks nil )"bool" paths nil )"bool" circuits nil )"bool" circuits nil )nil path_circ nil )"[below[length(fs)] -> T]" finite_sequencesnil )"int" integers nil )nil tree_paths nil ))nil )nil 3312299342"" (skosimp*)"" (lemma " dual_path_trunc" )"" (inst -1 "G!1" "p!1" "q!1" )"" (bddsimp)"" (delete -4 -5 -6 -7)"" (expand "dual_paths?" )"" (flatten)"" (lemma "plus_up" )"" (inst? -1)"" "seq(p!1)(0)" "seq(p!1)(length(p!1)-1)" )"" (assert )"" (bddsimp)"1" (install-rewrites "walks[T]" )"1" (assert )"1" case "length(p!1)=2" )"1" replace -1 * lr)"1" assert )"1" case "length(q!1)=2" )"1" replace -1 * lr)"1" assert )"1" "1" "1" "1" replace -1 * lr)"1" replace -2 * lr)"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (install-rewrites "walks[T]" )"2" (assert ) nil nil )) nil )"3" (install-rewrites "walks[T]" )"3" (assert ) nil nil )) nil )"4" (flatten)"4" (assert )"4" "path_one" )"4" "G!1" "p!1" "seq(p!1)(0)" "seq(p!1)(length(p!1)-1)" )"4" assert )"4" expand "path_from?" )"4" expand "from?" )"4" assert )"4" (grind) 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 )nil graphs nil )nil walks nil )"bool" paths nil )nil paths nil )nil path_circ nil )"bool" walks nil )"bool" graphs nil )"bool" walks nil )"bool" circuits nil )"bool" circuits nil )"bool" circuits nil )"bool" walks nil )"bool" circuits nil )"bool" paths nil )"bool" walks nil )"prewalk" walks nil )nil path_circ nil ))nil ))nil 3312300142"" (skosimp*)"" (expand "is_min_dual?" )"" (flatten)"" (lemma "dual_path_trunc" )"" (inst? -1)"" (bddsimp (-1 -2)) (("" (assert ) nil ))))))))))))nil )"bool" tree_paths nil )nil tree_paths nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil paths nil )"bool" paths nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )"bool" sets 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 tree_paths nil ))nil )nil 3312299267 ("" (subtype-tcc) nil nil ) nil nil ))nil 3312300240"" (skosimp*)"" (expand "is_min_dual?" )"" (flatten)"" (lemma "dual_path_trunc" )"" (inst? -1)"" (bddsimp (-1 -2)) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"bool" tree_paths nil )nil tree_paths nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil paths nil )"bool" paths nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )"bool" sets 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 tree_paths nil ))nil )nil 3312300182"" (skolem-typepred)"" "min[[Path(G!1), Path(G!1)], LAMBDA (r: Path(G!1), s: Path(G!1)): length(r) + length(s),LAMBDA (r: Path(G!1), s: Path(G!1)):") "1" (assert ) (("1" (expand "minimal?" ) (("1" (propax) nil )))))"2" (hide 2) (("2" (inst + "(r!1,s!1)" ) nil ))))))nil )nil nil )nil 3312299267 ("" (subtype-tcc) nil nil ) nil nil ))nil 3312300261"" (skosimp*)"" (expand "finseq_appl" )"" (expand "is_min_dual?" )"" (flatten)"" (lemma "dual_path_trunc" )"" (inst? -1)"" (bddsimp (-1 -2)) (("" (assert ) nil ))))))))))))))nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil tree_paths nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"bool" sets nil )nil graphs nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"bool" paths nil )nil paths nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil tree_paths nil )"bool" tree_paths nil ))nil )nil 3312299267 ("" (subtype-tcc) nil nil ) nil nil ))nil 3312300280"" (skosimp*)"" (expand "is_min_dual?" )"" (flatten)"" (lemma "dual_path_trunc" )"" (inst? -1)"" (bddsimp (-1 -2)) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"bool" tree_paths nil )nil tree_paths nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )nil paths nil )"bool" paths nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )"bool" sets 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 tree_paths nil ))nil )nil 3312299267 ("" (subtype-tcc) nil nil ) nil nil ))nil 3312299362"" (skosimp*)"" (expand "finseq_appl" )"" (lemma "dual_path_trunc" )"" (inst? -1)"" (inst -1 "q!1" )"" (expand "is_min_dual?" )"" (flatten)"" (bddsimp (-1 -2))"" "p!1^(0,length(p!1)-2)" "q!1^(0,length(q!1)-2)" )"1" (bddsimp)"1" (hide -1 -4 -5 -6 -7)"1" (install-rewrites "walks[T]" )"1" (assert ) nil nil )) nil ))nil )"2" (hide -1 -4 -5 -6 -7)"2" (install-rewrites "walks[T]" )"2" (assert ) nil nil )) nil ))nil )"3" (expand "dual_paths?" )"3" (expand "finseq_appl" )"3" (flatten)"3" (bddsimp)"1" expand "^" 2)"1" assert )"1" expand "min" )"1" (propax) nil nil ))nil ))nil ))nil )"2" expand "^" 2)"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil )"3" "3" "3" "walks[T]" )"3" "3" "3" "3" case "(LAMBDA (x: below[min(length(p!1) - 1, p!1`length)]): p!1`seq(x))(x!1) = LAMBDA (x: below[min (length(q!1) - 1, q!1`length)]): q!1`seq(x))(x!1)") "1" "1" "1" nil nil ))nil ))nil )"2" replace -6 1 lr)"2" (propax) nil nil ))nil )"3" "x!1" )"3" replace -6 -1 lr)"3" case "x!1=length(q!1)-1" )"1" replace -1 2 lr)"1" replace "1" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"4" "x!1" )"4" case "x!1=length(p!1)-1" )"1" replace -1 2 lr)"1" replace -7 -4 rl)"1" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (expand "dual_paths?" )"4" (expand "finseq_appl" )"4" (flatten)"4" (bddsimp)"1" expand "^" 2)"1" assert )"1" expand "min" )"1" "1" "p!1^(1,length(p!1)-1)" "q!1^(1,length(q!1)-1)" )"1" "1" "1" "walks[T]" )"1" (assert ) nil nil ))nil ))nil )"2" expand "dual_paths?" )"2" expand "finseq_appl" )"2" "1" expand "^" 1)"1" expand "min" )"1" nil nil ))nil ))nil )"2" expand "^" 1)"2" nil nil ))nil )"3" "3" "3" "walks[T]" )"3" assert )"3" "3" "3" "3" case "(LAMBDA (x: below[min(length(p!1) - 1, p!1`length - 1)]): p!1`seq(1 + x))(x!1-1) = LAMBDA (x: below[min (length(q!1) - 1, q!1`length - 1)]): q!1`seq(1 + x))(x!1-1)") "1" "1" assert )nil nil ))nil )"2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "^" 2)"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil )"3" expand "^" 2)"3" assert )"3" "3" expand "min" )"3" "walks[T]" )"3" "3" "3" "3" case "(LAMBDA (x: below[min(length(p!1) - 1, p!1`length)]): p!1`seq(x))(x!1) = LAMBDA (x: below[min (length(q!1) - 1, q!1`length)]): q!1`seq(x))(x!1)") "1" "1" "1" nil nil ))nil ))nil )"2" replace -6 1 lr)"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (bddsimp)"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[below[length(fs)] -> T]" finite_sequencesnil )"int" integers nil )nil tree_paths nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"bool" sets nil )nil graphs nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"bool" paths nil )nil paths nil )"bool" tree_paths nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )"posint" nil )"{k: int | k <= i AND k <= j}" nil )"int" integers nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil ) (< const-decl "bool" reals nil )"bool" tree_paths nil )"[numfield, numfield -> numfield]" number_fields nil )"Path[T](G!1)" tree_paths nil )"Graph[T]" tree_paths nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )"finseq" finite_sequences nil )"Path[T](G!1)" tree_paths nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )nil tree_paths nil ))nil ))nil 3312299267 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil tree_paths 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" sets nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )"bool" paths nil )nil paths nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set[T]" tree_paths nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" walks nil )"bool" graphs nil )"bool" walks nil )"bool" sets nil )"bool" sets nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" tree_paths nil )"bool" tree_paths nil ))nil ))nil 3312299267 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil tree_paths 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" sets nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )"bool" paths nil )nil paths nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set[T]" tree_paths nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" walks nil )"bool" graphs nil )"bool" walks nil )"bool" sets nil )"bool" sets nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" tree_paths nil )"bool" tree_paths nil ))nil ))nil 3312299391"" (skosimp*)"" (lemma "min_dual_reduc" )"" (expand "finseq_appl" )"" (inst? -1)"" (bddsimp (-1 -2))"" (expand "is_min_dual?" )"" (flatten)"" (lemma "dual_path_trunc" )"" (inst? -1)"" (bddsimp (-1 -2))"" (delete -4 -5 -6 -7)"" (hide -2 -3)"" (inst -2 "p!1^(0,i!1)" "q!1^(0,j!1)" )"1" (expand "dual_paths?" )"1" expand "finseq_appl" )"1" "1" "1" expand * "^" "min" )"1" (assert ) nil nil ))nil )"2" expand * "^" "min" )"2" (assert ) nil nil ))nil )"3" expand * "^" "min" )"3" (assert ) nil nil ))nil )"4" expand * "^" "min" )"4" (assert ) nil nil ))nil )"5" (expand * "^" "min" ) nil nil )"6" (expand * "^" "min" ) nil nil )"7" expand * "^" "min" )"7" "7" case " (LAMBDA (x: below[min(1 + i!1, p!1`length)]): p!1`seq(x))(1) = (LAMBDA (x: below[min(1 + j!1, q!1`length)]): q!1`seq(x))(1)" )"1" "1" (propax) nil nil ))nil )"2" replace -4 1 lr)"2" (propax) nil nil ))nil )"3" "3" (assert ) nil nil ))nil )"4" expand "min" )"4" (assert ) nil nil ))nil )"5" "5" (assert ) nil nil ))nil )"6" expand "min" )"6" (assert ) nil nil ))nil ))nil ))nil ))nil )"8" expand * "^" "min" )"8" "8" assert )"8" case " (LAMBDA (x: below[min(1 + i!1, p!1`length)]): p!1`seq(x))(1) = (LAMBDA (x: below[min(1 + j!1, q!1`length)]): q!1`seq(x))(1)" )"1" "1" (propax) nil nil ))nil )"2" replace -4 1 lr)"2" (propax) nil nil ))nil )"3" "3" (assert ) nil nil ))nil )"4" expand "min" )"4" (assert ) nil nil ))nil )"5" "5" (assert ) nil nil ))nil )"6" expand "min" )"6" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" "path?_caret" )"2" "G!1" "0" "j!1" "q!1" )"2" "j!1" )"2" expand "dual_paths?" )"2" expand "finseq_appl" )"2" "q!1" )"2" assert (-3 -4 -7))"2" "1" expand "^" 1)"1" expand "min" )"1" assert )nil nil ))nil ))nil )"2" expand "^" 1)"2" expand "min" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (bddsimp)"1" "path?_caret" )"1" "G!1" "0" "i!1" "p!1" )"1" "p!1" )"1" assert (-2 -3 -4))"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "path?_caret" )"2" "G!1" "0" "i!1" "p!1" )"2" "i!1" )"2" "p!1" )"2" assert (-2 -3 -4))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand * "^" min )"3" (assert ) nil nil ))nil )"4" expand * "^" min )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil tree_paths nil )nil tree_paths nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"bool" sets nil )nil graphs nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"bool" paths nil )nil paths nil )"bool" tree_paths nil )nil tree_paths nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )nil paths nil )"bool" tree_paths nil )"{k: nat | k <= i AND k <= j}" nil )"bool" reals nil ) (<= const-decl "bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"posint" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nonneg_int" nil )"Path[T](G!1)" tree_paths nil )"nat" tree_paths nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )"finseq" finite_sequences nil )"Graph[T]" tree_paths nil )"Path[T](G!1)" tree_paths nil )"nat" tree_paths nil )"(strict_total_order?[real])" real_props nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil ))nil 3312301088 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil tree_paths 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" sets nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )"bool" paths nil )nil paths nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set[T]" tree_paths nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" walks nil )"bool" graphs nil )"bool" walks nil )"bool" sets nil )"bool" sets nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" tree_paths nil ))nil ))nil 3312301088 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil tree_paths 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" sets nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )"bool" paths nil )nil paths nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set[T]" tree_paths nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" walks nil )"bool" graphs nil )"bool" walks nil )"bool" sets nil )"bool" sets nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" tree_paths nil ))nil ))nil 3312305764"" (skosimp*)"" (lemma "dual_path_trunc" )"" (inst? -1)"" (bddsimp (-1 -2))"1" (assert ) nil nil ) ("2" (propax) nil nil )) nil ))nil ))nil ))nil )nil tree_paths nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )nil paths nil )"bool" paths nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )"bool" sets 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 tree_paths nil ))nil )nil 3312301088 ("" (subtype-tcc) nil nil ) nil nil ))nil 3312305798"" (skosimp*)"" (hide -2)"" (lemma "dual_path_trunc" )"" (inst? -1)"" (bddsimp (-1 -2))"" (delete -4 -5 -6 -7)"" (lemma "walk_concat" )"" "G!1" "p!1`seq(0)" "q!1`seq(0)" "p!1`seq(length(p!1)-1)" "p!1" "q!1" )"" (expand "walk_from?" )"" (expand "dual_paths?" )"" (expand "finseq_appl" )"" (flatten)"" (typepred "p!1" )"" (typepred "q!1" )"" "" expand "path?" )"" "" "" "1" expand "trunc1" )"1" "1" expand "walk?" -6)"1" expand "finseq_appl" )"1" assert )nil nil ))nil ))nil )"2" expand "rev" 2)"2" expand "^" 2)"2" assert )"2" "2" nil 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 ))nil ))nil ))nil )nil tree_paths nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"bool" sets nil )nil graphs nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"bool" paths nil )nil paths nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" tree_paths nil )"prewalk" walks nil )"finseq[T]" doubletons nil )"{k: int | k <= i AND k <= j}" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"int" integers nil )"nonneg_int" nil )"finseq" finite_sequences nil )"posint" nil )"bool" walks nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" walks nil )nil walks nil )nil tree_paths nil ))nil )nil 3312301088 ("" (subtype-tcc) nil nil ) nil nil ))nil 3312301113"" (skosimp*)"" (lemma "dual_path_length" )"" (inst? -1)"" (bddsimp (-1 -2))"1" (hide -2)"1" (expand "cycle?" )"1" (expand "finseq_appl" )"1" (bddsimp)"1" (skosimp*)"1" (typepred "i!1" )"1" (typepred "j!1" )"1" (case "i!1<length(p!1)-1" )"1" (case "j!1<length(p!1)-1" )"1" (hide -6)"1" expand "dual_paths?" )"1" expand "finseq_appl" )"1" "1" "p!1" )"1" "q!1" )"1" expand "trunc1" )"1" expand "endpoint?" )"1" expand "o " )"1" expand *"^" min "1" expand "rev" )"1" "walks[T]" )"1" assert )"1" "1" "1" "i!1" "j!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "p!1" )"2" "q!1" )"2" expand "trunc1" )"2" expand "endpoint?" )"2" expand "o " )"2" expand *"^" min "2" expand "rev" )"2" "walks[T]" )"2" assert )"2" "2" "2" "i!1" "j!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" "length(q!1)+length(p!1)-j!1-2" )"1" assert )"1" expand "endpoint?" )"1" expand "o" 3)"1" expand "rev" 3)"1" expand "trunc1" 3)"1" expand "^" 3)"1" expand "min" 3)"1" expand "trunc1" -6)"1" expand "o" -6)"1" expand "rev" -6)"1" expand "^" -6)"1" expand "min" -6)"1" "1" assert )nil nil )"2" assert )"2" case "j!1=length(p!1)-1" )"1" replace "1" assert )"1" expand "dual_paths?" )"1" "1" expand "finseq_appl" )"1" replace "1" "p!1" )"1" expand "path?" )"1" "1" expand "finseq_appl" )"1" "length(p!1)-1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))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 )"2" assert )"2" "2" "walks[T]" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (case "j!1<length(p!1)-1" )"1" "j!1" "length(q!1)+length(p!1)-i!1-2" )"1" expand "endpoint?" )"1" "1" expand "o" )"1" expand "rev" )"1" expand "trunc1" )"1" expand * "^" min empty_seq)"1" "walks[T]" )"1" assert )"1" "1" (assert ) nil nil )"2" (assert ) nil nil )"3" assert )"3" case "i!1=length(p!1)-1" )"1" replace -1 * lr)"1" assert )"1" "1" expand "dual_paths?" )"1" "1" expand "finseq_appl" )"1" replace "1" "p!1" )"1" expand "path?" )"1" "1" expand "finseq_appl" )"1" "length(p!1)-1" "j!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "walks[T]" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide -4)"2" "q!1" )"2" expand "path?" )"2" expand "finseq_appl" )"2" "2" "2" "length(q!1)+length(p!1)-i!1-2" "length(q!1)+length(p!1)-j!1-2" )"1" expand "endpoint?" )"1" expand "o" )"1" expand "rev" )"1" expand "trunc1" )"1" expand *"^" min "1" "walks[T]" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "walks[T]" )"2" assert )"2" expand *"^" min "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "walks[T]" )"3" assert )"3" expand *"^" min "3" "3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "dual_paths?" )"2" (flatten)"2" (hide -1 -2)"2" (inst -1 "1" "1" )"2" (reveal -4)"2" (assert (-1 -2))"2" "1" expand "o" )"1" expand "trunc1" )"1" expand * "^" min empty_seq)"1" expand "rev" )"1" assert )"1" case "length(q!1)>1" )"1" (assert ) nil nil )"2" "2" expand "finseq_appl" )"2" case "length(q!1)=1" )"1" "walk_from_l" )"1" "q!1" "q!1`seq(0)" "q!1`seq(length(q!1)-1)" )"1" expand "from?" )"1" assert )"1" "1" replace "1" assert )"1" "path_one" )"1" "G!1" "p!1" "p!1`seq(0)" "p!1`seq(length(p!1)-1)" )"1" "p!1" )"1" expand "path_from?" )"1" expand "from?" )"1" expand "circuit?" )"1" expand "cyclically_reduced?" )"1" expand "finseq_appl" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "length(q!1)=1" )"1" "1" expand "finseq_appl" )"1" "walk_from_l" )"1" "q!1" "q!1`seq(0)" "q!1`seq(length(q!1)-1)" )"1" expand "from?" )"1" assert )"1" "1" replace -3 * lr)"1" assert )"1" "path_one" )"1" "G!1" "p!1" "p!1`seq(0)" "p!1`seq(length(p!1)-1)" )"1" "p!1" )"1" expand "path_from?" )"1" expand "from?" )"1" expand "trunc1" )"1" expand "o " )"1" expand "^" )"1" expand "min" )"1" expand "rev" )"1" replace "1" assert )"1" expand "circuit?" )"1" expand "cyclically_reduced?" )"1" expand "finseq_appl" )"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 ))nil )"2" assert )"2" "q!1" )"2" assert )"2" "2" "2" expand "o " )"2" expand "trunc1" )"2" expand "rev" )"2" expand *"^" min "2" expand "finseq_appl" )"2" case "length(q!1)=2" )"1" replace "1" assert )"1" "p!1" )"1" expand "path?" )"1" "1" "1" expand "finseq_appl" )"1" "1" "length(p!1)-1" )"1" replace "1" assert )nil nil ))nil ))nil ))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 ))nil ))nil ))nil )"3" (lemma "dual_path_trunc" )"3" (inst? -1)"3" (bddsimp (-1 -2))"3" (delete -4 -5 -6 7-)"3" (hide -1)"3" (hide -3 -4)"3" "walks[T]" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide -2)"4" (lemma "dual_path_trunc" )"4" (inst -1 "G!1" "p!1" "q!1" )"4" (bddsimp (-1 -2))"4" (delete -4 -5 -6 -7)"4" (expand "dual_paths?" )"4" "4" expand "pre_circuit?" )"4" expand "finseq_appl" )"4" "1" "walks[T]" )"1" (assert ) nil nil ))nil )"2" "walk_concat" )"2" "G!1" "p!1`seq(0)" "q!1`seq(0)" "p!1`seq(length(p!1)-1)" "p!1" "q!1" )"2" "p!1" )"2" "q!1" )"2" expand "path?" )"2" "2" "2" expand "walk_from?" )"2" "1" "1" expand "trunc1" )"1" nil nil ))nil ))nil )"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 )"2" (hide -2)"2" (expand "cycle?" )"2" (expand "finseq_appl" )"2" (bddsimp)"1" (skosimp*)"1" (typepred "i!1" )"1" (typepred "j!1" )"1" (case "i!1<length(p!1)-1" )"1" (case "j!1<length(p!1)-1" )"1" (hide -6)"1" expand "dual_paths?" )"1" expand "finseq_appl" )"1" "1" "p!1" )"1" "q!1" )"1" expand "trunc1" )"1" expand "endpoint?" )"1" expand "o " )"1" expand *"^" min "1" expand "rev" )"1" "walks[T]" )"1" assert )"1" "1" "1" "i!1" "j!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "p!1" )"2" "q!1" )"2" expand "trunc1" )"2" expand "endpoint?" )"2" expand "o " )"2" expand *"^" min "2" expand "rev" )"2" "walks[T]" )"2" assert )"2" "2" "2" "i!1" "j!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" "length(q!1)+length(p!1)-j!1-2" )"1" assert )"1" expand "endpoint?" )"1" expand "o" 3)"1" expand "rev" 3)"1" expand "trunc1" 3)"1" expand "^" 3)"1" expand "trunc1" -6)"1" expand "o" -6)"1" expand "rev" -6)"1" expand "^" -6)"1" expand "min" )"1" "1" assert )nil nil )"2" case "j!1=length(p!1)-1" )"1" replace "1" assert )"1" expand "dual_paths?" )"1" "1" "p!1" )"1" expand "path?" )"1" "1" expand "finseq_appl" )"1" replace "1" "i!1" "length(p!1)-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "walks[T]" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (case "j!1<length(p!1)-1" )"1" "j!1" "length(q!1)+length(p!1)-i!1-2" )"1" expand "endpoint?" )"1" "1" expand "o" )"1" expand "rev" )"1" expand "trunc1" )"1" expand * "^" min empty_seq)"1" "walks[T]" )"1" assert )"1" "1" (assert ) nil nil )"2" (assert ) nil nil )"3" case "i!1=length(p!1)-1" )"1" replace -1 * lr)"1" assert )"1" "1" expand "dual_paths?" )"1" "1" expand "finseq_appl" )"1" replace "1" "p!1" )"1" expand "path?" )"1" "1" expand "finseq_appl" )"1" "length(p!1)-1" "j!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "walks[T]" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide -4)"2" "q!1" )"2" expand "path?" )"2" "2" "2" expand "finseq_appl" )"2" "length(q!1)+length(p!1)-i!1-2" "length(q!1)+length(p!1)-j!1-2" )"1" expand "endpoint?" )"1" expand "o" )"1" expand "rev" )"1" expand "trunc1" )"1" expand *"^" min "1" "walks[T]" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "walks[T]" )"2" assert )"2" expand *"^" min "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "walks[T]" )"3" assert )"3" expand *"^" min "3" "3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "dual_paths?" )"2" (flatten)"2" (hide -1 -2)"2" (inst -1 "1" "1" )"2" (reveal -4)"2" (assert (-1 -2))"2" "1" expand "o" )"1" expand "trunc1" )"1" expand * "^" min empty_seq)"1" expand "rev" )"1" assert )"1" case "length(p!1)>1" )"1" assert )"1" case "length(p!1)=2" )"1" replace -1 * lr)"1" assert )"1" "q!1" )"1" expand "path?" )"1" "1" expand "finseq_appl" )"1" "length(q!1)-1" "1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" "dual_path_trunc" )"2" "2" "2" expand "dual_paths?" )"2" "2" "2" expand "finseq_appl" )"2" "walk_from_l" )"2" "2" "p!1`seq(0)" "p!1`seq(length(p!1)-1)" )"2" expand "from?" )"2" assert )"2" case "length(p!1)=1" )"1" replace "1" assert )"1" "path_one" )"1" "G!1" "q!1" "q!1`seq(0)" "q!1`seq(length(q!1)-1)" )"1" expand "path_from?" )"1" expand "from?" )"1" "1" expand "circuit?" )"1" expand "pre_circuit?" )"1" expand "cyclically_reduced?" )"1" expand "finseq_appl" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))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 ))nil ))nil ))nil ))nil )"2" case "length(p!1)=1" )"1" "1" replace -3 * lr)"1" assert )"1" expand "finseq_appl" )"1" replace -1 -2 lr)"1" "path_one" )"1" "G!1" "q!1" "q!1`seq(0)" "q!1`seq(length(q!1)-1)" )"1" expand "path_from?" )"1" expand "from?" )"1" expand "o " )"1" expand "rev" )"1" expand "trunc1" )"1" expand *"^" min "1" expand "circuit?" )"1" expand "cyclically_reduced?" )"1" expand "finseq_appl" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "finseq_appl" )"2" case "length(p!1)=2" )"1" replace -1 * lr)"1" assert )"1" "walks[T]" )"1" assert )"1" replace -1 * lr)"1" assert )"1" "q!1" )"1" expand "path?" )"1" "1" expand "finseq_appl" )"1" "length(q!1)-1" "1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "dual_path_trunc" )"3" (inst? -1)"3" (bddsimp)"3" (delete -4 -5 -6 -7)"3" (hide -1 -4)"3" (install-rewrites "walks[T]" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"4" (expand "pre_circuit?" )"4" (expand "finseq_appl" )"4" (bddsimp)"1" (lemma "dual_path_trunc" )"1" (inst? -1)"1" (bddsimp)"1" "1" expand "dual_paths?" )"1" "1" expand "finseq_appl" )"1" "1" "walks[T]" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "dual_path_trunc" )"2" (inst? -1)"2" (bddsimp)"2" "2" "2" expand "dual_paths?" )"2" expand "finseq_appl" )"2" "p!1" )"2" "q!1" )"2" expand "path?" )"2" "2" "2" "walk_concat" )"2" "G!1" "p!1`seq(0)" "q!1`seq(0)" "p!1`seq(length(p!1)-1)" "p!1" "q!1" )"2" expand "walk_from?" )"2" "1" expand "trunc1" )"1" nil nil ))nil )"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 tree_paths nil )"bool" cycles nil )nil naturalnumbers nil )"finseq[T]" doubletons nil )"prewalk" walks nil )nil walks nil )"finseq" finite_sequences nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"Graph[T]" tree_paths nil )"Path[T](G!1)" tree_paths nil )"Path[T](G!1)" tree_paths nil )"below(length(trunc1(p!1) o rev(q!1)))" nil )"{k: int | k <= i AND k <= j}" nil )"nonneg_int" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set[T]" tree_paths nil )"(strict_total_order?[real])" real_props nil )"bool" walks nil )"bool" graphs nil )"bool" walks nil )"finseq" finite_sequences nil )"posint" nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" paths nil )"bool" tree_paths nil )"below(length(trunc1(p!1) o rev(q!1)))" nil )"odd_int" integersnil )nil path_circ nil )"bool" circuits nil )"bool" circuits nil )"bool" paths nil )"even_int" integersnil )"posint" nil )"bool" walks nil )nil path_circ nil )nil tree_paths nil )"bool" walks nil )"bool" walks nil )nil walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"below(length(trunc1(p!1) o rev(q!1)))" nil )"below(length(trunc1(p!1) o rev(q!1)))" nil )nil paths nil )"bool" paths nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )"bool" sets 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 tree_paths nil ))nil ))nil 3253637225"" (skosimp*)"" (case "u!1=v!1" )"1" (lemma "tree_no_circuits" )"1" (inst-cp -1 "G!1" "p!1" )"1" (inst -1 "G!1" "q!1" )"1" (lemma "prewalk_same" )"1" (inst -1 "p!1" "q!1" "u!1" "v!1" )"1" (lemma "path_one" )"1" (inst-cp -1 "G!1" "p!1" "u!1" "v!1" )"1" (inst -1 "G!1" "q!1" "u!1" "v!1" )"1" (expand "path_from?" )"1" (bddsimp) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (expand "path_from?" -4)"2" (expand "path?" -4) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (expand "path_from?" -3)"2" (expand "path?" -3) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (lemma "tree_no_circuits" )"2" (lemma "min_dual_def" )"2" (inst -1 "G!1" "p!1" "q!1" )"1" "PROJ_1(min_dual_paths(G!1, p!1, q!1))" )"1" "PROJ_2(min_dual_paths(G!1, p!1, q!1))" )"1" (lemma "cycl_red_compos" )"1" "G!1" "PRO_1" "PRO_2" "PRO_1(0)" "PRO_1(length(PRO_1)-1)" )"1" (lemma "path_one" )"1" "G!1" "PRO_1" "PRO_1(0)" "PRO_1(length(PRO_1)-1)" )"1" "G!1" "PRO_2" "PRO_2(0)" "PRO_2(length(PRO_2)-1)" )"1" (inst-cp -5 "G!1" "PRO_1" )"1" (inst-cp -5 "G!1" "PRO_2" )"1" "G!1" "trunc1(PRO_1) o rev(PRO_2)" )"1" assert )"1" "back_short" )"1" "G!1" "PRO_1" "PRO_2" "PRO_1(0)" "PRO_1(length(PRO_1) -1)" )"1" "front_short" )"1" "G!1" "PRO_1" "PRO_2" "PRO_1(0)" "PRO_1(length(PRO_1) -1)" )"1" expand "circuit?" 1)"1" "two_walks" )"1" "G!1" "PRO_1" "PRO_2" "PRO_1(0)" "PRO_1(length(PRO_1) -1)" )"1" expand "pre_circuit?" )"1" assert )"1" expand "is_min_dual?" )"1" expand "dual_paths?" "1" "PRO_1" )"1" "PRO_2" )"1" expand "path_from?" )"1" "1" "1" expand "path?" "1" expand "path?" "1" "1" "1" "1" "1" expand "from?" "1" expand "from?" "1" "walkers" )"1" "PRO_1" "PRO_2" )"1" expand "finseq_appl" )"1" assert )"1" "1" replace "1" replace "1" assert )"1" "1" "1" "1" assert )"1" "1" case "seq(PRO_1)(0) = seq(PRO_1)(length(PRO_1) - 1)" )"1" assert )"1" "1" "1" "1" "prewalk_same" )"1" "PRO_1" "PRO_2" "seq(PRO_1)(0)" "seq(PRO_1)(length(PRO_1)-1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" case "seq(PRO_1)(length(PRO_1) - 2) /= seq(PRO_2)(length(PRO_2) - 2) AND ") "1" "1" assert )nil nil ))nil )"2" case "seq(PRO_1)(length(PRO_1) - 2) = seq(PRO_2)(length(PRO_2) - 2)" )"1" assert )"1" "1" "1" "pp!1" "qq!1" )"1" assert )"1" expand "from?" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" nil nil ))nil ))nil ))nil ))nil )"2" case "seq(PRO_1)(1) = seq(PRO_2)(1)" )"1" assert )"1" "1" "1" "pp!1" "qq!1" )"1" expand "from?" "1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil )"3" nil nil ))nil ))nil ))nil ))nil )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "path_from?" )"2" expand "dual_paths?" )"2" expand "from?" )"2" expand "finseq_appl" )"2" "PRO_1" )"2" "PRO_2" )"2" expand "path?" "2" assert )"2" "2" "2" replace "2" replace "2" "2" assert )"2" "2" "2" "1" "1" "1" "prewalk_same" )"1" "PRO_1" "PRO_2" "finseq_appl(PRO_1)(0)" "finseq_appl(PRO_1)(length(PRO_1) - 1)" )"1" assert )"1" expand "finseq_appl" )"1" case "length(PRO_1)>1" )"1" "walk_concat" )"1" "G!1" "seq(PRO_1)(0)" "seq(PRO_1)(0)" "seq(PRO_1)(length(PRO_1)-1)" "PRO_1" "PRO_2" )"1" "1" nil nil ))nil ))nil ))nil )"2" assert )"2" expand "path_from?" )"2" "2" 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 ))nil ))nil ))nil ))nil )"3" expand "dual_paths?" )"3" "3" expand "path_from?" )"3" "PRO_1" "PRO_2" )"3" "3" "3" "1" "1" "1" expand "from?" "1" "1" replace "1" replace "1" "1" assert )"1" expand "finseq_appl" )"1" "1" "1" "prewalk_same" )"1" "PRO_1" "PRO_2" "seq(PRO_1)(0)" "seq(PRO_1)(length(PRO_1)-1)" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "dual_paths?" )"2" expand "path_from?" )"2" "2" expand "from?" )"2" "2" expand "is_min_dual?" )"2" replace -6 -3 rl)"2" replace -7 -4 rl)"2" "2" expand "finseq_appl" )"2" assert )"2" "2" "2" expand "dual_paths?" )"2" "PRO_2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "PRO_1" )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" (typepred "PRO_2" )"2" (hide-all-but (-1) -)"2" (assert ) nil nil )) nil ))nil )"3" (typepred "PRO_2" )"3" (hide-all-but (-1) -)"3" (assert ) nil nil )) nil ))nil ))nil )"2" (typepred "PRO_1" )"2" (hide-all-but (-1) -)"2" (assert ) nil nil )) nil ))nil )"3" (typepred "PRO_1" )"3" (hide-all-but (-1) -)"3" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (typepred "PRO_1" )"2" (hide-all-but (-1) -)"2" (assert ) nil nil )) nil ))nil )"3" (typepred "PRO_1" )"3" (hide-all-but (-1) -)"3" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide -1 -2)"2" (expand "path_from?" )"2" (flatten)"2" (expand "from?" )"2" (flatten)"2" (assert )"2" (expand "dual_paths?" )"2" expand "finseq_appl" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide -1 -2)"3" (expand "path_from?" ) (("3" (assert ) nil nil ))nil ))nil )"4" (hide -1 -2)"4" (lemma "tree_nonempty" )"4" (inst?)"4" (assert )"4" (expand "empty?" )"4" (expand "nonempty?" )"4" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2)"2" (expand "path_from?" )"2" (flatten)"2" (assert )"2" (expand "from?" )"2" (flatten)"2" (expand "dual_paths?" )"2" (expand "finseq_appl" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide -1 -2)"3" (expand "path_from?" ) (("3" (flatten) nil nil ))nil ))nil )"4" (lemma "tree_nonempty" )"4" (inst -1 "G!1" )"4" (assert )"4" (expand "nonempty?" )"4" (expand "empty?" +)"4" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2) (("2" (grind) nil nil )) nil )"3" (hide -1 -2) (("3" (grind) nil nil )) nil )"4" (hide -1 -3 -4)"4" (lemma "tree_nonempty" )"4" (inst -1 "G!1" )"4" (assert )"4" (hide -1) (("4" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil tree_paths nil )"prewalk[T]" tree_paths nil )"graph[T]" tree_paths 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 graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil walks nil )"bool" paths nil )nil path_circ nil )nil path_circ nil )"bool" paths nil )"prewalk[T]" tree_paths nil )nil tree_circ nil )nil tree_paths nil )"bool" sets nil )"bool" sets nil )"Dual_paths(G)" tree_paths nil )nil tree_paths nil )"bool" tree_paths nil )"bool" graphs nil )nil trees nil )nil path_circ nil )"Path[T](G!1)" tree_paths nil )"posint" nil )"{k: int | k <= i AND k <= j}" nil )"int" integers nil )"nonneg_int" nil )nil application-judgement "finite_set[T]" tree_paths nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"bool" walks nil )"bool" graphs nil )"bool" walks nil )nil walks nil )nil path_circ nil )"bool" walks nil )"bool" tree_paths nil )NOT const-decl "[bool -> bool]" booleans nil )"prewalk[T]" tree_paths nil )"prewalk[T]" tree_paths nil )"prewalk[T]" tree_paths nil )"prewalk[T]" tree_paths nil )nil path_circ nil )"bool" walks nil )"bool" circuits nil )nil path_circ nil )nil path_circ nil )"finseq[T]" doubletons nil )"prewalk" walks nil )nil walks nil )"finseq" finite_sequences nil )"(strict_total_order?[real])" real_props nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[below[length(fs)] -> T]" finite_sequencesnil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"Path[T](G!1)" tree_paths nil )"bool" reals nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil paths nil )nil graphs nil )"bool" sets nil ))nil )nil 3253637114"" (skosimp*)"" (case "u!1=v!1" )"1" (lemma "tree_no_circuits" )"1" (inst-cp -1 "G!1" "p!1" )"1" (inst -1 "G!1" "q!1" )"1" (lemma "prewalk_same" )"1" (inst -1 "p!1" "q!1" "u!1" "v!1" )"1" (lemma "path_one" )"1" (inst-cp -1 "G!1" "p!1" "u!1" "v!1" )"1" (inst -1 "G!1" "q!1" "u!1" "v!1" )"1" (expand "path_from?" )"1" (bddsimp) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (expand "path_from?" -4)"2" (expand "path?" -4) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (expand "path_from?" -3)"2" (expand "path?" -3) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (lemma "tree_no_circuits" )"2" (lemma "min_dual_def" )"2" (inst -1 "G!1" "p!1" "q!1" )"1" "PROJ_1(min_dual_paths(G!1, p!1, q!1))" )"1" "PROJ_2(min_dual_paths(G!1, p!1, q!1))" )"1" (lemma "cycl_red_compos" )"1" "G!1" "PRO_1" "PRO_2" "PRO_1(0)" "PRO_1(length(PRO_1)-1)" )"1" (lemma "path_one" )"1" "G!1" "PRO_1" "PRO_1(0)" "PRO_1(length(PRO_1)-1)" )"1" "G!1" "PRO_2" "PRO_2(0)" "PRO_2(length(PRO_2)-1)" )"1" (inst-cp -5 "G!1" "PRO_1" )"1" (inst-cp -5 "G!1" "PRO_2" )"1" "G!1" "trunc1(PRO_1) o rev(PRO_2)" )"1" assert )"1" "back_short" )"1" "G!1" "PRO_1" "PRO_2" "PRO_1(0)" "PRO_1(length(PRO_1) -1)" )"1" "front_short" )"1" "G!1" "PRO_1" "PRO_2" "PRO_1(0)" "PRO_1(length(PRO_1) -1)" )"1" expand "circuit?" 1)"1" "two_walks" )"1" "G!1" "PRO_1" "PRO_2" "PRO_1(0)" "PRO_1(length(PRO_1) -1)" )"1" expand "pre_circuit?" )"1" assert )"1" expand "is_min_dual?" )"1" expand "dual_paths?" "1" "PRO_1" )"1" "PRO_2" )"1" expand "path_from?" )"1" "1" "1" expand "path?" "1" expand "path?" "1" "1" "1" "1" "1" expand "from?" "1" expand "from?" "1" "walkers" )"1" "PRO_1" "PRO_2" )"1" expand "finseq_appl" )"1" assert )"1" "1" replace "1" replace "1" assert )"1" "1" "1" "1" assert )"1" "1" case "seq(PRO_1)(0) = seq(PRO_1)(length(PRO_1) - 1)" )"1" assert )"1" "1" "1" assert )"1" "1" "prewalk_same" )"1" "PRO_1" "PRO_2" "seq(PRO_1)(0)" "seq(PRO_1)(length(PRO_1)-1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" case "seq(PRO_1)(length(PRO_1) - 2) /= seq(PRO_2)(length(PRO_2) - 2) AND ") "1" "1" assert )nil nil ))nil )"2" case "seq(PRO_1)(length(PRO_1) - 2) = seq(PRO_2)(length(PRO_2) - 2)" )"1" assert )"1" "1" "1" "pp!1" "qq!1" )"1" assert )"1" expand "from?" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" nil nil ))nil ))nil ))nil ))nil )"2" case "seq(PRO_1)(1) = seq(PRO_2)(1)" )"1" assert )"1" "1" "1" "pp!1" "qq!1" )"1" expand "from?" "1" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil )"3" nil nil ))nil ))nil ))nil ))nil )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "path_from?" )"2" expand "dual_paths?" )"2" expand "from?" )"2" expand "finseq_appl" )"2" "PRO_1" )"2" "PRO_2" )"2" expand "path?" "2" assert )"2" "2" "2" replace "2" replace "2" "2" assert )"2" "2" "2" "1" "1" "1" "prewalk_same" )"1" "PRO_1" "PRO_2" "finseq_appl(PRO_1)(0)" "finseq_appl(PRO_1)(length(PRO_1) - 1)" )"1" assert )"1" expand "finseq_appl" )"1" case "length(PRO_1)>1" )"1" "walk_concat" )"1" "G!1" "seq(PRO_1)(0)" "seq(PRO_1)(0)" "seq(PRO_1)(length(PRO_1)-1)" "PRO_1" "PRO_2" )"1" "1" nil nil ))nil ))nil ))nil )"2" assert )"2" expand "path_from?" )"2" assert )"2" "2" 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 ))nil ))nil ))nil ))nil )"3" expand "dual_paths?" )"3" "3" expand "path_from?" )"3" "PRO_1" "PRO_2" )"3" "3" "3" "1" "1" "1" expand "from?" "1" "1" replace "1" replace "1" "1" assert )"1" expand "finseq_appl" )"1" assert )"1" "1" "1" "prewalk_same" )"1" "PRO_1" "PRO_2" "seq(PRO_1)(0)" "seq(PRO_1)(length(PRO_1)-1)" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "dual_paths?" )"2" expand "path_from?" )"2" "2" expand "from?" )"2" "2" expand "is_min_dual?" )"2" replace -6 -3 rl)"2" replace -7 -4 rl)"2" "2" expand "finseq_appl" )"2" assert )"2" "2" "2" expand "dual_paths?" )"2" "PRO_2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "PRO_1" )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" (typepred "PRO_2" )"2" (hide-all-but (-1) -)"2" (assert ) nil nil )) nil ))nil )"3" (typepred "PRO_2" )"3" (hide-all-but (-1) -)"3" (assert ) nil nil )) nil ))nil ))nil )"2" (typepred "PRO_1" )"2" (hide-all-but (-1) -)"2" (assert ) nil nil )) nil ))nil )"3" (typepred "PRO_1" )"3" (hide-all-but (-1) -)"3" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (typepred "PRO_1" )"2" (hide-all-but (-1) -)"2" (assert ) nil nil )) nil ))nil )"3" (typepred "PRO_1" )"3" (hide-all-but (-1) -)"3" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (typepred "q!1" )"2" (hide -2 -3)"2" (expand "dual_paths?" )"2" (grind) nil nil )) nil ))nil ))nil )"3" (hide -1 -2)"3" (expand "path_from?" ) (("3" (assert ) nil nil ))nil ))nil )"4" (hide -1 -3 -4)"4" (lemma "tree_nonempty" )"4" (inst -1 "G!1" )"4" (assert ) (("4" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2) (("2" (grind) nil nil )) nil )"3" (hide -1 -2) (("3" (grind) nil nil )) nil )"4" (hide -1 -3 -4)"4" (lemma "tree_nonempty" )"4" (inst -1 "G!1" )"4" (assert )"4" (hide -1) (("4" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2) (("2" (grind) nil nil )) nil )"3" (hide -1 -2) (("3" (grind) nil nil )) nil )"4" (hide -1 -3 -4)"4" (lemma "tree_nonempty" )"4" (inst -1 "G!1" )"4" (assert )"4" (hide -1) (("4" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.357 Sekunden
(vorverarbeitet am 2026-04-28)
¤ *© Formatika GbR, Deutschland
2026-05-26
