---

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


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 : formal-sum(K;S)
5. y : formal-sum(K;S)
⊢ x + y = y + x ∈ formal-sum(K;S)
BY
{ ((InstLemma `bfs-equiv-rel` [⌜K⌝;⌜S⌝]⋅ THENA Auto) THEN DVar `x' THEN Try (DVar `y') THEN EqTypeCD THEN Auto) }

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

---

Latex:

---

Latex:

1.  S  :  Type
2.  K  :  RngSig
3.  \mforall{}[x,y:basic-formal-sum(K;S)].    (x  +  y  =  y  +  x)
4.  x  :  formal-sum(K;S)
5.  y  :  formal-sum(K;S)
\mvdash{}  x  +  y  =  y  +  x


By

---

Latex:
((InstLemma  `bfs-equiv-rel`  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  DVar  `x'
  THEN  Try  (DVar  `y')
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index