-- RELALG1proof


Derivation of

(R/\((R*C(I))/\(C(I)*R)))*L = ((((C(I)*R)/\R)*C(I))/\R)*L

Applying the axiom

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

at position [] of the preceding formula leads to 

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

Reducts have been simplified.

Applying the axiom

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

at position [0] of the preceding formula leads to 

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

Reducts have been simplified.

Applying the axiom

     (R2/\S)*Q = (R2*Q)/\(S*Q)
<=== (C(I)*R2)/\R2 = 0

at position [0] of the preceding formula leads to 

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

Reducts have been simplified.

Applying the axioms

  (     (R4/\S)*Q = (R4*Q)/\(S*Q)
   <=== (C(I)*R4)/\R4 = 0)
& (     (R3/\S)*Q = (R3*Q)/\(S*Q)
   <=== (C(I)*R3)/\R3 = 0)

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

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

Reducts have been simplified.

Applying the axioms

  (     Q*(R6/\S) = (Q*R6)/\(Q*S)
   <=== (R6*C(I))/\R6 = 0)
& (     (R5/\S)*Q = (R5*Q)/\(S*Q)
   <=== (C(I)*R5)/\R5 = 0)

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

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

Reducts have been simplified.

Applying the axiom

     (R7/\S)*Q = (R7*Q)/\(S*Q)
<=== (C(I)*R7)/\R7 = 0

at position [3] of the preceding formula leads to 

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

Reducts have been simplified.

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

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

Number of proof steps: 7