{ 
[n:
]. [a:Id]. (urand(n;a) 
n) }
{ Proof }
Definitions occuring in Statement :
urand: urand(n;a),
Id: Id,
int_seg: {i..j
},
nat_plus: ,
nat: ,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
natural_number: $n
Definitions :
uniform-fps: Error :uniform-fps,
atom: Atom$n,
strong-subtype: strong-subtype(A;B),
le: A 
B,
ge: i 
j ,
not: 
A,
less_than: a < b,
uimplies: b supposing a,
product: x:A 
B[x],
and: P 
Q,
uiff: uiff(P;Q),
subtype_rel: A 
r B,
int: 
,
set: {x:A| B[x]} ,
p-outcome: Outcome,
random: random(p;a;b),
all: x:A. B[x],
function: x:A B[x],
nat: ,
int_seg: {i..j},
natural_number: $n,
urand: urand(n;a),
axiom: Ax,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
Id: Id,
nat_plus: ,
member: t T,
equal: s = t,
Auto: Error :Auto,
CollapseTHEN: Error :CollapseTHEN,
Knd: Knd,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
lambda: 
x.A[x],
qadd_grp: <
+>,
grp_le: 
,
infix_ap: x f y,
pair: <a, b>,
quotient: x,y:A//B[x; y],
grp_leq: a b,
bool: 
,
qle: r s,
select: l[i],
qsum: 
a j < b. E[j],
l_all: (xL.P[x]),
cand: A c B,
map: map(f;as),
intensional-universe: IType,
apply: f a,
so_apply: x[s],
l_member: (x l),
so_lambda: 
x.t[x],
grp_car: |g|,
finite-prob-space: FinProbSpace,
proper-iseg: L1 < L2,
iseg: l1 l2,
gt: i > j,
sum-map: f[x] for x L,
sum: (f[x] | x < k),
imax: imax(a;b),
multiply: n * m,
assert: 
b,
valueall-type: valueall-type(T),
sqequal: s ~ t,
subtract: n - m,
add: n + m,
void: Void,
prop: 
,
length: ||as||,
rationals: ,
lelt: i j < k,
tag-by: zT,
rev_implies: P 
Q,
or: P 
Q,
iff: P 
Q,
record+: record+,
record: record(x.T[x]),
fset: FSet{T},
tuple-type: tuple-type(L),
stream: stream(A),
isect2: T1 T2,
b-union: A 
B,
union: left + right,
top: Top,
true: True,
deq: EqDecider(T),
guard: {T},
implies: P Q,
false: False,
universe: Type,
int_nzero: 
,
real: 
,
subtype: S T,
bag: Error :bag,
list: type List,
upto: upto(n),
CollapseTHENA: Error :CollapseTHENA
Lemmas :
length-map,
length_upto,
upto_wf,
nat_plus_inc,
subtype_rel_self,
subtype_rel_function,
nat_plus_properties,
nat_properties,
le_wf,
not_wf,
false_wf,
int_seg_properties,
length_wf_nat,
subtype_rel_set,
subtype_rel_sets,
finite-prob-space_wf,
top_wf,
intensional-universe_wf,
rationals_wf,
subtype_rel_list,
Id_wf,
nat_plus_wf,
random_wf,
Error :uniform-fps_wf,
member_wf,
int_seg_wf,
p-outcome_wf,
nat_wf,
subtype_rel_wf
\mforall{}[n:\mBbbN{}\msupplus{}]. \mforall{}[a:Id]. (urand(n;a) \mmember{} \mBbbN{} {}\mrightarrow{} \mBbbN{}n)
Date html generated:
2011_08_10-AM-07_54_17
Last ObjectModification:
2011_06_07-PM-06_20_57
Home
Index