| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/graphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 4 MB |
|
Quellcode-Bibliothek mappings.prfSprache: Lisp |
|||||||||||||||
|
(mappings (reachable_TCC1 0 (reachable_TCC1-1 nil 3318087528 ("" (skosimp*) (("" (typepred "vert(G!1)") (("" (lemma "finite_subset[T]") (("" (inst -1 "vert(G!1)" "{y: T | vert(G!1)(y) AND (EXISTS (w: Seq[T](G!1)): walk_from?[T](G!1, w, x!1, y))}") (("" (bddsimp) (("" (hide 2) (("" (expand "subset?") (("" (expand "member") (("" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil mappings nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans 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) (verts_in? const-decl "bool" walks nil) (Seq type-eq-decl nil walks nil) (walk_from? const-decl "bool" walks nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (finite_subset formula-decl nil finite_sets nil)) nil)) (reachable_subset 0 (reachable_subset-1 nil 3318087528 ("" (grind) 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (T formal-type-decl nil mappings nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (reachable const-decl "finite_set[T]" mappings nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (nil application-judgement "finite_set[T]" mappings nil)) nil)) (path_reach1 0 (path_reach1-2 "Valid3.2" 3318377422 ("" (skosimp*) (("" (split) (("1" (flatten) (("1" (expand "path_connected?" -1) (("1" (skosimp*) (("1" (expand "empty?" 1) (("1" (expand "empty?" 1) (("1" (skosimp*) (("1" (inst 1 "x!1") (("1" (expand "member" -1) (("1" (expand "reachable" 1) (("1" (split) (("1" (propax) nil nil) ("2" (apply-extensionality 1) (("2" (hide 2) (("2" (iff) (("2" (split) (("1" (bddsimp) nil nil) ("2" (flatten) (("2" (split) (("1" (propax) nil nil) ("2" (inst -3 "x!1" "x!2") (("2" (skosimp*) (("2" (inst 1 "w!1") (("1" (expand "walk_from?" 1) (("1" (assert) nil nil)) nil) ("2" (grind) (("2" (typepred "w!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "path_connected?") (("2" (skosimp*) (("2" (split) (("1" (expand "empty?") (("1" (expand "empty?") (("1" (inst -1 "x!1") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "reachable") (("2" (typepred "y!1") (("2" (typepred "x!2") (("2" (lemma "extensionality_postulate[T,bool]") (("2" (inst -1 "({y: T | vert(G!1)(y) AND (EXISTS (w: Seq(G!1)):walk_from?(G!1, w, x!1, y))})" "vert(G!1)") (("2" (flatten) (("2" (bddsimp -2 -6) (("1" (hide -2) (("1" (hide -5) (("1" (inst-cp -1 "x!2") (("1" (bddsimp -2 -3) (("1" (skolem! -1) (("1" (inst -2 "y!1") (("1" (beta -2) (("1" (bddsimp) (("1" (skolem! -2) (("1" (lemma "walk?_reverse") (("1" (inst-cp -1 "G!1" "x!1" "y!1" "w!2") (("1" (inst -1 "G!1" "x!1" "x!2" "w!1") (("1" (bddsimp) (("1" (hide -1 -3) (("1" (skolem!) (("1" (skolem! -2) (("1" (lemma "walk_merge") (("1" (inst -1 "G!1" "w!4" "w!3" "x!2" "y!1" "x!1") (("1" (bddsimp) (("1" (hide -1 -2) (("1" (expand "walk_from?" -1) (("1" (assert) (("1" (skolem! -1) (("1" (expand "walk?" -1) (("1" (expand "finseq_appl") (("1" (inst 1 "p!1") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "walk?" 1) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((path_connected? const-decl "bool" graph_conn_defs nil) (empty? const-decl "bool" graphs nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nil application-judgement "finite_set[T]" mappings nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (edge? const-decl "bool" graphs nil) (int_minus_int_is_int application-judgement "int" integers nil) (w!1 skolem-const-decl "Walk[T](G!1)" mappings nil) (Walk type-eq-decl nil walks nil) (walk? const-decl "bool" walks nil) (x!2 skolem-const-decl "T" mappings nil) (G!1 skolem-const-decl "graph[T]" mappings nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets 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) (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) (verts_in? const-decl "bool" walks nil) (Seq type-eq-decl nil walks nil) (walk_from? const-decl "bool" walks nil) (boolean nonempty-type-decl nil booleans nil) (reachable const-decl "finite_set[T]" mappings nil) (T formal-type-decl nil mappings nil) (empty? const-decl "bool" sets nil) (walk?_reverse formula-decl nil walks nil) (p!1 skolem-const-decl "prewalk[T]" mappings nil) (nil application-judgement "finite_set[T]" graphs nil) (walk_merge formula-decl nil walks nil) (extensionality_postulate formula-decl nil functions nil)) shostak) (path_reach1-1 nil 3318087528 ("" (skosimp*) (("" (split) (("1" (flatten) (("1" (expand "path_connected?" -1) (("1" (skosimp*) (("1" (expand "empty?" 1) (("1" (expand "empty?" 1) (("1" (skosimp*) (("1" (inst 1 "x!1") (("1" (expand "member" -1) (("1" (expand "reachable" 1) (("1" (split) (("1" (propax) nil nil) ("2" (apply-extensionality 1) (("2" (hide 2) (("2" (iff) (("2" (split) (("1" (bddsimp) nil nil) ("2" (flatten) (("2" (split) (("1" (propax) nil nil) ("2" (inst -3 "x!1" "x!2") (("2" (skosimp*) (("2" (inst 1 "w!1") (("1" (expand "walk_from?" 1) (("1" (assert) nil nil)) nil) ("2" (grind) (("2" (typepred "w!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "path_connected?") (("2" (skosimp*) (("2" (split) (("1" (expand "empty?") (("1" (expand "empty?") (("1" (inst -1 "x!1") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "reachable") (("2" (typepred "y!1") (("2" (typepred "x!2") (("2" (lemma "extensionality_postulate[T,bool]") (("2" (inst -1 "({y: T | vert(G!1)(y) AND (EXISTS (w: Seq(G!1)):walk_from?(G!1, w, x!1, y))})" "vert(G!1)") (("2" (flatten) (("2" (bddsimp -2 -6) (("1" (hide -2) (("1" (hide -5) (("1" (inst-cp -1 "x!2") (("1" (bddsimp -2 -3) (("1" (beta -1) (("1" (bddsimp) (("1" (skolem! -1) (("1" (inst -3 "y!1") (("1" (beta -3) (("1" (bddsimp -3) (("1" (skolem! -1) (("1" (lemma "walk?_reverse") (("1" (inst-cp -1 "G!1" "x!1" "y!1" "w!2") (("1" (inst -1 "G!1" "x!1" "x!2" "w!1") (("1" (bddsimp) (("1" (hide -1 -3) (("1" (skolem!) (("1" (skolem! -2) (("1" (lemma "walk_merge") (("1" (inst -1 "G!1" "w!4" "w!3" "x!2" "y!1" "x!1") (("1" (bddsimp) (("1" (hide -1 -2) (("1" (expand "walk_from?" -1) (("1" (assert) (("1" (skolem! -1) (("1" (expand "walk?" -1) (("1" (expand "finseq_appl") (("1" (inst 1 "p!1") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "walk?" 1) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((path_connected? const-decl "bool" graph_conn_defs nil) (empty? const-decl "bool" graphs nil) (edge? const-decl "bool" graphs nil) (Walk type-eq-decl nil walks nil) (walk? const-decl "bool" walks 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) (prewalk type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (Seq type-eq-decl nil walks nil) (walk_from? const-decl "bool" walks nil) (walk?_reverse formula-decl nil walks nil) (walk_merge formula-decl nil walks nil)) nil)) (path_reach2 0 (path_reach2-1 nil 3318087528 ("" (skosimp*) (("" (split) (("1" (flatten) (("1" (expand "path_connected?" -1) (("1" (skosimp*) (("1" (expand "empty?" 1) (("1" (expand "empty?" 1) (("1" (expand "member" 1) (("1" (skosimp*) (("1" (expand "reachable" 1) (("1" (split) (("1" (skosimp*) (("1" (apply-extensionality 1) (("1" (hide 2) (("1" (iff 1) (("1" (split) (("1" (bddsimp) nil nil) ("2" (bddsimp) (("2" (inst -4 "x!2" "x!3") (("2" (expand "walk_from?" +) (("2" (grind) (("2" (typepred "w!1") (("2" (expand "walk?" -2) (("2" (flatten) (("2" (expand "verts_in?" -2) (("2" (inst -2 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "path_reach1") (("2" (inst -1 "G!1") (("2" (flatten) (("2" (hide -1) (("2" (copy 2) (("2" (expand "path_connected?" 1) (("2" (split) (("1" (propax) nil nil) ("2" (expand "empty?" 2) (("2" (expand "empty?" 2) (("2" (hide 1) (("2" (skosimp*) (("2" (expand "member" -) (("2" (inst -2 "x!1") (("2" (bddsimp) (("2" (inst 1 "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((path_connected? const-decl "bool" graph_conn_defs nil) (empty? const-decl "bool" graphs nil) (member const-decl "bool" sets nil) (reachable const-decl "finite_set[T]" mappings nil) (G!1 skolem-const-decl "graph[T]" mappings nil) (x!3 skolem-const-decl "T" mappings nil) (walk? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (nil application-judgement "finite_set[T]" mappings nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (Walk type-eq-decl nil walks 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (w!1 skolem-const-decl "Walk[T](G!1)" mappings nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets 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) (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) (verts_in? const-decl "bool" walks nil) (Seq type-eq-decl nil walks nil) (walk_from? const-decl "bool" walks nil) (T formal-type-decl nil mappings nil) (boolean nonempty-type-decl nil booleans nil) (empty? const-decl "bool" sets nil) (path_reach1 formula-decl nil mappings nil)) nil)) (reachable_conn 0 (reachable_conn-2 "V3.2 ran" 3319386050 ("" (skosimp*) (("" (lemma "conn_eq_path[T]") (("" (inst -1 "subgraph(G!1, reachable(G!1, x!1))") (("" (iff -1) (("" (bddsimp) (("" (hide 1) (("" (expand "path_connected?") (("" (bddsimp) (("1" (install-rewrites "subgraphs") (("1" (assert) (("1" (inst -1 "x!1") (("1" (bddsimp) (("1" (inst 1 "(#length := 1, seq :=(LAMBDA (i:below(1)): x!1)#)") (("1" (assert) nil nil)) nil) ("2" (typepred "x!1") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "x!2") (("2" (typepred "y!1") (("2" (expand "subgraph" -) (("2" (flatten) (("2" (expand "reachable" -) (("2" (bddsimp) (("2" (skosimp*) (("2" (lemma "walk?_reverse") (("2" (inst-cp -1 "G!1" "x!1" "y!1" "w!1") (("2" (inst -1 "G!1" "x!1" "x!2" "w!2") (("2" (bddsimp) (("2" (skosimp*) (("2" (lemma "walk_merge") (("2" (inst -1 "G!1" "w!4" "w!3" "x!2" "y!1" "x!1") (("2" (bddsimp) (("2" (skosimp*) (("2" (inst 1 "p!1") (("1" (install-rewrites "walks") (("1" (assert) (("1" (bddsimp) nil nil)) nil)) nil) ("2" (assert) (("2" (install-rewrites "walks") (("2" (assert) (("2" (skosimp*) (("2" (bddsimp) (("1" (skosimp*) (("1" (bddsimp) (("1" (typepred "p!1") (("1" (inst -11 "n!1") (("1" (bddsimp) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst-cp -9 "n!1") (("1" (inst -9 "1+n!1") (("1" (hide -3 -4 -5 -6) (("1" (bddsimp (-2 -5 -6 1)) (("1" (hide -8 -9 -11 -12) (("1" (reveal -10 -11) (("1" (reveal (-1 -2 -7 -8)) (("1" (lemma "walk?_caret") (("1" (inst -1 "G!1" "0" "n!1" "p!1") (("1" (stop-rewrite) (("1" (assert) (("1" (case "walk?(G!1,p!1)") (("1" (bddsimp) (("1" (inst -8 "G!1" "x!2" "x!3" "p!1 ^ (0, n!1)") (("1" (expand "walk_from?" -8) (("1" (expand "^" -8 (1 2 3)) (("1" (bddsimp (-2 -8)) (("1" (skosimp*) (("1" (inst -9 "G!1" "w!5" "w!2" "x!1" "x!3" "x!2") (("1" (expand "walk_from?" -9 (1 2)) (("1" (typepred "w!2") (("1" (case "walk?(G!1,w!2)") (("1" (bddsimp) (("1" (skosimp*) (("1" (inst 1 "p!2") (("1" (expand "walk_from?" -12) (("1" (flatten) (("1" (expand "walk?" -14) (("1" (flatten) (("1" (hide-all-but (-4 -7 -12 -13 -14 -15 -25 -26) -) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but -12 -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -7 -8 -19) -) (("2" (hide 2) (("2" (install-rewrites "walks") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-8 1)) (("2" (expand "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal -10) (("2" (hide (-16 -17)) (("2" (hide-all-but (-1 -9 -12 -13 -14 -15) -) (("2" (hide 2) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -3) -) (("2" (assert) nil nil)) nil) ("3" (reveal -6 -7) (("3" (lemma "walk?_caret") (("3" (inst -1 "G!1" "0" "1+n!1" "p!1") (("3" (inst -3 "G!1" "x!2" "x!3" "p!1 ^ (0, 1 + n!1)") (("1" (typepred "n!1") (("1" (bddsimp (-1 -2 -4 -5 -8)) (("1" (skosimp*) (("1" (inst -6 "G!1" "w!5" "w!2" "x!1" "x!3" "x!2") (("1" (hide-all-but (-3 -6 -12 -13 -14) -) (("1" (typepred "w!2") (("1" (case "walk_from?(G!1, w!2, x!1, x!2)") (("1" (bddsimp (-1 -4 -5)) (("1" (skosimp*) (("1" (inst 1 "p!2") (("1" (hide-all-but -3 -) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but -3 -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 -5 -6 -7) -) (("2" (hide 2) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide (-5 -11 -12 -13 -14 -15 -16 -17 -18)) (("2" (assert) (("2" (bddsimp) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (hide -2 -5 -11 -12 -13 -14 -15 -16) (("3" (assert) (("3" (bddsimp) (("3" (typepred "p!1") (("3" (reveal -13) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide -4 -12 -15 3) (("4" (reveal -8) (("4" (hide 2) (("4" (assert) (("4" (bddsimp) nil nil)) nil)) nil)) nil)) nil) ("5" (assert) nil nil) ("6" (assert) nil nil) ("7" (assert) nil nil) ("8" (assert) nil nil)) nil)) nil) ("2" (hide -2 -9 -12 -15 2) (("2" (hide -1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (assert (-1 -2 1)) nil nil)) nil)) nil) ("2" (assert (-1 1)) nil nil)) nil) ("2" (assert (-1 1)) nil nil)) nil)) nil) ("3" (inst -9 "n!1") (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -7 "i!1") (("2" (bddsimp) (("2" (lemma "walk?_caret") (("2" (inst -1 "G!1" "0" "i!1" "p!1") (("2" (typepred "i!1") (("2" (reveal -4) (("2" (inst -1 "G!1" "x!2" "seq(p!1)(i!1)" "p!1 ^ (0, i!1)") (("1" (case "walk?(G!1,p!1)") (("1" (bddsimp (-1 -3 -4)) (("1" (expand "walk_from?" -4 1) (("1" (expand "^" -4 (1 2)) (("1" (expand "^" -4 1) (("1" (bddsimp (-3 -4 -10)) (("1" (skosimp*) (("1" (reveal -3) (("1" (inst -1 "G!1" "w!5" "w!2" "x!1" "seq(p!1)(i!1)" "x!2") (("1" (case "walk_from?(G!1, w!2, x!1, x!2)") (("1" (bddsimp (-1 -2 -5)) (("1" (skosimp*) (("1" (inst 1 "p!2") (("1" (hide-all-but -3 -) (("1" (grind) nil nil)) nil) ("2" (typepred "p!2") (("2" (hide-all-but (-1 -4) -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "walk_from?" 1) (("2" (hide-all-but (-14 -15 -16) -) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (reveal -2) (("2" (hide-all-but (-1 -10 -11 -12) -) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (reveal -2) (("2" (hide-all-but (-1 -10 -11 -12) -) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "^" 1) (("2" (expand "min" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil mappings nil) (conn_eq_path formula-decl nil graph_connected nil) (nil application-judgement "finite_set[T]" mappings nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (empty? const-decl "bool" graphs nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (Seq type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (walk_merge formula-decl nil walks nil) (G!1 skolem-const-decl "graph[T]" mappings nil) (x!1 skolem-const-decl "(vert(G!1))" mappings nil) (p!1 skolem-const-decl "prewalk[T]" mappings nil) (nil application-judgement "finite_set[T]" graphs nil) (int_minus_int_is_int application-judgement "int" integers nil) (p!2 skolem-const-decl "prewalk[T]" mappings nil) (i!1 skolem-const-decl "below(length(p!1))" mappings nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (walk?_caret formula-decl nil walks nil) (^ const-decl "finseq" finite_sequences nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (p!2 skolem-const-decl "prewalk[T]" mappings nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (p!2 skolem-const-decl "prewalk[T]" mappings nil) (n!1 skolem-const-decl "nat" mappings nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Walk type-eq-decl nil walks nil) (walk?_reverse formula-decl nil walks nil) (path_connected? const-decl "bool" graph_conn_defs nil) (reachable const-decl "finite_set[T]" mappings nil) (is_finite const-decl "bool" finite_sets nil) (subgraph const-decl "Subgraph(G)" subgraphs nil) (Subgraph type-eq-decl nil subgraphs nil) (subgraph? const-decl "bool" subgraphs 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)) shostak) (reachable_conn-1 nil 3318087528 ("" (skosimp*) (("" (lemma "conn_eq_path") (("" (inst -1 "subgraph(G!1, reachable(G!1, x!1))") (("" (iff -1) (("" (bddsimp) (("" (hide 1) (("" (expand "path_connected?") (("" (bddsimp) (("1" (install-rewrites "subgraphs") (("1" (assert) (("1" (inst -1 "x!1") (("1" (bddsimp) (("1" (inst 1 "(#l := 1, seq :=(LAMBDA (i:below(1)): x!1)#)") (("1" (assert) nil nil)) nil) ("2" (typepred "x!1") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "x!2") (("2" (typepred "y!1") (("2" (expand "subgraph" -) (("2" (flatten) (("2" (expand "reachable" -) (("2" (bddsimp) (("2" (skosimp*) (("2" (lemma "walk?_reverse") (("2" (inst-cp -1 "G!1" "x!1" "y!1" "w!1") (("2" (inst -1 "G!1" "x!1" "x!2" "w!2") (("2" (bddsimp) (("2" (skosimp*) (("2" (lemma "walk_merge") (("2" (inst -1 "G!1" "w!4" "w!3" "x!2" "y!1" "x!1") (("2" (bddsimp) (("2" (skosimp*) (("2" (inst 1 "p!1") (("1" (install-rewrites "walks") (("1" (assert) (("1" (bddsimp) nil nil)) nil)) nil) ("2" (assert) (("2" (install-rewrites "walks") (("2" (assert) (("2" (skosimp*) (("2" (bddsimp) (("1" (skosimp*) (("1" (bddsimp) (("1" (typepred "p!1") (("1" (inst -11 "n!1") (("1" (bddsimp) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst-cp -9 "n!1") (("1" (inst -9 "1+n!1") (("1" (hide -3 -4 -5 -6) (("1" (bddsimp (-2 -5 -6 1)) (("1" (hide -8 -9 -11 -12) (("1" (reveal -10 -11) (("1" (reveal (-1 -2 -7 -8)) (("1" (lemma "walk?_caret") (("1" (inst -1 "G!1" "0" "n!1" "p!1") (("1" (stop-rewrite) (("1" (assert) (("1" (case "walk?(G!1,p!1)") (("1" (bddsimp) (("1" (inst -8 "G!1" "x!2" "x!3" "p!1 ^ (0, n!1)") (("1" (expand "walk_from?" -8) (("1" (expand "^" -8 (1 2 3)) (("1" (bddsimp (-2 -8)) (("1" (skosimp*) (("1" (inst -9 "G!1" "w!5" "w!2" "x!1" "x!3" "x!2") (("1" (expand "walk_from?" -9 (1 2)) (("1" (typepred "w!2") (("1" (case "walk?(G!1,w!2)") (("1" (bddsimp) (("1" (skosimp*) (("1" (inst 1 "p!2") (("1" (expand "walk_from?" -12) (("1" (flatten) (("1" (expand "walk?" -14) (("1" (flatten) (("1" (hide-all-but (-4 -7 -12 -13 -14 -15 -25 -26) -) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but -12 -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -7 -8 -19) -) (("2" (hide 2) (("2" (install-rewrites "walks") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 -8 -9 -10 -11 -13) -) (("2" (hide 2) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal -10) (("2" (hide (-16 -17)) (("2" (hide-all-but (-1 -9 -12 -13 -14 -15) -) (("2" (hide 2) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -3) -) (("2" (assert) nil nil)) nil) ("3" (reveal -6 -7) (("3" (lemma "walk?_caret") (("3" (inst -1 "G!1" "0" "1+n!1" "p!1") (("3" (inst -3 "G!1" "x!2" "x!3" "p!1 ^ (0, 1 + n!1)") (("1" (typepred "n!1") (("1" (bddsimp (-1 -2 -4 -5 -8)) (("1" (skosimp*) (("1" (inst -6 "G!1" "w!5" "w!2" "x!1" "x!3" "x!2") (("1" (hide-all-but (-3 -6 -12 -13 -14) -) (("1" (typepred "w!2") (("1" (case "walk_from?(G!1, w!2, x!1, x!2)") (("1" (bddsimp (-1 -4 -5)) (("1" (skosimp*) (("1" (inst 1 "p!2") (("1" (hide-all-but -3 -) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but -3 -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 -5 -6 -7) -) (("2" (hide 2) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide (-5 -11 -12 -13 -14 -15 -16 -17 -18)) (("2" (assert) (("2" (bddsimp) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (hide -2 -5 -11 -12 -13 -14 -15 -16) (("3" (assert) (("3" (bddsimp) (("3" (typepred "p!1") (("3" (reveal -13) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide -4 -12 -15 3) (("4" (reveal -8) (("4" (hide 2) (("4" (assert) (("4" (bddsimp) nil nil)) nil)) nil)) nil)) nil) ("5" (assert) nil nil) ("6" (assert) nil nil) ("7" (assert) nil nil) ("8" (assert) nil nil)) nil)) nil) ("2" (hide -2 -9 -12 -15 2) (("2" (hide -1) (("2" (grind) nil nil)) nil)) nil) ("3" (assert (-6 1)) nil nil)) nil)) nil)) nil)) nil) ("4" (assert (-1 -2 1)) nil nil)) nil)) nil) ("2" (assert (-1 1)) nil nil)) nil) ("2" (assert (-1 1)) nil nil)) nil)) nil) ("3" (inst -9 "n!1") (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -7 "i!1") (("2" (bddsimp) (("2" (lemma "walk?_caret") (("2" (inst -1 "G!1" "0" "i!1" "p!1") (("2" (typepred "i!1") (("2" (reveal -4) (("2" (inst -1 "G!1" "x!2" "seq(p!1)(i!1)" "p!1 ^ (0, i!1)") (("1" (case "walk?(G!1,p!1)") (("1" (bddsimp (-1 -3 -4)) (("1" (expand "walk_from?" -4 1) (("1" (expand "^" -4 (1 2)) (("1" (expand "^" -4 1) (("1" (bddsimp (-3 -4 -10)) (("1" (skosimp*) (("1" (reveal -3) (("1" (inst -1 "G!1" "w!5" "w!2" "x!1" "seq(p!1)(i!1)" "x!2") (("1" (case "walk_from?(G!1, w!2, x!1, x!2)") (("1" (bddsimp (-1 -2 -5)) (("1" (skosimp*) (("1" (inst 1 "p!2") (("1" (hide-all-but -3 -) (("1" (grind) nil nil)) nil) ("2" (typepred "p!2") (("2" (hide-all-but (-1 -4) -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "walk_from?" 1) (("2" (hide-all-but (-14 -15 -16) -) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil) ("2" (reveal -2) (("2" (hide-all-but (-1 -10 -11 -12) -) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "^" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((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) (subgraph? const-decl "bool" subgraphs nil) (Subgraph type-eq-decl nil subgraphs nil) (subgraph const-decl "Subgraph(G)" subgraphs nil) (path_connected? const-decl "bool" graph_conn_defs nil) (walk?_reverse formula-decl nil walks nil) (Walk type-eq-decl nil walks nil) (walk?_caret formula-decl nil walks nil) (walk_merge formula-decl nil walks nil) (prewalk type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (Seq type-eq-decl nil walks nil) (empty? const-decl "bool" graphs nil) (walk_from? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (conn_eq_path formula-decl nil graph_connected nil)) nil)) (sub_tree_k 0 (sub_tree_k-1 nil 3318087528 ("" (skosimp*) (("" (inst -1 "size(G!1)-size(H!1)" "H!1" "G!1") (("1" (assert) nil nil) ("2" (lemma "subgraph_smaller") (("2" (inst -1 "G!1" "H!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (H!1 skolem-const-decl "graph[T]" mappings nil) (G!1 skolem-const-decl "graph[T]" mappings nil) (size const-decl "nat" graphs nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (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) (T formal-type-decl nil mappings nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (int_plus_int_is_int application-judgement "int" integers nil) (subgraph_smaller formula-decl nil subgraphs nil)) nil)) (sub_tree_0 0 (sub_tree_0-4 "trial" 3393153877 ("" (skosimp*) (("" (apply-extensionality 1) (("1" (apply-extensionality 1) (("1" (hide 2 3) (("1" (iff) (("1" (split) (("1" (expand "subgraph?" -) (("1" (flatten) (("1" (hide -3) (("1" (expand "subset?" -) (("1" (inst -3 "x!1") (("1" (assert) (("1" (expand "member" -) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "graph_connected[T].conn_eq_path") (("2" (inst -1 "H!1") (("2" (flatten) (("2" (iff -1) (("2" (flatten) (("2" (hide -2) (("2" (bddsimp) (("2" (hide -1) (("2" (lemma "tree_paths[T].tree_one_path") (("2" (lemma "path?_subgraph[T]") (("2" (typepred "x!1") (("2" (skosimp*) (("2" (name "pp" "(# length:= 2, seq:= (LAMBDA (ii:below(2)): IF ii=0 THEN x!2 ELSE y!1 ENDIF) #)") (("2" (case "path_from?(G!1,pp,x!2,y!1)") (("1" (hide -2) (("1" (expand "path_connected?" -5) (("1" (flatten) (("1" (inst -5 "x!2" "y!1") (("1" (skosimp*) (("1" (lemma "path_ops[T].walk_to_path_from") (("1" (inst -1 "H!1" "x!2" "y!1" "w!1") (("1" (typepred "w!1") (("1" (expand "walk_from?" -3) (("1" (bddsimp) (("1" (skosimp*) (("1" (copy -5) (("1" (copy -7) (("1" (expand "path_from?" (-7 -8)) (("1" (expand "from?" (-7 -8)) (("1" (flatten) (("1" (inst -14 "G!1" "H!1" "p!1") (("1" (bddsimp) (("1" (inst -16 "G!1" "pp" "p!1" "x!2" "y!1") (("1" (case "path_from?(H!1, p!1, x!2, y!1) AND path?(G!1,p!1) IMPLIES path_from?(G!1, p!1, x!2, y!1)" (("1" (bddsimp) (("1" (replace -18 -9 rl) (("1" (expand "path?" -9) (("1" (flatten) (("1" (hide (-1 -2 -3 -4 -6 -7 -10)) (("1" (hide (-4 -5 -6 -11 -13 -14)) (("1" (expand "walk?" -3) (("1" (flatten) (("1" (inst -4 "0") (("1" (case "length(pp)=2") (("1" (grind) nil nil) ("2" (assert) (("2" (reveal -19) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -6 -7) (("2" (hide -1 -2 -3 -4 -5 -6 -9 -10 -11 -12) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 -4 -6 4) (("2" (expand "subgraph?" -3) (("2" (install-rewrites "finite_sets") (("2" (flatten) (("2" (expand "size" -5) (("2" (assert) (("2" (case "vert(G!1)(y!1)") (("1" (assert) (("1" (lemma "finite_sets[T].card_diff_subset") (("1" (inst -1 "vert(H!1)" "vert(G!1)") (("1" (expand "subset?" -1) (("1" (expand "member" -1) (("1" (bddsimp) (("1" (expand "difference" -2) (("1" (replace -7 -2) (("1" (case "card(vert(G!1))=card[T](vert(G!1))") (("1" (assert) (("1" (lemma "finite_sets[T].empty_card") (("1" (inst -1 "{x: T | vert(G!1)(x) AND NOT vert(H!1)(x)}") (("1" (flatten) (("1" (hide -1 -10) (("1" (bddsimp) (("1" (hide -1 -4) (("1" (expand "empty?" -1) (("1" (inst -1 "y!1") (("1" (expand "member" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_difference[T]") (("2" (inst -1 "vert(G!1)" "vert(H!1)") (("2" (hide-all-but -1 -) (("2" (hide 2 3 4) (("2" (auto-rewrite-defs :always? t) (("2" (expand "is_finite") (("2" (skosimp*) (("2" (inst + "N!1" "f!1") (("2" (skosimp*) (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "finite_sets[T].card_diff_subset") (("2" (inst -1 "vert(H!1)" "vert(G!1)") (("2" (expand "subset?" -1) (("2" (expand "member" -1) (("2" (bddsimp) (("2" (case "card[T](vert(H!1))=card(vert(H!1))") (("1" (case "card[T](vert(G!1))=card(vert(G!1))") (("1" (assert) (("1" (replace -1 -4) (("1" (replace -1 -4 rl) (("1" (replace -2 -4 rl) (("1" (replace -9 -4) (("1" (assert) (("1" (lemma "finite_sets[T].empty_card") (("1" (inst -1 "difference(vert(G!1), vert(H!1))") (("1" (bddsimp) (("1" (expand "empty?" -1) (("1" (inst -1 "y!1") (("1" (expand "member" 1) (("1" (expand "difference" 1) (("1" (case "edges(G!1)(x!1)") (("1" (assert) (("1" (typepred "G!1") (("1" (inst -1 "x!1") (("1" (bddsimp -1 -2) (("1" (inst -1 "y!1") (("1" (assert) (("1" (hide-all-but -6 -) (("1" (hide-all-but 1 +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 -3 -4 -6 4) (("3" (expand "size" -4) (("3" (lemma "finite_sets[T].card_diff_subset") (("3" (inst -1 "vert(H!1)" "vert(G!1)") (("3" (expand "subset?" -1) (("3" (expand "member" -1) (("3" (bddsimp) (("1" (case "card[T](vert(H!1))=card(vert(H!1))") (("1" (case "card[T](vert(G!1))=card(vert(G!1))") (("1" (assert) (("1" (replace -1 -3 rl) (("1" (replace -2 -3 rl) (("1" (replace -7 -3) (("1" (assert) (("1" (lemma "finite_sets[T].empty_card") (("1" (inst -1 "difference(vert(G!1), vert(H!1))") (("1" (bddsimp) (("1" (expand "empty?" -1) (("1" (inst -1 "x!2") (("1" (expand "member" 1) (("1" (expand "difference" 1) (("1" (case "edges(G!1)(x!1)") (("1" (assert) (("1" (typepred "G!1") (("1" (inst -1 "x!1") (("1" (bddsimp -1 -2) (("1" (inst -1 "x!2") (("1" (expand "member" 1) (("1" (hide (-2 -3 -4 -5 -7 -8 -9)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide -1 -2 -4) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 -4 -5 -7 -8 -9) (("2" (expand "path_from?" 1) (("2" (expand "path?" 1) (("2" (expand "from?" 1) (("2" (expand "walk?" 1) (("2" (expand "verts_in?" +) (("2" (expand "finseq_appl") (("2" (case "edges(G!1)(x!1)") (("1" (bddsimp) (("1" (grind) (("1" (case "length(pp)=2") (("1" (replace -1 1) (("1" (assert) (("1" (case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)") (("1" (hide -2 -3 -4 -5 2 3) (("1" (grind) nil nil)) nil) ("2" (hide -2 -4 2 3 4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)") (("1" (hide -2 -3 -4 2 3) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (hide -1 -3 2 3 4) (("2" (assert) nil nil)) nil)) nil) ("3" (case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)") (("1" (case "length(pp)=2") (("1" (hide -3 -4 3) (("1" (grind) nil nil)) nil) ("2" (hide -1 -2 -4 2 3 4) (("2" (grind) nil nil)) nil)) nil) ("2" (hide -1 -3 2 3 4) (("2" (grind) nil nil)) nil)) nil) ("4" (case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)") (("1" (case "length(pp)=2") (("1" (hide -4 3) (("1" (expand "edge?" 1) (("1" (replace -1 1) (("1" (assert) (("1" (skosimp*) (("1" (typepred "n!1") (("1" (case "n!1=0") (("1" (replace -1 1) (("1" (assert) (("1" (replace -4 1) (("1" (beta 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -3 -4 -6 2 3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -4 2 3 4) (("2" (assert) nil nil)) nil)) nil) ("2" (hide -1 -3 2 3 4) (("2" (assert) nil nil)) nil)) nil) ("5" (case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)") (("1" (case "length(pp)=2") (("1" (typepred "G!1") (("1" (inst -1 "x!1") (("1" (bddsimp -1 -4) (("1" (inst-cp -1 "x!2") (("1" (inst -1 "y!1") (("1" (skosimp*) (("1" (hide -6 3) (("1" (typepred "i!1") (("1" (replace -4 -1) (("1" (replace -5 1) (("1" (case "i!1=0 OR i!1=1") (("1" (split) (("1" (replace -1 1) (("1" (hide -6 -7) (("1" (beta) (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1 1) (("2" (hide -6 -7) (("2" (beta) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (hide -3 -4 -5 -6 -7 -8 2 3) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide -1 -2 -4 2 3 4) (("2" (grind) nil nil)) nil)) nil) ("2" (hide -1 -3 2 3 4) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (split) (("1" (hide-all-but -1 -) (("1" (grind) nil nil)) nil) ("2" (hide-all-but -1 -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "vert(H!1)=vert(G!1)") (("1" (propax) nil nil) ("2" (hide 2 3) (("2" (hide -1 -4) (("2" (expand "size") (("2" (expand "subgraph?" -) (("2" (flatten) (("2" (lemma "finite_sets[T].card_diff_subset") (("2" (inst -1 "vert(H!1)" "vert(G!1)") (("2" (bddsimp -1 -2) (("1" (hide -2 -3) (("1" (case "card[T](vert(H!1))=card(vert(H!1))") (("1" (case "card[T](vert(G!1))=card(vert(G!1))") (("1" (replace -1 -3 rl) (("1" (replace -2 -3 rl) (("1" (assert -3 -4) (("1" (replace -4 -3) (("1" (assert -3) (("1" (lemma "finite_sets[T].empty_card") (("1" (inst -1 "difference(vert(G!1), vert(H!1))") (("1" (bddsimp) (("1" (expand "empty?" -1) (("1" (apply-extensionality 1) (("1" (hide 2) (("1" (inst -1 "x!1") (("1" (expand "member" 2) (("1" (expand "difference" 2) (("1" (copy 2) (("1" (delete 3) (("1" (expand "member" 1) (("1" (reveal -4) (("1" (expand "subset?" -1) (("1" (inst -1 "x!1") (("1" (expand "member" -1) (("1" (hide -2 -3 -4) (("1" (hide -2) (("1" (bddsimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil mappings 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) (graph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (subgraph? const-decl "bool" subgraphs nil) (path?_subgraph formula-decl nil subgraph_paths 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_from? const-decl "bool" paths nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (path_connected? const-decl "bool" graph_conn_defs nil) (H!1 skolem-const-decl "graph[T]" mappings nil) (x!2 skolem-const-decl "T" mappings nil) (y!1 skolem-const-decl "T" mappings nil) (walk_to_path_from formula-decl nil path_ops nil) (path? const-decl "bool" paths nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" graph_deg_sum nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (nil application-judgement "finite_set[T]" mappings nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (edge? const-decl "bool" graphs nil) (empty? const-decl "bool" sets nil) (empty? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" graphs nil) (from? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil) (Walk type-eq-decl nil walks nil) (finite_difference application-judgement "finite_set[T]" graph_deg_sum nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (is_finite const-decl "bool" finite_sets nil) (difference const-decl "set" sets nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (empty_card formula-decl nil finite_sets nil) (finite_difference judgement-tcc nil finite_sets nil) (injective? const-decl "bool" functions nil) (G!1 skolem-const-decl "graph[T]" mappings nil) (card_diff_subset formula-decl nil finite_sets nil) (size const-decl "nat" graphs nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (even_minus_odd_is_odd application-judgement "odd_int" integers 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posint nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (tree_one_path formula-decl nil tree_paths nil) (conn_eq_path formula-decl nil graph_connected nil)) nil) (sub_tree_0-3 "trial" 3319141305 ("" (skosimp*) (("" (apply-extensionality 1) (("1" (apply-extensionality 1) (("1" (hide 2 3) (("1" (iff) (("1" (split) (("1" (expand "subgraph?" -) (("1" (flatten) (("1" (hide -3) (("1" (expand "subset?" -) (("1" (inst -3 "x!1") (("1" (assert) (("1" (expand "member" -) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "graph_connected[T].conn_eq_path") (("2" (inst -1 "H!1") (("2" (flatten) (("2" (iff -1) (("2" (flatten) (("2" (hide -2) (("2" (bddsimp) (("2" (hide -1) (("2" (lemma "tree_paths[T].tree_one_path") (("2" (lemma "meng_scaff_defs[T].path?_subgraph") (("2" (typepred "x!1") (("2" (skosimp*) (("2" (name "pp" "(# l:= 2, seq:= (LAMBDA (ii:below(2)): IF ii=0 THEN x!2 ELSE y!1 ENDIF) #)") (("2" (case "path_from?(G!1,pp,x!2,y!1)") (("1" (hide -2) (("1" (expand "path_connected?" -5) (("1" (flatten) (("1" (inst -5 "x!2" "y!1") (("1" (skosimp*) (("1" (lemma "path_ops[T].walk_to_path_from") (("1" (inst -1 "H!1" "x!2" "y!1" "w!1") (("1" (typepred "w!1") (("1" (expand "walk_from?" -3) (("1" (bddsimp) (("1" (skosimp*) (("1" (copy -5) (("1" (copy -7) (("1" (expand "path_from?" (-7 -8)) (("1" (expand "from?" (-7 -8)) (("1" (flatten) (("1" (inst -14 "G!1" "H!1" "p!1") (("1" (bddsimp) (("1" (inst -16 "G!1" "pp" "p!1" "x!2" "y!1") (("1" (case "path_from?(H!1, p!1, x!2, y!1) AND path?(G!1,p!1) IMPLIES path_from?(G!1, p!1, x!2, y!1)" (("1" (bddsimp) (("1" (replace -18 -9 rl) (("1" (expand "path?" -9) (("1" (flatten) (("1" (hide (-1 -2 -3 -4 -6 -7 -10)) (("1" (hide (-4 -5 -6 -11 -13 -14)) (("1" (expand "walk?" -3) (("1" (flatten) (("1" (inst -4 "0") (("1" (case "length(pp)=2") (("1" (grind) nil nil) ("2" (assert) (("2" (reveal -19) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -6 -7) (("2" (hide -1 -2 -3 -4 -5 -6 -9 -10 -11 -12) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-11 -12) -) (("2" (grind) (("1" (grind) (("1" (reveal -21) (("1" (assert) nil nil)) nil)) nil) ("2" (reveal -21) (("2" (assert) nil nil)) nil) ("3" (reveal -21) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (bddsimp) (("1" (reveal -3) (("1" (hide-all-but (-1) -) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "pp") (("2" (propax) nil nil)) nil) ("3" (expand "pp") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 -4 -6 4) (("2" (expand "subgraph?" -3) (("2" (install-rewrites "finite_sets") (("2" (flatten) (("2" (expand "size" -5) (("2" (assert) (("2" (case "vert(G!1)(y!1)") (("1" (assert) (("1" (lemma "finite_sets[T].card_diff_subset") (("1" (inst -1 "vert(H!1)" "vert(G!1)") (("1" (expand "subset?" -1) (("1" (expand "member" -1) (("1" (bddsimp) (("1" (expand "difference" -2) (("1" (replace -7 -2) (("1" (case "card(vert(G!1))=card[T](vert(G!1))") (("1" (assert) (("1" (lemma "finite_sets[T].empty_card") (("1" (inst -1 "{x: T | vert(G!1)(x) AND NOT vert(H!1)(x)}") (("1" (flatten) (("1" (hide -1 -10) (("1" (bddsimp) (("1" (hide -1 -4) (("1" (expand "empty?" -1) (("1" (inst -1 "y!1") (("1" (expand "member" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_difference[T]") (("2" (inst -1 "vert(G!1)" "vert(H!1)") (("2" (hide-all-but -1 -) (("2" (hide 2 3 4) (("2" (auto-rewrite-defs :always? t) (("2" (expand "is_finite") (("2" (skosimp*) (("2" (inst + "N!1" "f!1") (("2" (skosimp*) (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "finite_sets[T].card_diff_subset") (("2" (inst -1 "vert(H!1)" "vert(G!1)") (("2" (expand "subset?" -1) (("2" (expand "member" -1) (("2" (bddsimp) (("2" (case "card[T](vert(H!1))=card(vert(H!1))") (("1" (case "card[T](vert(G!1))=card(vert(G!1))") (("1" (assert) (("1" (replace -1 -4) (("1" (replace -1 -4 rl) (("1" (replace -2 -4 rl) (("1" (replace -9 -4) (("1" (assert) (("1" (lemma "finite_sets[T].empty_card") (("1" (inst -1 "difference(vert(G!1), vert(H!1))") (("1" (bddsimp) (("1" (expand "empty?" -1) (("1" (inst -1 "y!1") (("1" (expand "member" 1) (("1" (expand "difference" 1) (("1" (case "edges(G!1)(x!1)") (("1" (assert) (("1" (typepred "G!1") (("1" (inst -1 "x!1") (("1" (bddsimp -1 -2) (("1" (inst -1 "y!1") (("1" (assert) (("1" (hide-all-but -6 -) (("1" (hide-all-but 1 +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 -3 -4 -6 4) (("3" (expand "size" -4) (("3" (lemma "finite_sets[T].card_diff_subset") (("3" (inst -1 "vert(H!1)" "vert(G!1)") (("3" (expand "subset?" -1) (("3" (expand "member" -1) (("3" (bddsimp) (("1" (case "card[T](vert(H!1))=card(vert(H!1))") (("1" (case "card[T](vert(G!1))=card(vert(G!1))") (("1" (assert) (("1" (replace -1 -3 rl) (("1" (replace -2 -3 rl) (("1" (replace -7 -3) (("1" (assert) (("1" (lemma "finite_sets[T].empty_card") (("1" (inst -1 "difference(vert(G!1), vert(H!1))") (("1" (bddsimp) (("1" (expand "empty?" -1) (("1" (inst -1 "x!2") (("1" (expand "member" 1) (("1" (expand "difference" 1) (("1" (case "edges(G!1)(x!1)") (("1" (assert) (("1" (typepred "G!1") (("1" (inst -1 "x!1") (("1" (bddsimp -1 -2) (("1" (inst -1 "x!2") (("1" (expand "member" 1) (("1" (hide (-2 -3 -4 -5 -7 -8 -9)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide -1 -2 -4) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 -4 -5 -7 -8 -9) (("2" (expand "path_from?" 1) (("2" (expand "path?" 1) (("2" (expand "from?" 1) (("2" (expand "walk?" 1) (("2" (expand "verts_in?" +) (("2" (case "edges(G!1)(x!1)") (("1" (bddsimp) (("1" (grind) (("1" (case "length(pp)=2") (("1" (replace -1 1) (("1" (assert) (("1" (case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)") (("1" (hide -2 -3 -4 -5 2 3) (("1" (grind) nil nil)) nil) ("2" (hide -2 -4 2 3 4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)") (("1" (hide -2 -3 -4 2 3) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (hide -1 -3 2 3 4) (("2" (assert) nil nil)) nil)) nil) ("3" (case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)") (("1" (case "length(pp)=2") (("1" (hide -3 -4 3) (("1" (grind) nil nil)) nil) ("2" (hide -1 -2 -4 2 3 4) (("2" (grind) nil nil)) nil)) nil) ("2" (hide -1 -3 2 3 4) (("2" (grind) nil nil)) nil)) nil) ("4" (case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)") (("1" (case "length(pp)=2") (("1" (hide -4 3) (("1" (expand "edge?" 1) (("1" (replace -1 1) (("1" (assert) (("1" (skosimp*) (("1" (typepred "n!1") (("1" (case "n!1=0") (("1" (replace -1 1) (("1" (assert) (("1" (replace -4 1) (("1" (beta 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -3 -4 -6 2 3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -4 2 3 4) (("2" (assert) nil nil)) nil)) nil) ("2" (hide -1 -3 2 3 4) (("2" (assert) nil nil)) nil)) nil) ("5" (case "seq(pp)=(LAMBDA (ii: below(2)): IF ii = 0 THEN x!2 ELSE y!1 ENDIF)") (("1" (case "length(pp)=2") (("1" (typepred "G!1") (("1" (inst -1 "x!1") (("1" (bddsimp -1 -4) (("1" (inst-cp -1 "x!2") (("1" (inst -1 "y!1") (("1" (skosimp*) (("1" (hide -6 3) (("1" (typepred "i!1") (("1" (replace -4 -1) (("1" (replace -5 1) (("1" (case "i!1=0 OR i!1=1") (("1" (split) (("1" (replace -1 1) (("1" (hide -6 -7) (("1" (beta) (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1 1) (("2" (hide -6 -7) (("2" (beta) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (hide -3 -4 -5 -6 -7 -8 2 3) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide -1 -2 -4 2 3 4) (("2" (grind) nil nil)) nil)) nil) ("2" (hide -1 -3 2 3 4) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (split) (("1" (hide-all-but -1 -) (("1" (grind) nil nil)) nil) ("2" (hide-all-but -1 -) (("2" (grind) nil nil)) nil) ("3" (hide-all-but -1 -) (("3" (grind) nil nil)) nil) ("4" (hide-all-but -1 -) (("4" (grind) nil nil)) nil) ("5" (hide-all-but -1 -) (("5" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "vert(H!1)=vert(G!1)") (("1" (propax) nil nil) ("2" (hide 2 3) (("2" (hide -1 -4) (("2" (expand "size") (("2" (expand "subgraph?" -) (("2" (flatten) (("2" (lemma "finite_sets[T].card_diff_subset") (("2" (inst -1 "vert(H!1)" "vert(G!1)") (("2" (bddsimp -1 -2) (("1" (hide -2 -3) (("1" (case "card[T](vert(H!1))=card(vert(H!1))") (("1" (case "card[T](vert(G!1))=card(vert(G!1))") (("1" (replace -1 -3 rl) (("1" (replace -2 -3 rl) (("1" (assert -3 -4) (("1" (replace -4 -3) (("1" (assert -3) (("1" (lemma "finite_sets[T].empty_card") (("1" (inst -1 "difference(vert(G!1), vert(H!1))") (("1" (bddsimp) (("1" (expand "empty?" -1) (("1" (apply-extensionality 1) (("1" (hide 2) (("1" (inst -1 "x!1") (("1" (expand "member" 2) (("1" (expand "difference" 2) (("1" (copy 2) (("1" (delete 3) (("1" (expand "member" 1) (("1" (reveal -4) (("1" (expand "subset?" -1) (("1" (inst -1 "x!1") (("1" (expand "member" -1) (("1" (hide -2 -3 -4) (("1" (hide -2) (("1" (bddsimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((conn_eq_path formula-decl nil graph_connected nil) (tree_one_path formula-decl nil tree_paths nil) (size const-decl "nat" graphs nil) (finite_difference application-judgement "finite_set[T]" graph_deg_sum nil) (Walk type-eq-decl nil walks nil) (walk? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (from? const-decl "bool" walks nil) (nil application-judgement "finite_set[T]" graphs nil) (empty? const-decl "bool" graphs nil) (edge? const-decl "bool" graphs nil) (verts_in? const-decl "bool" walks nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" graph_deg_sum nil) (path? const-decl "bool" paths nil) (walk_to_path_from formula-decl nil path_ops nil) (path_connected? const-decl "bool" graph_conn_defs nil) (prewalk type-eq-decl nil walks nil) (path_from? const-decl "bool" paths nil) (subgraph? const-decl "bool" subgraphs nil) (graph type-eq-decl nil graphs nil) (pregraph type-eq-decl nil graphs nil) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil)) nil) (sub_tree_0-2 "trial" 3319140197 ("" (skosimp*) (("" (apply-extensionality 1) (("1" (apply-extensionality 1) (("1" (hide 2 3) (("1" (iff) (("1" (split) (("1" (expand "subgraph?" -) (("1" (flatten) (("1" (hide -3) (("1" (expand "subset?" -) (("1" (inst -3 "x!1") (("1" (assert) (("1" (expand "member" -) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "graph_connected[T].conn_eq_path") (("2" (inst -1 "H!1") (("2" (flatten) (("2" (iff -1) (("2" (flatten) (("2" (hide -2) (("2" (bddsimp) (("2" (hide -1) (("2" (lemma "tree_paths[T].tree_one_path") (("2" (lemma "meng_scaff_defs[T].path?_subgraph") (("2" (typepred "x!1") (("2" (skosimp*) (("2" (name "pp" "(# l:= 2, seq:= (LAMBDA (ii:below(2)): IF ii=0 THEN x!2 ELSE y!1 ENDIF) #)") (("2" (case "path_from?(G!1,pp,x!2,y!1)") (("1" (hide -2) (("1" (expand "path_connected?" -5) (("1" (flatten) (("1" (inst -5 "x!2" "y!1") (("1" (skosimp*) (("1" (lemma "path_ops[T].walk_to_path_from") (("1" (inst -1 "H!1" "x!2" "y!1" "w!1") (("1" (typepred "w!1") (("1" (expand "walk_from?" -3) (("1" (bddsimp) (("1" (skosimp*) (("1" (copy -5) (("1" (copy -7) (("1" (expand "path_from?" (-7 -8)) (("1" (expand "from?" (-7 -8)) (("1" (flatten) (("1" (inst -14 "G!1" "H!1" "p!1") (("1" (bddsimp) (("1" (inst -16 "G!1" "pp" "p!1" "x!2" "y!1") (("1" (case "path_from?(H!1, p!1, x!2, y!1) AND path?(G!1,p!1) IMPLIES path_from?(G!1, p!1, x!2, y!1)" (("1" (bddsimp) (("1" (replace -18 -9 rl) (("1" (expand "path?" -9) (("1" (flatten) (("1" (hide (-1 -2 -3 -4 -6 -7 -10)) (("1" (hide (-4 -5 -6 -11 -13 -14)) (("1" (expand "walk?" -3) (("1" (flatten) (("1" (inst -4 "0") (("1" (expand "finseq_appl") (("1" (case "length(pp)=2") (("1" (grind) nil nil) ("2" (assert) (("2" (reveal -19) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -6 -7) (("2" (hide -1 -2 -3 -4 -5 -6 -9 -10 -11 -12) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-11 -12) -) (("2" (grind) (("1" (grind) (("1" (reveal -21) (("1" (assert) nil nil)) nil)) nil) ("2" (reveal -21) (("2" (assert) nil nil)) nil) ("3" (reveal -21) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (bddsimp) (("1" (reveal -3) (("1" (hide-all-but (-1) -) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "pp") (("2" (propax) nil nil)) nil) ("3" (expand "pp") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 -4 -6 4) (("2" (expand "subgraph?" -3) (("2" (install-rewrites "finite_sets") (("2" (flatten) (("2" (expand "size" -5) (("2" (assert) (("2" (case "vert(G!1)(y!1)") (("1" (assert) (("1" (lemma "finite_sets[T].card_diff_subset") (("1" (inst -1 "vert(H!1)" "vert(G!1)") (("1" (expand "subset?" -1) (("1" (expand "member" -1) (("1" (bddsimp) (("1" (expand "difference" -2) (("1" (replace -7 -2) (("1" (case "card(vert(G!1))=card[T](vert(G!1))") (("1" (assert) (("1" (lemma "finite_sets[T].empty_card") (("1" (inst -1 "{x: T | vert(G!1)(x) AND NOT vert(H!1)(x)}") (("1" (flatten) (("1" (hide --> -------------------- --> maximum size reached --> --------------------
¤ 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.0.958Bemerkung: (vorverarbeitet am 2026-04-30) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26