Nuprl Lemma : ohc_v1_prune_off_units_wf
[Cmd:ValueAllType]. (ohc_v1_prune_off_units(Cmd) 
(Cmd?) List 
(Cmd List))
Proof not projected
Definitions occuring in Statement :
ohc_v1_prune_off_units: ohc_v1_prune_off_units(Cmd),
uall: [x:A]. B[x],
unit: Unit,
member: t T,
function: x:A B[x],
union: left + right,
list: type List,
vatype: ValueAllType
Definitions :
uall: [x:A]. B[x],
vatype: ValueAllType,
member: t T,
ohc_v1_prune_off_units: ohc_v1_prune_off_units(Cmd),
assert: 
b,
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
uimplies: b supposing a,
sq_type: SQType(T),
all: x:A. B[x],
implies: P 
Q,
guard: {T},
prop: 
Lemmas :
mapfilter_wf,
unit_wf2,
isl_wf,
outl_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
assert_wf,
valueall-type_wf,
assert_elim
\mforall{}[Cmd:ValueAllType]. (ohc\_v1\_prune\_off\_units(Cmd) \mmember{} (Cmd?) List {}\mrightarrow{} (Cmd List))
Date html generated:
2012_02_20-PM-05_22_23
Last ObjectModification:
2012_02_13-PM-01_05_07
Home
Index