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 :
exists: ∃x:A. B[x],
coW-dom: coW-dom(a.B[a];w),
coW-equiv: coW-equiv(a.B[a];w;w'),
coW-item: coW-item(w;b)
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:
2019_06_20-PM-01_10_56
Last ObjectModification:
2019_01_02-PM-01_35_08
Theory : co-recursion-2
Home
Index