diff --git a/NEWS b/NEWS index 8284ce0cc..022609fa9 100644 --- a/NEWS +++ b/NEWS @@ -38,11 +38,8 @@ New in spot 2.9.8.dev (not yet released) a strategy for each subformula before recombining them into a circuit. - - ltlsynt -x "minimization-level=[0-5]" determines how to minimize - the strategy (a monitor). 0, no minimization; 1, regular DFA - minimization; 2, signature based minimization with - output assignement; 3, SAT based minimization; 4, 1 then 3; - 5, 2 then 3. + - ltlsynt --simplify=no|bisim|bwoa|sat|bisim-sat|bwoa-sat + specifies how to simplify the synthesized controler. - ltl2tgba, autfilt, dstar2tgba, and randaut learned a --buchi option, or -b for short. This outputs Büchi automata without diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 9047046ef..29dd5ce0c 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -51,6 +51,7 @@ enum OPT_PRINT_AIGER, OPT_PRINT_HOA, OPT_REAL, + OPT_SIMPLIFY, OPT_VERBOSE, OPT_VERIFY }; @@ -78,7 +79,13 @@ static const argp_option options[] = " \"lar.old\": old version of LAR, for benchmarking.\n", 0 }, { "decompose", OPT_DECOMPOSE, "yes|no", 0, "whether to decompose the specification as multiple output-disjoint " - "problems to solve independently (enabled by default)", 0}, + "problems to solve independently (enabled by default)", 0 }, + { "simplify", OPT_SIMPLIFY, "no|bisim|bwoa|sat|bisim-sat|bwoa-sat", 0, + "simplification to apply to the controler (no) nothing, " + "(bisim) bisimulation-based reduction, (bwoa) bissimulation-based " + "reduction with output assignment, (sat) SAT-based minimization, " + "(bisim-sat) SAT after bisim, (bwoa-sat) SAT after bwoa. Defaults " + "to 'bwoa'.", 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Output options:", 20 }, { "print-pg", OPT_PRINT, nullptr, 0, @@ -182,6 +189,27 @@ static bool decompose_values[] = ARGMATCH_VERIFY(decompose_args, decompose_values); bool opt_decompose_ltl = true; +static const char* const simplify_args[] = + { + "no", "false", "disabled", "0", + "bisim", "1", + "bwoa", "bisim-with-output-assignment", "2", + "sat", "3", + "bisim-sat", "4", + "bwoa-sat", "5", + nullptr + }; +static unsigned simplify_values[] = + { + 0, 0, 0, 0, + 1, 1, + 2, 2, 2, + 3, 3, + 4, 4, + 5, 5, + }; +ARGMATCH_VERIFY(simplify_args, simplify_values); + namespace { auto str_tolower = [] (std::string s) @@ -389,11 +417,12 @@ namespace { spot::stopwatch sw_min; sw_min.start(); - bool do_split = 3 <= gi->opt.get("minimization-level", 1); + unsigned simplify = gi->minimize_lvl; + bool do_split = 3 <= simplify; if (do_split) split_2step_fast_here(strat.strat_like, spot::get_synthesis_outputs(strat.strat_like)); - minimize_strategy_here(strat.strat_like, gi->minimize_lvl); + minimize_strategy_here(strat.strat_like, simplify); if (do_split) strat.strat_like = spot::unsplit_2step(strat.strat_like); auto delta = sw_min.stop(); @@ -619,6 +648,10 @@ parse_opt(int key, char *arg, struct argp_state *) case OPT_REAL: opt_real = true; break; + case OPT_SIMPLIFY: + gi->minimize_lvl = XARGMATCH("--simplify", arg, + simplify_args, simplify_values); + break; case OPT_VERBOSE: gi->verbose_stream = &std::cerr; if (not gi->bv) @@ -632,8 +665,6 @@ parse_opt(int key, char *arg, struct argp_state *) const char* opt = gi->opt.parse_options(arg); if (opt) error(2, 0, "failed to parse --options near '%s'", opt); - // Dispatch the options to the gi structure - gi->minimize_lvl = gi->opt.get("minimization-level", 1); } break; } diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 4977c8e42..c4905c2e9 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -237,18 +237,6 @@ sets. By default this is only enabled when options -B or -S are used.") }, "Chose which simulation based reduction to use: 1 force the \ signature-based BDD implementation, 2 force matrix-based and 0, the default, \ is a heristic wich choose which implementation to use.") }, - { nullptr, 0, nullptr, 0, "Synthesis options:", 0 }, - { DOC("minimization-level", - "Specify how AIGER circuits should be simplified. " - "(0) no simplification, " - "(1) bisimulation-based reduction, " - "(2) simplification using language inclusion and output assignments, " - "(3) exact minimization using a SAT solver, " - "(4) bisimulation-based reduction before exact minimization via " - "SAT solver, " - "(5) simplification using output assignments before exact " - "minimization via SAT solver. " - "The default value is 1.") }, { nullptr, 0, nullptr, 0, nullptr, 0 } }; diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org index 9b62bb587..45b4b2b1c 100644 --- a/doc/org/ltlsynt.org +++ b/doc/org/ltlsynt.org @@ -136,23 +136,35 @@ Otherwise, conversion to parity game (represented by the blue zone) is done using one of several algorithms specified by the =--algo= option. The game is then solved, producing a strategy if the game is realizable. -If an =ltlsynt= is in =--realizability= mode, the process stops here +If =ltlsynt= is in =--realizability= mode, the process stops here + +In synthesis mode, the strategy is first simplified. How this is done +can be fine-tuned with option =--simplify=: +#+BEGIN_SRC sh :exports results +ltlsynt --help | sed -n '/--simplify=/,/^$/p' | sed '$d' +#+END_SRC +#+RESULTS: +: --simplify=no|bisim|bwoa|sat|bisim-sat|bwoa-sat +: simplification to apply to the controler (no) +: nothing, (bisim) bisimulation-based reduction, +: (bwoa) bissimulation-based reduction with output +: assignment, (sat) SAT-based minimization, +: (bisim-sat) SAT after bisim, (bwoa-sat) SAT after +: bwoa. Defaults to 'bwoa'. -In =--aiger= mode, the strategy is first simplified. How this is done -is controled by option =-x minimize-level=N=. See the [[./man/spot-x.7.html][=spot-x=]](7) -manpage for details. Finally, the strategy is encoded into [[http://fmv.jku.at/aiger/][AIGER]]. The =--aiger= option can -take an argument to specify a type of encoding to use: by default -it is =ite= for if-then-else, because it follows the structure of BDD -used to encode the conditions in the strategy. An alternative encoding -is =isop= where condition are first put into irredundant-sum-of-product, -or =both= if both encodings should be tried. Additionally, these optiosn -can accept the suffix =+ud= (use dual) to attempt to encode each condition -and its negation and keep the smallest one, =+dc= (don't care) to take -advantage of /don't care/ values in the output, and one of =+sub0=, -=+sub1=, or =+sub2= to test various grouping of variables in the encoding. -Multiple encodings can be tried by separating them using commas. -For instance =--aiger=isop,isop+dc,isop+ud= will try three different encodings. +take an argument to specify a type of encoding to use: by default it +is =ite= for if-then-else, because it follows the structure of BDD +used to encode the conditions in the strategy. An alternative +encoding is =isop= where condition are first put into +irredundant-sum-of-product, or =both= if both encodings should be +tried. Additionally, these optiosn can accept the suffix =+ud= (use +dual) to attempt to encode each condition and its negation and keep +the smallest one, =+dc= (don't care) to take advantage of /don't care/ +values in the output, and one of =+sub0=, =+sub1=, or =+sub2= to test +various grouping of variables in the encoding. Multiple encodings can +be tried by separating them using commas. For instance +=--aiger=isop,isop+dc,isop+ud= will try three different encodings. * Other useful options diff --git a/spot/twaalgos/game.hh b/spot/twaalgos/game.hh index 9f3530f12..add0325a6 100644 --- a/spot/twaalgos/game.hh +++ b/spot/twaalgos/game.hh @@ -132,7 +132,7 @@ namespace spot game_info() : force_sbacc{false}, s{solver::LAR}, - minimize_lvl{0}, + minimize_lvl{2}, bv{}, verbose_stream{nullptr}, dict(make_bdd_dict()) diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index a19da2fe9..37c5f46e0 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -156,7 +156,8 @@ i0 a o0 b o1 c EOF -ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' --algo=ds --aiger=isop >out +ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \ + --algo=ds --simplify=no --aiger=isop >out diff out exp cat >exp < (GFb & GFc)' \ - --algo=ds --aiger=isop+dc >out + --algo=ds --simplify=no --aiger=isop+dc >out diff out exp cat >exp < (GFb & GFc)' --algo=ds --aiger=ite >out +ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \ + --algo=ds --simplify=no --aiger=ite >out diff out exp cat >exp < out +ltlsynt --outs=p0 -x tls-impl=0 --simpl=no -f '!XXF(p0 & (p0 M Gp0))' > out diff out exp cat >exp <err grep 'DPA has 12 states' err +ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=no | grep 'States: 5' +ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bisim | grep 'States: 5' +ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bwoa | grep 'States: 4' +ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" | grep 'States: 4' +ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=sat | grep 'States: 2' +ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bisim-sat | grep 'States: 2' +ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bwoa-sat | grep 'States: 4' + cat >exp <X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\ - --aiger=isop --algo=lar --decompose=no >out + --aiger=isop --algo=lar --decompose=no --simpl=no >out diff out exp cat >exp <X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\ - --aiger=isop --algo=lar --decompose=yes >out + --aiger=isop --algo=lar --decompose=yes --simpl=no >out diff out exp ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\ - --aiger=isop --algo=lar >out + --aiger=isop --algo=lar --simpl=no >out diff out exp # Issue #477 diff --git a/tests/python/games.ipynb b/tests/python/games.ipynb index 09073f423..299a5e06d 100644 --- a/tests/python/games.ipynb +++ b/tests/python/games.ipynb @@ -47,153 +47,153 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "7->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -285,153 +285,153 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "7->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -499,153 +499,153 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", "\n", - "0\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", "\n", - "1\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", "\n", - "3\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", "\n", - "2\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", "\n", - "4\n", + "4\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", "\n", - "6\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", "\n", - "5\n", + "5\n", "\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", "\n", - "7\n", + "7\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", "\n", - "8\n", + "8\n", "\n", "\n", "\n", "7->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -698,649 +698,649 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | (Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")))\n", - "[parity max odd 4]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")))\n", + "[parity max odd 4]\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "I->9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "25\n", - "\n", - "25\n", + "\n", + "25\n", "\n", "\n", "\n", "9->25\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", "\n", "26\n", - "\n", - "26\n", + "\n", + "26\n", "\n", "\n", "\n", "9->26\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", "\n", "27\n", - "\n", - "27\n", + "\n", + "27\n", "\n", "\n", "\n", "9->27\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", "\n", "\n", "28\n", - "\n", - "28\n", + "\n", + "28\n", "\n", "\n", "\n", "9->28\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "0->10\n", - "\n", - "\n", - "!i1\n", - "\n", + "\n", + "\n", + "!i1\n", + "\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "0->11\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "i1\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "10->1\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "11->0\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", "\n", "\n", "1->12\n", - "\n", - "\n", - "!i1\n", - "\n", + "\n", + "\n", + "!i1\n", + "\n", "\n", "\n", "\n", "13\n", - "\n", - "13\n", + "\n", + "13\n", "\n", "\n", "\n", "1->13\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "i1\n", + "\n", "\n", "\n", "\n", "12->1\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "13->0\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "14\n", - "\n", - "14\n", + "\n", + "14\n", "\n", "\n", "\n", "2->14\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "i1\n", + "\n", "\n", "\n", "\n", "16\n", - "\n", - "16\n", + "\n", + "16\n", "\n", "\n", "\n", "2->16\n", - "\n", - "\n", - "!i1\n", - "\n", + "\n", + "\n", + "!i1\n", + "\n", "\n", "\n", "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", "\n", "\n", "14->15\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "16->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "3->13\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "i1\n", + "\n", "\n", "\n", "\n", "17\n", - "\n", - "17\n", + "\n", + "17\n", "\n", "\n", "\n", "3->17\n", - "\n", - "\n", - "!i1\n", - "\n", + "\n", + "\n", + "!i1\n", + "\n", "\n", "\n", "\n", "17->2\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "17->3\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "4->14\n", - "\n", - "\n", - "i0\n", - "\n", + "\n", + "\n", + "i0\n", + "\n", "\n", "\n", "\n", "18\n", - "\n", - "18\n", + "\n", + "18\n", "\n", "\n", "\n", "4->18\n", - "\n", - "\n", - "!i0\n", - "\n", + "\n", + "\n", + "!i0\n", + "\n", "\n", "\n", "\n", "18->4\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "5->14\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", "\n", "\n", "5->16\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", "\n", "5->18\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", "\n", "\n", "19\n", - "\n", - "19\n", + "\n", + "19\n", "\n", "\n", "\n", "5->19\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", "\n", "19->5\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", "\n", "6->11\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", "\n", "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", "\n", "\n", "6->20\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", "\n", "21\n", - "\n", - "21\n", + "\n", + "21\n", "\n", "\n", "\n", "6->21\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", "\n", "\n", "20->4\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "20->7\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "21->4\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "21->6\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "7->12\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", "\n", "7->13\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", "\n", "\n", "22\n", - "\n", - "22\n", + "\n", + "22\n", "\n", "\n", "\n", "7->22\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", "\n", "23\n", - "\n", - "23\n", + "\n", + "23\n", "\n", "\n", "\n", "7->23\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", "\n", "\n", "22->4\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "22->7\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "23->4\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "23->6\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->13\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", "\n", "\n", "8->17\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", "\n", "8->23\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", "\n", "\n", "24\n", - "\n", - "24\n", + "\n", + "24\n", "\n", "\n", "\n", "8->24\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", "\n", "24->5\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "24->8\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "25->8\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "26->3\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "27->6\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "28->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "15->14\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7c803ebb10> >" + " *' at 0x7f0ddc16bd50> >" ] }, "metadata": {}, @@ -1377,588 +1377,588 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | (Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")))\n", - "[parity max odd 4]\n", + " viewBox=\"0.00 0.00 650.45 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")))\n", + "[parity max odd 4]\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "I->9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "25\n", - "\n", - "25\n", + "\n", + "25\n", "\n", "\n", "\n", "9->25\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "26\n", - "\n", - "26\n", + "\n", + "26\n", "\n", "\n", "\n", "9->26\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "27\n", - "\n", - "27\n", + "\n", + "27\n", "\n", "\n", "\n", "9->27\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "28\n", - "\n", - "28\n", + "\n", + "28\n", "\n", "\n", "\n", "9->28\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "0->10\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "0->11\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "10->1\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "11->0\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", "\n", "\n", "1->12\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "13\n", - "\n", - "13\n", + "\n", + "13\n", "\n", "\n", "\n", "1->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "12->1\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "13->0\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "14\n", - "\n", - "14\n", + "\n", + "14\n", "\n", "\n", "\n", "2->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "16\n", - "\n", - "16\n", + "\n", + "16\n", "\n", "\n", "\n", "2->16\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", "\n", "\n", "14->15\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "16->2\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "3->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "17\n", - "\n", - "17\n", + "\n", + "17\n", "\n", "\n", "\n", "3->17\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "17->2\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "17->3\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "4->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "18\n", - "\n", - "18\n", + "\n", + "18\n", "\n", "\n", "\n", "4->18\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "18->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "5->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "5->16\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "5->18\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "19\n", - "\n", - "19\n", + "\n", + "19\n", "\n", "\n", "\n", "5->19\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "19->5\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "6->11\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", "\n", "\n", "6->20\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "21\n", - "\n", - "21\n", + "\n", + "21\n", "\n", "\n", "\n", "6->21\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "20->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "20->7\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "21->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "21->6\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "7->12\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "7->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "22\n", - "\n", - "22\n", + "\n", + "22\n", "\n", "\n", "\n", "7->22\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "23\n", - "\n", - "23\n", + "\n", + "23\n", "\n", "\n", "\n", "7->23\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "22->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "22->7\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "23->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "23->6\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "8->17\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "8->23\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "24\n", - "\n", - "24\n", + "\n", + "24\n", "\n", "\n", "\n", "8->24\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "24->5\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "24->8\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "25->8\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "26->3\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "27->6\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "28->0\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "15->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -1997,217 +1997,217 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "i0 & !i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!i0 & !i1 & !o0\n", + "\n", + "\n", + "!i0 & !i1 & !o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "i0 & !i1 & !o0\n", + "\n", + "\n", + "i0 & !i1 & !o0\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!i0 & i1 & !o0\n", + "\n", + "\n", + "!i0 & i1 & !o0\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "i0 & i1 & !o0\n", + "\n", + "\n", + "i0 & i1 & !o0\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!i1 & !o0\n", + "\n", + "\n", + "!i1 & !o0\n", "\n", "\n", "\n", "2->4\n", - "\n", - "\n", - "i1 & !o0\n", + "\n", + "\n", + "i1 & !o0\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!i0 & i1 & o0\n", + "\n", + "\n", + "!i0 & i1 & o0\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "i0 & i1 & o0\n", + "\n", + "\n", + "i0 & i1 & o0\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "3->5\n", - "\n", - "\n", - "i0 & !i1 & o0\n", + "\n", + "\n", + "i0 & !i1 & o0\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", - "!i0 & !i1 & o0\n", + "\n", + "\n", + "!i0 & !i1 & o0\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "i1 & o0\n", + "\n", + "\n", + "i1 & o0\n", "\n", "\n", "\n", "4->5\n", - "\n", - "\n", - "!i1 & o0\n", + "\n", + "\n", + "!i1 & o0\n", "\n", "\n", "\n", "5->4\n", - "\n", - "\n", - "i1 & !o0\n", + "\n", + "\n", + "i1 & !o0\n", "\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "!i1 & !o0\n", + "\n", + "\n", + "!i1 & !o0\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "!i0 & i1 & !o0\n", + "\n", + "\n", + "!i0 & i1 & !o0\n", "\n", "\n", "\n", "6->4\n", - "\n", - "\n", - "i0 & i1 & !o0\n", + "\n", + "\n", + "i0 & i1 & !o0\n", "\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "i0 & !i1 & !o0\n", + "\n", + "\n", + "i0 & !i1 & !o0\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "!i0 & !i1 & !o0\n", + "\n", + "\n", + "!i0 & !i1 & !o0\n", "\n", "\n", "\n" @@ -2232,123 +2232,123 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "i0 & !i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "i0 & !i1 & !o0\n", + "\n", + "\n", + "i0 & !i1 & !o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!i0 & !i1 & !o0\n", + "\n", + "\n", + "!i0 & !i1 & !o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "i0 & i1 & !o0\n", + "\n", + "\n", + "i0 & i1 & !o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!i0 & i1 & !o0\n", + "\n", + "\n", + "!i0 & i1 & !o0\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "i0 & !i1 & o0\n", + "\n", + "\n", + "i0 & !i1 & o0\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "!i0 & !i1 & o0\n", + "\n", + "\n", + "!i0 & !i1 & o0\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "i0 & i1 & o0\n", + "\n", + "\n", + "i0 & i1 & o0\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!i0 & i1 & o0\n", + "\n", + "\n", + "!i0 & i1 & o0\n", "\n", "\n", "\n" @@ -2373,89 +2373,89 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "i0 & i1 & o0\n", + "\n", + "\n", + "i0 & i1 & o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!i0 & i1 & o0\n", + "\n", + "\n", + "!i0 & i1 & o0\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "i0 & !i1 & o0\n", + "\n", + "\n", + "i0 & !i1 & o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!i0 & !i1 & o0\n", + "\n", + "\n", + "!i0 & !i1 & o0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "i0 & i1 & !o0\n", + "\n", + "\n", + "i0 & i1 & !o0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!i0 & i1 & !o0\n", + "\n", + "\n", + "!i0 & i1 & !o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "i0 & !i1 & !o0\n", + "\n", + "\n", + "i0 & !i1 & !o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!i0 & !i1 & !o0\n", + "\n", + "\n", + "!i0 & !i1 & !o0\n", "\n", "\n", "\n" @@ -2480,61 +2480,61 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "i1 & o0\n", + "\n", + "\n", + "i1 & o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!i1 & o0\n", + "\n", + "\n", + "!i1 & o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "i1 & !o0\n", + "\n", + "\n", + "i1 & !o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!i1 & !o0\n", + "\n", + "\n", + "!i1 & !o0\n", "\n", "\n", "\n" @@ -2559,61 +2559,61 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "0->0\n", - "\n", - "\n", - "!i1 & !o0\n", + "\n", + "\n", + "!i1 & !o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "i1 & !o0\n", + "\n", + "\n", + "i1 & !o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!i1 & o0\n", + "\n", + "\n", + "!i1 & o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "i1 & o0\n", + "\n", + "\n", + "i1 & o0\n", "\n", "\n", "\n" @@ -2638,61 +2638,61 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "i1 & o0\n", + "\n", + "\n", + "i1 & o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!i1 & o0\n", + "\n", + "\n", + "!i1 & o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "i1 & !o0\n", + "\n", + "\n", + "i1 & !o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!i1 & !o0\n", + "\n", + "\n", + "!i1 & !o0\n", "\n", "\n", "\n" @@ -2732,405 +2732,405 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "i0 & !i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "0->8\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "8->7\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "13\n", - "\n", - "13\n", + "\n", + "13\n", "\n", "\n", "\n", "1->13\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "18\n", - "\n", - "18\n", + "\n", + "18\n", "\n", "\n", "\n", "1->18\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "19\n", - "\n", - "19\n", + "\n", + "19\n", "\n", "\n", "\n", "1->19\n", - "\n", - "\n", - "i0 & !i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", "\n", "\n", "1->20\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "13->7\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "18->5\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "19->3\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "20->1\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "3->13\n", - "\n", - "\n", - "i1\n", + "\n", + "\n", + "i1\n", "\n", "\n", "\n", "3->19\n", - "\n", - "\n", - "!i1\n", + "\n", + "\n", + "!i1\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "5->10\n", - "\n", - "\n", - "i0 & !i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "5->11\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", "\n", "\n", "5->15\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "16\n", - "\n", - "16\n", + "\n", + "16\n", "\n", "\n", "\n", "5->16\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "10->9\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "11->7\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "14\n", - "\n", - "14\n", + "\n", + "14\n", "\n", "\n", "\n", "15->14\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "16->5\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "7->10\n", - "\n", - "\n", - "!i1\n", + "\n", + "\n", + "!i1\n", "\n", "\n", "\n", "7->11\n", - "\n", - "\n", - "i1\n", + "\n", + "\n", + "i1\n", "\n", "\n", "\n", "9->13\n", - "\n", - "\n", - "i1\n", + "\n", + "\n", + "i1\n", "\n", "\n", "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", "\n", "\n", "9->12\n", - "\n", - "\n", - "!i1\n", + "\n", + "\n", + "!i1\n", "\n", "\n", "\n", "12->9\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "14->13\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "14->18\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "14->12\n", - "\n", - "\n", - "i0 & !i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "17\n", - "\n", - "17\n", + "\n", + "17\n", "\n", "\n", "\n", "14->17\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "17->14\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7c803ebf90> >" + " *' at 0x7f0ddc16b720> >" ] }, "execution_count": 11, @@ -3163,253 +3163,253 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | (Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))))\n", - "[parity max odd 5]\n", + " viewBox=\"0.00 0.00 566.58 353.20\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))))\n", + "[parity max odd 5]\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "I->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "4->10\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "4->11\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "0->5\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "5->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "6->1\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1->6\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "1->7\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "7->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "8->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "3->9\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "9->2\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", + "\n", "\n", "\n", "\n", "9->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "10->0\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", + "\n", "\n", "\n", "\n", "10->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "11->1\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", + "\n", "\n", "\n", "\n", "11->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7c803ebd20> >" + " *' at 0x7f0ddc16bf30> >" ] }, "execution_count": 12, @@ -3526,253 +3526,253 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | (Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))))\n", - "[parity max odd 5]\n", + " viewBox=\"0.00 0.00 566.58 353.20\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))))\n", + "[parity max odd 5]\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "I->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "4->10\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "4->11\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "0->5\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "5->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "6->1\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1->6\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "1->7\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "7->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "8->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "3->9\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "9->2\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", + "\n", "\n", "\n", "\n", "9->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "10->0\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", + "\n", "\n", "\n", "\n", "10->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "11->1\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", + "\n", "\n", "\n", "\n", "11->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7c803ddea0> >" + " *' at 0x7f0ddc30cab0> >" ] }, "execution_count": 15, @@ -3862,102 +3862,102 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "2\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o1o1\n", - "\n", - "o1\n", + "\n", + "o1\n", "\n", "\n", "\n", "6->o1o1:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "10->o0o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -4041,40 +4041,40 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "(!i0 & !i1 & !o0 & !o1) | (!i0 & i1 & o0 & !o1) | (i0 & !i1 & o0 & !o1) | (i0 & i1 & !o0 & o1)\n", + "\n", + "\n", + "(!i0 & !i1 & !o0 & !o1) | (!i0 & i1 & o0 & !o1) | (i0 & !i1 & o0 & !o1) | (i0 & i1 & !o0 & o1)\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7c804061b0> >" + " *' at 0x7f0ddc26b480> >" ] }, "metadata": {}, @@ -4117,91 +4117,91 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | (Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")))\n", - "[parity max odd 4]\n", + " viewBox=\"0.00 0.00 383.00 109.72\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")))\n", + "[parity max odd 4]\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "3->0\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7c80406540> >" + " *' at 0x7f0ddc26bea0> >" ] }, "execution_count": 22, @@ -4226,54 +4226,36 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "L0_out\n", - "\n", + "\n", + "\n", + "\n", "\n", - "\n", + "\n", "o0o0\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "2->o0o0:s\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "L0\n", - "\n", - "L0\n", + "\n", + "o0\n", "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "Const\n", + "\n", + "Const\n", "\n", - "\n", + "\n", "\n", - "0->L0\n", - "\n", - "\n", + "0->o0o0:s\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 23, @@ -4291,7 +4273,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "By handing over the input and output propositions explicitly, you can force their appearance of the propositions in the circuit" + "By handing over the input and output propositions explicitly, you can force their occurrence in the propositions of the circuit" ] }, { @@ -4305,66 +4287,48 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "L0_out\n", - "\n", + "\n", + "\n", + "\n", "\n", - "\n", + "\n", "o0o0\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "2->o0o0:s\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "L0\n", - "\n", - "L0\n", + "\n", + "o0\n", "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "Const\n", + "\n", + "Const\n", "\n", - "\n", + "\n", "\n", - "0->L0\n", - "\n", - "\n", + "0->o0o0:s\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "o1o1\n", - "\n", - "o1\n", + "\n", + "o1\n", "\n", "\n", - "\n", + "\n", "0->o1o1:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 24, @@ -4376,6 +4340,13 @@ "aig2 = spot.strategy_to_aig(strat, \"isop\", [], [\"o0\", \"o1\"])\n", "aig2" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { @@ -4394,7 +4365,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.7.3" + "version": "3.9.2" } }, "nbformat": 4,