Proof Step: c_0_45

name: c_0_45 syntax: thf role: axiom file: '/home/yan/atp/benchmarks/isa/deeper/B-mesh-th0/problems/HOL-Library/0131_Float/prob_00723_022817.p' file node: fact_101_mult_Oleft__commute

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

Input Dependencies

c_0_45

Assumptions

None

Conclusion

c_0_45

Dependents

c_0_191

Formula

! [X17: real,X6: real,X18: real] :
  ( ( times_times_real @ X17 @ ( times_times_real @ X6 @ X18 ) )
  = ( times_times_real @ X6 @ ( times_times_real @ X17 @ X18 ) ) )

Source

file('/home/yan/atp/benchmarks/isa/deeper/B-mesh-th0/problems/HOL-Library/0131_Float/prob_00723_022817.p',fact_101_mult_Oleft__commute)