Proof Step: c_0_161

name: c_0_161 syntax: thf role: plain inference: evalgc

Proof State Overview

proof_step c_0_28 ⊕ ring_1_of_int_real one_one_int = one_one_real c_0_132 ⊕ ring_1_of_int_real one_one_int = one_one_real c_0_28->c_0_132 c_0_161 ⊕ ring_1_of_int_real one_one_int = one_one_real c_0_132->c_0_161 c_0_196 ⊕ ring_1_of_int_real one_one_int = one_one_real c_0_161->c_0_196

Input Dependencies

c_0_28

Assumptions

c_0_132

Conclusion

c_0_161

Dependents

c_0_196

Formula

( ( ring_1_of_int_real @ one_one_int )
= one_one_real )

Source

inference(evalgc,[status(thm)],[c_0_132])