{ 
[a:Atom]. (str1-to-nat(a) 
) }
{ Proof }
Definitions occuring in Statement :
str1-to-nat: str1-to-nat(a),
nat: ,
uall: [x:A]. B[x],
member: t T,
atom: Atom
Definitions :
uall: [x:A]. B[x],
member: t T,
nat: ,
str1-to-nat: str1-to-nat(a),
ifthenelse: if b then t else f fi ,
all: x:A. B[x],
implies: P 
Q,
btrue: tt,
prop: 
,
le: A 
B,
not: 
A,
false: False,
bfalse: ff,
bool: 
,
unit: Unit,
iff: P 
Q,
and: P 
Q,
it: 
Lemmas :
eq_atom_wf,
bool_wf,
iff_weakening_uiff,
uiff_transitivity,
assert_wf,
eqtt_to_assert,
assert_of_eq_atom,
le_wf,
not_wf,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_uiff
\mforall{}[a:Atom]. (str1-to-nat(a) \mmember{} \mBbbN{})
Date html generated:
2011_08_10-AM-07_42_29
Last ObjectModification:
2011_06_18-AM-08_09_40
Home
Index