Nuprl Lemma : sm-do-ops_wf
[S,Op,R:Type]. [s:S]. [f:S 
Op (S 
R)]. [L:Op List]. (sm-do-ops(s;f;L) 
S (R List))
Proof not projected
Definitions occuring in Statement :
sm-do-ops: sm-do-ops(s;f;L),
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
list: type List,
universe: Type
Definitions :
cons: [car / cdr],
append: as @ bs,
apply: f a,
spread: spread def,
nil: [],
pair: <a, b>,
lambda: 
x.A[x],
so_lambda: 
x y.t[x; y],
all: x:A. B[x],
list_accum: list_accum(x,a.f[x; a];y;l),
axiom: Ax,
sm-do-ops: sm-do-ops(s;f;L),
equal: s = t,
universe: Type,
product: x:A B[x],
function: x:A B[x],
uall: [x:A]. B[x],
member: t T,
list: type List,
isect: 
x:A. B[x]
Lemmas :
list_accum_wf,
append_wf
\mforall{}[S,Op,R:Type]. \mforall{}[s:S]. \mforall{}[f:S {}\mrightarrow{} Op {}\mrightarrow{} (S \mtimes{} R)]. \mforall{}[L:Op List]. (sm-do-ops(s;f;L) \mmember{} S \mtimes{} (R List))
Date html generated:
2011_10_20-PM-04_08_46
Last ObjectModification:
2011_01_24-PM-05_10_50
Home
Index