---

Step * of Lemma formal-sum-add_functionality

∀S:Type. ∀K:RngSig. ∀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
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN Assert ⌜∀x,x',y:basic-formal-sum(K;S).  (bfs-equiv(K;S;x;x') ⇒ bfs-equiv(K;S;x + y;x' + y))⌝⋅
   ) }

1
.....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))

2
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'))

---

Latex:

---

Latex:
\mforall{}S:Type.  \mforall{}K:RngSig.  \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:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Assert  \mkleeneopen{}\mforall{}x,x',y:basic-formal-sum(K;S).    (bfs-equiv(K;S;x;x')  {}\mRightarrow{}  bfs-equiv(K;S;x  +  y;x'  +  y))\mkleeneclose{}\mcdot{}
  )

---

Home Index