Proof Step: c_0_7

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

Proof State Overview

proof_step c_0_1 ⊕ transi72828568clp_dB X49 X50 X50 c_0_5 ⊕ transi72828568clp_dB X15 X1 X1 c_0_1->c_0_5 c_0_7 ⊕ transi72828568clp_dB X15 X1 X1 c_0_5->c_0_7 c_0_8 ⊕ $false c_0_7->c_0_8

Input Dependencies

c_0_1

Assumptions

c_0_5

Conclusion

c_0_7

Dependents

c_0_8

Formula

! [X15: dB > dB > $o,X1: dB] : ( transi72828568clp_dB @ X15 @ X1 @ X1 )

Source

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