Nuprl Lemma : not_bfalse_btrue_const_fn_equal_union
((
x.tt) = (x.ff))
Proof
Definitions occuring in Statement :
b-union: A 
B,
bfalse: ff,
btrue: tt,
bool: 
,
nat: 
,
not: A,
lambda: x.A[x],
function: x:A 
B[x],
base: Base,
equal: s = t
Definitions :
not: A,
implies: P 
Q,
member: t 
T,
false: False,
ifthenelse: if b then t else f fi ,
nat: ,
btrue: tt,
bfalse: ff,
top: Top,
all: 
x:A. B[x],
le: A 
B,
exists: 
x:A. B[x],
squash: 
T,
true: True,
b-union: A B,
uall: [x:A]. B[x],
bool: ,
sq_type: SQType(T),
uimplies: b supposing a,
guard: {T},
unit: Unit,
assert: 
b,
uiff: uiff(P;Q),
and: P 
Q,
prop: 
,
bnot: 
b,
or: P 
Q,
it: 
Lemmas :
equal_wf,
b-union_wf,
base_wf,
nat_wf,
bool_wf,
btrue_wf,
bfalse_wf,
subtype_base_sq,
subtype_rel_self,
top_wf,
eqtt_to_assert,
le_wf,
eqff_to_assert,
bool_cases_sqequal,
bool_subtype_base,
Error :assert-bnot
\mneg{}((\mlambda{}x.tt) = (\mlambda{}x.ff))
Date html generated:
2013_03_20-AM-09_45_48
Last ObjectModification:
2012_12_05-AM-01_49_23
Home
Index