content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  
  module Grisette.SymPrim.Prim.BoolTests (boolTests) where
  
  import Grisette.Internal.SymPrim.BV (IntN, WordN)
  import Grisette.Internal.SymPrim.Prim.Term
    ( PEvalNumTerm (pevalAddNumTerm),
      SupportedPrim (pevalITETerm),
      Term,
      andTerm,
      conTerm,
      eqTerm,
      notTerm,
      orTerm,
      pevalAndTerm,
      pevalEqTerm,
      pevalImplyTerm,
      pevalNEqTerm,
      pevalNotTerm,
      pevalOrTerm,
      pevalXorTerm,
      ssymTerm,
    )
  import Test.Framework (Test, testGroup)
  import Test.Framework.Providers.HUnit (testCase)
  import Test.HUnit ((@?=))
  
  boolTests :: Test
  boolTests =
    testGroup
      "Bool"
      [ testGroup
          "Not"
          [ testCase "On concrete" $ do
              pevalNotTerm (conTerm True) @?= conTerm False
              pevalNotTerm (conTerm True) @?= conTerm False,
            testCase "On general symbolic" $ do
              pevalNotTerm (ssymTerm "a") @?= notTerm (ssymTerm "a" :: Term Bool),
            testCase "On Not" $ do
              pevalNotTerm (pevalNotTerm (ssymTerm "a")) @?= ssymTerm "a",
            testCase "On Or Not" $ do
              pevalNotTerm (pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b"))
                @?= pevalAndTerm (ssymTerm "a") (pevalNotTerm (ssymTerm "b"))
              pevalNotTerm (pevalOrTerm (ssymTerm "a") (pevalNotTerm (ssymTerm "b")))
                @?= pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b"),
            testCase "On And Not" $ do
              pevalNotTerm (pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b"))
                @?= pevalOrTerm (ssymTerm "a") (pevalNotTerm (ssymTerm "b"))
              pevalNotTerm (pevalAndTerm (ssymTerm "a") (pevalNotTerm (ssymTerm "b")))
                @?= pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")
          ],
        testGroup
          "Eqv & NEqv"
          [ testCase "Eqv on both concrete" $ do
              pevalEqTerm (conTerm True) (conTerm True) @?= conTerm True
              pevalEqTerm (conTerm True) (conTerm False) @?= conTerm False
              pevalEqTerm (conTerm False) (conTerm True) @?= conTerm False
              pevalEqTerm (conTerm False) (conTerm False) @?= conTerm True
              pevalEqTerm (conTerm (1 :: Integer)) (conTerm 1) @?= conTerm True
              pevalEqTerm (conTerm (1 :: Integer)) (conTerm 2) @?= conTerm False
              pevalEqTerm (conTerm (1 :: IntN 4)) (conTerm 1) @?= conTerm True
              pevalEqTerm (conTerm (1 :: IntN 4)) (conTerm 2) @?= conTerm False
              pevalEqTerm (conTerm (1 :: WordN 4)) (conTerm 1) @?= conTerm True
              pevalEqTerm (conTerm (1 :: WordN 4)) (conTerm 2) @?= conTerm False,
            testCase "Eqv on single concrete always put concrete ones in the right" $ do
              pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
                @?= eqTerm (ssymTerm "a" :: Term Integer) (conTerm 1 :: Term Integer)
              pevalEqTerm (conTerm 1) (ssymTerm "a" :: Term Integer)
                @?= eqTerm (ssymTerm "a" :: Term Integer) (conTerm 1 :: Term Integer),
            testCase "Eqv on general symbolic" $ do
              pevalEqTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
                @?= eqTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b" :: Term Integer),
            testCase "Eqv on Bool with single concrete" $ do
              pevalEqTerm (conTerm True) (ssymTerm "a") @?= ssymTerm "a"
              pevalEqTerm (ssymTerm "a") (conTerm True) @?= ssymTerm "a"
              pevalEqTerm (conTerm False) (ssymTerm "a") @?= pevalNotTerm (ssymTerm "a")
              pevalEqTerm (ssymTerm "a") (conTerm False) @?= pevalNotTerm (ssymTerm "a"),
            testCase "NEqv on general symbolic" $ do
              pevalNEqTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")
                @?= pevalNotTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (ssymTerm "b")),
            testCase "Eqv(Not(x), x) / Eqv(x, Not(x))" $ do
              pevalEqTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "a") @?= conTerm False
              pevalEqTerm (ssymTerm "a") (pevalNotTerm (ssymTerm "a")) @?= conTerm False,
            testCase "Eqv(n1+x, n2)" $ do
              pevalEqTerm (pevalAddNumTerm (conTerm 1 :: Term Integer) (ssymTerm "a")) (conTerm 3)
                @?= pevalEqTerm (ssymTerm "a") (conTerm 2 :: Term Integer)
              pevalEqTerm (pevalAddNumTerm (conTerm 1 :: Term (IntN 4)) (ssymTerm "a")) (conTerm 3)
                @?= pevalEqTerm (ssymTerm "a") (conTerm 2 :: Term (IntN 4))
              pevalEqTerm (pevalAddNumTerm (conTerm 1 :: Term (WordN 4)) (ssymTerm "a")) (conTerm 3)
                @?= pevalEqTerm (ssymTerm "a") (conTerm 2 :: Term (WordN 4)),
            testCase "Eqv(n1, n2+x)" $ do
              pevalEqTerm (conTerm 3) (pevalAddNumTerm (conTerm 1 :: Term Integer) (ssymTerm "a"))
                @?= pevalEqTerm (ssymTerm "a") (conTerm 2 :: Term Integer)
              pevalEqTerm (conTerm 3) (pevalAddNumTerm (conTerm 1 :: Term (IntN 4)) (ssymTerm "a"))
                @?= pevalEqTerm (ssymTerm "a") (conTerm 2 :: Term (IntN 4))
              pevalEqTerm (conTerm 3) (pevalAddNumTerm (conTerm 1 :: Term (WordN 4)) (ssymTerm "a"))
                @?= pevalEqTerm (ssymTerm "a") (conTerm 2 :: Term (WordN 4)),
            testCase "Eqv(l, ITE(c, l, f)) / Eqv(l, ITE(c, t, l) / Eqv(ITE(c, r, f), r) / Eqv(ITE(c, t, r), r)" $ do
              pevalEqTerm (ssymTerm "a" :: Term Integer) (pevalITETerm (ssymTerm "b") (ssymTerm "a") (ssymTerm "c"))
                @?= pevalOrTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a") (ssymTerm "c" :: Term Integer))
              pevalEqTerm (ssymTerm "a" :: Term Integer) (pevalITETerm (ssymTerm "b") (ssymTerm "c") (ssymTerm "a"))
                @?= pevalOrTerm (pevalNotTerm $ ssymTerm "b") (pevalEqTerm (ssymTerm "a") (ssymTerm "c" :: Term Integer))
              pevalEqTerm (pevalITETerm (ssymTerm "b") (ssymTerm "a") (ssymTerm "c")) (ssymTerm "a" :: Term Integer)
                @?= pevalOrTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "c") (ssymTerm "a" :: Term Integer))
              pevalEqTerm (pevalITETerm (ssymTerm "b") (ssymTerm "c") (ssymTerm "a")) (ssymTerm "a" :: Term Integer)
                @?= pevalOrTerm (pevalNotTerm $ ssymTerm "b") (pevalEqTerm (ssymTerm "c") (ssymTerm "a" :: Term Integer))
          ],
        testGroup
          "Or"
          [ testCase "On both concrete" $ do
              pevalOrTerm (conTerm True) (conTerm True) @?= conTerm True
              pevalOrTerm (conTerm True) (conTerm False) @?= conTerm True
              pevalOrTerm (conTerm False) (conTerm True) @?= conTerm True
              pevalOrTerm (conTerm False) (conTerm False) @?= conTerm False,
            testCase "On general symbolic" $ do
              pevalOrTerm (ssymTerm "a") (ssymTerm "b")
                @?= orTerm (ssymTerm "a" :: Term Bool) (ssymTerm "b" :: Term Bool),
            testCase "Or(x, y) -> True" $ do
              pevalOrTerm (conTerm True) (ssymTerm "b") @?= conTerm True
              pevalOrTerm (ssymTerm "a") (conTerm True) @?= conTerm True
              pevalOrTerm
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
                @?= conTerm True
              pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "a") @?= conTerm True
              pevalOrTerm (ssymTerm "a") (pevalNotTerm (ssymTerm "a")) @?= conTerm True,
            testCase "Or(x, y) -> x" $ do
              pevalOrTerm (ssymTerm "a") (conTerm False) @?= ssymTerm "a"
              pevalOrTerm
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
                @?= pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
              pevalOrTerm (ssymTerm "a") (ssymTerm "a") @?= ssymTerm "a",
            testCase "Or(x, y) -> y" $ do
              pevalOrTerm (conTerm False) (ssymTerm "a") @?= ssymTerm "a"
              pevalOrTerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                @?= pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1),
            testCase "Or(x, Or(y1, y2)) -> True" $ do
              pevalOrTerm (pevalNotTerm (ssymTerm "a")) (pevalOrTerm (ssymTerm "a") (ssymTerm "b")) @?= conTerm True
              pevalOrTerm (ssymTerm "a") (pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")) @?= conTerm True
              pevalOrTerm
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                @?= conTerm True
  
              pevalOrTerm (pevalNotTerm (ssymTerm "a")) (pevalOrTerm (ssymTerm "b") (ssymTerm "a")) @?= conTerm True
              pevalOrTerm (ssymTerm "a") (pevalOrTerm (ssymTerm "b") (pevalNotTerm (ssymTerm "a"))) @?= conTerm True
              pevalOrTerm
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                @?= conTerm True,
            testCase "Or(x, Or(y1, y2)) -> Or(x, y2)" $ do
              pevalOrTerm
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                @?= pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
            testCase "Or(x, Or(y1, y2)) -> Or(x, y1)" $ do
              pevalOrTerm
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalOrTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                @?= pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
            testCase "Or(x, y@Or(y1, y2)) -> y" $ do
              pevalOrTerm (ssymTerm "a") (pevalOrTerm (ssymTerm "a") (ssymTerm "b"))
                @?= pevalOrTerm (ssymTerm "a") (ssymTerm "b")
              pevalOrTerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
                (pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"))
                @?= pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b")
              pevalOrTerm (ssymTerm "a") (pevalOrTerm (ssymTerm "b") (ssymTerm "a"))
                @?= pevalOrTerm (ssymTerm "b") (ssymTerm "a")
              pevalOrTerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
                (pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)))
                @?= pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
            testCase "Or(Or(x1, x2), y) -> True" $ do
              pevalOrTerm (pevalOrTerm (ssymTerm "a") (ssymTerm "b")) (pevalNotTerm (ssymTerm "a")) @?= conTerm True
              pevalOrTerm (pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")) (ssymTerm "a") @?= conTerm True
              pevalOrTerm
                (pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                @?= conTerm True
  
              pevalOrTerm (pevalOrTerm (ssymTerm "b") (ssymTerm "a")) (pevalNotTerm (ssymTerm "a")) @?= conTerm True
              pevalOrTerm (pevalOrTerm (ssymTerm "b") (pevalNotTerm (ssymTerm "a"))) (ssymTerm "a") @?= conTerm True
              pevalOrTerm
                (pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                @?= conTerm True,
            testCase "Or(x@Or(x1, x2), y) -> x" $ do
              pevalOrTerm (pevalOrTerm (ssymTerm "a") (ssymTerm "b")) (ssymTerm "a")
                @?= pevalOrTerm (ssymTerm "a") (ssymTerm "b")
              pevalOrTerm
                (pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"))
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
                @?= pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b")
              pevalOrTerm (pevalOrTerm (ssymTerm "b") (ssymTerm "a")) (ssymTerm "a")
                @?= pevalOrTerm (ssymTerm "b") (ssymTerm "a")
              pevalOrTerm
                (pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)))
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
                @?= pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
            testCase "Or(Or(x1, x2), y) -> Or(x2, y)" $ do
              pevalOrTerm
                (pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                @?= pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
            testCase "Or(Or(x1, x2), y) -> Or(x1, y)" $ do
              pevalOrTerm
                (pevalOrTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                @?= pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
            testCase "Or(x, And(y1, y2)) -> x" $ do
              pevalOrTerm
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                @?= pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
              pevalOrTerm
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                @?= pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1),
            testCase "Or(x, And(y1, y2)) -> Or(x, y2)" $ do
              pevalOrTerm (ssymTerm "a") (pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b"))
                @?= pevalOrTerm (ssymTerm "a") (ssymTerm "b")
              pevalOrTerm (pevalNotTerm (ssymTerm "a")) (pevalAndTerm (ssymTerm "a") (ssymTerm "b"))
                @?= pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")
              pevalOrTerm
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalAndTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                @?= pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
            testCase "Or(And(x1, x2), y) -> y" $ do
              pevalOrTerm
                (pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                @?= pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
              pevalOrTerm
                (pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                @?= pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1),
            testCase "Or(x, And(y1, y2)) -> Or(x, y1)" $ do
              pevalOrTerm (ssymTerm "a") (pevalAndTerm (ssymTerm "b") (pevalNotTerm (ssymTerm "a")))
                @?= pevalOrTerm (ssymTerm "a") (ssymTerm "b")
              pevalOrTerm (pevalNotTerm (ssymTerm "a")) (pevalAndTerm (ssymTerm "b") (ssymTerm "a"))
                @?= pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")
              pevalOrTerm
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalAndTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                @?= pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
            testCase "Or(Not(x), Not(y)) -> Not(And(x, y))" $ do
              pevalOrTerm (pevalNotTerm (ssymTerm "a")) (pevalNotTerm (ssymTerm "b"))
                @?= pevalNotTerm (pevalAndTerm (ssymTerm "a") (ssymTerm "b"))
          ],
        testGroup
          "And"
          [ testCase "Oith both concrete" $ do
              pevalAndTerm (conTerm True) (conTerm True) @?= conTerm True
              pevalAndTerm (conTerm True) (conTerm False) @?= conTerm False
              pevalAndTerm (conTerm False) (conTerm True) @?= conTerm False
              pevalAndTerm (conTerm False) (conTerm False) @?= conTerm False,
            testCase "On general symbolic" $ do
              pevalAndTerm (ssymTerm "a") (ssymTerm "b")
                @?= andTerm (ssymTerm "a" :: Term Bool) (ssymTerm "b" :: Term Bool),
            testCase "And(x, y) -> False" $ do
              pevalAndTerm (conTerm False) (ssymTerm "b") @?= conTerm False
              pevalAndTerm (ssymTerm "a") (conTerm False) @?= conTerm False
              pevalAndTerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
                @?= conTerm False
              pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "a") @?= conTerm False
              pevalAndTerm (ssymTerm "a") (pevalNotTerm (ssymTerm "a")) @?= conTerm False,
            testCase "And(x, y) -> x" $ do
              pevalAndTerm (ssymTerm "a") (conTerm True) @?= ssymTerm "a"
              pevalAndTerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
                @?= pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
              pevalAndTerm (ssymTerm "a") (ssymTerm "a") @?= ssymTerm "a",
            testCase "And(x, y) -> y" $ do
              pevalAndTerm (conTerm True) (ssymTerm "a") @?= ssymTerm "a"
              pevalAndTerm
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                @?= pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1),
            testCase "And(x, And(y1, y2)) -> False" $ do
              pevalAndTerm (pevalNotTerm (ssymTerm "a")) (pevalAndTerm (ssymTerm "a") (ssymTerm "b")) @?= conTerm False
              pevalAndTerm (ssymTerm "a") (pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")) @?= conTerm False
              pevalAndTerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                @?= conTerm False
  
              pevalAndTerm (pevalNotTerm (ssymTerm "a")) (pevalAndTerm (ssymTerm "b") (ssymTerm "a")) @?= conTerm False
              pevalAndTerm (ssymTerm "a") (pevalAndTerm (ssymTerm "b") (pevalNotTerm (ssymTerm "a"))) @?= conTerm False
              pevalAndTerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                @?= conTerm False,
            testCase "And(x, And(y1, y2)) -> And(x, y2)" $ do
              pevalAndTerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalAndTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                @?= pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
            testCase "And(x, And(y1, y2)) -> And(x, y1)" $ do
              pevalAndTerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalAndTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                @?= pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
            testCase "And(x, y@And(y1, y2)) -> y" $ do
              pevalAndTerm (ssymTerm "a") (pevalAndTerm (ssymTerm "a") (ssymTerm "b"))
                @?= pevalAndTerm (ssymTerm "a") (ssymTerm "b")
              pevalAndTerm
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
                (pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"))
                @?= pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b")
              pevalAndTerm (ssymTerm "a") (pevalAndTerm (ssymTerm "b") (ssymTerm "a"))
                @?= pevalAndTerm (ssymTerm "b") (ssymTerm "a")
              pevalAndTerm
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
                (pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)))
                @?= pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
            testCase "And(And(x1, x2), y) -> False" $ do
              pevalAndTerm (pevalAndTerm (ssymTerm "a") (ssymTerm "b")) (pevalNotTerm (ssymTerm "a")) @?= conTerm False
              pevalAndTerm (pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")) (ssymTerm "a") @?= conTerm False
              pevalAndTerm
                (pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                @?= conTerm False
  
              pevalAndTerm (pevalAndTerm (ssymTerm "b") (ssymTerm "a")) (pevalNotTerm (ssymTerm "a")) @?= conTerm False
              pevalAndTerm (pevalAndTerm (ssymTerm "b") (pevalNotTerm (ssymTerm "a"))) (ssymTerm "a") @?= conTerm False
              pevalAndTerm
                (pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                @?= conTerm False,
            testCase "And(x@And(x1, x2), y) -> x" $ do
              pevalAndTerm (pevalAndTerm (ssymTerm "a") (ssymTerm "b")) (ssymTerm "a")
                @?= pevalAndTerm (ssymTerm "a") (ssymTerm "b")
              pevalAndTerm
                (pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"))
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
                @?= pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b")
              pevalAndTerm (pevalAndTerm (ssymTerm "b") (ssymTerm "a")) (ssymTerm "a")
                @?= pevalAndTerm (ssymTerm "b") (ssymTerm "a")
              pevalAndTerm
                (pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)))
                (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))
                @?= pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
            testCase "And(And(x1, x2), y) -> And(x2, y)" $ do
              pevalAndTerm
                (pevalAndTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                @?= pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
            testCase "And(And(x1, x2), y) -> And(x1, y)" $ do
              pevalAndTerm
                (pevalAndTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                @?= pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)),
            testCase "And(x, Or(y1, y2)) -> x" $ do
              pevalAndTerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                @?= pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
              pevalAndTerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                @?= pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1),
            testCase "And(x, Or(y1, y2)) -> And(x, y2)" $ do
              pevalAndTerm (ssymTerm "a") (pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b"))
                @?= pevalAndTerm (ssymTerm "a") (ssymTerm "b")
              pevalAndTerm (pevalNotTerm (ssymTerm "a")) (pevalOrTerm (ssymTerm "a") (ssymTerm "b"))
                @?= pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")
              pevalAndTerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                @?= pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
            testCase "And(Or(x1, x2), y) -> y" $ do
              pevalAndTerm
                (pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                @?= pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)
              pevalAndTerm
                (pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                @?= pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1),
            testCase "And(x, Or(y1, y2)) -> And(x, y1)" $ do
              pevalAndTerm (ssymTerm "a") (pevalOrTerm (ssymTerm "b") (pevalNotTerm (ssymTerm "a")))
                @?= pevalAndTerm (ssymTerm "a") (ssymTerm "b")
              pevalAndTerm (pevalNotTerm (ssymTerm "a")) (pevalOrTerm (ssymTerm "b") (ssymTerm "a"))
                @?= pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")
              pevalAndTerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalOrTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                @?= pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b"),
            testCase "And(Not(x), Not(y)) -> Not(Or(x, y))" $ do
              pevalAndTerm (pevalNotTerm (ssymTerm "a")) (pevalNotTerm (ssymTerm "b"))
                @?= pevalNotTerm (pevalOrTerm (ssymTerm "a") (ssymTerm "b"))
          ],
        testGroup
          "ITE"
          [ testCase "On concrete condition" $ do
              pevalITETerm (conTerm True) (ssymTerm "a" :: Term Integer) (ssymTerm "b")
                @?= ssymTerm "a"
              pevalITETerm (conTerm False) (ssymTerm "a" :: Term Integer) (ssymTerm "b")
                @?= ssymTerm "b",
            testCase "On same branches" $ do
              pevalITETerm (ssymTerm "c") (ssymTerm "a" :: Term Integer) (ssymTerm "a")
                @?= ssymTerm "a",
            testCase "On both not" $ do
              pevalITETerm (ssymTerm "c") (pevalNotTerm $ ssymTerm "a") (pevalNotTerm $ ssymTerm "b")
                @?= pevalNotTerm (pevalITETerm (ssymTerm "c") (ssymTerm "a") (ssymTerm "b")),
            testCase "On not in condition" $ do
              pevalITETerm (pevalNotTerm $ ssymTerm "c") (ssymTerm "a" :: Term Integer) (ssymTerm "b")
                @?= pevalITETerm (ssymTerm "c") (ssymTerm "b") (ssymTerm "a"),
            testCase "On all arguments as ITE with same conditions" $ do
              pevalITETerm
                (pevalITETerm (ssymTerm "a") (ssymTerm "b") (ssymTerm "c"))
                (pevalITETerm (ssymTerm "a") (ssymTerm "d" :: Term Integer) (ssymTerm "e"))
                (pevalITETerm (ssymTerm "a") (ssymTerm "f" :: Term Integer) (ssymTerm "g"))
                @?= pevalITETerm
                  (ssymTerm "a")
                  (pevalITETerm (ssymTerm "b") (ssymTerm "d") (ssymTerm "f"))
                  (pevalITETerm (ssymTerm "c") (ssymTerm "e") (ssymTerm "g")),
            testCase "On with true branch as ITE" $ do
              pevalITETerm
                (ssymTerm "a")
                (pevalITETerm (ssymTerm "a") (ssymTerm "b" :: Term Integer) (ssymTerm "c"))
                (ssymTerm "d")
                @?= pevalITETerm (ssymTerm "a") (ssymTerm "b") (ssymTerm "d")
              pevalITETerm
                (ssymTerm "a")
                (pevalITETerm (ssymTerm "b") (ssymTerm "c" :: Term Integer) (ssymTerm "d"))
                (ssymTerm "c")
                @?= pevalITETerm
                  (pevalOrTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b"))
                  (ssymTerm "c")
                  (ssymTerm "d")
              pevalITETerm
                (ssymTerm "a")
                (pevalITETerm (ssymTerm "b") (ssymTerm "c" :: Term Integer) (ssymTerm "d"))
                (ssymTerm "d")
                @?= pevalITETerm
                  (pevalAndTerm (ssymTerm "a") (ssymTerm "b"))
                  (ssymTerm "c")
                  (ssymTerm "d"),
            testCase "On false branch as ITE" $ do
              pevalITETerm
                (ssymTerm "a")
                (ssymTerm "b")
                (pevalITETerm (ssymTerm "a") (ssymTerm "c" :: Term Integer) (ssymTerm "d"))
                @?= pevalITETerm (ssymTerm "a") (ssymTerm "b") (ssymTerm "d")
              pevalITETerm
                (ssymTerm "a")
                (ssymTerm "b")
                (pevalITETerm (ssymTerm "c") (ssymTerm "b" :: Term Integer) (ssymTerm "d"))
                @?= pevalITETerm
                  (pevalOrTerm (ssymTerm "a") (ssymTerm "c"))
                  (ssymTerm "b")
                  (ssymTerm "d")
              pevalITETerm
                (ssymTerm "a")
                (ssymTerm "b")
                (pevalITETerm (ssymTerm "c") (ssymTerm "d" :: Term Integer) (ssymTerm "b"))
                @?= pevalITETerm
                  (pevalOrTerm (ssymTerm "a") (pevalNotTerm $ ssymTerm "c"))
                  (ssymTerm "b")
                  (ssymTerm "d"),
            testCase "On both And" $ do
              pevalITETerm
                (ssymTerm "a")
                (pevalAndTerm (ssymTerm "b") (ssymTerm "c"))
                (pevalAndTerm (ssymTerm "b") (ssymTerm "d"))
                @?= pevalAndTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d"))
              pevalITETerm
                (ssymTerm "a")
                (pevalAndTerm (ssymTerm "c") (ssymTerm "b"))
                (pevalAndTerm (ssymTerm "b") (ssymTerm "d"))
                @?= pevalAndTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d"))
              pevalITETerm
                (ssymTerm "a")
                (pevalAndTerm (ssymTerm "b") (ssymTerm "c"))
                (pevalAndTerm (ssymTerm "d") (ssymTerm "b"))
                @?= pevalAndTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d"))
              pevalITETerm
                (ssymTerm "a")
                (pevalAndTerm (ssymTerm "c") (ssymTerm "b"))
                (pevalAndTerm (ssymTerm "d") (ssymTerm "b"))
                @?= pevalAndTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d")),
            testCase "On left And" $ do
              pevalITETerm
                (ssymTerm "a")
                (pevalAndTerm (ssymTerm "b") (ssymTerm "c"))
                (ssymTerm "b")
                @?= pevalAndTerm (ssymTerm "b") (pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "c"))
              pevalITETerm
                (ssymTerm "a")
                (pevalAndTerm (ssymTerm "b") (ssymTerm "c"))
                (ssymTerm "c")
                @?= pevalAndTerm (ssymTerm "c") (pevalOrTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b"))
              pevalITETerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                (ssymTerm "c")
                @?= pevalAndTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "c")
              pevalITETerm
                (ssymTerm "a")
                (pevalAndTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b"))
                (ssymTerm "c")
                @?= pevalAndTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "c")
              pevalITETerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                (ssymTerm "c")
                @?= pevalAndTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "c")
              pevalITETerm
                (ssymTerm "a")
                (pevalAndTerm (ssymTerm "b") (pevalNotTerm $ ssymTerm "a"))
                (ssymTerm "c")
                @?= pevalAndTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "c")
              pevalITETerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalAndTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                (ssymTerm "c")
                @?= pevalITETerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b") (ssymTerm "c")
              pevalITETerm
                (ssymTerm "a")
                (pevalAndTerm (ssymTerm "a") (ssymTerm "b"))
                (ssymTerm "c")
                @?= pevalITETerm (ssymTerm "a") (ssymTerm "b") (ssymTerm "c")
              pevalITETerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalAndTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                (ssymTerm "c")
                @?= pevalITETerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b") (ssymTerm "c")
              pevalITETerm
                (ssymTerm "a")
                (pevalAndTerm (ssymTerm "b") (ssymTerm "a"))
                (ssymTerm "c")
                @?= pevalITETerm (ssymTerm "a") (ssymTerm "b") (ssymTerm "c"),
            testCase "On right And" $ do
              pevalITETerm
                (ssymTerm "a")
                (ssymTerm "b")
                (pevalAndTerm (ssymTerm "b") (ssymTerm "c"))
                @?= pevalAndTerm (ssymTerm "b") (pevalOrTerm (ssymTerm "a") (ssymTerm "c"))
              pevalITETerm
                (ssymTerm "a")
                (ssymTerm "c")
                (pevalAndTerm (ssymTerm "b") (ssymTerm "c"))
                @?= pevalAndTerm (ssymTerm "c") (pevalOrTerm (ssymTerm "a") (ssymTerm "b")),
            testCase "On both Or" $ do
              pevalITETerm
                (ssymTerm "a")
                (pevalOrTerm (ssymTerm "b") (ssymTerm "c"))
                (pevalOrTerm (ssymTerm "b") (ssymTerm "d"))
                @?= pevalOrTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d"))
              pevalITETerm
                (ssymTerm "a")
                (pevalOrTerm (ssymTerm "c") (ssymTerm "b"))
                (pevalOrTerm (ssymTerm "b") (ssymTerm "d"))
                @?= pevalOrTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d"))
              pevalITETerm
                (ssymTerm "a")
                (pevalOrTerm (ssymTerm "b") (ssymTerm "c"))
                (pevalOrTerm (ssymTerm "d") (ssymTerm "b"))
                @?= pevalOrTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d"))
              pevalITETerm
                (ssymTerm "a")
                (pevalOrTerm (ssymTerm "c") (ssymTerm "b"))
                (pevalOrTerm (ssymTerm "d") (ssymTerm "b"))
                @?= pevalOrTerm (ssymTerm "b") (pevalITETerm (ssymTerm "a") (ssymTerm "c") (ssymTerm "d")),
            testCase "On left Or" $ do
              pevalITETerm
                (ssymTerm "a")
                (pevalOrTerm (ssymTerm "b") (ssymTerm "c"))
                (ssymTerm "b")
                @?= pevalOrTerm (ssymTerm "b") (pevalAndTerm (ssymTerm "a") (ssymTerm "c"))
              pevalITETerm
                (ssymTerm "a")
                (pevalOrTerm (ssymTerm "b") (ssymTerm "c"))
                (ssymTerm "c")
                @?= pevalOrTerm (ssymTerm "c") (pevalAndTerm (ssymTerm "a") (ssymTerm "b"))
              pevalITETerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                (ssymTerm "c")
                @?= pevalITETerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b") (ssymTerm "c")
              pevalITETerm
                (ssymTerm "a")
                (pevalOrTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b"))
                (ssymTerm "c")
                @?= pevalITETerm (ssymTerm "a") (ssymTerm "b") (ssymTerm "c")
              pevalITETerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalOrTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                (ssymTerm "c")
                @?= pevalITETerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "b") (ssymTerm "c")
              pevalITETerm
                (ssymTerm "a")
                (pevalOrTerm (ssymTerm "b") (pevalNotTerm $ ssymTerm "a"))
                (ssymTerm "c")
                @?= pevalITETerm (ssymTerm "a") (ssymTerm "b") (ssymTerm "c")
              pevalITETerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalOrTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b"))
                (ssymTerm "c")
                @?= pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "c")
              pevalITETerm
                (ssymTerm "a")
                (pevalOrTerm (ssymTerm "a") (ssymTerm "b"))
                (ssymTerm "c")
                @?= pevalOrTerm (ssymTerm "a") (ssymTerm "c")
              pevalITETerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalOrTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)))
                (ssymTerm "c")
                @?= pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "c")
              pevalITETerm
                (ssymTerm "a")
                (pevalOrTerm (ssymTerm "b") (ssymTerm "a"))
                (ssymTerm "c")
                @?= pevalOrTerm (ssymTerm "a") (ssymTerm "c"),
            testCase "On right Or" $ do
              pevalITETerm
                (ssymTerm "a")
                (ssymTerm "b")
                (pevalOrTerm (ssymTerm "b") (ssymTerm "c"))
                @?= pevalOrTerm (ssymTerm "b") (pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "c"))
              pevalITETerm
                (ssymTerm "a")
                (ssymTerm "c")
                (pevalOrTerm (ssymTerm "b") (ssymTerm "c"))
                @?= pevalOrTerm (ssymTerm "c") (pevalAndTerm (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")),
            testCase "On const boolean in branches" $ do
              pevalITETerm
                (ssymTerm "a")
                (conTerm True)
                (ssymTerm "b")
                @?= pevalOrTerm (ssymTerm "a") (ssymTerm "b")
              pevalITETerm
                (ssymTerm "a")
                (conTerm False)
                (ssymTerm "b")
                @?= pevalAndTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b")
              pevalITETerm
                (ssymTerm "a")
                (ssymTerm "b")
                (conTerm True)
                @?= pevalOrTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b")
              pevalITETerm
                (ssymTerm "a")
                (ssymTerm "b")
                (conTerm False)
                @?= pevalAndTerm (ssymTerm "a") (ssymTerm "b"),
            testCase "On condition equal to some branch" $ do
              pevalITETerm
                (ssymTerm "a")
                (ssymTerm "a")
                (ssymTerm "b")
                @?= pevalOrTerm (ssymTerm "a") (ssymTerm "b")
              pevalITETerm
                (ssymTerm "a")
                (ssymTerm "b")
                (ssymTerm "a")
                @?= pevalAndTerm (ssymTerm "a") (ssymTerm "b"),
            testCase "On left Not" $ do
              pevalITETerm (ssymTerm "a") (pevalNotTerm (ssymTerm "a")) (ssymTerm "b")
                @?= pevalAndTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b"),
            testCase "On right Not" $ do
              pevalITETerm (ssymTerm "a") (ssymTerm "b") (pevalNotTerm (ssymTerm "a"))
                @?= pevalOrTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b"),
            testCase "On left Not And" $ do
              pevalITETerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalNotTerm (pevalAndTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b")))
                (ssymTerm "c")
                @?= pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "c")
              pevalITETerm
                (ssymTerm "a")
                (pevalNotTerm (pevalAndTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b")))
                (ssymTerm "c")
                @?= pevalOrTerm (ssymTerm "a") (ssymTerm "c")
              pevalITETerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalNotTerm (pevalAndTerm (ssymTerm "b") (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))))
                (ssymTerm "c")
                @?= pevalOrTerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (ssymTerm "c")
              pevalITETerm
                (ssymTerm "a")
                (pevalNotTerm (pevalAndTerm (ssymTerm "b") (pevalNotTerm $ ssymTerm "a")))
                (ssymTerm "c")
                @?= pevalOrTerm (ssymTerm "a") (ssymTerm "c")
              pevalITETerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalNotTerm (pevalAndTerm (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2)) (ssymTerm "b")))
                (ssymTerm "c")
                @?= pevalITETerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (pevalNotTerm $ ssymTerm "b") (ssymTerm "c")
              pevalITETerm
                (ssymTerm "a")
                (pevalNotTerm (pevalAndTerm (ssymTerm "a") (ssymTerm "b")))
                (ssymTerm "c")
                @?= pevalITETerm (ssymTerm "a") (pevalNotTerm $ ssymTerm "b") (ssymTerm "c")
              pevalITETerm
                (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1))
                (pevalNotTerm (pevalAndTerm (ssymTerm "b") (pevalNEqTerm (ssymTerm "a" :: Term Integer) (conTerm 2))))
                (ssymTerm "c")
                @?= pevalITETerm (pevalEqTerm (ssymTerm "a" :: Term Integer) (conTerm 1)) (pevalNotTerm $ ssymTerm "b") (ssymTerm "c")
              pevalITETerm
                (ssymTerm "a")
                (pevalNotTerm (pevalAndTerm (ssymTerm "b") (ssymTerm "a")))
                (ssymTerm "c")
                @?= pevalITETerm (ssymTerm "a") (pevalNotTerm $ ssymTerm "b") (ssymTerm "c")
          ],
        testGroup
          "Imply"
          [ testCase "pevalImplyTerm" $ do
              ssymTerm "a"
                `pevalImplyTerm` ssymTerm "b"
                @?= pevalOrTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b")
          ],
        testGroup
          "Xor"
          [ testCase "pevalXorTerm" $ do
              ssymTerm "a"
                `pevalXorTerm` ssymTerm "b"
                @?= pevalOrTerm
                  (pevalAndTerm (pevalNotTerm $ ssymTerm "a") (ssymTerm "b"))
                  (pevalAndTerm (ssymTerm "a") (pevalNotTerm $ ssymTerm "b"))
          ]
      ]
  