path_circ.prf
Interaktion und
(path_circnil 3253636829 ("" (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 )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 ) (< const-decl "bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"graph[T]" path_circ nil )"bool" walks nil )"bool" graphs nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set[T]" path_circ nil )nil path_circ nil )"bool" walks nil )"boolean" notequal nil ))nil ))nil 3253636829"" (skosimp*)"" (typepred "p!1" )"" (install-rewrites "paths" ) (("" (grind) nil nil )) nil ))nil ))nil )nil paths 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 path_circ nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil application-judgement "finite_set[T]" path_circ nil )"(strict_total_order?[real])" real_props nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" graphs nil )"bool" walks nil )"bool" circuits nil )"bool" circuits nil )"(total_order?[real])" nil )"posint" nil )"int" integers 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 )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )nil integers nil ))nil ))nil 3253636829"" (expand "trunc1" ) (("" (skosimp*) (("" (grind) nil nil )) nil ))nil )"(total_order?[real])" nil )"int" integers nil )"posint" nil )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"nonneg_int" nil )"finseq" finite_sequences nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"prewalk" walks nil ))nil ))nil 3253636829"" (skosimp*)"" (expand "trunc1" )"" (expand "walk?" )"" (flatten)"" (prop)"1" (grind) nil nil )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (inst - "n!1" )"2" (expand * "^" min empty_seq)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"prewalk" walks nil )nil application-judgement "finite_set[T]" path_circ nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"{k: int | k <= i AND k <= j}" nil )"posint" nil )"int" integers nil )"bool" graphs nil )"boolean" notequal nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" walks nil )nil path_circ nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"(strict_total_order?[real])" real_props 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil nat_types nil )nil finite_sequences nil )"bool" reals nil )nil walks nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil naturalnumbers nil )"bool" walks nil ))nil ))nil 3253636829 ("" (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 )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 path_circ nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )nil application-judgement "finite_set[T]" path_circ nil ))nil ))nil 3253636829 ("" (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 )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 path_circ nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" circuits nil )"bool" circuits nil )nil application-judgement "finite_set[T]" path_circ nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil path_circ nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" circuits nil )"bool" circuits nil )nil application-judgement "finite_set[T]" path_circ nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil path_circ nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" circuits nil )"bool" circuits nil )nil application-judgement "finite_set[T]" path_circ nil ))nil ))nil 3253636829 ("" (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 )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 )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil path_circ nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" circuits nil )"bool" circuits nil )nil application-judgement "finite_set[T]" path_circ nil ))nil ))nil 3253636829 ("" (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 )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 )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil path_circ nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" circuits nil )"bool" circuits nil )nil application-judgement "finite_set[T]" path_circ nil ))nil ))nil 3253636829"" (lemma "trunc_long" )"" (lemma "verts_in?_concat" )"" (lemma "trunc_walk" )"" (skosimp*)"" (inst -3 "u!1" "w!1" )"" (inst -2 "G!1" "trunc1(u!1)" "w!1" )"1" (inst -1 "G!1" "u!1" ) (("1" (grind) nil nil )) nil )"2" (grind) nil nil ) ("3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil path_circ nil )nil walks nil )"(total_order?[real])" nil )"bool" reals nil )"prewalk[T]" path_circ nil )"prewalk" walks nil )nil walks nil )"graph[T]" path_circ nil )"bool" walks nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil ) (Seq type-eq-decl nil walks nil )nil application-judgement "finite_set[T]" path_circ nil )"int" integers nil )"posint" nil )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"nonneg_int" nil )"bool" circuits nil )"bool" circuits nil )"finseq" finite_sequences nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" walks nil )"bool" graphs nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" finite_sequences nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def 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 )"[numfield, numfield -> numfield]" number_fields nil )"even_int" integersnil )"odd_int" integersnil )nil integers nil )nil integers nil )"below(IF 0 > length(u!1) - 2 THEN 0 ELSE length(u!1) - 1 ENDIF)" nil )"prewalk[T]" path_circ nil )"odd_int" integers nil )"below(length(u!1) + w!1`length - 1)" nil )"(strict_total_order?[real])" real_props nil )nil walks 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 )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil path_circ nil )nil path_circ nil ))nil ))nil 3253636829"" (expand "trunc1" )"" (skosimp*)"" (expand "reduced?" 2)"" (expand "reducible?" -)"" (skolem! -8)"" (case "k!1 < length(u!1)-1" )"1" (hide -3)"1" (expand "reduced?" -5)"1" (expand "reducible?" 1)"1" (inst 1 "k!1" )"1" (assert )"1" (expand "finseq_appl" )"1" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (case "k!1 >length(u!1) -1" )"1" (expand "reduced?" -6)"1" (expand "reducible?" 2)"1" (inst 2 "k!1 - length(u!1) +1" )"1" (assert )"1" (expand "finseq_appl" )"1" (grind) nil nil )) nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil )"2" (hide -1)"2" (assert )"2" (expand "finseq_appl" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" circuits nil )nil walks nil )nil finite_sequences nil )nil path_circ nil )nil nat_types nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals 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 )"int" integers nil )"[below[length(fs)] -> T]" finite_sequencesnil )"nonneg_int" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"{k: int | k <= i AND k <= j}" nil )"posint" nil )nil application-judgement "finite_set[T]" path_circ nil )"bool" walks nil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"finseq" finite_sequences nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posnat" path_circ nil )"prewalk[T]" path_circ nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" circuits nil )"prewalk" walks nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil path_circ nil )"finseq[T]" doubletons nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil path_circ nil )"finseq[T]" doubletons nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil path_circ nil )"finseq[T]" doubletons nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil path_circ nil )"finseq[T]" doubletons nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil ))nil 3253636829"" (install-rewrites ("paths" ))"" (skosimp*) (("" (assert ) nil nil )) nil )) nil )nil path_circ nil )"finseq[T]" doubletons nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(total_order?[real])" nil ))nil ))nil 3253636829"" (skosimp*)"" (expand "rev" )"" (apply-extensionality)"" (apply-extensionality 1) nil nil )) nil ))nil ))nil )"finseq[T]" doubletons nil )nil naturalnumbers nil )nil walks nil )"bool" reals nil )nil finite_sequences nil )nil path_circ nil )nil nat_types nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans 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 booleans nil )nil numbers nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil path_circ nil )"finseq[T]" doubletons nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil ) nil nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil path_circ nil )"finseq[T]" doubletons nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil path_circ nil )"finseq[T]" doubletons nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil ))nil 3253636829"" (skosimp*)"" (install-rewrites ("paths" )) (("" (assert ) nil nil )) nil ))nil )nil path_circ nil )"finseq[T]" doubletons nil )"[below[length(fs)] -> T]" finite_sequencesnil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil path_circ nil )"bool" walks nil )"boolean" notequal nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )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 )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil path_circ nil )"bool" walks nil )"boolean" notequal nil )"prewalk" walks nil )"finseq[T]" doubletons nil )"finseq" finite_sequences nil )"posint" nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil path_circ nil )"bool" walks nil )"boolean" notequal nil ))nil ))nil 3253636829"" (expand "trunc1" ) (("" (skosimp*) (("" (grind) nil nil )) nil ))nil )"finseq" finite_sequences nil )"finseq[T]" doubletons nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" walks nil )nil path_circ nil )"int" integers nil )"posint" nil )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nonneg_int" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"prewalk" walks nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil path_circ nil )"bool" walks nil )"boolean" notequal nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )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 path_circ nil )"bool" walks nil )"boolean" notequal nil )"prewalk" walks nil )"finseq[T]" doubletons nil )"finseq" finite_sequences nil )"posint" nil )"nonneg_int" nil ))nil ))nil 3253636829"" (expand "trunc1" ) (("" (skosimp*) (("" (grind) nil nil )) nil ))nil )"finseq" finite_sequences nil )"finseq[T]" doubletons nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" walks nil )nil path_circ nil )"int" integers nil )"posint" nil )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nonneg_int" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"prewalk" walks nil ))nil ))nil 3253636829"" (skolem-typepred)"" (flatten)"" (extensionality "prewalk" )"" (inst -1 "p!1" "q!1" )"" (assert )"" (grind)"" (extensionality "[below[length(p!1)]-> T]" )"" (inst -1 "p!1`seq" "q!1`seq" )"1" (assert ) nil nil )"2" (assert )"2" (skosimp*) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" walks nil )"int" integers nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )"(strict_total_order?[real])" real_props nil )nil walks nil )nil finite_sequences nil )nil path_circ nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )nil path_circ nil )"bool" walks nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )nil path_circ nil )"bool" walks nil ))nil ))nil 3253636829"" (skosimp*) (("" (grind) nil nil )) nil )"int" integers nil )"nonneg_int" nil )"(total_order?[real])" nil )"{k: int | k <= i AND k <= j}" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"finseq" finite_sequences nil )"finseq[T]" doubletons nil )"prewalk" walks nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" walks nil )nil path_circ nil ))nil ))nil 3253636829 ("" (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 )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 )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )nil path_circ nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" walks nil )"bool" paths nil )nil application-judgement "finite_set[T]" path_circ nil ))nil ))nil 3253636829 ("" (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 )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 )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )nil path_circ nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" walks nil )"bool" paths nil )nil application-judgement "finite_set[T]" path_circ nil ))nil ))nil 3253636829 ("" (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 )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 )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil path_circ nil )"bool" walks nil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" walks nil )"bool" paths nil )nil application-judgement "finite_set[T]" path_circ nil ))nil ))nil 3253636829 ("" (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 )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 )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )"(total_order?[real])" nil )"nonneg_int" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields 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 )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"graph[T]" path_circ nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil path_circ nil )"bool" walks nil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" walks nil )"bool" paths nil )"prewalk" walks nil )"finseq[T]" doubletons nil )"finseq" finite_sequences nil )nil application-judgement "finite_set[T]" path_circ nil )"posint" nil )"boolean" notequal nil ))nil ))nil 3253636829"" (skosimp*)"" (lemma "path_reduc" )"" (lemma "path?_rev" )"" (lemma "walks_concat_red" )"" (lemma "index_rev" )"" (inst -1 "q!1" )"" (inst -3 "G!1" "q!1" )"" (inst-cp -4 "G!1" "p!1" )"1" (inst -2 "G!1" "p!1" "rev(q!1)" )"1" (lemma "path_from_l" )"1" (inst-cp -1 "G!1" "p!1" "s!1" "t!1" )"1" (inst-cp -1 "G!1" "q!1" "s!1" "t!1" )"1" (hide -1)"1" (hide -6)"1" "1" "G!1" "rev(q!1)" )"1" expand "path_from?" )"1" "1" expand "from?" )"1" expand "finseq_appl" )"1" "1" assert )"1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) (("2" (grind) nil nil )) nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil path_circ nil )nil path_circ nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil walks nil )"bool" paths nil )"graph[T]" path_circ nil )"prewalk[T]" path_circ nil )nil paths nil )nil paths nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(total_order?[real])" nil )"int" integers nil )"nonneg_int" nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )"posint" nil )nil application-judgement "finite_set[T]" path_circ 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 )"prewalk" walks nil )"finseq" finite_sequences nil )"bool" circuits nil )"bool" circuits nil )"bool" walks nil )"bool" paths nil )"finseq" finite_sequences nil )"prewalk[T]" path_circ nil )"finseq[T]" doubletons nil )"(strict_total_order?[real])" real_props 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 path_circ nil )nil paths nil )nil path_circ nil ))nil ))nil 3253636829 ("" (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 )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 )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )nil path_circ nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" walks nil )"bool" paths nil )nil application-judgement "finite_set[T]" path_circ nil ))nil ))nil 3253636829 ("" (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 )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 )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )nil path_circ nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" walks nil )"bool" paths nil )nil application-judgement "finite_set[T]" path_circ nil ))nil ))nil 3253636829"" (lemma "red_compos" )"" (skosimp 1)"" (expand "cyclically_reduced?" 4)"" (lemma "index_rev" )"" (inst -2 "G!1" "p!1" "q!1" "s!1" "t!1" )"" (inst -1 "q!1" )"" (lemma "compose_long" )"" (inst -1 "p!1" "q!1" "s!1" "t!1" )"" (lemma "second_in_cat" )"" (lemma "sec_from_last" )"" (inst -1 "p!1" "q!1" "s!1" "t!1" )"" (inst -2 "p!1" "q!1" "s!1" "t!1" )"" (assert )"" (expand "finseq_appl" )"" expand "path_from?" -7)"" assert )"" "1" (assert ) nil nil )"2" (grind) nil nil )"3" (grind) nil nil )"4" (grind) nil nil )"5" (grind) nil nil )"6" (grind) nil nil )"7" (grind) nil nil )"8" (grind) nil nil )"9" (grind) nil nil )"10" (grind) nil nil )"11" (grind) nil nil )"12" (grind) nil nil )"13" (grind) nil nil )"14" (grind) nil nil )"15" (grind) nil nil )"16" (grind) nil nil )"17" (grind) nil nil )"18" (grind) nil nil )"19" (grind) nil nil )"20" (grind) nil nil )"21" (grind) nil nil )"22" (grind) nil nil )"23" (grind) nil nil )"24" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil path_circ nil )nil path_circ nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil application-judgement "finite_set[T]" path_circ nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"nonneg_int" nil )"{k: int | k <= i AND k <= j}" nil )"posint" nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"prewalk" walks nil )"finseq[T]" doubletons nil )"finseq" finite_sequences nil )"bool" circuits nil )"bool" circuits nil )"bool" walks nil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" walks nil )"even_int" integersnil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil integers nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"even_int" integersnil )"bool" paths nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil path_circ nil )nil path_circ 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 path_circ nil )"bool" circuits nil )nil path_circ nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil ) nil nil ))nil 3253636829 ("" (subtype-tcc) nil nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil ))nil 3253636829 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 )"[below[length(fs)] -> T]" finite_sequencesnil )nil path_circ nil )"bool" walks nil ))nil ))nil 3253636829 ("" (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 )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 path_circ nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" walks nil )"bool" paths nil )nil application-judgement "finite_set[T]" path_circ nil ))nil ))nil 3253636829"" (skolem-typepred)"" (expand "circuit?" )"" (flatten)"" (split)"1" (expand "path_from?" )"1" (expand "cyclically_reduced?" )"1" (expand "finseq_appl" )"1" (lemma "path_reduc" )"1" (inst -1 "G!1" "p!1" )"1" (assert )"1" (expand "path?" )"1" (expand "finseq_appl" )"1" (flatten)"1" (inst -6 "1" "length(p!1)-2" )"1" assert )"1" "1" expand "walk?" )"1" expand "finseq_appl" )"1" "1" "1" )"1" assert )"1" expand "edge?" -7)"1" expand "from?" -9)"1" "1" "1" "1" expand "reduced?" "1" expand "reducible?" "1" expand "finseq_appl" )"1" "1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "from?" -4)"2" assert )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" circuits nil )"bool" circuits nil )nil path_circ nil )"(strict_total_order?[real])" real_props 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 )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil application-judgement "finite_set[T]" path_circ nil )"bool" graphs nil )"bool" circuits nil )nil integers nil )nil integers nil )"bool" circuits nil )"bool" walks nil )"bool" walks nil )nil paths nil )"prewalk[T]" path_circ nil )"graph[T]" path_circ nil )"bool" paths nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" paths nil )"bool" walks nil )"bool" walks nil )"posint" 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 )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 path_circ nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3253636829"" (skosimp*)"" (apply-extensionality 1 :hide? t)"1" (expand "rev" ) (("1" (propax) nil nil )) nil )"2" (lemma "rev_rev" )"2" (inst-cp -1 "p!1" )"2" (inst -1 "q!1" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil naturalnumbers nil )nil nat_types nil )nil path_circ nil )nil finite_sequences nil )nil walks 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 )"finseq[T]" doubletons nil )"int" integers nil )nil path_circ nil ))nil ))nil 3253636829"" (skosimp*)"" (expand "from?" ) (("" (flatten) (("" (assert ) nil nil )) nil ))nil ))nil )"bool" walks nil )"(strict_total_order?[real])" real_props nil )"int" integers nil ))nil ))nil 3253636829"" (skosimp*)"" (install-rewrites ("walks" ))"" (assert )"" (prop) (("1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil )nil path_circ nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"int" integers nil ))nil ))nil 3253636829"" (skosimp*) (("" (grind) nil nil )) nil )"(total_order?[real])" nil )"int" integers nil )"bool" walks nil )nil path_circ nil ))nil ))nil 3253636829"" (skosimp*)"" (lemma "walk_from_l" )"" (inst -1 "q!1" "s!1" "t!1" )"" (bddsimp) (("" (prop) nil nil )) nil )) nil ))nil ))nil )nil path_circ nil )nil walks 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 )nil finite_sequences nil )nil path_circ nil )nil nat_types nil )nil naturalnumbers nil ))nil ))nil 3253636829"" (skosimp*)"" (apply-extensionality 2 :hide? t)"1" (hide-all-but (-3 1)) (("1" (grind) nil nil )) nil )"2" (lemma "l_trunc1" )"2" (inst-cp -1 "p!1" )"2" (inst - "q!1" )"2" (lemma "front_back" )"2" (expand "finseq_appl" )"2" (inst -1 "p!1" "q!1" "s!1" "t!1" )"2" (lemma "walk_from_l" )"2" (expand "trunc1" *)"2" (inst-cp -1 "p!1" "s!1" "t!1" )"2" (inst -1 "q!1" "s!1" "t!1" )"2" (assert )"2" (apply-extensionality 1 :hide? t)"2" "2" "x!1" )"2" expand * "^" min )"2" "(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" (assert ) nil nil )"2" replace -10)"2" (propax) nil nil ))nil )"3" "3" "3" "x!2" )"3" expand "min" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" "4" expand "min" )"4" (assert ) nil nil ))nil ))nil )"5" expand "min" )"5" (assert ) nil nil ))nil )"6" "6" "6" (assert ) nil nil ))nil ))nil )"7" "7" expand "min" )"7" (assert ) nil nil ))nil ))nil )"8" "8" "x!1 = length(p!1) - 1" )"1" (assert ) nil nil )"2" "2" expand "min" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )nil nat_types nil )nil path_circ nil )nil finite_sequences nil )nil walks 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 )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"{k: int | k <= i AND k <= j}" nil )"posint" nil )"int" integers nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"prewalk" walks nil )nil path_circ nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil path_circ nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil walks nil ))nil ))nil 3253636829 ("" (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 )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 )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 )"nonneg_int" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil path_circ nil )"bool" walks nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"prewalk" walks nil )"finseq[T]" doubletons nil )"finseq" finite_sequences nil )nil application-judgement "finite_set[T]" path_circ nil )"posint" nil ))nil ))nil 3253636829"" (skosimp*)"" (lemma "walk_concat" )"" (lemma "walk_from_l" )"" (inst -1 "p!1" "s!1" "t!1" )"" (inst -2 "G!1" "s!1" "s!1" "t!1" "p!1" "q!1" )"" (expand "pre_circuit?" +)"" (expand "walk_from?" -)"" (assert )"" (expand "from?" )"" (expand "trunc1" )"" (expand "finseq_appl" )"" (assert )"" (bddsimp) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil path_circ nil )nil walks nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil walks nil )"bool" walks nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"prewalk" walks nil )"(total_order?[real])" nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" walks nil )"bool" walks nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil path_circ nil ))nil ))nil 3253636829"" (skosimp*)"" (inst 3 "p!1^(0,length(p!1)-2)" "q!1^(0,length(q!1)-2)" )"1" (lemma "plus_up" )"1" (inst -1 "p!1" "q!1" "s!1" "t!1" )"1" (lemma "path?_trunc1" )"1" (inst-cp -1 "G!1" "p!1" )"1" (inst -1 "G!1" "q!1" )"1" (lemma "walk_from_l" )"1" (inst-cp -1 "p!1" "s!1" "t!1" )"1" (inst -1 "q!1" "s!1" "t!1" )"1" (expand "path_from?" )"1" (expand "trunc1" )"1" (assert )"1" (flatten)"1" assert )"1" expand "from?" -6)"1" expand "from?" -8)"1" expand "finseq_appl" )"1" assert )"1" "1" "1" assert )"1" (grind) nil nil ))nil )"2" assert )"2" (grind) nil nil ))nil )"3" (grind) nil nil )"4" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ) ("3" (grind) nil nil )"4" (grind) nil nil ) ("5" (grind) nil nil ))nil ))nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"prewalk[T]" path_circ nil )nil walks nil )"bool" reals nil )nil finite_sequences nil )nil path_circ nil )nil nat_types nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 )"finseq" finite_sequences nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"prewalk[T]" path_circ 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 path_circ nil )"prewalk" walks nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"posint" nil )"{k: int | k <= i AND k <= j}" nil )"int" integers nil )nil application-judgement "finite_set[T]" path_circ nil )"bool" paths nil )"bool" walks nil )"bool" graphs nil )"bool" walks nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" paths nil )nil paths nil )nil path_circ nil )nil naturalnumbers nil )"bool" reals nil )"finseq" finite_sequences nil ))nil ))nil 3253636829 ("" (subtype-tcc) nil nil )nil path_circ nil )"bool" walks nil )"finseq[T]" doubletons nil ))nil ))nil 3253636829 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans 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 path_circ nil )"bool" walks nil )"finseq[T]" doubletons nil )"int" integers nil ))nil ))nil 3253636829 ("" (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 )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 )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil path_circ nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" walks nil )"bool" paths nil )nil application-judgement "finite_set[T]" path_circ nil ))nil ))nil 3253636829 ("" (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 )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 )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil path_circ nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" walks nil )"bool" paths nil )nil application-judgement "finite_set[T]" path_circ nil ))nil ))nil 3253636829"" (skosimp*)"" "(rev(p!1))^(0,length(p!1)-2)" "(rev(q!1))^(0,length(q!1)-2)" )"1" (lemma "plus_up" )"1" (inst -1 "rev(p!1)" "rev(q!1)" "t!1" "s!1" )"1" (lemma "path?_trunc1" )"1" (inst-cp -1 "G!1" "rev(p!1)" )"1" (inst -1 "G!1" "rev(q!1)" )"1" (lemma "walk_from_l" )"1" (inst-cp -1 "p!1" "s!1" "t!1" )"1" (inst -1 "q!1" "s!1" "t!1" )"1" (expand "path_from?" )"1" (expand "trunc1" )"1" (assert )"1" (flatten)"1" assert )"1" "ind_rev_rev" )"1" "p!1" )"1" "q!1" )"1" "index_rev" )"1" "p!1" )"1" "q!1" )"1" assert )"1" "1" expand "from?" -17)"1" expand "from?" "1" "path?_rev" )"1" "G!1" "p!1" )"1" "G!1" "q!1" )"1" "rev_eq" )"1" "p!1" "q!1" )"1" assert )"1" "from_rev" )"1" assert )"1" "p!1" "s!1" "t!1" )"1" "q!1" "s!1" "t!1" )"1" assert )"1" expand "finseq_appl" )"1" assert )"1" "1" "1" "1" assert )"1" nil nil ))nil )"2" assert )"2" nil nil ))nil )"3" assert )nil nil )"4" assert )nil nil )"5" nil nil )"6" 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" (assert ) (("2" (grind) nil nil )) nil ))nil )"2" (grind) nil nil ))nil ))nil )"2" (grind) nil nil ) ("3" (grind) nil nil ))nil ))nil )"2" (grind) nil nil ) ("3" (grind) nil nil )"4" (grind) nil nil ) ("5" (grind) nil nil ))nil ))nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"prewalk[T]" path_circ nil )nil walks nil )"bool" reals nil )nil finite_sequences nil )nil path_circ nil )nil nat_types nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 )"finseq[T]" doubletons nil )"finseq" finite_sequences nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"prewalk[T]" path_circ 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 path_circ nil )"prewalk" walks nil )nil path_circ nil )"bool" walks nil )nil paths nil )nil path_circ nil )"posint" nil )"{k: int | k <= i AND k <= j}" nil )"int" integers nil )nil application-judgement "finite_set[T]" path_circ nil )"bool" paths nil )"bool" walks nil )"bool" graphs nil )"bool" walks nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil path_circ nil )nil path_circ nil )"bool" paths nil )nil paths nil )nil path_circ nil )nil naturalnumbers nil )"bool" reals nil )"finseq" finite_sequences nil ))nil ))nil 3330871439 ("" (subtype-tcc) nil nil ) nil nil ))nil 3330871439 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil path_circ 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 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" walks nil )nil walks nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil ))nil ))nil 3330871439 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil path_circ 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 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" walks nil )nil walks nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set[T]" path_circ nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"(total_order?[real])" nil )"graph[T]" path_circ nil )"boolean" notequal nil ))nil ))nil 3330871463"" (skosimp*)"" (install-rewrites "walks[T]" )"" (assert )"" (grind)"" (apply-extensionality 2 :hide? t)"1" (install-rewrites "walks[T]" )"1" (lift-if 1)"1" (case "x!2<length(w!1)" )"1" (prop)"1" (case "x!2<length(w!1)-1" )"1" (assert ) nil nil )"2" (lift-if 2) (("2" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"graph[T]" path_circ nil )"Seq[T](G!1)" path_circ nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil naturalnumbers nil )nil walks nil )"bool" walks nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil walks nil )"bool" reals nil )nil finite_sequences nil )nil nat_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans 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 booleans nil )nil numbers nil )nil path_circ nil )"prewalk" walks nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"prewalk" walks nil )"Seq(G)" walks nil )"finseq[T]" doubletons nil )"finseq" finite_sequences nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"posint" nil )"posint" nil )"(total_order?[real])" nil )"{k: int | k <= i AND k <= j}" nil )"int" integers nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.61 Sekunden
(vorverarbeitet am 2026-04-28)
¤ *© Formatika GbR, Deutschland
2026-05-26
