Proof Step: c_0_17

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

Proof State Overview

proof_step c_0_3 ⊕ field_b bot_bo1343651123od_b_b = bot_bot_set_b c_0_11 ⊕ field_b bot_bo1343651123od_b_b = bot_bot_set_b c_0_3->c_0_11 c_0_17 ⊕ field_b bot_bo1343651123od_b_b = bot_bot_set_b c_0_11->c_0_17 c_0_24 ⊕ field_b bot_bo1343651123od_b_b = bot_bot_set_b c_0_17->c_0_24

Input Dependencies

c_0_3

Assumptions

c_0_11

Conclusion

c_0_17

Dependents

c_0_24

Formula

( ( field_b @ bot_bo1343651123od_b_b )
= bot_bot_set_b )

Source

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