Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456

EQ_TAC : tactic

SYNOPSIS

Reduces goal of equality of boolean terms to forward and backward implication.

DESCRIPTION

When applied to a goal A ?- t1 <=> t2, where t1 and t2 have type bool, the tactic EQ_TAC returns the subgoals A ?- t1 ==> t2 and A ?- t2 ==> t1.

             A ?- t1 <=> t2
   =================================  EQ_TAC
    A ?- t1 ==> t2   A ?- t2 ==> t1

FAILURE CONDITIONS

Fails unless the conclusion of the goal is an equation between boolean terms.

SEE ALSO

EQ_IMP_RULE, IMP_ANTISYM_RULE.