Quelle circuit_deg.prf
Sprache: Lisp
(circuit_deg"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" "1" "1" "dbl[T](a!1, z!1)" )"1" "dbl[T](b!1, z!1)" )"1" "1" "doubletons[T]" )"1" assert )"1" replace -3 -6 rl)"1" "1" "1" "doubletons[T].dbl_eq" )"1" "a!1" "b!1" "z!1" "z!1" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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 )"bool" graphs nil )"nat" graph_deg nil )"(singleton?)" sets nil )nil doubletons nil )"non_empty_finite_set" finite_sets nil )nil finite_sets nil )"(total_order?[real])" nil )nil finite_sets nil )"bool" sets nil )"bool" sets nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil circuit_deg nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"set[T]" doubletons nil )nil doubletons nil )"bool" finite_sets nil )nil finite_sets nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"finite_set[doubleton[T]]" graph_degnil ))nil 3251049115"" (skosimp*)"" (expand "edge?" )"" (flatten)"" (expand "deg" )"" case "subset?(e_duo(dbl(a!1,z!1),dbl(b!1,z!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" "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" "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" "1" assert )"1" expand "dbl" )"1" (propax) nil )))))))))"2" (replace -1)"2" "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" nil )))))))))))))))))))))))"3" (inst 1 "b!1" "z!1" ) (("3" (assert ) nil )))"4" (inst?) (("4" (assert ) nil ))))))))))))nil )"bool" graphs nil )"nat" graph_deg nil )nil doubletons nil )"set[T]" doubletons nil )nil doubletons nil )nil graphs nil )nil graphs nil )"finite_set[doubleton[T]]" graph_degnil ))nil ))nil 3251049115 ("" (subtype-tcc) nil nil )nil booleans nil )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 )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil graphs nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )"bool" walks nil )nil walks nil ) (< const-decl "bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"graph[T]" circuit_deg nil )"bool" graphs nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set[T]" circuit_deg nil )nil circuit_deg nil )"bool" walks nil )"boolean" notequal nil ))nil ))"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" "w!1(1)" "w!1(length(w!1)-2)" )"1" expand "finseq_appl" )"1" "1" "1" "walks[T]" )"1" assert )"1" "i!1" )nil nil ))nil ))nil ))nil )"2" replace -1 1 lr)"2" replace -5 * rl)"2" "2" "walks[T]" )"2" assert )"2" "1" "w!1" )"1" expand "walk?" )"1" expand "finseq_appl" )"1" "1" "0" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "0" )"2" assert )"2" expand "dbl" )"2" "2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" replace -1 1 lr)"3" "3" "w!1" )"3" expand "walk?" )"3" expand "finseq_appl" )"3" "3" "length(w!1)-2" )"1" assert )"1" "walks[T]" )"1" assert )"1" "1" "1" "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" "walks[T]" )"2" assert )"2" "length(w!1)-2" )nil nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil )"4" "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" " w!1`seq(1)" "w!1`seq(length(w!1) - 2)" )"1" "1" "1" "w!1" )"1" "walks[T]" )"1" assert )"1" (inst 1 "0" ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "w!1" )"2" "walks[T]" )"2" assert )"2" "1" "0" )"1" "1" (assert ) nil nil )"2" assert )nil nil ))nil ))nil )"2" "0" )"2" "2" assert )"2" "dbl_comm" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "pre_circuit?" )"3" expand "finseq_appl" )"3" replace -4 1 lr)"3" "3" "w!1" )"3" "walks[T]" )"3" assert )"3" "3" "1" assert )"1" "1" "length(w!1)-2" )"1" assert )nil nil ))nil ))nil ))nil )"2" "length(w!1)-2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "walks[T]" )"2" assert )"2" "length(w!1)-2" )nil nil ))nil ))nil ))nil )"3" (assert ) nil nil )"4" "4" "walks[T]" )"4" assert )"4" (inst 1 "1" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "seq(w!1)(i!1-1)" "seq(w!1)(i!1+1)" )"1" "1" "1" "1" "walks[T]" )"1" assert )"1" "1" assert )"1" "w!1" )"1" assert )"1" "1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" rewrite "dbl_comm" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "w!1" )"2" "walks[T]" )"2" assert )"2" "1" "i!1-1" )"1" (assert ) nil nil ))nil )"2" "i!1-1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "reduced?" )"3" expand "reducible?" )"3" expand "finseq_appl" )"3" "i!1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" "w!1" )"4" "walks[T]" )"4" assert )"4" (inst 3 "i!1" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "w!1" )"2" "walks[T]" )"2" assert )"2" "2" "i!1+1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil )"4" "4" "w!1" )"4" "walks[T]" )"4" assert )"4" "4" "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 )nil circuit_deg nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" circuits nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" circuits nil )"bool" circuits nil )"int" integers nil )nil application-judgement "finite_set[T]" circuit_deg nil )"finite_set[doubleton[T]]" walks nil )"bool" graphs nil )OR const-decl "[bool, bool -> bool]" booleans nil )"posint" nil )"odd_int" integers nil )"bool" walks nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"finite_set[T]" walks nil )"Walk[T](G!1)" circuit_deg nil )"graph[T]" circuit_deg nil )"(total_order?[real])" nil )"bool" walks nil )"posint" nil )"below(length(w!1))" circuit_deg nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )nil integers nil )nil doubletons nil )"bool" circuits nil )NOT const-decl "[bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"Subgraph(G)" subgraphs_from_walk nil )nil subgraphs nil )"bool" subgraphs nil )nil walks nil )"bool" walks nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil circuit_deg nil ))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 )"set[T]" doubletons nil )nil doubletons nil )nil graphs nil )nil graphs nil )nil walks nil )"bool" walks nil )nil walks nil )"bool" subgraphs nil )nil subgraphs nil )"Subgraph(G)" subgraphs_from_walk nil )"bool" circuits nil )nil subgraphs_from_walk nil )"bool" walks nil )nil subgraphs_from_walk nil )nil subgraphs_from_walk nil )"bool" circuits nil )"bool" circuits nil )"finite_set[T]" walks nil )"bool" circuits nil ))nil ))nil 3251049115"" (subtype-tcc) nil nil )nil booleans nil )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 )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil graphs nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )"bool" walks nil )nil walks nil ) (< const-decl "bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"graph[T]" circuit_deg nil )"bool" graphs nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set[T]" circuit_deg nil )nil circuit_deg nil )"bool" walks nil )"boolean" notequal nil ))nil ))"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" )"" "1" expand "empty?" )"1" expand "member" )"1" "seq(w!1)(0)" )"1" "1" "walks[T]" )"1" assert )"1" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_sets[T].card_empty?" )"2" "({e: doubleton[T] | AND e(seq(w!1)(0))})") "1" "1" "1" "1" expand "singleton_elt" )"1" expand "member" )"1" expand "the" )"1" "finite_sets[doubleton[T]].nonempty_card" )"1" "{e: doubleton[T] | AND e(seq(w!1)(0))}") "1" "1" expand "nonempty?" )"1" expand "empty?" )"1" "1" expand "member" )"1" "1" "1" "1" "edge_in_card_gt_1" )"1" "G_from(G!1, w!1)" "x!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" "finite_sets[doubleton[T]].finite_subset" )"2" "{e: doubleton[T] | " "{e: doubleton[T] | AND e(seq(w!1)(0))}") "1" "1" "1" nil nil ))nil ))nil )"2" "2" expand "G_from" )"2" expand "edges_of" )"2" "finite_sets[doubleton[T]].finite_subset" )"2" "{e: doubleton[T] | " "{e: doubleton[T] |EXISTS (i: below(length(w!1) - 1)): ") "1" "1" "1" "walks[T]" )"1" assert )"1" "1" "1" replace "1" "i!1" )"1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "graphs[T]" )"2" "G!1" )"2" "edges(G!1)" )"2" "2" case "edges(G!1)={e: doubleton[T] | edges(G!1)(e)}" )"1" replace "1" nil nil ))nil )"2" "2" "2" 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" (assert ) nil nil )"3" "3" expand "empty?" 1)"3" "3" expand "member" )"3" "edge_in_card_gt_1" )"3" "G_from(G!1,w!1)" "x!1" )"1" "1" assert )nil nil )"2" expand "singleton_elt" )"2" expand "singleton" )"2" expand "member" )"2" expand "the" )"2" "2" "epsilons[doubleton[T]].epsilon_ax" )"1" "LAMBDA (x: doubleton[T]): AND x(seq(w!1)(0))") "1" "1" "1" "edge_in_card_gt_1" )"1" "G_from(G!1,w!1)" "epsilon(LAMBDA (x: doubleton[T]): AND x(seq(w!1)(0)))") "1" assert )nil nil )"2" "finite_sets[doubleton[T]].nonempty_card" )"2" "{e: doubleton[T] | AND e(seq(w!1)(0))}") "1" assert )"1" "1" expand "nonempty?" )"1" expand "empty?" )"1" "1" expand "member" )"1" "1" "x!3" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "finite_sets[doubleton[T]].finite_subset" )"2" "{e: doubleton[T] | " "{e: doubleton[T] | AND e(seq(w!1)(0))}") "1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" expand "G_from" )"2" expand "edges_of" )"2" "finite_sets[doubleton[T]].finite_subset" )"2" "{e: doubleton[T] | " "{e: doubleton[T] |EXISTS (i: below(length(w!1) - 1)): ") "1" "1" "1" "walks[T]" )"1" assert )"1" "1" "1" replace "1" "i!1" )"1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "graphs[T]" )"2" "G!1" )"2" "edges(G!1)" )"2" "2" case "edges(G!1)={e: doubleton[T] | edges(G!1)(e)}" )"1" replace "1" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_sets[doubleton[T]].nonempty_card" )"2" "{e: doubleton[T] | AND e(seq(w!1)(0))}") "1" "1" "1" assert )"1" expand "nonempty?" )"1" expand "empty?" )"1" "1" "1" expand "member" )"1" "x!3" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "finite_sets[doubleton[T]].finite_subset" )"2" "{e: doubleton[T] | " "{e: doubleton[T] | AND e(seq(w!1)(0))}") "1" "1" "1" nil nil ))nil ))nil )"2" "2" expand "G_from" )"2" expand "edges_of" )"2" "finite_sets[doubleton[T]].finite_subset" )"2" "{e: doubleton[T] | " "{e: doubleton[T] |EXISTS (i: below(length(w!1) - 1)): ") "1" "1" "1" "walks[T]" )"1" assert )"1" "1" "i!1" )"1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "graphs[T]" )"2" "edges(G!1)" )"2" case "edges(G!1)={e: doubleton[T] | edges(G!1)(e)}" )"1" replace "1" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_sets[doubleton[T]].nonempty_card" )"2" "2" "{e: doubleton[T] | AND e(seq(w!1)(0))}") "1" expand "nonempty?" )"1" expand "empty?" )"1" "1" assert )nil nil )"2" "2" expand "member" )"2" "x!3" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_sets[doubleton[T]].finite_subset" )"2" "{e: doubleton[T] | " "{e: doubleton[T] | AND e(seq(w!1)(0))}") "1" "1" "1" nil nil ))nil ))nil )"2" "2" expand "G_from" )"2" expand "edges_of" )"2" "finite_sets[doubleton[T]].finite_subset" )"2" "{e: doubleton[T] | " "{e: doubleton[T] |EXISTS (i: below(length(w!1) - 1)): ") "1" "1" "1" "walks[T]" )"1" assert )"1" "1" "i!1" )"1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "graphs[T]" )"2" "edges(G!1)" )"2" case "edges(G!1)={e: doubleton[T] | edges(G!1)(e)}" )"1" replace "1" nil nil ))nil )"2" "2" 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" "2" "1" "1" "1" expand "singleton" )"1" expand "G_from" )"1" expand "verts_of" )"1" "1" "1" "seq(w!1)(0)" )"1" "1" "1" "1" "seq(w!1)(1)" )"1" "1" "1" replace "1" nil nil ))nil )"2" "1" )nil nil ))nil ))nil ))nil ))nil )"2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "walks[T]" )"2" "2" expand "circuit?" )"2" "2" expand "cyclically_reduced?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (assert ) nil nil ))nil ))nil )"2" "walks[T]" )"2" "2" expand "circuit?" )"2" "2" expand "cyclically_reduced?" )"2" "2" "2" assert )"2" expand "verts_of" )"2" case " card({t: T | EXISTS (i: below(length(w!1))): seq(w!1)(i) = t}) =1" )"1" assert )"1" "1" "1" "finite_sets[T].card_one" )"1" "1" "1" "1" "1" "1" "1" "seq(w!1)(0)" )"1" "seq(w!1)(1)" )"1" "1" "1" "0" )"1" assert )nil nil ))nil )"2" "1" )nil nil )"3" "0" )nil nil )"4" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "is_finite({t: T | EXISTS (i: below(length(w!1))): seq(w!1)(i) = t})" )"1" "1" nil nil ))nil )"2" "2" "finite_sets[T].finite_subset" )"2" "vert(G!1)" )"2" "vert(G!1)" "{t: T | EXISTS (i: below(length(w!1))): seq(w!1)(i) = t}" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "is_finite({t: T | EXISTS (i: below(length(w!1))): seq(w!1)(i) = t})" )"1" "1" nil nil ))nil )"2" "2" "finite_sets[T].finite_subset" )"2" "vert(G!1)" )"2" "vert(G!1)" "{t: T | EXISTS (i: below(length(w!1))): seq(w!1)(i) = t}" )"2" "2" "2" 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 )"finite_set[doubleton[T]]" graph_degnil )"bool" circuits nil )"bool" circuits nil )"finite_set[doubleton[T]]" walks nil )nil graphs nil )nil doubletons nil )"bool" graphs nil )"bool" walks nil )"finite_set[T]" walks nil )"nat" graph_deg nil )"bool" subgraphs nil )nil subgraphs nil )"Subgraph(G)" subgraphs_from_walk nil )nil walks nil )"bool" walks nil )nil walks nil )nil graphs nil )nil graphs nil )nil doubletons nil )"set[T]" doubletons nil ))nil 3251049115"" (skosimp*)"" (expand "circuit?" )"" (expand "cyclically_reduced?" )"" (expand "pre_circuit?" )"" (flatten)"" (typepred "w!1" )"" (expand "walk?" )"" (flatten)"" case "subset?(add[T](finseq_appl(w!1)(0), singleton[T](finseq_appl(w!1)(1))),vert(G_from(G!1, w!1)))" )"1" (lemma "card_subset[T]" )"1" (inst?)"1" (assert )"1" "card(add[T](finseq_appl(w!1)(0), singleton[T](finseq_appl(w!1)(1)))) = 2" )"1" (assert ) nil nil )"2" (hide -1 -2 -3 -4 -5 -6 -7 -8 2 3)"2" rewrite "card_add" )"2" rewrite "card_singleton" )"2" "2" "2" "2" expand "singleton" )"2" "w!1" )"2" expand "walk?" )"2" "2" assert )"2" expand "edge?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2 -3 -5 -6 3)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" circuits nil )"bool" walks nil )nil walks nil )"bool" walks nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil walks nil )nil finite_sequences nil )nil circuit_deg nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil naturalnumbers nil )"finite_set[T]" walks nil )"bool" sets nil )nil finite_sets nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"non_empty_finite_set" finite_sets nil )"(partial_order?[set[T]])" nil )nil finite_sets nil )"even_int" integersnil )"posint" nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" graphs nil )nil application-judgement "finite_set[T]" circuit_deg nil )"nonneg_int" nil )nil finite_sets nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"bool" finite_sets nil )"non_empty_finite_set" nil )"bool" sets nil )"bool" sets nil )"(nonempty?)" sets nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" sets nil )"(singleton?)" sets nil )"bool" subgraphs nil )nil subgraphs nil )"Subgraph(G)" subgraphs_from_walk nil )"bool" circuits nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.84 Sekunden
(vorverarbeitet am 2026-04-29)
¤ *© Formatika GbR, Deutschland
2026-05-26
