Proof Step: c_0_82

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

Proof State Overview

proof_step c_0_6 ⊕ times_times_real = ? c_0_71 ⊕ times_times_real X2050 X2051 = times_times_real X2051 X2050 c_0_6->c_0_71 c_0_82 ⊕ times_times_real X1 X5 = times_times_real X5 X1 c_0_71->c_0_82 c_0_90 ⊕ times_times_real X1 X5 = times_times_real X5 X1 c_0_82->c_0_90

Input Dependencies

c_0_6

Assumptions

c_0_71

Conclusion

c_0_82

Dependents

c_0_90

Formula

! [X5: real,X1: real] :
  ( ( times_times_real @ X1 @ X5 )
  = ( times_times_real @ X5 @ X1 ) )

Source

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