Nuprl Lemma : aa_max_w_unit_wf
u1,u2:
?. (aa_max_w_unit(u1;u2) 
?)
Proof
Definitions occuring in Statement :
aa_max_w_unit: aa_max_w_unit(u1;u2),
all: x:A. B[x],
unit: Unit,
member: t T,
union: left + right,
int:
Definitions :
all: x:A. B[x],
member: t T,
aa_max_w_unit: aa_max_w_unit(u1;u2),
uall: [x:A]. B[x]
Lemmas :
imax_wf,
unit_wf2
\mforall{}u1,u2:\mBbbZ{}?. (aa\_max\_w\_unit(u1;u2) \mmember{} \mBbbZ{}?)
Date html generated:
2013_03_20-AM-09_52_11
Last ObjectModification:
2012_11_27-AM-10_32_16
Home
Index