544544(rule (simplify (bor ty (band ty (bnot ty y) x) y)) (bor ty y x))
545545(rule (simplify (bor ty y (band ty x (bnot ty y)))) (bor ty y x))
546546(rule (simplify (bor ty (band ty x (bnot ty y)) y)) (bor ty y x))
547-
548- ;; ((x & ~y) - (x & y)) --> ((x ^ y) - y)
549- (rule (simplify (isub ty (band ty x (bnot ty y)) (band ty x y))) (isub ty (bxor ty x y) y))
550- (rule (simplify (isub ty (band ty x (bnot ty y)) (band ty y x))) (isub ty (bxor ty x y) y))
551- (rule (simplify (isub ty (band ty (bnot ty y) x) (band ty x y))) (isub ty (bxor ty x y) y))
552- (rule (simplify (isub ty (band ty (bnot ty y) x) (band ty y x))) (isub ty (bxor ty x y) y))
553- (rule (simplify (isub ty (band ty x y) (band ty x (bnot ty y)))) (isub ty y (bxor ty x y)))
554- (rule (simplify (isub ty (band ty x y) (band ty (bnot ty y) x))) (isub ty y (bxor ty x y)))
555- (rule (simplify (isub ty (band ty y x) (band ty x (bnot ty y)))) (isub ty y (bxor ty x y)))
556- (rule (simplify (isub ty (band ty y x) (band ty (bnot ty y) x))) (isub ty y (bxor ty x y)))
557-
558- ;; (x & ~y) | (~x & y) --> (x ^ y)
559- (rule (simplify (bor ty (band ty x (bnot ty y)) (band ty (bnot ty x) y))) (bxor ty x y))
560- (rule (simplify (bor ty (band ty (bnot ty x) y) (band ty x (bnot ty y)))) (bxor ty x y))
561- (rule (simplify (bor ty (band ty x (bnot ty y)) (band ty y (bnot ty x)))) (bxor ty x y))
562- (rule (simplify (bor ty (band ty y (bnot ty x)) (band ty x (bnot ty y)))) (bxor ty x y))
563- (rule (simplify (bor ty (band ty (bnot ty y) x) (band ty (bnot ty x) y))) (bxor ty x y))
564- (rule (simplify (bor ty (band ty (bnot ty x) y) (band ty (bnot ty y) x))) (bxor ty x y))
565- (rule (simplify (bor ty (band ty (bnot ty y) x) (band ty y (bnot ty x)))) (bxor ty x y))
566- (rule (simplify (bor ty (band ty y (bnot ty x)) (band ty (bnot ty y) x))) (bxor ty x y))
567-
568- ;; (x & ~y) | (x ^ y) --> (x ^ y)
569- (rule (simplify (bor ty (band ty x (bnot ty y)) (bxor ty x y))) (bxor ty x y))
570- (rule (simplify (bor ty (bxor ty x y) (band ty x (bnot ty y)))) (bxor ty x y))
571- (rule (simplify (bor ty (band ty x (bnot ty y)) (bxor ty y x))) (bxor ty x y))
572- (rule (simplify (bor ty (bxor ty y x) (band ty x (bnot ty y)))) (bxor ty x y))
573- (rule (simplify (bor ty (band ty (bnot ty y) x) (bxor ty x y))) (bxor ty x y))
574- (rule (simplify (bor ty (bxor ty x y) (band ty (bnot ty y) x))) (bxor ty x y))
575- (rule (simplify (bor ty (band ty (bnot ty y) x) (bxor ty y x))) (bxor ty x y))
576- (rule (simplify (bor ty (bxor ty y x) (band ty (bnot ty y) x))) (bxor ty x y))
577-
578- ;; (x & ~y) ^ ~x --> ~(x & y)
579- (rule (simplify (bxor ty (band ty x (bnot ty y)) (bnot ty x))) (bnot ty (band ty x y)))
580- (rule (simplify (bxor ty (bnot ty x) (band ty x (bnot ty y)))) (bnot ty (band ty x y)))
581- (rule (simplify (bxor ty (band ty (bnot ty y) x) (bnot ty x))) (bnot ty (band ty x y)))
582- (rule (simplify (bxor ty (bnot ty x) (band ty (bnot ty y) x))) (bnot ty (band ty x y)))
583-
584- ;; (~x & y) ^ x --> x | y
585- (rule (simplify (bxor ty (band ty (bnot ty x) y) x)) (bor ty x y))
586- (rule (simplify (bxor ty x (band ty (bnot ty x) y))) (bor ty x y))
587- (rule (simplify (bxor ty (band ty y (bnot ty x)) x)) (bor ty x y))
588- (rule (simplify (bxor ty x (band ty y (bnot ty x)))) (bor ty x y))
589-
590- ;; (x | y) & ~(x ^ y) --> x & y
591- (rule (simplify (band ty (bor ty x y) (bnot ty (bxor ty x y)))) (band ty x y))
592- (rule (simplify (band ty (bnot ty (bxor ty x y)) (bor ty x y))) (band ty x y))
593- (rule (simplify (band ty (bor ty x y) (bnot ty (bxor ty y x)))) (band ty x y))
594- (rule (simplify (band ty (bnot ty (bxor ty y x)) (bor ty x y))) (band ty x y))
595- (rule (simplify (band ty (bor ty y x) (bnot ty (bxor ty x y)))) (band ty x y))
596- (rule (simplify (band ty (bnot ty (bxor ty x y)) (bor ty y x))) (band ty x y))
597- (rule (simplify (band ty (bor ty y x) (bnot ty (bxor ty y x)))) (band ty x y))
598- (rule (simplify (band ty (bnot ty (bxor ty y x)) (bor ty y x))) (band ty x y))
599-
600- ;; x | ~(x ^ y) --> x | ~y
601- (rule (simplify (bor ty x (bnot ty (bxor ty x y)))) (bor ty x (bnot ty y)))
602- (rule (simplify (bor ty (bnot ty (bxor ty x y)) x)) (bor ty x (bnot ty y)))
603- (rule (simplify (bor ty x (bnot ty (bxor ty y x)))) (bor ty x (bnot ty y)))
604- (rule (simplify (bor ty (bnot ty (bxor ty y x)) x)) (bor ty x (bnot ty y)))
605-
606- ;; x | ((~x) ^ y) --> x | ~y
607- (rule (simplify (bor ty x (bxor ty (bnot ty x) y))) (bor ty x (bnot ty y)))
608- (rule (simplify (bor ty (bxor ty (bnot ty x) y) x)) (bor ty x (bnot ty y)))
609- (rule (simplify (bor ty x (bxor ty y (bnot ty x)))) (bor ty x (bnot ty y)))
610- (rule (simplify (bor ty (bxor ty y (bnot ty x)) x)) (bor ty x (bnot ty y)))
611-
612- ;; x & ~(x ^ y) --> x & y
613- (rule (simplify (band ty x (bnot ty (bxor ty x y)))) (band ty x y))
614- (rule (simplify (band ty (bnot ty (bxor ty x y)) x)) (band ty x y))
615- (rule (simplify (band ty x (bnot ty (bxor ty y x)))) (band ty x y))
616- (rule (simplify (band ty (bnot ty (bxor ty y x)) x)) (band ty x y))
617-
618- ;; x & ((~x) ^ y) --> x & y
619- (rule (simplify (band ty x (bxor ty (bnot ty x) y))) (band ty x y))
620- (rule (simplify (band ty (bxor ty (bnot ty x) y) x)) (band ty x y))
621- (rule (simplify (band ty x (bxor ty y (bnot ty x)))) (band ty x y))
622- (rule (simplify (band ty (bxor ty y (bnot ty x)) x)) (band ty x y))
623-
624- ;; (x | y) | (x ^ y) --> (x | y)
625- (rule (simplify (bor ty (bor ty x y) (bxor ty x y))) (bor ty x y))
626- (rule (simplify (bor ty (bxor ty x y) (bor ty x y))) (bor ty x y))
627- (rule (simplify (bor ty (bor ty x y) (bxor ty y x))) (bor ty x y))
628- (rule (simplify (bor ty (bxor ty y x) (bor ty x y))) (bor ty x y))
629- (rule (simplify (bor ty (bor ty y x) (bxor ty x y))) (bor ty x y))
630- (rule (simplify (bor ty (bxor ty x y) (bor ty y x))) (bor ty x y))
631- (rule (simplify (bor ty (bor ty y x) (bxor ty y x))) (bor ty x y))
632- (rule (simplify (bor ty (bxor ty y x) (bor ty y x))) (bor ty x y))
633-
634- ;; (x ^ y) & (x ^ (y ^ z)) --> (x ^ y) & ~z
635- (rule (simplify (band ty (bxor ty x y) (bxor ty (bxor ty y z) x))) (band ty (bxor ty x y) (bnot ty z)))
636- (rule (simplify (band ty (bxor ty (bxor ty y z) x) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
637- (rule (simplify (band ty (bxor ty x y) (bxor ty x (bxor ty y z)))) (band ty (bxor ty x y) (bnot ty z)))
638- (rule (simplify (band ty (bxor ty x (bxor ty y z)) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
639- (rule (simplify (band ty (bxor ty x y) (bxor ty (bxor ty z y) x))) (band ty (bxor ty x y) (bnot ty z)))
640- (rule (simplify (band ty (bxor ty (bxor ty z y) x) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
641- (rule (simplify (band ty (bxor ty x y) (bxor ty x (bxor ty z y)))) (band ty (bxor ty x y) (bnot ty z)))
642- (rule (simplify (band ty (bxor ty x (bxor ty z y)) (bxor ty x y))) (band ty (bxor ty x y) (bnot ty z)))
643- (rule (simplify (band ty (bxor ty y x) (bxor ty (bxor ty y z) x))) (band ty (bxor ty x y) (bnot ty z)))
644- (rule (simplify (band ty (bxor ty (bxor ty y z) x) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
645- (rule (simplify (band ty (bxor ty y x) (bxor ty x (bxor ty y z)))) (band ty (bxor ty x y) (bnot ty z)))
646- (rule (simplify (band ty (bxor ty x (bxor ty y z)) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
647- (rule (simplify (band ty (bxor ty y x) (bxor ty (bxor ty z y) x))) (band ty (bxor ty x y) (bnot ty z)))
648- (rule (simplify (band ty (bxor ty (bxor ty z y) x) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
649- (rule (simplify (band ty (bxor ty y x) (bxor ty x (bxor ty z y)))) (band ty (bxor ty x y) (bnot ty z)))
650- (rule (simplify (band ty (bxor ty x (bxor ty z y)) (bxor ty y x))) (band ty (bxor ty x y) (bnot ty z)))
651-
652- ;; (~x & y) ^ z --> (x & y) ^ (z ^ y)
653- (rule (simplify (bxor ty (band ty (bnot ty x) y) z)) (bxor ty (band ty x y) (bxor ty z y)))
654- (rule (simplify (bxor ty z (band ty (bnot ty x) y))) (bxor ty (band ty x y) (bxor ty z y)))
655- (rule (simplify (bxor ty (band ty y (bnot ty x)) z)) (bxor ty (band ty x y) (bxor ty z y)))
656- (rule (simplify (bxor ty z (band ty y (bnot ty x)))) (bxor ty (band ty x y) (bxor ty z y)))
657-
658- ;; ~x - ~y --> y - x
659- (rule (simplify (isub ty (bnot ty x) (bnot ty y))) (isub ty y x))
660-
661- ;; (~x & y) | ~(x | y) --> ~x
662- (rule (simplify (bor ty (band ty (bnot ty x) y) (bnot ty (bor ty x y)))) (bnot ty x))
663- (rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty (bnot ty x) y))) (bnot ty x))
664- (rule (simplify (bor ty (band ty (bnot ty x) y) (bnot ty (bor ty y x)))) (bnot ty x))
665- (rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty (bnot ty x) y))) (bnot ty x))
666- (rule (simplify (bor ty (band ty y (bnot ty x)) (bnot ty (bor ty x y)))) (bnot ty x))
667- (rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty y (bnot ty x)))) (bnot ty x))
668- (rule (simplify (bor ty (band ty y (bnot ty x)) (bnot ty (bor ty y x)))) (bnot ty x))
669- (rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty y (bnot ty x)))) (bnot ty x))
670-
671- ;; (~x | y) & ~(x & y) --> ~x
672- (rule (simplify (band ty (bor ty (bnot ty x) y) (bnot ty (band ty x y)))) (bnot ty x))
673- (rule (simplify (band ty (bnot ty (band ty x y)) (bor ty (bnot ty x) y))) (bnot ty x))
674- (rule (simplify (band ty (bor ty (bnot ty x) y) (bnot ty (band ty y x)))) (bnot ty x))
675- (rule (simplify (band ty (bnot ty (band ty y x)) (bor ty (bnot ty x) y))) (bnot ty x))
676- (rule (simplify (band ty (bor ty y (bnot ty x)) (bnot ty (band ty x y)))) (bnot ty x))
677- (rule (simplify (band ty (bnot ty (band ty x y)) (bor ty y (bnot ty x)))) (bnot ty x))
678- (rule (simplify (band ty (bor ty y (bnot ty x)) (bnot ty (band ty y x)))) (bnot ty x))
679- (rule (simplify (band ty (bnot ty (band ty y x)) (bor ty y (bnot ty x)))) (bnot ty x))
680-
681- ;; (x & y) | ~(x | y) --> ~(x ^ y)
682- (rule (simplify (bor ty (band ty x y) (bnot ty (bor ty x y)))) (bnot ty (bxor ty x y)))
683- (rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty x y))) (bnot ty (bxor ty x y)))
684- (rule (simplify (bor ty (band ty x y) (bnot ty (bor ty y x)))) (bnot ty (bxor ty x y)))
685- (rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty x y))) (bnot ty (bxor ty x y)))
686- (rule (simplify (bor ty (band ty y x) (bnot ty (bor ty x y)))) (bnot ty (bxor ty x y)))
687- (rule (simplify (bor ty (bnot ty (bor ty x y)) (band ty y x))) (bnot ty (bxor ty x y)))
688- (rule (simplify (bor ty (band ty y x) (bnot ty (bor ty y x)))) (bnot ty (bxor ty x y)))
689- (rule (simplify (bor ty (bnot ty (bor ty y x)) (band ty y x))) (bnot ty (bxor ty x y)))
690-
691- ;; (~x | y) ^ (x ^ y) --> x | ~y
692- (rule (simplify (bxor ty (bor ty (bnot ty x) y) (bxor ty x y))) (bor ty x (bnot ty y)))
693- (rule (simplify (bxor ty (bxor ty x y) (bor ty (bnot ty x) y))) (bor ty x (bnot ty y)))
694- (rule (simplify (bxor ty (bor ty (bnot ty x) y) (bxor ty y x))) (bor ty x (bnot ty y)))
695- (rule (simplify (bxor ty (bxor ty y x) (bor ty (bnot ty x) y))) (bor ty x (bnot ty y)))
696- (rule (simplify (bxor ty (bor ty y (bnot ty x)) (bxor ty x y))) (bor ty x (bnot ty y)))
697- (rule (simplify (bxor ty (bxor ty x y) (bor ty y (bnot ty x)))) (bor ty x (bnot ty y)))
698- (rule (simplify (bxor ty (bor ty y (bnot ty x)) (bxor ty y x))) (bor ty x (bnot ty y)))
699- (rule (simplify (bxor ty (bxor ty y x) (bor ty y (bnot ty x)))) (bor ty x (bnot ty y)))
0 commit comments