---

Step * 2 of Lemma formal-sum-add_functionality


1. S : Type
2. K : RngSig
3. ∀x,x',y:basic-formal-sum(K;S).  (bfs-equiv(K;S;x;x') ⇒ bfs-equiv(K;S;x + y;x' + y))
⊢ ∀x,x',y,y':basic-formal-sum(K;S).  (bfs-equiv(K;S;y;y') ⇒ bfs-equiv(K;S;x;x') ⇒ bfs-equiv(K;S;x + y;x' + y'))
BY
{ (Auto
   THEN All (Unfolds ``basic-formal-sum formal-sum-add``)
   THEN Auto
   THEN (InstLemma `bfs-equiv-rel` [⌜K⌝;⌜S⌝]⋅ THENA Auto)
   THEN UseTrans ⌜x' + y⌝⋅
   THEN RWO  "bag-append-comm" 0
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Auto
  THEN  All  (Unfolds  ``basic-formal-sum  formal-sum-add``)
  THEN  Auto
  THEN  (InstLemma  `bfs-equiv-rel`  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  UseTrans  \mkleeneopen{}x'  +  y\mkleeneclose{}\mcdot{}
  THEN  RWO    "bag-append-comm"  0
  THEN  Auto)

---

Home Index