---

Step * of Lemma formal-sum-mul_functionality

∀S:Type. ∀K:CRng. ∀x,x':basic-formal-sum(K;S). ∀k,k':|K|.
  bfs-equiv(K;S;x;x') ⇒ bfs-equiv(K;S;k * x;k' * x') supposing k = k' ∈ |K|
BY
{ ((Auto THEN (RWO "-2<" 0 THENA Auto))
   THEN InstLemma `bfs-equiv-implies` [⌜S⌝;⌜K⌝;⌜λ2a b.bfs-equiv(K;S;k * a;k * b)⌝;⌜x⌝;⌜x'⌝]⋅
   THEN Auto) }

1
1. S : Type
2. K : CRng
3. x : basic-formal-sum(K;S)
4. x' : basic-formal-sum(K;S)
5. k : |K|
6. k' : |K|
7. k = k' ∈ |K|
8. bfs-equiv(K;S;x;x')
9. x1 : basic-formal-sum(K;S)
10. y : basic-formal-sum(K;S)
11. bfs-reduce(K;S;x1;y)
⊢ bfs-equiv(K;S;k * x1;k * y)

2
.....antecedent..... 
1. S : Type
2. K : CRng
3. x : basic-formal-sum(K;S)
4. x' : basic-formal-sum(K;S)
5. k : |K|
6. k' : |K|
7. k = k' ∈ |K|
8. bfs-equiv(K;S;x;x')
⊢ EquivRel(basic-formal-sum(K;S);x,y.bfs-equiv(K;S;k * x;k * y))

---

Latex:

---

Latex:
\mforall{}S:Type.  \mforall{}K:CRng.  \mforall{}x,x':basic-formal-sum(K;S).  \mforall{}k,k':|K|.
    bfs-equiv(K;S;x;x')  {}\mRightarrow{}  bfs-equiv(K;S;k  *  x;k'  *  x')  supposing  k  =  k'


By

---

Latex:
((Auto  THEN  (RWO  "-2<"  0  THENA  Auto))
  THEN  InstLemma  `bfs-equiv-implies`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}a  b.bfs-equiv(K;S;k  *  a;k  *  b)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index