Proof Step: c_0_13

name: c_0_13 syntax: thf role: plain inference: split_conjunct

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 c_0_19 ⊕ image_nat_nat X78 bot_bot_set_nat = bot_bot_set_nat c_0_13->c_0_19

Input Dependencies

c_0_1

Assumptions

c_0_9

Conclusion

c_0_13

Dependents

c_0_19

Formula

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

Source

inference(split_conjunct,[status(thm)],[c_0_9])