Nuprl Lemma : contrapos_elim2
P,Q:
.  ((
R:
. (
R 
 (
R))) ![](../FONT/eq.png)
 ((![](../FONT/not.png)
Q) ![](../FONT/eq.png)
 (![](../FONT/not.png)
P)) ![](../FONT/eq.png)
 {(
P) ![](../FONT/eq.png)
 (
Q)})
Proof
Definitions occuring in Statement : 
prop:
, 
guard: {T}, 
all:
x:A. B[x], 
not:
A, 
squash:
T, 
implies: P ![](../FONT/eq.png)
 Q, 
or: P 
 Q
Definitions : 
all:
x:A. B[x], 
prop:
, 
implies: P ![](../FONT/eq.png)
 Q, 
squash:
T, 
not:
A, 
guard: {T}, 
true: True, 
member: t 
 T, 
false: False, 
so_lambda: ![](../FONT/lam.png)
x.t[x], 
or: P 
 Q, 
uall:
[x:A]. B[x], 
so_apply: x[s]
Lemmas : 
squash_wf, 
not_wf, 
all_wf, 
or_wf
\mforall{}P,Q:\mBbbP{}.    ((\mforall{}R:\mBbbP{}.  (\mdownarrow{}R  \mvee{}  (\mneg{}R)))  {}\mRightarrow{}  ((\mneg{}\mdownarrow{}Q)  {}\mRightarrow{}  (\mneg{}\mdownarrow{}P))  {}\mRightarrow{}  \{(\mdownarrow{}P)  {}\mRightarrow{}  (\mdownarrow{}Q)\})
Date html generated:
2013_03_20-AM-10_48_58
Last ObjectModification:
2013_02_25-PM-06_11_38
Home
Index