| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/graphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 59 kB |
|
Quelle meng_scaff_defs.prf Sprache: Lisp |
|||||||||
|
(meng_scaff_defs
(H_TCC1 0 (H_TCC1-1 nil 3507100603 ("" (skosimp*) (("" (expand "subgraph?") (("" (split 1) (("1" (expand "subset?") (("1" (skosimp*) (("1" (expand "path_comp") (("1" (expand "subgraph") (("1" (expand "del_vert") (("1" (expand "member") (("1" (flatten) (("1" (hide -2) (("1" (expand "remove") (("1" (expand "member") (("1" (flatten) (("1" (propax) nil))))))))))))))))))))))) ("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "member") (("2" (expand "path_comp") (("2" (expand "subgraph") (("2" (flatten) (("2" (hide -2) (("2" (expand "del_vert") (("2" (flatten) (("2" (propax) nil)))))))))))))))))))))))) nil) ((subgraph? const-decl "bool" subgraphs nil) (subset? const-decl "bool" sets nil) (path_comp const-decl "Subgraph(G)" meng_scaff_defs nil) (del_vert const-decl "graph[T]" graph_ops nil) (remove const-decl "set" sets nil) (member const-decl "bool" sets nil) (subgraph const-decl "Subgraph(G)" subgraphs nil)) nil)) (incident_TCC1 0 (incident_TCC1-1 nil 3507100603 ("" (skosimp*) (("" (lemma "finite_subset[Dbl]") (("" (inst?) (("" (inst -1 "edges(G!1)") (("" (assert) (("" (hide 2) (("" (expand "subset?") (("" (skosimp*) (("" (expand "member") (("" (skosimp*) nil)))))))))))))))))) nil) ((Dbl 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 meng_scaff_defs nil) (finite_subset formula-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (H const-decl "Subgraph(G)" meng_scaff_defs 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)) nil)) (meng_TCC1 0 (meng_TCC1-1 nil 3507100603 ("" (skosimp*) (("" (inst?) (("" (assert) nil)))) nil) ((T formal-type-decl nil meng_scaff_defs nil) (boolean nonempty-type-decl nil booleans 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)) nil)) (meng_TCC2 0 (meng_TCC2-1 nil 3507100603 ("" (skosimp*) (("" (inst?) (("" (assert) nil)))) nil) ((T formal-type-decl nil meng_scaff_defs nil) (boolean nonempty-type-decl nil booleans 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)) nil)) (meng_TCC3 0 (meng_TCC3-1 nil 3507100603 ("" (skosimp*) (("" (expand "add") (("" (flatten) (("" (expand "member") (("" (flatten) (("" (split -1) (("1" (replace -1 * rl) (("1" (hide -1) (("1" (expand "dbl") (("1" (ground) nil))))))) ("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "dbl") (("2" (ground) nil))))))) ("3" (expand "union") (("3" (expand "member") (("3" (split -1) (("1" (typepred "H(G!1, x!1, w1!1, w2!1)") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) nil))))))))) ("2" (expand "incident") (("2" (skosimp*) (("2" (replace -2) (("2" (hide -2) (("2" (expand "dbl") (("2" (split -) (("1" (replace -1) (("1" (propax) nil))) ("2" (replace -1) (("2" (propax) nil))))))))))))))) ("3" (expand "incident") (("3" (skosimp*) (("3" (replace -2) (("3" (hide -2) (("3" (expand "dbl" -3) (("3" (split -3) (("1" (replace -1) (("1" (propax) nil))) ("2" (assert) nil)))))))))))))))))))))))))))))) nil) ((add const-decl "(nonempty?)" sets nil) (member const-decl "bool" sets nil) (dbl const-decl "set[T]" doubletons nil) (nil application-judgement "finite_set[T]" meng_scaff_defs nil) (incident const-decl "finite_set[doubleton[T]]" meng_scaff_defs nil) (H const-decl "Subgraph(G)" meng_scaff_defs nil) (Subgraph type-eq-decl nil subgraphs nil) (subgraph? const-decl "bool" subgraphs 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) (= 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 meng_scaff_defs nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (union const-decl "set" sets nil)) nil)) (vert_H_s 0 (vert_H_s-1 nil 3507100603 ("" (skosimp*) (("" (assert) (("" (expand "H") (("" (expand "path_comp") (("" (expand "subgraph") (("" (expand "del_vert") (("" (expand "remove") (("" (expand "member") (("" (expand "path_verts") (("" (expand "walk_from?") (("" (inst + "gen_seq1(G!1,s!1)") (("" (expand "gen_seq1") (("" (expand "walk?") (("" (expand "verts_in?") (("" (propax) nil)))))))))))))))))))))))))))) nil) ((path_comp const-decl "Subgraph(G)" meng_scaff_defs nil) (del_vert const-decl "graph[T]" graph_ops nil) (member const-decl "bool" sets nil) (walk_from? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil) (gen_seq1 const-decl "Seq(G)" walks nil) (Seq type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks 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) (> 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) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil meng_scaff_defs nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (path_verts const-decl "set[T]" paths nil) (remove const-decl "set" sets nil) (subgraph const-decl "Subgraph(G)" subgraphs nil) (H const-decl "Subgraph(G)" meng_scaff_defs nil)) nil)) (path_H_W 0 (path_H_W-1 nil 3507100603 ("" (skosimp*) (("" (expand "path?") (("" (flatten) (("" (hide -2) (("" (expand "walk?") (("" (flatten) (("" (hide -2) (("" (expand "verts_in?") (("" (expand "H") (("" (expand "path_comp") (("" (expand "subgraph") (("" (expand "del_vert") (("" (expand "remove") (("" (expand "member") (("" (expand "verts_of") (("" (expand "finseq_appl") (("" (split 1) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil))))) ("2" (assert) (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil)))))))))))))))))))))))))))))))))))))))) nil) ((path? const-decl "bool" paths nil) (verts_in? const-decl "bool" walks nil) (path_comp const-decl "Subgraph(G)" meng_scaff_defs nil) (del_vert const-decl "graph[T]" graph_ops nil) (member const-decl "bool" sets nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (below type-eq-decl nil naturalnumbers nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil meng_scaff_defs nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (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) (verts_of const-decl "finite_set[T]" walks nil) (remove const-decl "set" sets nil) (subgraph const-decl "Subgraph(G)" subgraphs nil) (H const-decl "Subgraph(G)" meng_scaff_defs nil) (walk? const-decl "bool" walks nil)) nil)) (path_comp_in 0 (path_comp_in-1 nil 3507100603 ("" (skosimp*) (("" (expand "path?") (("" (split 1) (("1" (flatten) (("1" (typepred "H(G!1, s!1, w1!1, w2!1)") (("1" (hide -1 -4) (("1" (lemma "walk?_subgraph") (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil) ((path? const-decl "bool" paths 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) (walk?_subgraph formula-decl nil subgraph_paths 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 meng_scaff_defs 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) (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) (subgraph? const-decl "bool" subgraphs nil) (Subgraph type-eq-decl nil subgraphs nil) (H const-decl "Subgraph(G)" meng_scaff_defs nil)) nil)) (walk?_H_TCC1 0 (walk?_H_TCC1-1 nil 3507100603 ("" (subtype-tcc) nil nil) ((T formal-type-decl nil meng_scaff_defs 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) (nil application-judgement "finite_set[T]" meng_scaff_defs nil)) nil)) (walk?_H 0 (walk?_H-1 nil 3507100603 ("" (skosimp*) (("" (expand "H") (("" (expand "path_comp") (("" (expand "walk?") (("" (flatten) (("" (split +) (("1" (hide -2) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (inst?) (("1" (expand "subgraph") (("1" (expand "del_vert") (("1" (expand "remove") (("1" (expand "member") (("1" (assert) (("1" (expand "verts_of") (("1" (inst?) (("1" (expand "finseq_appl") (("1" (inst?) (("1" (assert) (("1" (expand "path_verts") (("1" (expand "walk_from?") (("1" (inst 1 "p!1^(0,i!1)") (("1" (expand* "^" min empty_seq) (("1" (expand "walk?") (("1" (split +) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (reveal -1) (("1" (inst?) (("1" (assert) (("1" (reveal 2 3) (("1" (expand "finseq_appl") (("1" (hide 4 5 -2) (("1" (inst?) (("1" (inst?) (("1" (assert) nil))))))))))))))))))))) ("2" (expand "finseq_appl") (("2" (skosimp*) (("2" (expand "edge?") (("2" (hide -2 2 3) (("2" (reveal -3) (("2" (inst - "n!1") (("2" (assert) (("2" (expand "finseq_appl") (("2" (expand "edge?") (("2" (flatten) (("2" (assert) (("2" (hide -1 -3) (("2" (reveal 4 5) (("2" (expand "finseq_appl") (("2" (inst-cp + "n!1") (("2" (inst + "n!1+1") (("2" (inst-cp + "n!1") (("2" (inst + "n!1+1") (("2" (expand "dbl") (("2" (ground) nil))))))))))))))))))))))))))))))))))))))))))))) ("2" (expand* "^" min empty_seq) (("2" (assert) nil))))))))))))))))))))))))))))))))))))) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (expand "edge?") (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (expand "subgraph") (("2" (expand "del_vert") (("2" (split +) (("1" (expand "verts_of" 2) (("1" (inst-cp + "n!1") (("1" (inst + "n!1+1") (("1" (expand "finseq_appl") (("1" (expand "dbl") (("1" (ground) nil))))))))))) ("2" (expand "verts_of" 3) (("2" (inst-cp + "n!1") (("2" (inst + "n!1+1") (("2" (expand "finseq_appl") (("2" (expand "dbl") (("2" (ground) nil))))))))))) ("3" (skosimp*) (("3" (expand "path_verts") (("3" (expand "walk_from?") (("3" (expand "dbl") (("3" (split -1) (("1" (inst 1 "p!1^(0,n!1)") (("1" (expand* "^" min empty_seq) (("1" (assert) (("1" (expand "walk?") (("1" (split +) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (expand "remove") (("1" (expand "member") (("1" (inst?) (("1" (assert) (("1" (expand "verts_of") (("1" (inst + "i!1") (("1" (inst + "i!1") (("1" (expand "finseq_appl") (("1" (ground) nil))))))))))))))))))))) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (expand "edge?") (("2" (assert) (("2" (reveal -1) (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (expand "dbl") (("2" (expand "verts_of") (("2" (inst-cp + "n!2") (("2" (inst + "n!2+1") (("2" (inst-cp + "n!2") (("2" (inst + "n!2+1") (("2" (expand "finseq_appl") (("2" (ground) nil))))))))))))))))))))))))))))))))))))))))) ("2" (expand* "^" min empty_seq) (("2" (assert) nil))))) ("2" (inst 1 "p!1^(0,n!1+1)") (("1" (expand* "^" min empty_seq) (("1" (assert) (("1" (expand "walk?") (("1" (split +) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (expand "remove") (("1" (expand "member") (("1" (inst?) (("1" (assert) (("1" (expand "verts_of") (("1" (inst-cp + "i!1") (("1" (inst + "i!1+1") (("1" (inst-cp + "i!1") (("1" (inst + "i!1+1") (("1" (expand "finseq_appl") (("1" (assert) nil))) ("2" (assert) (("2" (typepred "i!1") (("2" (expand "finseq_appl") (("2" (assert) nil))))))))))) ("2" (expand "finseq_appl") (("2" (assert) (("2" (typepred "i!1") (("2" (inst?) (("2" (assert) nil))))))))))))))))))))))))))) ("2" (skosimp*) (("2" (expand "edge?") (("2" (expand "finseq_appl") (("2" (reveal -1) (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (expand "verts_of") (("2" (expand "finseq_appl") (("2" (inst-cp + "n!2") (("2" (inst + "n!2+1") (("2" (inst-cp + "n!2") (("2" (inst + "n!2+1") (("2" (expand "dbl") (("2" (ground) nil))))))))))))))))))))))))))))))))))))))) ("2" (expand* "^" min empty_seq) (("2" (assert) nil)))))))))))))))))))))))))))))))))))))))))))))) nil) ((H const-decl "Subgraph(G)" meng_scaff_defs nil) (walk? const-decl "bool" walks nil) (verts_in? const-decl "bool" walks nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil meng_scaff_defs nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (below type-eq-decl nil naturalnumbers nil) (del_vert const-decl "graph[T]" graph_ops nil) (member const-decl "bool" sets nil) (verts_of const-decl "finite_set[T]" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (walk_from? const-decl "bool" walks nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (real_lt_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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (dbl const-decl "set[T]" doubletons nil) (int_minus_int_is_int application-judgement "int" integers nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" meng_scaff_defs nil) (i!1 skolem-const-decl "below(length(p!1))" meng_scaff_defs nil) (p!1 skolem-const-decl "prewalk[T]" meng_scaff_defs nil) (^ const-decl "finseq" finite_sequences nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (path_verts const-decl "set[T]" paths nil) (remove const-decl "set" sets nil) (subgraph const-decl "Subgraph(G)" subgraphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (i!1 skolem-const-decl "below(2 + n!1)" meng_scaff_defs nil) (n!1 skolem-const-decl "nat" meng_scaff_defs nil) (path_comp const-decl "Subgraph(G)" meng_scaff_defs nil)) nil)) (vert_meng_sub_TCC1 0 (vert_meng_sub_TCC1-1 nil 3507100603 ("" (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 meng_scaff_defs 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) (/= const-decl "boolean" notequal nil) (disjoint? const-decl "bool" meng_scaff_defs nil) (in? const-decl "bool" meng_scaff_defs nil)) nil)) (vert_meng_sub_TCC2 0 (vert_meng_sub_TCC2-1 nil 3507100603 ("" (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 meng_scaff_defs 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) (/= const-decl "boolean" notequal nil) (disjoint? const-decl "bool" meng_scaff_defs nil) (in? const-decl "bool" meng_scaff_defs nil)) nil)) (vert_meng_sub_TCC3 0 (vert_meng_sub_TCC3-1 nil 3507100603 ("" (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 meng_scaff_defs 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) (/= const-decl "boolean" notequal nil) (disjoint? const-decl "bool" meng_scaff_defs nil) (in? const-decl "bool" meng_scaff_defs nil)) nil)) (vert_meng_sub_TCC4 0 (vert_meng_sub_TCC4-1 nil 3507100603 ("" (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 meng_scaff_defs 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) (/= const-decl "boolean" notequal nil) (disjoint? const-decl "bool" meng_scaff_defs nil) (in? const-decl "bool" meng_scaff_defs nil)) nil)) (vert_meng_sub 0 (vert_meng_sub-1 nil 3507100603 ("" (skosimp*) (("" (expand "subset?") (("" (expand "member") (("" (skosimp*) (("" (expand "meng") (("" (expand "add") (("" (expand "member") (("" (assert) (("" (expand "H") (("" (expand "path_comp") (("" (expand "subgraph") (("" (expand "del_vert") (("" (expand "remove") (("" (expand "member") (("" (expand "in?") (("" (flatten) (("" (expand "disjoint?") (("" (flatten) (("" (assert) nil)))))))))))))))))))))))))))))))))))) nil) ((subset? const-decl "bool" sets nil) (add const-decl "(nonempty?)" sets nil) (path_comp const-decl "Subgraph(G)" meng_scaff_defs nil) (del_vert const-decl "graph[T]" graph_ops nil) (disjoint? const-decl "bool" meng_scaff_defs nil) (in? const-decl "bool" meng_scaff_defs nil) (remove const-decl "set" sets nil) (subgraph const-decl "Subgraph(G)" subgraphs nil) (H const-decl "Subgraph(G)" meng_scaff_defs nil) (meng const-decl "graph[T]" meng_scaff_defs nil) (member const-decl "bool" sets nil)) nil)) (del_vert_comm 0 (del_vert_comm-1 nil 3507100603 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("1" (apply-extensionality 1 :hide? t) (("1" (expand "del_vert") (("1" (iff 1) (("1" (ground) nil))))))) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "del_vert") (("2" (expand "remove") (("2" (expand "member") (("2" (iff 1) (("2" (ground) nil)))))))))))))) nil) ((T formal-type-decl nil meng_scaff_defs 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) (del_vert const-decl "graph[T]" graph_ops nil) (graph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (remove const-decl "set" sets nil)) nil)) (H_comm 0 (H_comm-1 nil 3507100603 ("" (skosimp*) (("" (expand "H") (("" (expand "path_comp") (("" (rewrite "del_vert_comm") nil)))))) nil) ((H const-decl "Subgraph(G)" meng_scaff_defs nil) (del_vert_comm formula-decl nil meng_scaff_defs nil) (T formal-type-decl nil meng_scaff_defs 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) (path_comp const-decl "Subgraph(G)" meng_scaff_defs nil)) nil)) (incident_comm 0 (incident_comm-1 nil 3507100603 ("" (skosimp*) (("" (expand "incident") (("" (rewrite "H_comm") nil)))) nil) ((incident const-decl "finite_set[doubleton[T]]" meng_scaff_defs 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 meng_scaff_defs nil) (H_comm formula-decl nil meng_scaff_defs nil)) nil)) (meng_comm_TCC1 0 (meng_comm_TCC1-1 nil 3507100603 ("" (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 meng_scaff_defs 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) (/= const-decl "boolean" notequal nil)) nil)) (meng_comm_TCC2 0 (meng_comm_TCC2-1 nil 3507100603 ("" (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 meng_scaff_defs 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) (/= const-decl "boolean" notequal nil)) nil)) (meng_comm 0 (meng_comm-1 nil 3507100603 ("" (skosimp*) (("" (hide -1) (("" (expand "meng") (("" (case-replace "H(G!1, t!1, w2!1, w1!1) = H(G!1, t!1, w1!1, w2!1)") (("1" (split 3) (("1" (hide -1) (("1" (apply-extensionality 1 :hide? t) (("1" (expand "add") (("1" (expand "member") (("1" (iff) (("1" (ground) nil))))))))))) ("2" (apply-extensionality 1 :hide? t) (("1" (expand "union") (("1" (expand "add") (("1" (expand "member") (("1" (iff) (("1" (lemma "incident_comm") (("1" (inst?) (("1" (lemma "incident_comm") (("1" (inst -1 "G!1" "t!1" "w2!1" "w1!1" "w2!1") (("1" (replace -1) (("1" (hide -1) (("1" (replace -1) (("1" (hide -1) (("1" (ground) nil))))))))))))))))))))))))) ("2" (inst?) (("2" (assert) nil))) ("3" (inst?) (("3" (assert) nil))))))) ("2" (hide 4) (("2" (lemma "H_comm") (("2" (inst?) nil)))))))))))) nil) ((T formal-type-decl nil meng_scaff_defs 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) (subgraph? const-decl "bool" subgraphs nil) (Subgraph type-eq-decl nil subgraphs nil) (H const-decl "Subgraph(G)" meng_scaff_defs nil) (incident const-decl "finite_set[doubleton[T]]" meng_scaff_defs nil) (is_finite const-decl "bool" finite_sets nil) (union const-decl "set" sets nil) (nil application-judgement "finite_set[T]" meng_scaff_defs nil) (finite_union application-judgement "finite_set" finite_sets nil) (incident_comm formula-decl nil meng_scaff_defs nil) (member const-decl "bool" sets nil) (nonempty_add_finite application-judgement "non_empty_finite_set" finite_sets nil) (nonempty? const-decl "bool" sets nil) (add const-decl "(nonempty?)" sets nil) (H_comm formula-decl nil meng_scaff_defs nil) (meng const-decl "graph[T]" meng_scaff_defs nil)) nil))) ¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28