Nuprl Definition : weakly-safe-seq
weakly-safe-seq(R;n;s) == w∃∞q.homogeneous(R;n + 1;s.q@n)
Definitions occuring in Statement :
homogeneous: homogeneous(R;n;s),
weakly-infinite: w∃∞p.S[p],
seq-add: s.x@n,
add: n + m,
natural_number: $n
Definitions occuring in definition :
weakly-infinite: w∃∞p.S[p],
homogeneous: homogeneous(R;n;s),
add: n + m,
natural_number: $n,
seq-add: s.x@n
FDL editor aliases :
weakly-safe-seq
Latex:
weakly-safe-seq(R;n;s) == w\mexists{}\minfty{}q.homogeneous(R;n + 1;s.q@n)
Date html generated:
2016_05_13-PM-03_50_32
Last ObjectModification:
2015_09_22-PM-05_45_21
Theory : bar-induction
Home
Index