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
NOT_INTRO : thm -> thm
SYNOPSIS
Transforms |- t ==> F into |- ~t.
DESCRIPTION
When applied to a theorem A |- t ==> F, the inference rule NOT_INTRO
returns the theorem A |- ~t.
A |- t ==> F
-------------- NOT_INTRO
A |- ~t
FAILURE CONDITIONS
Fails unless the theorem has an implicative conclusion with F
as the consequent.
EXAMPLE
# let th = TAUT `F ==> F`;;
val th : thm = |- F ==> F
# NOT_INTRO th;;
val it : thm = |- ~F