Proof Step: c_0_9

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

Proof State Overview

proof_step c_0_1 ⊕ image_nat_nat X327 bot_bot_set_nat = bot_bot_set_nat c_0_9 ⊕ image_nat_nat X3420 bot_bot_set_nat = bot_bot_set_nat c_0_1->c_0_9 c_0_13 ⊕ image_nat_nat X78 bot_bot_set_nat = bot_bot_set_nat c_0_9->c_0_13

Input Dependencies

c_0_1

Assumptions

c_0_1

Conclusion

c_0_9

Dependents

c_0_13

Formula

! [X3420: nat > nat] :
  ( ( image_nat_nat @ X3420 @ bot_bot_set_nat )
  = bot_bot_set_nat )

Source

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