Nuprl Definition : bfs-reduce

Formal sums, as and bs, should be equivalent if one can be obtained
from the other by either "removing zeros" or "combining coefficients".

This relation states a "single step" of that relation, without assuming that
it is decidable. We don't need to be able to decide which coefficients are
zero, or which "elements" in the formal sum have the same "generator".
(To do that would require that the scalars K have decidable equality
and the generators S have decidable equality.)

We then define bfs-equiv to be the least equivalence relation
containing this relation (i.e. the transitive-reflexive-symmetric closure
of this relation).⋅

bfs-reduce(K;S;as;bs) ==
  (∃s:bag(S). (as = (bs + 0 * s) ∈ basic-formal-sum(K;S)))
  ∨ (∃cs:basic-formal-sum(K;S)
      ∃k,k':|K|
       ∃fs:basic-formal-sum(K;S)

        ((as = (cs + k +K k' * fs) ∈ basic-formal-sum(K;S)) ∧ (bs = (cs + k * fs + k' * fs) ∈ basic-formal-sum(K;S))))

Definitions occuring in Statement : zero-bfs: 0 * ss, formal-sum-mul: k * x, basic-formal-sum: basic-formal-sum(K;S), infix_ap: x f y, exists: ∃x:A. B[x], or: P ∨ Q, and: P ∧ Q, equal: s = t ∈ T, rng_plus: +r, rng_car: |r|, bag-append: as + bs, bag: bag(T)
Definitions occuring in definition : or: P ∨ Q, bag: bag(T), zero-bfs: 0 * ss, rng_car: |r|, exists: ∃x:A. B[x], and: P ∧ Q, infix_ap: x f y, rng_plus: +r, equal: s = t ∈ T, basic-formal-sum: basic-formal-sum(K;S), bag-append: as + bs, formal-sum-mul: k * x
FDL editor aliases : bfs-reduce

Latex:
bfs-reduce(K;S;as;bs) == (\mexists{}s:bag(S). (as = (bs + 0 * s))) \mvee{} (\mexists{}cs:basic-formal-sum(K;S) \mexists{}k,k':|K| \mexists{}fs:basic-formal-sum(K;S). ((as = (cs + k +K k' * fs)) \mwedge{} (bs = (cs + k * fs + k' * fs)))) Date html generated: 2019_10_31-AM-06_28_27 Last ObjectModification: 2019_08_16-PM-04_10_34 Theory : linear!algebra Home Index