Proof Step: c_0_13

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

Proof State Overview

proof_step c_0_3 c_0_3 c_0_13 ⊖ member_msg X2667 synth X2668 ⊖ member_msg X2669 synth X2668 ⊕ member_msg mPair X2667 X2669 synth X2668 c_0_3->c_0_13 c_0_19 ⊕ member_msg mPair X1 X2 synth X3 ⊖ member_msg X1 synth X3 ⊖ member_msg X2 synth X3 c_0_13->c_0_19

Input Dependencies

c_0_3

Assumptions

c_0_3

Conclusion

c_0_13

Dependents

c_0_19

Formula

! [X2667: msg,X2668: set_msg,X2669: msg] :
  ( ~ ( member_msg @ X2667 @ ( synth @ X2668 ) )
  | ~ ( member_msg @ X2669 @ ( synth @ X2668 ) )
  | ( member_msg @ ( mPair @ X2667 @ X2669 ) @ ( synth @ X2668 ) ) )

Source

inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])