Nuprl Definition : fs-predicate
fs-predicate(K;S;p.P[p];f) == ↓∃b:basic-formal-sum(K;S). ((f = b ∈ formal-sum(K;S)) ∧ bfs-predicate(K;S;p.P[p];b))
Definitions occuring in Statement :
formal-sum: formal-sum(K;S),
bfs-predicate: bfs-predicate(K;S;p.P[p];b),
basic-formal-sum: basic-formal-sum(K;S),
exists: ∃x:A. B[x],
squash: ↓T,
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
squash: ↓T,
exists: ∃x:A. B[x],
basic-formal-sum: basic-formal-sum(K;S),
and: P ∧ Q,
equal: s = t ∈ T,
formal-sum: formal-sum(K;S),
bfs-predicate: bfs-predicate(K;S;p.P[p];b)
FDL editor aliases :
fs-predicate
Latex:
fs-predicate(K;S;p.P[p];f) == \mdownarrow{}\mexists{}b:basic-formal-sum(K;S). ((f = b) \mwedge{} bfs-predicate(K;S;p.P[p];b))
Date html generated:
2019_10_31-AM-06_28_56
Last ObjectModification:
2019_08_19-AM-10_50_59
Theory : linear!algebra
Home
Index