Proof Step: c_0_19

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

Proof State Overview

proof_step c_0_1 ⊕ image_nat_nat X327 bot_bot_set_nat = bot_bot_set_nat c_0_13 ⊕ image_nat_nat X78 bot_bot_set_nat = bot_bot_set_nat c_0_1->c_0_13 c_0_19 ⊕ image_nat_nat X78 bot_bot_set_nat = bot_bot_set_nat c_0_13->c_0_19 c_0_25 ⊕ image_nat_nat X78 bot_bot_set_nat = bot_bot_set_nat c_0_19->c_0_25

Input Dependencies

c_0_1

Assumptions

c_0_13

Conclusion

c_0_19

Dependents

c_0_25

Formula

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

Source

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