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
CONTR : term -> thm -> thm
SYNOPSIS
Implements the intuitionistic contradiction rule.
DESCRIPTION
When applied to a term t and a theorem A |- F, the inference rule CONTR
returns the theorem A |- t.
A |- F
-------- CONTR `t`
A |- t
FAILURE CONDITIONS
Fails unless the term has type bool and the theorem has F as its
conclusion.
EXAMPLE
# let th = REWRITE_RULE[ARITH] (ASSUME `1 = 0`);;
val th : thm = 1 = 0 |- F
# CONTR `Russell:Person = Pope` th;;
val it : thm = 1 = 0 |- Russell = Pope