Nuprl Lemma : Threshold-Combinator_wf
[S,A,B:
']. [X:EClass'(A)]. [R:A 
S 
]. [init_state:Id bag(S)]. [accum:A S S]. [f:Id
A
S
bag(B)].
(Threshold-Combinator(R;X;init_state;accum;f) 
EClass'(B))
Proof not projected
Definitions occuring in Statement :
Threshold-Combinator: Threshold-Combinator(R;X;init_state;accum;f),
Message: Message,
eclass: EClass(A[eo; e]),
Id: Id,
bool: ,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
universe: Type,
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
eclass: EClass(A[eo; e]),
member: t T,
Threshold-Combinator: Threshold-Combinator(R;X;init_state;accum;f),
let: let,
all: x:A. B[x],
subtype: S 
T
Lemmas :
simple-loc-comb-2_wf,
Message_wf,
concat-lifting-loc-2_wf,
ifthenelse_wf,
bag_wf,
empty-bag_wf,
Id_wf,
Memory-class_wf,
bool_wf,
event-ordering+_wf,
es-E_wf,
event-ordering+_inc
\mforall{}[S,A,B:\mBbbU{}']. \mforall{}[X:EClass'(A)]. \mforall{}[R:A {}\mrightarrow{} S {}\mrightarrow{} \mBbbB{}]. \mforall{}[init$_{state}$:Id {}\mrightarrow{} bag(S)]. \000C\mforall{}[accum:A {}\mrightarrow{} S {}\mrightarrow{} S].
\mforall{}[f:Id {}\mrightarrow{} A {}\mrightarrow{} S {}\mrightarrow{} bag(B)].
(Threshold-Combinator(R;X;init$_{state}$;accum;f) \mmember{} EClass'(B))
Date html generated:
2012_01_23-PM-01_04_40
Last ObjectModification:
2012_01_10-AM-00_28_06
Home
Index