# Implies

Posted on 2018-01-18 by nbloomf

This page is part of a series on Arithmetic Made Difficult.

This post is literate Haskell; you can load the source into GHCi and play along.

{-# LANGUAGE NoImplicitPrelude #-}
module Implies (
impl, _test_impl, main_impl
) where

import Testing
import Booleans
import Not
import And
import Or

Next we define implication on booleans.

We define $$\bimpl : \bool \rightarrow \bool \rightarrow \bool$$ by $\bimpl(p,q) = \bif{p}{q}{\btrue}.$

impl :: (Boolean b) => b -> b -> b
impl p q = ifThenElse p q true

$$\bimpl$$ is equivalent to an $$\bor$$.

For all $$p,q \in \bool$$, we have $\bimpl(p,q) = \bor(\bnot(p),q).$

If $$p = \bfalse$$, we have $\begin{eqnarray*} & & \bimpl(\bfalse,q) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#def-implies} = & \bif{\bfalse}{q}{\btrue} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \btrue \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \bor(\btrue,q) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \bor(\bnot(\bfalse),q) \end{eqnarray*}$ as needed. Suppose then that $$p = \btrue$$. Then $\begin{eqnarray*} & & \bimpl(\btrue,q) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#def-implies} = & \bif{\btrue}{q}{\btrue} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & q \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-left} = & \bor(\bfalse,q) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-true} = & \bor(\bnot(\btrue),q) \end{eqnarray*}$ as needed.

_test_impl_or :: (Boolean b, Equal b)
=> b -> Test (b -> b -> Bool)
_test_impl_or _ =
testName "impl(p,q) == or(not(p),q)" $\p q -> eq (impl p q) (or (not p) q)  $$\bfalse$$ implies anything. If $$p \in \bool$$, we have $$\bimpl(\bfalse,p) = \btrue$$. We have $\begin{eqnarray*} & & \bimpl(\bfalse,p) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(\bfalse),p) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \bor(\btrue,p) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \btrue \end{eqnarray*}$ as claimed. _test_impl_false_hyp :: (Boolean b, Equal b) => b -> Test (b -> Bool) _test_impl_false_hyp _ = testName "impl(false,p) == true"$
\p -> eq (impl false p) true

$$\bfalse$$ interacts with $$\bimpl$$ in the right argument.

If $$p \in \bool$$, we have $$\bimpl(p,\bfalse) = \bnot(p)$$.

We have $\begin{eqnarray*} & & \bimpl(p,\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(p),\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-right} = & \bnot(p) \end{eqnarray*}$ as claimed.

_test_impl_false_conc :: (Boolean b, Equal b)
=> b -> Test (b -> Bool)
_test_impl_false_conc _ =
testName "impl(p,false) == not(p)" $\p -> eq (impl p false) (not p) $$\btrue$$ is left-neutral. For all $$p \in \bool$$ we have $$\bimpl(\btrue,p) = p$$. We have $\begin{eqnarray*} & & \bimpl(\btrue,p) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(\btrue),p) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-true} = & \bor(\bfalse,p) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-left} = & p \end{eqnarray*}$ as claimed. _test_impl_true_hyp :: (Boolean b, Equal b) => b -> Test (b -> Bool) _test_impl_true_hyp _ = testName "impl(true,p) == p"$
\p -> eq (impl true p) p

$$\btrue$$ is right-absorptive.

If $$p \in \bool$$, we have $$\bimpl(p,\btrue) = \btrue$$.

We have $\begin{eqnarray*} & & \bimpl(p,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(p),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-right} = & \btrue \end{eqnarray*}$ as claimed.

_test_impl_true_conc :: (Boolean b, Equal b)
=> b -> Test (b -> Bool)
_test_impl_true_conc _ =
testName "impl(p,true) == true" $\p -> eq (impl p true) true $$\bimpl$$ is… idemp-constant? Not sure what to call this. If $$p \in \bool$$ we have $$\bimpl(p,p) = \btrue$$. If $$p = \btrue$$, we have $\begin{eqnarray*} & & \bimpl(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(\btrue),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-right} = & \btrue \end{eqnarray*}$ as claimed. If $$p = \bfalse$$, we have $\begin{eqnarray*} & & \bimpl{\bfalse,\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \btrue \end{eqnarray*}$ as claimed. _test_impl_reflexive :: (Boolean b, Equal b) => b -> Test (b -> Bool) _test_impl_reflexive _ = testName "impl(p,p) == true"$
\p -> eq (impl p p) true

$$\bimpl$$ is antisymmetric.

For all $$p,q \in \bool$$ we have $$\bor(\bimpl(p,q),\bimpl(q,p))$$.

We have $\begin{eqnarray*} & & \bor(\bimpl(p,q),\bimpl(q,p)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bor(\bnot(p),q),\bimpl(q,p)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bor(\bnot(p),q),\bor(\bnot(q),p)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-associative} = & \bor(\bnot(p),\bor(q,\bor(\bnot(q),p))) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-associative} = & \bor(\bnot(p),\bor(\bor(q,\bnot(q)),p)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-not} = & \bor(\bnot(p),\bor(\btrue,p)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \bor(\bnot(p),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-right} = & \btrue \end{eqnarray*}$ as needed.

_test_impl_total :: (Boolean b, Equal b)
=> b -> Test (b -> b -> Bool)
_test_impl_total _ =
testName "or(impl(p,q),impl(q,p)) == true" $\p q -> eq (or (impl p q) (impl q p)) true $$\bimpl$$ is left-commutative. For all $$p,q,r \in \bool$$ we have $\bimpl(p,\bimpl(q,r)) = \bimpl(q,\bimpl(p,r)).$ We have $\begin{eqnarray*} & & \bimpl(p,\bimpl(q,r)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(p),\bimpl(q,r)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(p),\bor(\bnot(q),r)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-associative} = & \bor(\bor(\bnot(p),\bnot(q)),r) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-commutative} = & \bor(\bor(\bnot(q),\bnot(p)),r) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-associative} = & \bor(\bnot(q),\bor(\bnot(p),r)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(q),\bimpl(p,r)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bimpl(q,\bimpl(p,r)) \end{eqnarray*}$ as claimed. _test_impl_antecedents_commute :: (Boolean b, Equal b) => b -> Test (b -> b -> b -> Bool) _test_impl_antecedents_commute _ = testName "impl(p,impl(q,r)) == impl(q,impl(p,r))"$
\p q r -> eq (impl p (impl q r)) (impl q (impl p r))

$$\bimpl$$ has a kind of transitivity.

For all $$p,q,r \in \bool$$ we have $\bimpl(\bimpl(p,q),\bimpl(\bimpl(q,r),\bimpl(p,r))).$

If $$p = \bfalse$$, we have $\begin{eqnarray*} & & \bimpl(\bimpl(p,q),\bimpl(\bimpl(q,r),\bimpl(p,r))) \\ & \let{p = \bfalse} = & \bimpl(\bimpl(\bfalse,q),\bimpl(\bimpl(q,r),\bimpl(\bfalse,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \bimpl(\btrue,\bimpl(\bimpl(q,r),\bimpl(\bfalse,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \bimpl(\btrue,\bimpl(\bimpl(q,r),\btrue)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\bimpl(q,r),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(\bimpl(q,r)),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-right} = & \btrue \end{eqnarray*}$ as claimed. If $$p = \btrue$$, we have $\begin{eqnarray*} & & \bimpl(\bimpl(p,q),\bimpl(\bimpl(q,r),\bimpl(p,r))) \\ & \let{p = \btrue} = & \bimpl(\bimpl(\btrue,q),\bimpl(\bimpl(q,r),\bimpl(\btrue,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(q,\bimpl(\bimpl(q,r),\bimpl(\btrue,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(q,\bimpl(\bimpl(q,r),r)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-left-commutative} = & \bimpl(\bimpl(q,r),\bimpl(q,r)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-self} = & \btrue \end{eqnarray*}$ as claimed.

_test_impl_transitive :: (Boolean b, Equal b)
=> b -> Test (b -> b -> b -> Bool)
_test_impl_transitive _ =
testName "impl(impl(p,q),impl(impl(q,r),impl(p,r)))" $\p q r -> isTrue$ impl (impl p q) (impl (impl q r) (impl p r))

$$\bimpl$$ has a kind of distributivity.

For all $$p,q,r \in \bool$$ we have $\bimpl(\bimpl(p,\bimpl(q,r)),\bimpl(\bimpl(p,q),\bimpl(p,r))).$

If $$p = \bfalse$$, we have $\begin{eqnarray*} & & \bimpl(\bimpl(p,\bimpl(q,r)),\bimpl(\bimpl(p,q),\bimpl(p,r))) \\ & \let{p = \bfalse} = & \bimpl(\bimpl(\bfalse,\bimpl(q,r)),\bimpl(\bimpl(\bfalse,q),\bimpl(\bfalse,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \bimpl(\btrue,\bimpl(\bimpl(\bfalse,q),\bimpl(\bfalse,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \bimpl(\btrue,\bimpl(\btrue,\bimpl(\bfalse,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \bimpl(\btrue,\bimpl(\btrue,\btrue)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \btrue \end{eqnarray*}$ Suppose instead that $$p = \btrue$$. Now $\begin{eqnarray*} & & \bimpl(\bimpl(p,\bimpl(q,r)),\bimpl(\bimpl(p,q),\bimpl(p,r))) \\ & \let{p = \btrue} = & \bimpl(\bimpl(\btrue,\bimpl(q,r)),\bimpl(\bimpl(\btrue,q),\bimpl(\btrue,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\bimpl(q,r),\bimpl(\bimpl(\btrue,q),\bimpl(\btrue,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\bimpl(q,r),\bimpl(q,\bimpl(\btrue,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\bimpl(q,r),\bimpl(q,r)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-self} = & \btrue \end{eqnarray*}$ as claimed.

_test_impl_distributive :: (Boolean b, Equal b)
=> b -> Test (b -> b -> b -> Bool)
_test_impl_distributive _ =
testName "impl(impl(p,impl(q,r)),impl(impl(p,q),impl(p,r)))" $\p q r -> isTrue$ impl (impl p (impl q r)) (impl (impl p q) (impl p r))

$$\bimpl$$ interacts with $$\band$$.

For all $$p,q,r,s \in \bool$$, if $$\bimpl(p,r)$$ and $$\bimpl(q,s)$$, then $$\bimpl(\band(p,q),\band(r,s))$$.

If $$p = \bfalse$$, we have $\begin{eqnarray*} & & \bimpl(\band(\bimpl(p,r),\bimpl(q,s)),\bimpl(\band(p,q),\band(r,s))) \\ & \let{p = \bfalse} = & \bimpl(\band(\bimpl(\bfalse,r),\bimpl(q,s)),\bimpl(\band(\bfalse,q),\band(r,s))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \bimpl(\band(\btrue,\bimpl(q,s)),\bimpl(\band(\bfalse,q),\band(r,s))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \bimpl(\band(\btrue,\bimpl(q,s)),\bimpl(\bfalse,\band(r,s))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \bimpl(\band(\btrue,\bimpl(q,s)),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(\band(\btrue,\bimpl(q,s))),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-right} = & \btrue \end{eqnarray*}$ as claimed. suppose $$p = \btrue$$. If $$r = \bfalse$$, we have $\begin{eqnarray*} & & \bimpl(\band(\bimpl(p,r),\bimpl(q,s)),\bimpl(\band(p,q),\band(r,s))) \\ & \let{p = \btrue} = & \bimpl(\band(\bimpl(\btrue,r),\bimpl(q,s)),\bimpl(\band(\btrue,q),\band(r,s))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \bimpl(\band(\bimpl(\btrue,r),\bimpl(q,s)),\bimpl(q,\band(r,s))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\band(r,\bimpl(q,s)),\bimpl(q,\band(r,s))) \\ & \let{r = \bfalse} = & \bimpl(\band(\bfalse,\bimpl(q,s)),\bimpl(q,\band(\bfalse,s))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \bimpl(\bfalse,\bimpl(q,\band(\bfalse,s))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \btrue \end{eqnarray*}$ as claimed. If $$r = \btrue$$, we have $\begin{eqnarray*} & & \bimpl(\band(\bimpl(p,r),\bimpl(q,s)),\bimpl(\band(p,q),\band(r,s))) \\ & \let{p = \btrue} = & \bimpl(\band(\bimpl(\btrue,r),\bimpl(q,s)),\bimpl(\band(\btrue,q),\band(r,s))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \bimpl(\band(\bimpl(\btrue,r),\bimpl(q,s)),\bimpl(q,\band(r,s))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\band(r,\bimpl(q,s)),\bimpl(q,\band(r,s))) \\ & \let{r = \btrue} = & \bimpl(\band(\btrue,\bimpl(q,s)),\bimpl(q,\band(\btrue,s))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \bimpl(\bimpl(q,s),\bimpl(q,\band(\btrue,s))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \bimpl(\bimpl(q,s),\bimpl(q,s)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-self} = & \btrue \end{eqnarray*}$ as claimed.

_test_impl_and_compatible
:: (Boolean b, Equal b)
=> b -> Test (b -> b -> b -> b -> Bool)
_test_impl_and_compatible _ =
testName "if and(impl(p,r),impl(q,s)) then impl(and(p,q),and(r,s))" $\p q r s -> isTrue$ ifThenElse (and (impl p r) (impl q s))
(impl (and p q) (and r s))
(true)

$$\bimpl$$ interacts with $$\band$$ and $$\bif{\ast}{\ast}{\ast}$$.

Let $$p,q,r \in \bool$$. If $$\bimpl(r,q)$$, then $\bif{\band(p,q)}{\btrue}{r} = \bif{p}{q}{r}.$

If $$q = \btrue$$ then $\begin{eqnarray*} & & \bimpl(\bimpl(r,q),\beq(\bif{\band(p,q)}{\btrue}{r},\bif{p}{q}{r})) \\ & \let{q = \btrue} = & \bimpl(\bimpl(r,\btrue),\beq(\bif{\band(p,\btrue)}{\btrue}{r},\bif{p}{\btrue}{r})) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-conc} = & \bimpl(\btrue,\beq(\bif{\band(p,\btrue)}{\btrue}{r},\bif{p}{\btrue}{r})) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-right} = & \bimpl(\btrue,\beq(\bif{p}{\btrue}{r},\bif{p}{\btrue}{r})) \\ & \href{/posts/arithmetic-made-difficult/Testing.html#thm-eq-reflexive} = & \bimpl(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \btrue \end{eqnarray*}$ as claimed. If $$q = \bfalse$$ and $$r = \bfalse$$, we have $\begin{eqnarray*} & & \bimpl(\bimpl(r,q),\beq(\bif{\band(p,q)}{\btrue}{r},\bif{p}{q}{r})) \\ & \let{q = \bfalse} = & \bimpl(\bimpl(r,\bfalse),\beq(\bif{\band(p,\bfalse)}{\btrue}{r},\bif{p}{\bfalse}{r})) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-conc} = & \bimpl(\bnot(r),\beq(\bif{\band(p,\bfalse)}{\btrue}{r},\bif{p}{\bfalse}{r})) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-right} = & \bimpl(\bnot(r),\beq(\bif{\bfalse}{\btrue}{r},\bif{p}{\bfalse}{r})) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bimpl(\bnot(r),\beq(r,\bif{p}{\bfalse}{r})) \\ & \let{r = \bfalse} = & \bimpl(\bnot(\bfalse),\beq(\bfalse,\bif{p}{\bfalse}{\bfalse})) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \bimpl(\btrue,\beq(\bfalse,\bif{p}{\bfalse}{\bfalse})) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \bimpl(\btrue,\beq(\bfalse,\bfalse)) \\ & \href{/posts/arithmetic-made-difficult/Testing.html#thm-eq-reflexive} = & \bimpl(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \btrue \end{eqnarray*}$ as claimed. And if $$q = \bfalse$$ and $$r = \btrue$$, we have $\begin{eqnarray*} & & \bimpl(\bimpl(r,q),\beq(\bif{\band(p,q)}{\btrue}{r},\bif{p}{q}{r})) \\ & \let{q = \bfalse} = & \bimpl(\bimpl(r,\bfalse),\beq(\bif{\band(p,\bfalse)}{\btrue}{r},\bif{p}{\bfalse}{r})) \\ & \let{r = \btrue} = & \bimpl(\bimpl(\btrue,\bfalse),\beq(\bif{\band(p,\bfalse)}{\btrue}{\btrue},\bif{p}{\bfalse}{\btrue})) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\bfalse,\beq(\bif{\band(p,\bfalse)}{\btrue}{\btrue},\bif{p}{\bfalse}{\btrue})) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \btrue \end{eqnarray*}$ as claimed.

_test_impl_and_if :: (Boolean b, Equal b)
=> b -> Test (b -> b -> b -> Bool)
_test_impl_and_if _ =
testName "if impl(r,q) then if(and(p,q),true,r) == if(p,q,r)" \$
\p q r -> if isTrue (impl r q)
then eq
(ifThenElse (and p q) true r)
(ifThenElse p q r)
else true

## Testing

Suite:

_test_impl ::
( TypeName b, Boolean b, Arbitrary b, Show b, Equal b
) => b -> Int -> Int -> IO ()
_test_impl p size cases = do
testLabel1 "implies" p

let args = testArgs size cases

runTest args (_test_impl_or p)
runTest args (_test_impl_false_hyp p)
runTest args (_test_impl_false_conc p)
runTest args (_test_impl_true_hyp p)
runTest args (_test_impl_true_conc p)
runTest args (_test_impl_reflexive p)
runTest args (_test_impl_total p)
runTest args (_test_impl_antecedents_commute p)
runTest args (_test_impl_transitive p)
runTest args (_test_impl_distributive p)
runTest args (_test_impl_and_compatible p)
runTest args (_test_impl_and_if p)

Main:

main_impl :: IO ()
main_impl = _test_impl (true :: Bool) 20 100