Drule.cj

STRUCTURE

SYNOPSIS

Returns the i’th conjunct of a “guarded” theorem

DESCRIPTION

A call to cj i th, where th has the form

   |- !x1 .. xn. p1 /\ .. /\ pm ==> !y... q1 /\ .. ==> ... ==>
                                          c1 /\ c2 /\ ... ck

returns the theorem

   |- !x1 .. xn. p1 /\ .. /\ pm ==> !y... q1 /\ .. ==> ... ==> ci

Note that the indexing starts at 1. The conjuncts are stripped apart without regard to the way in which they are associated, as per the behaviour of CONJUNCTS.

FAILURE

Fails if the conclusion of the guarded theorem does not contain at least i conjuncts. A bare term is always considered to be 1 conjunct.

SEEALSO

BODY_CONJUNCTS, CONJUNCTS, underAIs