---

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


1. [K] : RngSig
2. [S] : Type
3. [T] : Type
4. strong-subtype(S;T)
5. [as] : bag(|K| × S)
6. [bs] : bag(|K| × S)
7. s : bag(T)
8. as = (bs + 0 * s) ∈ bag(|K| × T)
9. strong-subtype(bag(|K| × S);bag(|K| × T))
10. ∀b:bag(|K| × T). ∀a:bag(|K| × S).  ((b = a ∈ bag(|K| × T)) ⇒ (b = a ∈ bag(|K| × S)))
11. ∀x:|K| × T. (x ↓∈ 0 * s ⇒ x ↓∈ as)
12. 0 * s ∈ bag(|K| × S)
⊢ s ∈ bag(S)
BY
{ (BLemma `bag-in-subtype` THEN Auto) }

1
1. K : RngSig
2. S : Type
3. T : Type
4. strong-subtype(S;T)
5. as : bag(|K| × S)
6. bs : bag(|K| × S)
7. s : bag(T)
8. as = (bs + 0 * s) ∈ bag(|K| × T)
9. strong-subtype(bag(|K| × S);bag(|K| × T))
10. ∀b:bag(|K| × T). ∀a:bag(|K| × S).  ((b = a ∈ bag(|K| × T)) ⇒ (b = a ∈ bag(|K| × S)))
11. ∀x:|K| × T. (x ↓∈ 0 * s ⇒ x ↓∈ as)
12. 0 * s ∈ bag(|K| × S)
13. x : T
14. x ↓∈ s
⊢ x ∈ S

---

Latex:

---

Latex:

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


By

---

Latex:
(BLemma  `bag-in-subtype`  THEN  Auto)

---

Home Index