---

Step * 1 2 of Lemma bfs-reduce-strong-subtype


1. [K] : RngSig
2. [S] : Type
3. [T] : Type
4. strong-subtype(S;T)
5. [as] : basic-formal-sum(K;S)
6. [bs] : basic-formal-sum(K;S)
7. s : bag(T)
8. as = (bs + 0 * s) ∈ basic-formal-sum(K;T)
9. strong-subtype(basic-formal-sum(K;S);basic-formal-sum(K;T))
10. ∀b:basic-formal-sum(K;T). ∀a:basic-formal-sum(K;S).
      ((b = a ∈ basic-formal-sum(K;T)) ⇒ (b = a ∈ basic-formal-sum(K;S)))
11. s ∈ bag(S)
⊢ ∃s:bag(S). (as = (bs + 0 * s) ∈ basic-formal-sum(K;S))
BY
{ (All (Fold `formal-sum-add`) THEN D 0 With ⌜s⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  [K]  :  RngSig
2.  [S]  :  Type
3.  [T]  :  Type
4.  strong-subtype(S;T)
5.  [as]  :  basic-formal-sum(K;S)
6.  [bs]  :  basic-formal-sum(K;S)
7.  s  :  bag(T)
8.  as  =  (bs  +  0  *  s)
9.  strong-subtype(basic-formal-sum(K;S);basic-formal-sum(K;T))
10.  \mforall{}b:basic-formal-sum(K;T).  \mforall{}a:basic-formal-sum(K;S).    ((b  =  a)  {}\mRightarrow{}  (b  =  a))
11.  s  \mmember{}  bag(S)
\mvdash{}  \mexists{}s:bag(S).  (as  =  (bs  +  0  *  s))


By

---

Latex:
(All  (Fold  `formal-sum-add`)  THEN  D  0  With  \mkleeneopen{}s\mkleeneclose{}    THEN  Auto)

---

Home Index