-- RELALG2proof


Derivation of

      T(C(R*A))*(R*L) =/= L
    & (R*L)/\(A*L) = A*L
    & (R/\I)*L = R*L
==> (R*L)/\(A*L) = R*L

Applying the axioms

  (     (R1/\S)*Q = (R1*Q)/\(S*Q)
   <=== (C(I)*R1)/\R1 = 0)
& T(C(R0)) = C(T(R0))

at positions [0,2],[0,0] of the preceding formula leads to 

      C(T(R*A))*(R*L) =/= L
    & (R*L)/\(A*L) = A*L
    & (R*L)/\(I*L) = R*L
    & (C(I)*R)/\R = 0
==> (R*L)/\(A*L) = R*L

Reducts have been simplified.

Applying the axioms

  I*R3 = R3
& T(R2*S) = T(S)*T(R2)

at positions [0,2],[0,0] of the preceding formula leads to 

      C(T(A)*T(R))*(R*L) =/= L
    & (R*L)/\(A*L) = A*L
    & (R*L)/\L = R*L
    & (C(I)*R)/\R = 0
==> (R*L)/\(A*L) = R*L

Reducts have been simplified.

Reversing the subtrees at positions [0,2,0,0],[0,2,0,1] of the preceding formula leads to 

      C(T(A)*T(R))*(R*L) =/= L
    & (R*L)/\(A*L) = A*L
    & L/\(R*L) = R*L
    & (C(I)*R)/\R = 0
==> (R*L)/\(A*L) = R*L

Reducts have been simplified.

Applying the axiom

L/\R4 = R4

at position [0,2] of the preceding formula leads to 

      C(T(A)*T(R))*(R*L) =/= L
    & (R*L)/\(A*L) = A*L
    & (C(I)*R)/\R = 0
==> (R*L)/\(A*L) = R*L

Reducts have been simplified.

Narrowing the preceding formula leads to 

      (C(T(A)*T(R))*R)*L =/= L
    & (R*L)/\(A*L) = A*L
    & (C(I)*R)/\R = 0
==> (R*L)/\(A*L) = R*L

Reducts have been simplified.

Number of proof steps: 5