---

Step * 1 1 of Lemma formal-sum-add-comm

.....antecedent..... 
1. S : Type
2. K : RngSig
3. ∀[x,y:basic-formal-sum(K;S)].  (x + y = y + x ∈ basic-formal-sum(K;S))
4. x : Base
5. x1 : Base
6. x = x1 ∈ pertype(λa,b. ((a ∈ basic-formal-sum(K;S)) ∧ (b ∈ basic-formal-sum(K;S)) ∧ bfs-equiv(K;S;a;b)))
7. x ∈ basic-formal-sum(K;S)
8. x1 ∈ basic-formal-sum(K;S)
9. bfs-equiv(K;S;x;x1)
10. y : Base
11. y1 : Base
12. y = y1 ∈ pertype(λa,b. ((a ∈ basic-formal-sum(K;S)) ∧ (b ∈ basic-formal-sum(K;S)) ∧ bfs-equiv(K;S;a;b)))
13. y ∈ basic-formal-sum(K;S)
14. y1 ∈ basic-formal-sum(K;S)
15. bfs-equiv(K;S;y;y1)
16. EquivRel(basic-formal-sum(K;S);a,b.bfs-equiv(K;S;a;b))
⊢ bfs-equiv(K;S;x + y;y1 + x1)
BY
{ (UseTrans ⌜y + x⌝⋅ THENL [(InstHyp [⌜x⌝;⌜y⌝] 3⋅ THEN Auto); (BLemma `formal-sum-add_functionality` THEN Auto)]) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  S  :  Type
2.  K  :  RngSig
3.  \mforall{}[x,y:basic-formal-sum(K;S)].    (x  +  y  =  y  +  x)
4.  x  :  Base
5.  x1  :  Base
6.  x  =  x1
7.  x  \mmember{}  basic-formal-sum(K;S)
8.  x1  \mmember{}  basic-formal-sum(K;S)
9.  bfs-equiv(K;S;x;x1)
10.  y  :  Base
11.  y1  :  Base
12.  y  =  y1
13.  y  \mmember{}  basic-formal-sum(K;S)
14.  y1  \mmember{}  basic-formal-sum(K;S)
15.  bfs-equiv(K;S;y;y1)
16.  EquivRel(basic-formal-sum(K;S);a,b.bfs-equiv(K;S;a;b))
\mvdash{}  bfs-equiv(K;S;x  +  y;y1  +  x1)


By

---

Latex:
(UseTrans  \mkleeneopen{}y  +  x\mkleeneclose{}\mcdot{}
  THENL  [(InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  3\mcdot{}  THEN  Auto);  (BLemma  `formal-sum-add\_functionality`  THEN  Auto)]
)

---

Home Index