Drule.CONJ

STRUCTURE

SYNOPSIS

Discharges an assumption and conjoins it to both sides of an equation.

DESCRIPTION

Given an term t and a theorem A |- t1 = t2, which is an equation between boolean terms, CONJ_DISCH returns A - {t} |- (t /\ t1) = (t /\ t2), i.e. conjoins t to both sides of the equation, removing t from the assumptions if it was there.

            A |- t1 = t2
   ------------------------------  CONJ_DISCH "t"
    A - {t} |- t /\ t1 = t /\ t2

FAILURE

Fails unless the theorem is an equation, both sides of which, and the term provided are of type bool.

SEEALSO

CONJ_DISCHL