Proof Step: c_0_224

name: c_0_224 syntax: thf role: plain inference: split_conjunct

Proof State Overview

proof_step c_0_45 ⊕ times_times_real X17 times_times_real X6 X18 = times_times_real X6 times_times_real X17 X18 c_0_191 ⊕ times_times_real X2321 times_times_real X2322 X2323 = times_times_real X2322 times_times_real X2321 X2323 c_0_45->c_0_191 c_0_224 ⊕ times_times_real X2 times_times_real X4 X6 = times_times_real X4 times_times_real X2 X6 c_0_191->c_0_224 c_0_253 ⊕ times_times_real X2 times_times_real X4 X6 = times_times_real X4 times_times_real X2 X6 c_0_224->c_0_253

Input Dependencies

c_0_45

Assumptions

c_0_191

Conclusion

c_0_224

Dependents

c_0_253

Formula

! [X2: real,X4: real,X6: real] :
  ( ( times_times_real @ X2 @ ( times_times_real @ X4 @ X6 ) )
  = ( times_times_real @ X4 @ ( times_times_real @ X2 @ X6 ) ) )

Source

inference(split_conjunct,[status(thm)],[c_0_191])