Nuprl Definition : coWmem
coWmem(a.B[a];z;w) == ∃b:coW-dom(a.B[a];w). coW-equiv(a.B[a];z;coW-item(w;b))
Definitions occuring in Statement :
coW-equiv: coW-equiv(a.B[a];w;w'),
coW-item: coW-item(w;b),
coW-dom: coW-dom(a.B[a];w),
exists: ∃x:A. B[x]
Definitions occuring in definition :
coW-item: coW-item(w;b),
coW-equiv: coW-equiv(a.B[a];w;w'),
coW-dom: coW-dom(a.B[a];w),
exists: ∃x:A. B[x]
FDL editor aliases :
coWmem
Latex:
coWmem(a.B[a];z;w) == \mexists{}b:coW-dom(a.B[a];w). coW-equiv(a.B[a];z;coW-item(w;b))
Date html generated:
2018_07_25-PM-01_48_05
Last ObjectModification:
2018_06_20-PM-05_56_35
Theory : co-recursion
Home
Index