Nuprl Definition : iterated-classrel

`iterated-classrel(es;S;A;f;init;X;e;v) ==`
`  fix((λiterated-classrel,e,v. ∃z:S`
`                                (if first(e) then z ↓∈ init loc(e) else iterated-classrel pred(e) z fi `
`                                ∧ ((∃a:A. (a ∈ X(e) ∧ (v = (f a z) ∈ S))) ∨ ((∀a:A. (¬a ∈ X(e))) ∧ (v = z ∈ S)))))) `
`  e `
`  v`

Definitions occuring in Statement :  classrel: `v ∈ X(e)` es-first: `first(e)` es-pred: `pred(e)` es-loc: `loc(e)` ifthenelse: `if b then t else f fi ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` or: `P ∨ Q` and: `P ∧ Q` apply: `f a` fix: `fix(F)` lambda: `λx.A[x]` equal: `s = t ∈ T` bag-member: `x ↓∈ bs`
FDL editor aliases :  iterated-classrel
iterated-classrel(es;S;A;f;init;X;e;v)  ==
fix((\mlambda{}iterated-classrel,e,v.  \mexists{}z:S
(if  first(e)
then  z  \mdownarrow{}\mmember{}  init  loc(e)
else  iterated-classrel  pred(e)  z
fi
\mwedge{}  ((\mexists{}a:A.  (a  \mmember{}  X(e)  \mwedge{}  (v  =  (f  a  z))))
\mvee{}  ((\mforall{}a:A.  (\mneg{}a  \mmember{}  X(e)))  \mwedge{}  (v  =  z))))))
e
v

Date html generated: 2015_07_17-PM-00_25_57
Last ObjectModification: 2012_07_02-PM-04_10_48

Home Index