Proof Step: c_0_1

name: c_0_1 syntax: thf role: axiom file: '/home/yan/atp/benchmarks/isa/deeper/B-mesh-th0/problems/HOL-Proofs-Lambda/0002_Lambda/prob_00161_004528.p' file node: fact_20_rtranclp_Ortrancl__refl

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

Input Dependencies

c_0_1

Assumptions

None

Conclusion

c_0_1

Dependents

c_0_3

Formula

! [X49: dB > dB > $o,X50: dB] : ( transi72828568clp_dB @ X49 @ X50 @ X50 )

Source

file('/home/yan/atp/benchmarks/isa/deeper/B-mesh-th0/problems/HOL-Proofs-Lambda/0002_Lambda/prob_00161_004528.p',fact_20_rtranclp_Ortrancl__refl)