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