Proof Step: c_0_7

name: c_0_7 syntax: thf role: negated_conjecture inference: assume_negation

Proof State Overview

proof_step c_0_1 c_0_1 c_0_7 c_0_7 c_0_1->c_0_7 c_0_9 c_0_9 c_0_7->c_0_9

Input Dependencies

c_0_1

Assumptions

c_0_1

Conclusion

c_0_7

Dependents

c_0_9

Formula

~ ( ( member_msg @ ( mPair @ x @ y ) @ ( synth @ ( analz @ h ) ) )
<=> ( ( member_msg @ x @ ( synth @ ( analz @ h ) ) )
    & ( member_msg @ y @ ( synth @ ( analz @ h ) ) ) ) )

Source

inference(assume_negation,[status(cth)],[c_0_1])