Nuprl Lemma : not_base_decidable_eq_weaker
((
t:Base. ((
(t)
) 
(t))) 
(t:Base. (((t ~ bottom())) (t)))) ((t1,t2:Base. Dec(t1 = t2)))
Proof
Definitions occuring in Statement :
decidable: Dec(P),
all: x:A. B[x],
not: A,
implies: P Q,
or: P Q,
base: Base,
sqequal: s ~ t,
equal: s = t,
bottom: bottom(),
has-value: (a)
Definitions :
so_lambda: 
x.t[x],
prop: 
,
member: t 
T,
false: False,
not: A,
implies: P Q,
all: x:A. B[x],
guard: {T},
or: P Q,
so_apply: x[s],
uall: [x:A]. B[x],
decidable: Dec(P),
uimplies: b supposing a
Lemmas :
base_sq,
has-value_wf_base,
not_wf,
or_wf,
equal_wf,
decidable_wf,
base_wf,
all_wf,
Error :not_has-value_decidable_on_base,
bottom_diverge,
Error :no-value-bottom-base
((\mforall{}t:Base. ((\mneg{}\mneg{}(t)\mdownarrow{}) {}\mRightarrow{} (t)\mdownarrow{})) \mvee{} (\mforall{}t:Base. ((\mneg{}(t \msim{} bottom())) {}\mRightarrow{} (t)\mdownarrow{})))
{}\mRightarrow{} (\mneg{}(\mforall{}t1,t2:Base. Dec(t1 = t2)))
Date html generated:
2013_03_20-AM-09_48_35
Last ObjectModification:
2012_11_27-AM-10_32_01
Home
Index