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

EQF_INTRO : thm -> thm

SYNOPSIS

Converts negation to equality with F.

DESCRIPTION

     A |- ~tm
   ---------------  EQF_INTRO
    A |- tm <=> F

FAILURE CONDITIONS

Fails if the argument theorem is not a negation.

EXAMPLE

  # let th = ASSUME `~p`;;
  val th : thm = ~p |- ~p

  # EQF_INTRO th;;
  val it : thm = ~p |- p <=> F