Nuprl Lemma : ohc_v2_roundout1_wf
[Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)]. [flrs:
].
(ohc_v2_roundout1(Cmd;cmdeq;flrs) 
A:
'. (A 
Cmd Id Cmd List (Id List) bag(Cmd? Cmd)))
Proof not projected
Definitions occuring in Statement :
ohc_v2_roundout1: ohc_v2_roundout1(Cmd;cmdeq;flrs),
Id: Id,
uall: [x:A]. B[x],
unit: Unit,
member: t T,
isect: x:A. B[x],
function: x:A B[x],
product: x:A B[x],
union: left + right,
list: type List,
int: ,
universe: Type,
deq: EqDecider(T),
bag: bag(T),
vatype: ValueAllType
Definitions :
uall: [x:A]. B[x],
vatype: ValueAllType,
member: t T,
ohc_v2_roundout1: ohc_v2_roundout1(Cmd;cmdeq;flrs),
nat: 
,
all: x:A. B[x]
Lemmas :
ifthenelse_wf,
eq_int_wf,
length_wf,
bag_wf,
unit_wf2,
poss-maj_wf,
single-bag_wf,
it_wf,
empty-bag_wf,
Id_wf,
deq_wf,
valueall-type_wf
\mforall{}[Cmd:ValueAllType]. \mforall{}[cmdeq:EqDecider(Cmd)]. \mforall{}[flrs:\mBbbZ{}].
(ohc\_v2\_roundout1(Cmd;cmdeq;flrs) \mmember{} \mcap{}A:\mBbbU{}'
(A
{}\mrightarrow{} \mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id
{}\mrightarrow{} Cmd List \mtimes{} (Id List)
{}\mrightarrow{} bag(Cmd? \mtimes{} Cmd)))
Date html generated:
2012_02_20-PM-05_33_22
Last ObjectModification:
2012_02_17-PM-10_31_46
Home
Index