|
(circuit_deg
(cir_deg_G 0
(cir_deg_G-2 "Did not use e_duo" 3368433600
("" (skosimp*)
(("" (expand "edge?")
(("" (flatten)
(("" (expand "deg")
(("" (case " card(incident_edges(z!1, G!1)) =0")
(("1" (lemma "finite_sets[doubleton[T]].card_empty?")
(("1" (inst?)
(("1" (iff)
(("1" (bddsimp)
(("1" (expand "empty?")
(("1" (inst -2 "dbl[T](a!1, z!1)")
(("1" (expand "member")
(("1" (hide -1 -4 5)
(("1" (install-rewrites "graphs[T]")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case " card(incident_edges(z!1, G!1)) =1")
(("1" (lemma "finite_sets[doubleton[T]].card_one")
(("1" (inst?)
(("1" (bddsimp)
(("1" (skosimp*)
(("1" (hide -1 1 5)
(("1" (install-rewrites "graphs[T]")
(("1" (assert)
(("1" (grind)
(("1"
(expand "incident_edges")
(("1"
(expand "singleton")
(("1"
(decompose-equality -1)
(("1"
(copy -1)
(("1"
(inst -1 "dbl[T](a!1, z!1)")
(("1"
(inst -2 "dbl[T](b!1, z!1)")
(("1"
(bddsimp)
(("1"
(install-rewrites
"doubletons[T]")
(("1"
(assert)
(("1"
(replace -3 -6 rl)
(("1"
(hide -1 -3 -4)
(("1"
(grind)
(("1"
(lemma
"doubletons[T].dbl_eq")
(("1"
(inst
-1
"a!1"
"b!1"
"z!1"
"z!1")
(("1"
(prop)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(install-rewrites
"doubletons[T]")
(("2" (assert) nil nil))
nil)
("3" (assert) nil nil)
("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nil application-judgement "finite_set[T]" circuit_deg nil)
(edge? const-decl "bool" graphs nil)
(deg const-decl "nat" graph_deg nil)
(singleton const-decl "(singleton?)" sets nil)
(dbl_eq formula-decl nil doubletons nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(card_one formula-decl nil finite_sets nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(card_empty? formula-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-type-decl nil circuit_deg 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)
(dbl const-decl "set[T]" doubletons nil)
(doubleton type-eq-decl nil doubletons nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(Card const-decl "nat" finite_sets nil)
(card const-decl "{n: nat | n = Card(S)}" 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)
(incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
nil))
shostak)
(cir_deg_G-1 nil 3251049115
("" (skosimp*)
(("" (expand "edge?")
(("" (flatten)
(("" (expand "deg")
((""
(case "subset?(e_duo(dbl(a!1,z!1),dbl(b!1,z!1)),
incident_edges(z!1, G!1))")
(("1" (lemma "card_subset[doubleton[T]]")
(("1" (inst?)
(("1"
(case "card(e_duo(dbl(a!1, z!1), dbl(b!1, z!1))) = 2")
(("1" (assert) nil)
("2" (hide -1 -2 3)
(("2" (expand "e_duo")
(("2" (rewrite "card_add[doubleton[T]]")
(("2" (rewrite "card_singleton[doubleton[T]]")
(("2" (lift-if)
(("2" (ground)
(("2"
(hide 1)
(("2"
(expand "singleton")
(("2"
(case
"dbl(a!1, z!1)(a!1) = dbl(b!1, z!1)(a!1)")
(("1"
(case
"dbl(a!1, z!1)(b!1) = dbl(b!1, z!1)(b!1)")
(("1"
(hide -3)
(("1"
(expand "dbl")
(("1" (propax) nil)))))
("2" (assert) nil)))
("2"
(assert)
nil)))))))))))))))))))))
("2" (hide -1 3)
(("2" (assert)
(("2" (inst 1 "b!1" "z!1")
(("2" (assert) nil)))))))
("3" (inst?) (("3" (assert) nil)))))))
("2" (hide 3)
(("2" (expand "subset?")
(("2" (skosimp*)
(("2" (expand "member")
(("2" (expand "incident_edges")
(("2"
(case "x!1 = dbl(a!1, z!1) OR x!1 = dbl(b!1, z!1)")
(("1" (hide -2)
(("1" (split -1)
(("1" (replace -1)
(("1"
(hide -1)
(("1"
(assert)
(("1"
(expand "dbl")
(("1" (propax) nil)))))))))
("2" (replace -1)
(("2"
(hide -1)
(("2"
(assert)
(("2"
(expand "dbl")
(("2" (propax) nil)))))))))))))
("2" (hide -2 -3 -4 2 3)
(("2" (expand "e_duo")
(("2" (expand "add")
(("2"
(expand "member")
(("2"
(expand "singleton")
(("2"
(ground)
nil)))))))))))))))))))))))
("3" (inst 1 "b!1" "z!1") (("3" (assert) nil)))
("4" (inst?) (("4" (assert) nil))))))))))))
nil)
((edge? const-decl "bool" graphs nil)
(deg const-decl "nat" graph_deg nil)
(dbl_eq formula-decl nil doubletons 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)
(incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
nil))
nil))
(circuit_deg_TCC1 0
(circuit_deg_TCC1-1 nil 3251049115 ("" (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)
(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)
(walk? const-decl "bool" walks nil)
(Walk type-eq-decl nil walks 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)
(G!1 skolem-const-decl "graph[T]" circuit_deg nil)
(edge? const-decl "bool" graphs nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nil application-judgement "finite_set[T]" circuit_deg nil)
(T formal-type-decl nil circuit_deg nil)
(verts_in? const-decl "bool" walks nil)
(/= const-decl "boolean" notequal nil))
nil))
(circuit_deg 0
(circuit_deg-2 "Update from cir_deg_G" 3368440612
("" (skosimp*)
(("" (lemma " cir_deg_G")
(("" (inst -1 "G_from(G!1,w!1)" "w!1`seq(i!1)")
(("" (expand "finseq_appl")
(("" (bddsimp)
(("" (hide 2)
(("" (typepred "i!1")
(("" (expand "circuit?")
(("" (expand "cyclically_reduced?")
(("" (expand "finseq_appl")
(("" (flatten)
(("" (case "i!1=length(w!1)-1")
(("1" (expand "pre_circuit?")
(("1" (expand "finseq_appl")
(("1"
(inst 1 "w!1(1)" "w!1(length(w!1)-2)")
(("1"
(expand "finseq_appl")
(("1"
(prop)
(("1"
(hide -4)
(("1"
(install-rewrites "walks[T]")
(("1"
(assert)
(("1"
(inst 1 "i!1")
nil
nil))
nil))
nil))
nil)
("2"
(replace -1 1 lr)
(("2"
(replace -5 * rl)
(("2"
(hide -4)
(("2"
(install-rewrites
"walks[T]")
(("2"
(assert)
(("2"
(prop)
(("1"
(typepred "w!1")
(("1"
(expand "walk?")
(("1"
(expand
"finseq_appl")
(("1"
(prop)
(("1"
(inst -3 "0")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst 1 "0")
(("2"
(assert)
(("2"
(expand "dbl")
(("2"
(ground)
(("2"
(grind)
(("2"
(apply-extensionality
1
:hide?
t)
(("2"
(iff)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(replace -1 1 lr)
(("3"
(hide -4)
(("3"
(typepred "w!1")
(("3"
(expand "walk?")
(("3"
(expand "finseq_appl")
(("3"
(flatten)
(("3"
(inst
-3
"length(w!1)-2")
(("1"
(assert)
(("1"
(install-rewrites
"walks[T]")
(("1"
(assert)
(("1"
(flatten)
(("1"
(bddsimp)
(("1"
(inst
2
"length(w!1)-2")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "finseq_appl")
(("2"
(assert)
(("2"
(install-rewrites "walks[T]")
(("2"
(assert)
(("2"
(inst 1 "length(w!1)-2")
nil
nil))
nil))
nil))
nil))
nil)
("3" (assert) nil nil)
("4"
(install-rewrites "walks[T]")
(("4"
(assert)
(("4" (inst 1 "1") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "i!1=0")
(("1" (replace -1 + lr)
(("1"
(inst
2
" w!1`seq(1)"
"w!1`seq(length(w!1) - 2)")
(("1"
(prop)
(("1"
(hide -4 -5)
(("1"
(typepred "w!1")
(("1"
(install-rewrites "walks[T]")
(("1"
(assert)
(("1" (inst 1 "0") nil nil))
nil))
nil))
nil))
nil)
("2"
(hide -4 -5)
(("2"
(typepred "w!1")
(("2"
(install-rewrites "walks[T]")
(("2"
(assert)
(("2"
(prop)
(("1"
(inst -4 "0")
(("1"
(prop)
(("1" (assert) nil nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(inst 1 "0")
(("2"
(hide -2 -3)
(("2"
(assert)
(("2"
(lemma "dbl_comm")
(("2"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide -4)
(("3"
(expand "pre_circuit?")
(("3"
(expand "finseq_appl")
(("3"
(replace -4 1 lr)
(("3"
(hide -4)
(("3"
(typepred "w!1")
(("3"
(install-rewrites
"walks[T]")
(("3"
(assert)
(("3"
(flatten)
(("3"
(bddsimp)
(("1"
(assert)
(("1"
(reveal -1)
(("1"
(inst
-4
"length(w!1)-2")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(inst
1
"length(w!1)-2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -4 -5)
(("2"
(install-rewrites "walks[T]")
(("2"
(assert)
(("2"
(inst 1 "length(w!1)-2")
nil
nil))
nil))
nil))
nil)
("3" (assert) nil nil)
("4"
(hide -4 -5)
(("4"
(install-rewrites "walks[T]")
(("4"
(assert)
(("4" (inst 1 "1") nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst 3 "seq(w!1)(i!1-1)"
"seq(w!1)(i!1+1)")
(("1"
(hide -4)
(("1"
(bddsimp)
(("1"
(hide -3)
(("1"
(install-rewrites "walks[T]")
(("1"
(assert)
(("1"
(prop)
(("1"
(assert)
(("1"
(typepred "w!1")
(("1"
(assert)
(("1"
(flatten)
(("1"
(inst -3 "i!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst 1 "i!1")
(("2"
(rewrite "dbl_comm")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -3)
(("2"
(typepred "w!1")
(("2"
(install-rewrites "walks[T]")
(("2"
(assert)
(("2"
(bddsimp)
(("1"
(inst -3 "i!1-1")
(("1" (assert) nil nil))
nil)
("2"
(inst 3 "i!1-1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(prop)
(("3"
(expand "reduced?")
(("3"
(expand "reducible?")
(("3"
(expand "finseq_appl")
(("3"
(inst 3 "i!1")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("4"
(typepred "w!1")
(("4"
(install-rewrites "walks[T]")
(("4"
(assert)
(("4" (inst 3 "i!1") nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -3 -4)
(("2"
(typepred "w!1")
(("2"
(install-rewrites "walks[T]")
(("2"
(assert)
(("2"
(flatten)
(("2"
(inst 1 "i!1+1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (assert) nil nil)
("4"
(hide -3 -4)
(("4"
(typepred "w!1")
(("4"
(install-rewrites "walks[T]")
(("4"
(assert)
(("4"
(flatten)
(("4"
(inst 1 "i!1-1")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("5" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cir_deg_G formula-decl nil circuit_deg nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(circuit? const-decl "bool" circuits nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(reduced? const-decl "bool" circuits nil)
(reducible? const-decl "bool" circuits nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nil application-judgement "finite_set[T]" circuit_deg nil)
(edges_of const-decl "finite_set[doubleton[T]]" walks nil)
(edge? const-decl "bool" graphs nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(verts_in? const-decl "bool" walks nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(verts_of const-decl "finite_set[T]" walks nil)
(w!1 skolem-const-decl "Walk[T](G!1)" circuit_deg nil)
(G!1 skolem-const-decl "graph[T]" circuit_deg nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pre_circuit? const-decl "bool" walks nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(i!1 skolem-const-decl "below(length(w!1))" circuit_deg nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(dbl_comm formula-decl nil doubletons nil)
(cyclically_reduced? const-decl "bool" circuits nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(G_from const-decl "Subgraph(G)" subgraphs_from_walk nil)
(Subgraph type-eq-decl nil subgraphs nil)
(subgraph? const-decl "bool" subgraphs nil)
(Walk type-eq-decl nil walks nil)
(walk? 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)
(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 circuit_deg nil))
shostak)
(circuit_deg-1 nil 3251049115
("" (skosimp*)
(("" (rewrite "cir_deg_G")
(("" (expand "circuit?")
(("" (expand "cyclically_reduced?")
(("" (flatten)
(("" (case "i!1 = 0")
(("1" (hide 2)
(("1" (inst 1 "w!1(length(w!1)-2)" "w!1(i!1+1)")
(("1" (prop)
(("1" (rewrite "vert_G_from") nil nil)
("2" (replace -2)
(("2" (hide -2)
(("2" (assert)
(("2" (reveal 2) (("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("3" (expand "pre_circuit?")
(("3" (lemma "edge?_G_from")
(("3" (inst?)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("4" (rewrite "edge?_G_from_rev") nil nil))
nil)
("2" (rewrite "vert_G_from") nil nil)
("3" (assert) nil nil)
("4" (rewrite "vert_G_from") nil nil)
("5" (assert) nil nil))
nil))
nil)
("2" (case "i!1 = length(w!1)-1")
(("1" (inst 2 "w!1(length(w!1)-2)" "w!1(1)")
(("1" (prop)
(("1" (rewrite "vert_G_from") nil nil)
("2" (assert) nil nil)
("3" (replace -1)
(("3" (hide -1)
(("3" (rewrite "edge?_G_from") nil nil)) nil))
nil)
("4" (expand "pre_circuit?")
(("4" (replace -1)
(("4" (hide -1)
(("4" (lemma "edge?_G_from_rev")
(("4" (inst -1 "G!1" "w!1" 0)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "vert_G_from") nil nil)
("3" (assert)
(("3" (rewrite "vert_G_from") nil nil)) nil)
("4" (hide 3 4) (("4" (assert) nil nil)) nil))
nil)
("2" (inst 3 "w!1(i!1-1)" "w!1(i!1+1)")
(("1" (prop)
(("1" (expand "G_from")
(("1" (expand "verts_of")
(("1" (inst 1 "i!1") nil nil)) nil))
nil)
("2" (expand "reduced?")
(("2" (expand "reducible?")
(("2" (inst?)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("3" (rewrite "edge?_G_from") nil nil)
("4" (rewrite "edge?_G_from_rev") nil nil))
nil)
("2" (rewrite "vert_G_from") nil nil)
("3" (assert) nil nil)
("4" (rewrite "vert_G_from") nil nil)
("5" (assert) 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)
(prewalk type-eq-decl nil walks nil)
(walk? const-decl "bool" walks nil)
(Walk type-eq-decl nil walks nil)
(subgraph? const-decl "bool" subgraphs nil)
(Subgraph type-eq-decl nil subgraphs nil)
(G_from const-decl "Subgraph(G)" subgraphs_from_walk nil)
(cyclically_reduced? const-decl "bool" circuits nil)
(edge?_G_from_rev formula-decl nil subgraphs_from_walk nil)
(pre_circuit? const-decl "bool" walks nil)
(edge?_G_from formula-decl nil subgraphs_from_walk nil)
(vert_G_from formula-decl nil subgraphs_from_walk nil)
(reduced? const-decl "bool" circuits nil)
(reducible? const-decl "bool" circuits nil)
(verts_of const-decl "finite_set[T]" walks nil)
(circuit? const-decl "bool" circuits nil))
nil))
(circuit_subgraph_len_1_TCC1 0
(circuit_subgraph_len_1_TCC1-1 nil 3251049115
("" (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)
(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)
(walk? const-decl "bool" walks nil)
(Walk type-eq-decl nil walks 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)
(G!1 skolem-const-decl "graph[T]" circuit_deg nil)
(edge? const-decl "bool" graphs nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nil application-judgement "finite_set[T]" circuit_deg nil)
(T formal-type-decl nil circuit_deg nil)
(verts_in? const-decl "bool" walks nil)
(/= const-decl "boolean" notequal nil))
nil))
(circuit_subgraph_len_1 1
(circuit_subgraph_len_1-2 "why long" 3368532619
("" (skosimp*)
(("" (lemma "circuit_deg")
(("" (inst?)
(("" (typepred "w!1")
(("" (inst -3 "0")
(("" (bddsimp)
(("" (hide -3)
(("" (lemma "finite_sets[T].card_empty?")
(("" (inst?)
(("" (iff)
(("" (lemma "finite_sets[T].card_one")
(("" (inst?)
(("" (expand "deg")
(("" (expand "incident_edges")
((""
(bddsimp -2)
(("1"
(expand "empty?")
(("1"
(expand "member")
(("1"
(inst -2 "seq(w!1)(0)")
(("1"
(hide -1 -2 -5 2)
(("1"
(install-rewrites "walks[T]")
(("1"
(assert)
(("1"
(inst 1 "0")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "finite_sets[T].card_empty?")
(("2"
(inst
-1
"({e: doubleton[T] |
edges(G_from(G!1, w!1))(e) AND e(seq(w!1)(0))})")
(("1"
(iff)
(("1"
(bddsimp)
(("1"
(hide -2 -3 -4 3)
(("1"
(expand "singleton_elt")
(("1"
(expand "member")
(("1"
(expand "the")
(("1"
(lemma
"finite_sets[doubleton[T]].nonempty_card")
(("1"
(inst
-1
"{e: doubleton[T] |
edges(G_from(G!1, w!1))(e) AND e(seq(w!1)(0))}")
(("1"
(bddsimp)
(("1"
(expand
"nonempty?")
(("1"
(expand
"empty?")
(("1"
(skosimp*)
(("1"
(expand
"member")
(("1"
(reveal
1)
(("1"
(flatten)
(("1"
(hide
-3
-8)
(("1"
(lemma
"edge_in_card_gt_1")
(("1"
(inst
-1
"G_from(G!1, w!1)"
"x!1")
(("1"
(prop)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(hide -1 -4 2 3)
(("2"
(lemma
"finite_sets[doubleton[T]].finite_subset")
(("2"
(inst
-1
"{e: doubleton[T] |
edges(G_from[T](G!1, w!1))(e) }"
"{e: doubleton[T] |
edges(G_from[T](G!1, w!1))(e) AND e(seq(w!1)(0))}")
(("1"
(bddsimp)
(("1"
(hide 2)
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand
"G_from")
(("2"
(expand
"edges_of")
(("2"
(lemma
"finite_sets[doubleton[T]].finite_subset")
(("2"
(inst
-1
"{e: doubleton[T] |
edges(G!1)(e) }"
"{e: doubleton[T] |EXISTS (i: below(length(w!1) - 1)):
e = dbl(seq(w!1)(i), seq(w!1)(1 + i))
}")
(("1"
(bddsimp)
(("1"
(hide
2)
(("1"
(install-rewrites
"walks[T]")
(("1"
(assert)
(("1"
(bddsimp)
(("1"
(skosimp*)
(("1"
(replace
-1
1
lr)
(("1"
(inst
-4
"i!1")
(("1"
(typepred
"i!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(install-rewrites
"graphs[T]")
(("2"
(typepred
"G!1")
(("2"
(typepred
"edges(G!1)")
(("2"
(hide
-2
-4)
(("2"
(case
"edges(G!1)={e: doubleton[T] | edges(G!1)(e)}")
(("1"
(replace
-1
-2
lr)
(("1"
(propax)
nil
nil))
nil)
("2"
(hide
-1
2)
(("2"
(grind)
(("2"
(apply-extensionality
1
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.88Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
