| products/sources/formale sprachen/Isabelle/ZF/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: topology.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(tree_paths
(dual_paths?_TCC1 0 (dual_paths?_TCC1-1 nil 3253637114 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (dual_paths?_TCC2 0 (dual_paths?_TCC2-1 nil 3253637114 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (dual_paths?_TCC3 0 (dual_paths?_TCC3-1 nil 3253637114 ("" (subtype-tcc) nil nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil)) nil)) (dual_paths?_TCC4 0 (dual_paths?_TCC4-1 nil 3253637114 ("" (subtype-tcc) nil nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil)) nil)) (min_dual_paths_TCC1 0 (min_dual_paths_TCC1-1 nil 3253637114 ("" (skolem-typepred) (("" (inst + "(r!1,s!1)") nil nil)) nil) ((dual_paths? const-decl "bool" tree_paths nil) (Path type-eq-decl nil paths nil) (path? const-decl "bool" paths nil) (prewalk type-eq-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (Graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil) (graph type-eq-decl nil graphs nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil tree_paths nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (min_dual_paths_TCC2 0 (min_dual_paths_TCC2-1 nil 3253637114 ("" (skolem-typepred) (("" (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)): dual_paths?(G!1, r, s)]") (("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) (minimal? const-decl "bool" abstract_min nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (dual_paths? const-decl "bool" tree_paths nil) (Path type-eq-decl nil paths nil) (path? const-decl "bool" paths nil) (prewalk type-eq-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (Graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil) (graph type-eq-decl nil graphs nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil tree_paths nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (min_dual_def 0 (min_dual_def-1 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") (("" (typepred "min[[Path(G!1), Path(G!1)], LAMBDA (r: Path(G!1), s_2847: Path(G!1)): length(r) + length(s_2847), LAMBDA (r: Path(G!1), s_2848: Path(G!1)): dual_paths?(G!1, r, s_2848)]") (("1" (name-replace minp "min[[Path(G!1), Path(G!1)], LAMBDA (r: Path(G!1), s_2847: Path(G!1)): length(r) + length(s_2847), LAMBDA (r: Path(G!1), s_2848: Path(G!1)): dual_paths?(G!1, r, s_2848)]") (("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) ((min_dual_paths const-decl "Dual_paths(G)" tree_paths nil) (Dual_paths type-eq-decl nil tree_paths nil) (dual_paths? const-decl "bool" tree_paths nil) (is_min_dual? const-decl "bool" tree_paths nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (min const-decl "{S: T | minimal?(S)}" abstract_min nil) (minimal? const-decl "bool" abstract_min nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Path type-eq-decl nil paths nil) (path? const-decl "bool" paths nil) (prewalk type-eq-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (Graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil) (graph type-eq-decl nil graphs nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil tree_paths nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (min_dual_exists 0 (min_dual_exists-1 nil 3312299029 ("" (skosimp*) (("" (inst 1 "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) ((s!1 skolem-const-decl "Path[T](G!1)" tree_paths nil) (r!1 skolem-const-decl "Path[T](G!1)" tree_paths nil) (G!1 skolem-const-decl "Graph[T]" tree_paths nil) (Graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil) (dual_paths? const-decl "bool" tree_paths nil) (Path type-eq-decl nil paths nil) (path? const-decl "bool" paths nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (graph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil tree_paths nil) (Dual_paths type-eq-decl nil tree_paths nil) (min_dual_paths const-decl "Dual_paths(G)" tree_paths nil) (min_dual_def formula-decl nil tree_paths nil)) nil)) (dual_path_trunc_TCC1 0 (dual_path_trunc_TCC1-1 nil 3312299267 ("" (skosimp*) (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (dual_path_trunc_TCC2 0 (dual_path_trunc_TCC2-1 nil 3312299267 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil tree_paths nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil) (Graph type-eq-decl nil graphs nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks nil) (path? const-decl "bool" paths nil) (Path type-eq-decl nil paths nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (verts_in? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nil application-judgement "finite_set[T]" tree_paths nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (dual_paths? const-decl "bool" tree_paths nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (dual_path_trunc_TCC3 0 (dual_path_trunc_TCC3-1 nil 3312299267 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl 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) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil) (Graph type-eq-decl nil graphs nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks nil) (Path type-eq-decl nil paths nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T formal-type-decl nil tree_paths nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (dual_paths? const-decl "bool" tree_paths nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nil application-judgement "finite_set[T]" tree_paths nil)) nil)) (dual_path_trunc_TCC4 0 (dual_path_trunc_TCC4-1 nil 3312299267 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl 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) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil) (Graph type-eq-decl nil graphs nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks nil) (Path type-eq-decl nil paths nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T formal-type-decl nil tree_paths nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (dual_paths? const-decl "bool" tree_paths nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nil application-judgement "finite_set[T]" tree_paths nil)) nil)) (dual_path_trunc_TCC5 0 (dual_path_trunc_TCC5-1 nil 3312299267 ("" (subtype-tcc) nil nil) ((T formal-type-decl nil tree_paths nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (dual_paths? const-decl "bool" tree_paths nil) (nil application-judgement "finite_set[T]" tree_paths nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (dual_path_trunc_TCC6 0 (dual_path_trunc_TCC6-1 nil 3312299267 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl 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) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil) (Graph type-eq-decl nil graphs nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks nil) (Path type-eq-decl nil paths nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T formal-type-decl nil tree_paths nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (dual_paths? const-decl "bool" tree_paths nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nil application-judgement "finite_set[T]" tree_paths nil)) nil)) (dual_path_trunc_TCC7 0 (dual_path_trunc_TCC7-1 nil 3312299267 ("" (subtype-tcc) nil nil) ((T formal-type-decl nil tree_paths nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (dual_paths? const-decl "bool" tree_paths nil) (nil application-judgement "finite_set[T]" tree_paths nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (dual_path_trunc_TCC8 0 (dual_path_trunc_TCC8-1 nil 3312299267 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl 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) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil) (Graph type-eq-decl nil graphs nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks nil) (Path type-eq-decl nil paths nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T formal-type-decl nil tree_paths nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (dual_paths? const-decl "bool" tree_paths nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nil application-judgement "finite_set[T]" tree_paths nil)) nil)) (dual_path_trunc 0 (dual_path_trunc-2 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" (inst -3 "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" (flatten) (("1" (case "length(q!1)=1") (("1" (apply-extensionality 2 :hide? t) (("1" (apply-extensionality 1 :hide? t) (("1" (grind) nil))))) ("2" (assert) nil))))))))))))))))))))))))) ("2" (assert) nil)))))))) nil) ((Path type-eq-decl nil paths nil) (Graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil) (path? const-decl "bool" paths nil) (graph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (prewalk type-eq-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil tree_paths nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (dual_paths? const-decl "bool" tree_paths nil) (path?_caret formula-decl nil paths nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (G!1 skolem-const-decl "Graph[T]" tree_paths nil) (q!1 skolem-const-decl "Path[T](G!1)" tree_paths nil) (p!1 skolem-const-decl "Path[T](G!1)" tree_paths nil) (nil application-judgement "finite_set[T]" tree_paths nil) (walk? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (verts_in? const-decl "bool" walks nil)) nil) (dual_path_trunc-1 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) (("" (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" (delete -5 -6) (("1" (delete 3 4) (("1" (apply-extensionality 1 :hide? t) (("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" (lemma "path_one") (("4" (inst -1 "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" (propax) nil)))))))))))))))))))))))))))))))))))))) nil) nil nil)) (dual_path_length 0 (dual_path_length-2 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" (inst -1 "p!1" "q!1" "seq(p!1)(0)" "seq(p!1)(length(p!1)-1)") (("1" (assert) (("1" (prop) (("1" (expand "trunc1") (("1" (decompose-equality 1) (("1" (expand* "^" "min") (("1" (assert) nil nil)) nil) ("2" (decompose-equality 1) (("2" (typepred "x!1") (("2" (expand* "^" "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "path_one") (("2" (inst -1 "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" (flatten) (("2" (expand "cyclically_reduced?") (("2" (propax) 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) ((T formal-type-decl nil tree_paths nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil) (Graph type-eq-decl nil graphs nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (path? const-decl "bool" paths nil) (Path type-eq-decl nil paths nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (dual_paths? const-decl "bool" tree_paths nil) (plus_up formula-decl nil path_circ nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "finseq" finite_sequences nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (trunc1 const-decl "prewalk" walks nil) (from? const-decl "bool" walks nil) (path_from? const-decl "bool" paths nil) (cyclically_reduced? const-decl "bool" circuits nil) (circuit? const-decl "bool" circuits nil) (path_one formula-decl nil path_circ nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (int_minus_int_is_int application-judgement "int" integers nil) (dual_path_trunc formula-decl nil tree_paths nil)) nil) (dual_path_length-1 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) (("" (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" (delete -5 -6) (("1" (delete 3 4) (("1" (apply-extensionality 1 :hide? t) (("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" (lemma "path_one") (("4" (inst -1 "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) ((dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (Graph type-eq-decl nil graphs nil) (prewalk type-eq-decl nil walks nil) (path? const-decl "bool" paths nil) (Path type-eq-decl nil paths nil) (path_one formula-decl nil path_circ nil) (verts_in? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (reducible? const-decl "bool" circuits nil) (reduced? const-decl "bool" circuits nil) (cyclically_reduced? const-decl "bool" circuits nil) (pre_circuit? const-decl "bool" walks nil) (circuit? const-decl "bool" circuits nil) (path_from? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (trunc1 const-decl "prewalk" walks nil) (plus_up formula-decl nil path_circ nil)) nil)) (min_dual_reduc_TCC1 0 (min_dual_reduc_TCC1-2 nil 3312300142 ("" (skosimp*) (("" (expand "is_min_dual?") (("" (flatten) (("" (lemma "dual_path_trunc") (("" (inst? -1) (("" (bddsimp (-1 -2)) (("" (assert) nil)))))))))))) nil) ((is_min_dual? const-decl "bool" tree_paths nil) (dual_path_trunc formula-decl nil tree_paths nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Path type-eq-decl nil paths nil) (path? const-decl "bool" paths nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil) (graph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil tree_paths nil)) nil) (min_dual_reduc_TCC1-1 nil 3312299267 ("" (subtype-tcc) nil nil) nil nil)) (min_dual_reduc_TCC2 0 (min_dual_reduc_TCC2-3 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) ((is_min_dual? const-decl "bool" tree_paths nil) (dual_path_trunc formula-decl nil tree_paths nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Path type-eq-decl nil paths nil) (path? const-decl "bool" paths nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil) (graph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil tree_paths nil)) nil) (min_dual_reduc_TCC2-2 nil 3312300182 ("" (skolem-typepred) (("" (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)): dual_paths?(G!1, r, s)]") (("1" (assert) (("1" (expand "minimal?") (("1" (propax) nil))))) ("2" (hide 2) (("2" (inst + "(r!1,s!1)") nil)))))) nil) nil nil) (min_dual_reduc_TCC2-1 nil 3312299267 ("" (subtype-tcc) nil nil) nil nil)) (min_dual_reduc_TCC3 0 (min_dual_reduc_TCC3-2 nil 3312300261 ("" (skosimp*) (("" (expand "finseq_appl") (("" (expand "is_min_dual?") (("" (flatten) (("" (lemma "dual_path_trunc") (("" (inst? -1) (("" (bddsimp (-1 -2)) (("" (assert) nil)))))))))))))) nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (T formal-type-decl nil tree_paths nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil) (Graph type-eq-decl nil graphs nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (path? const-decl "bool" paths nil) (Path type-eq-decl nil paths nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (dual_path_trunc formula-decl nil tree_paths nil) (is_min_dual? const-decl "bool" tree_paths nil)) nil) (min_dual_reduc_TCC3-1 nil 3312299267 ("" (subtype-tcc) nil nil) nil nil)) (min_dual_reduc_TCC4 0 (min_dual_reduc_TCC4-2 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) ((is_min_dual? const-decl "bool" tree_paths nil) (dual_path_trunc formula-decl nil tree_paths nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Path type-eq-decl nil paths nil) (path? const-decl "bool" paths nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil) (graph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil tree_paths nil)) nil) (min_dual_reduc_TCC4-1 nil 3312299267 ("" (subtype-tcc) nil nil) nil nil)) (min_dual_reduc 0 (min_dual_reduc-1 nil 3312299362 ("" (skosimp*) (("" (expand "finseq_appl") (("" (lemma "dual_path_trunc") (("" (inst? -1) (("" (inst -1 "q!1") (("" (expand "is_min_dual?") (("" (flatten) (("" (bddsimp (-1 -2)) (("" (inst -8 "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" (flatten) (("3" (hide -5 -6 -7 -8) (("3" (install-rewrites "walks[T]") (("3" (apply-extensionality 1) (("3" (apply-extensionality 1 :hide? t) (("3" (flatten) (("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" (hide -7) (("1" (beta -1) (("1" (propax) nil nil)) nil)) nil) ("2" (replace -6 1 lr) (("2" (propax) nil nil)) nil) ("3" (typepred "x!1") (("3" (replace -6 -1 lr) (("3" (case "x!1=length(q!1)-1") (("1" (replace -1 2 lr) (("1" (replace -7 -4 lr) (("1" (propax) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("4" (typepred "x!1") (("4" (case "x!1=length(p!1)-1") (("1" (replace -1 2 lr) (("1" (replace -7 -4 rl) (("1" (propax) 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" (reveal -1) (("1" (inst -1 "p!1^(1,length(p!1)-1)" "q!1^(1,length(q!1)-1)") (("1" (bddsimp) (("1" (hide -6 -7 -8 -9) (("1" (install-rewrites "walks[T]") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "dual_paths?") (("2" (expand "finseq_appl") (("2" (bddsimp) (("1" (expand "^" 1) (("1" (expand "min") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "^" 1) (("2" (propax) nil nil)) nil) ("3" (flatten) (("3" (hide -6 -7 -8 -9) (("3" (install-rewrites "walks[T]") (("3" (assert) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.602 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
