If the tactic’s application is not valid because the resulting theorem has the wrong conclusion, CONJ_VALIDATE tac g will fail. If the resulting theorem has hypotheses not present in the goal state, then these hypotheses are added to the new goals as new proof obligations. The way in which this addition is done depends on how many subgoals tac generated when applied to g.

If tac completely solves g (though in an invalid way), the excess hypotheses h1...hn are bundled into a big conjunction and this becomes the one remaining goal. If tac g results in more than one new goal, then CONJ_VALIDATE tac g will produce one extra goal, consisting of a conjunction of hypotheses, as above. Finally, if tac g produces exactly one new goal to prove, and if the new goal’s assumptions are a subset of the original goal’s, CONJ_VALIDATE tac g will do the same, but with the conjunction of extra hypotheses to prove conjoined to that one goal’s conclusion. If there is one new goal, but its assumptions are not a subset, then a separate sub-goal is generated.

Because CONJ_VALIDATE prefers to generate just one sub-goal, the result may be a state where one ends up having to prove a hypothesis in a weaker context (with fewer assumptions) to hand than if VALIDATE had been used.