Proof Step: c_0_3

name: c_0_3 syntax: thf role: plain inference: variable_rename

Proof State Overview

proof_step c_0_1 ⊕ transi72828568clp_dB X49 X50 X50 c_0_3 ⊕ transi72828568clp_dB X2708 X2709 X2709 c_0_1->c_0_3 c_0_5 ⊕ transi72828568clp_dB X15 X1 X1 c_0_3->c_0_5

Input Dependencies

c_0_1

Assumptions

c_0_1

Conclusion

c_0_3

Dependents

c_0_5

Formula

! [X2708: dB > dB > $o,X2709: dB] : ( transi72828568clp_dB @ X2708 @ X2709 @ X2709 )

Source

inference(variable_rename,[status(thm)],[c_0_1])