Result of llprover

You are the 1-st user of this script.

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

            ------- Ax                   ------- Ax
            b --> b                      c --> c
------- Ax  ---------- R\/1  ------- Ax  ---------- R\/2
a --> a     b --> b\/c       a --> a     c --> b\/c
---------------------- R*    ---------------------- R*
   a,b --> a*(b\/c)             a,c --> a*(b\/c)
   ---------------- L*          ---------------- L*
   a*b --> a*(b\/c)             a*c --> a*(b\/c)
   --------------------------------------------- L\/
               a*b\/a*c --> a*(b\/c)

CPU Time = 312 msec.

Naoyuki Tamura