Result of llprover

You are the 2-nd user of this script.

System: CLL
Formula: (a*b)\/(a*c) --> a*(b\/c)
Output style: twosided, tex

\begin{displaymath}
\infer[\LR{\dsum}]{A \tprod B \dsum A \tprod C \drv A \tprod (B \dsum C)}{
  \infer[\LR{\tprod}]{A \tprod B \drv A \tprod (B \dsum C)}{
    \infer[\RR{\tprod}]{A, B \drv A \tprod (B \dsum C)}{
      \infer[\Ax]{A \drv A}{}
      &
      \infer[\RR{\dsum_{1}}]{B \drv B \dsum C}{
        \infer[\Ax]{B \drv B}{}
      }
    }
  }
  &
  \infer[\LR{\tprod}]{A \tprod C \drv A \tprod (B \dsum C)}{
    \infer[\RR{\tprod}]{A, C \drv A \tprod (B \dsum C)}{
      \infer[\Ax]{A \drv A}{}
      &
      \infer[\RR{\dsum_{2}}]{C \drv B \dsum C}{
        \infer[\Ax]{C \drv C}{}
      }
    }
  }
}
\end{displaymath}

CPU Time = 218 msec.

Naoyuki Tamura