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,  squash: ↓T,  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.  (\mdownarrow{}\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_22_49
Last ObjectModification: 2012_07_02-PM-04_10_38

Home Index