Proof Step: c_0_35

name: c_0_35 syntax: thf role: plain inference: distribute

Proof State Overview

proof_step c_0_5 c_0_5 c_0_29 c_0_29 c_0_5->c_0_29 c_0_35 c_0_35 c_0_29->c_0_35 c_0_40 ⊕ member_msg X1 analz X3 ⊖ member_msg mPair X1 X2 analz X3 c_0_35->c_0_40

Input Dependencies

c_0_5

Assumptions

c_0_29

Conclusion

c_0_35

Dependents

c_0_40

Formula

! [X2615: msg,X2616: msg,X2617: set_msg] :
  ( ( ( member_msg @ X2615 @ ( analz @ X2617 ) )
    | ~ ( member_msg @ ( mPair @ X2615 @ X2616 ) @ ( analz @ X2617 ) ) )
  & ( ( member_msg @ X2616 @ ( analz @ X2617 ) )
    | ~ ( member_msg @ ( mPair @ X2615 @ X2616 ) @ ( analz @ X2617 ) ) ) )

Source

inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_29])])])