---

Step * 1 of Lemma formal-sum-add_functionality

.....assertion..... 
1. S : Type
2. K : RngSig
⊢ ∀x,x',y:basic-formal-sum(K;S).  (bfs-equiv(K;S;x;x') ⇒ bfs-equiv(K;S;x + y;x' + y))
BY
{ (Auto THEN InstLemma `bfs-equiv-implies` [⌜S⌝;⌜K⌝;⌜λ2a b.bfs-equiv(K;S;a + y;b + y)⌝;⌜x⌝;⌜x'⌝]⋅ THEN Auto) }

1
1. S : Type
2. K : RngSig
3. x : basic-formal-sum(K;S)
4. x' : basic-formal-sum(K;S)
5. y : basic-formal-sum(K;S)
6. bfs-equiv(K;S;x;x')
7. x1 : basic-formal-sum(K;S)
8. y@0 : basic-formal-sum(K;S)
9. bfs-reduce(K;S;x1;y@0)
⊢ bfs-equiv(K;S;x1 + y;y@0 + y)

2
.....antecedent..... 
1. S : Type
2. K : RngSig
3. x : basic-formal-sum(K;S)
4. x' : basic-formal-sum(K;S)
5. y : basic-formal-sum(K;S)
6. bfs-equiv(K;S;x;x')
⊢ EquivRel(basic-formal-sum(K;S);x,y@0.bfs-equiv(K;S;x + y;y@0 + y))

---

Latex:

---

Latex:
.....assertion..... 
1.  S  :  Type
2.  K  :  RngSig
\mvdash{}  \mforall{}x,x',y:basic-formal-sum(K;S).    (bfs-equiv(K;S;x;x')  {}\mRightarrow{}  bfs-equiv(K;S;x  +  y;x'  +  y))


By

---

Latex:
(Auto
  THEN  InstLemma  `bfs-equiv-implies`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}a  b.bfs-equiv(K;S;a  +  y;b  +  y)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index