Proof Step: c_0_25

name: c_0_25 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_19 ⊕ image_nat_nat X78 bot_bot_set_nat = bot_bot_set_nat c_0_1->c_0_19 c_0_25 ⊕ image_nat_nat X78 bot_bot_set_nat = bot_bot_set_nat c_0_19->c_0_25 c_0_30 ⊕ keysFor X4 = bot_bot_set_nat ⊖ ? = bot_bot_nat_o c_0_25->c_0_30

Input Dependencies

c_0_1

Assumptions

c_0_19

Conclusion

c_0_25

Dependents

c_0_30

Formula

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

Source

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