Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
circuits.prf
Sprache: Lisp
|
(Eulerian
(no_repeat_subseq?_TCC1 0
(no_repeat_subseq?_TCC1-1 nil 3561330533 ("" (subtype-tcc) nil nil)
nil nil))
(no_repeat_subseq?_TCC2 0
(no_repeat_subseq?_TCC2-1 nil 3561330533 ("" (subtype-tcc) nil nil)
nil nil))
(no_repeat_subseq?_TCC3 0
(no_repeat_subseq?_TCC3-1 nil 3561330533 ("" (subtype-tcc) nil nil)
nil nil))
(no_repeat_subseq?_TCC4 0
(no_repeat_subseq?_TCC4-1 nil 3561330533 ("" (subtype-tcc) nil nil)
nil nil))
(cycle_is_pre_Eulerian_circuit 0
(cycle_is_pre_Eulerian_circuit-1 nil 3564331623
("" (skeep)
(("" (expand "cycle?")
(("" (expand "pre_Eulerian_circuit?")
(("" (flatten)
(("" (assert)
(("" (expand "pre_Eulerian_walk?")
(("" (expand "circuit?")
(("" (expand "pre_circuit?")
(("" (flatten)
(("" (assert)
(("" (expand "no_repeat_subseq?")
(("" (expand "finseq_appl")
(("" (skeep)
(("" (inst -4 "i" "j")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cycle? const-decl "bool" cycles nil)
(pre_Eulerian_walk? const-decl "bool" Eulerian nil)
(pre_circuit? const-decl "bool" circuits 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)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil Eulerian 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(no_repeat_subseq? const-decl "bool" Eulerian nil)
(circuit? const-decl "bool" circuits nil)
(pre_Eulerian_circuit? const-decl "bool" Eulerian nil))
shostak))
(pre_Eulerian_circuit_is_a_circuit 0
(pre_Eulerian_circuit_is_a_circuit-1 nil 3559650097
("" (auto-rewrite "finseq_appl")
(("" (skeep)
((""
(expand* "pre_Eulerian_circuit?" "circuit?"
"pre_Eulerian_walk?" "pre_circuit?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(pre_Eulerian_circuit? const-decl "bool" Eulerian nil)
(pre_Eulerian_walk? const-decl "bool" Eulerian nil)
(pre_circuit? const-decl "bool" circuits nil)
(circuit? const-decl "bool" circuits nil))
shostak))
(Eulerian_circuit_is_circuit 0
(Eulerian_circuit_is_circuit-1 nil 3561331484
("" (auto-rewrite "finseq_appl")
(("" (skeep)
((""
(expand* "Eulerian_circuit?" "pre_Eulerian_circuit?" "circuit?"
"pre_circuit?" "pre_Eulerian_walk?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(Eulerian_circuit? const-decl "bool" Eulerian nil)
(circuit? const-decl "bool" circuits nil)
(pre_Eulerian_walk? const-decl "bool" Eulerian nil)
(pre_circuit? const-decl "bool" circuits nil)
(pre_Eulerian_circuit? const-decl "bool" Eulerian nil))
shostak))
(Eulerian_walk_is_Eulerian_circuit 0
(Eulerian_walk_is_Eulerian_circuit-1 nil 3561331889
("" (auto-rewrite "finseq_appl")
(("" (skeep)
((""
(expand* "Eulerian_circuit?" "pre_Eulerian_circuit?"
"Eulerian_walk?" "pre_Eulerian_walk?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((Eulerian_circuit? const-decl "bool" Eulerian nil)
(Eulerian_walk? const-decl "bool" Eulerian nil)
(pre_Eulerian_walk? const-decl "bool" Eulerian nil)
(pre_Eulerian_circuit? const-decl "bool" Eulerian nil))
shostak))
(circuit_subwalk_pre_Eulerian_TCC1 0
(circuit_subwalk_pre_Eulerian_TCC1-1 nil 3563040767
("" (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)
(edgetype type-eq-decl nil digraphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(predigraph type-eq-decl nil digraphs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(digraph type-eq-decl nil digraphs 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)
(T formal-type-decl nil Eulerian nil)
(verts_in? const-decl "bool" walks nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(edge? const-decl "bool" digraphs nil)
(walk? const-decl "bool" walks nil)
(pre_circuit? const-decl "bool" circuits nil)
(circuit? const-decl "bool" circuits nil))
nil))
(circuit_subwalk_pre_Eulerian 0
(circuit_subwalk_pre_Eulerian-1 nil 3563040846
("" (skeep)
(("" (lemma "circuit_subwalk_cycle")
(("" (inst -1 "G" "w")
(("" (assert)
(("" (skeep)
(("" (inst 1 "w1")
(("" (assert)
(("" (rewrite "cycle_is_pre_Eulerian_circuit") nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil Eulerian nil)
(circuit_subwalk_cycle formula-decl nil cycles nil)
(cycle_is_pre_Eulerian_circuit formula-decl nil Eulerian 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)
(digraph type-eq-decl nil digraphs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(predigraph type-eq-decl nil digraphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(edgetype type-eq-decl nil digraphs nil))
shostak))
(pre_Eulerian_circuit_prefix_TCC1 0
(pre_Eulerian_circuit_prefix_TCC1-1 nil 3563121186
("" (subtype-tcc) nil nil)
((T formal-type-decl nil Eulerian nil)
(verts_in? const-decl "bool" walks nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(edge? const-decl "bool" digraphs nil)
(walk? const-decl "bool" walks nil)
(pre_circuit? const-decl "bool" circuits nil)
(circuit? const-decl "bool" circuits nil)
(no_repeat_subseq? const-decl "bool" Eulerian nil)
(pre_Eulerian_walk? const-decl "bool" Eulerian nil)
(pre_Eulerian_circuit? const-decl "bool" Eulerian nil)
(O const-decl "finseq" finite_sequences nil))
nil))
(pre_Eulerian_circuit_prefix 0
(pre_Eulerian_circuit_prefix-1 nil 3563121188
("" (skeep)
(("" (lemma "cycle_prefix")
(("" (inst -1 "G" "w")
(("" (assert)
(("" (split)
(("1" (rewrite "cycle_is_pre_Eulerian_circuit") nil nil)
("2" (skeep)
(("2" (inst 2 "w1" "w2")
(("2" (assert)
(("2" (hide-all-but (-2 2))
(("2" (rewrite "cycle_is_pre_Eulerian_circuit") nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil Eulerian nil)
(cycle_prefix formula-decl nil cycles nil)
(cycle_is_pre_Eulerian_circuit formula-decl nil Eulerian 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)
(digraph type-eq-decl nil digraphs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(predigraph type-eq-decl nil digraphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(edgetype type-eq-decl nil digraphs nil))
shostak))
(pre_Eulerian_circuit_o_circuit_TCC1 0
(pre_Eulerian_circuit_o_circuit_TCC1-1 nil 3563123153
("" (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)
(edgetype type-eq-decl nil digraphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(predigraph type-eq-decl nil digraphs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(digraph type-eq-decl nil digraphs 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)
(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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(T formal-type-decl nil Eulerian nil)
(verts_in? const-decl "bool" walks nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(edge? const-decl "bool" digraphs nil)
(walk? const-decl "bool" walks nil)
(pre_circuit? const-decl "bool" circuits nil)
(circuit? const-decl "bool" circuits nil)
(no_repeat_subseq? const-decl "bool" Eulerian nil)
(pre_Eulerian_walk? const-decl "bool" Eulerian nil)
(pre_Eulerian_circuit? const-decl "bool" Eulerian nil)
(rest const-decl "finseq" seq_extras "structures/")
(O const-decl "finseq" finite_sequences nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(pre_Eulerian_circuit_o_circuit 0
(pre_Eulerian_circuit_o_circuit-1 nil 3563036557
("" (skeep)
(("" (lemma "cycle_o_circuit")
(("" (inst -1 "G" "w")
(("" (assert)
(("" (split)
(("1" (hide -2 2)
(("1" (rewrite "cycle_is_pre_Eulerian_circuit") nil nil))
nil)
("2" (skeep)
(("2" (inst 2 "w1" "w2")
(("2" (assert)
(("2" (hide-all-but (-2 2))
(("2" (rewrite "cycle_is_pre_Eulerian_circuit") nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil Eulerian nil)
(cycle_o_circuit formula-decl nil cycles nil)
(cycle_is_pre_Eulerian_circuit formula-decl nil Eulerian 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)
(digraph type-eq-decl nil digraphs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(predigraph type-eq-decl nil digraphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(edgetype type-eq-decl nil digraphs nil))
shostak)))
[ Seitenstruktur0.32Drucken
etwas mehr zur Ethik
]
|
|
