---

Step * 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. cs : basic-formal-sum(K;T)
8. k : |K|
9. k' : |K|
10. fs : basic-formal-sum(K;T)
11. as = (cs + k +K k' * fs) ∈ basic-formal-sum(K;T)
12. bs = (cs + k * fs + k' * fs) ∈ basic-formal-sum(K;T)
13. strong-subtype(basic-formal-sum(K;S);basic-formal-sum(K;T))
14. ∀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)))
⊢ ∃cs:basic-formal-sum(K;S)
   ∃k,k':|K|
    ∃fs:basic-formal-sum(K;S)
     ((as = (cs + k +K k' * fs) ∈ basic-formal-sum(K;S)) ∧ (bs = (cs + k * fs + k' * fs) ∈ basic-formal-sum(K;S)))
BY
{ Assert ⌜cs ∈ basic-formal-sum(K;S)⌝⋅ }

1
.....assertion..... 
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. cs : basic-formal-sum(K;T)
8. k : |K|
9. k' : |K|
10. fs : basic-formal-sum(K;T)
11. as = (cs + k +K k' * fs) ∈ basic-formal-sum(K;T)
12. bs = (cs + k * fs + k' * fs) ∈ basic-formal-sum(K;T)
13. strong-subtype(basic-formal-sum(K;S);basic-formal-sum(K;T))
14. ∀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)))
⊢ cs ∈ basic-formal-sum(K;S)

2
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. cs : basic-formal-sum(K;T)
8. k : |K|
9. k' : |K|
10. fs : basic-formal-sum(K;T)
11. as = (cs + k +K k' * fs) ∈ basic-formal-sum(K;T)
12. bs = (cs + k * fs + k' * fs) ∈ basic-formal-sum(K;T)
13. strong-subtype(basic-formal-sum(K;S);basic-formal-sum(K;T))
14. ∀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)))
15. cs ∈ basic-formal-sum(K;S)
⊢ ∃cs:basic-formal-sum(K;S)
   ∃k,k':|K|
    ∃fs:basic-formal-sum(K;S)
     ((as = (cs + k +K k' * fs) ∈ basic-formal-sum(K;S)) ∧ (bs = (cs + k * fs + k' * fs) ∈ basic-formal-sum(K;S)))

---

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.  cs  :  basic-formal-sum(K;T)
8.  k  :  |K|
9.  k'  :  |K|
10.  fs  :  basic-formal-sum(K;T)
11.  as  =  (cs  +  k  +K  k'  *  fs)
12.  bs  =  (cs  +  k  *  fs  +  k'  *  fs)
13.  strong-subtype(basic-formal-sum(K;S);basic-formal-sum(K;T))
14.  \mforall{}b:basic-formal-sum(K;T).  \mforall{}a:basic-formal-sum(K;S).    ((b  =  a)  {}\mRightarrow{}  (b  =  a))
\mvdash{}  \mexists{}cs:basic-formal-sum(K;S)
      \mexists{}k,k':|K|
        \mexists{}fs:basic-formal-sum(K;S).  ((as  =  (cs  +  k  +K  k'  *  fs))  \mwedge{}  (bs  =  (cs  +  k  *  fs  +  k'  *  fs)))


By

---

Latex:
Assert  \mkleeneopen{}cs  \mmember{}  basic-formal-sum(K;S)\mkleeneclose{}\mcdot{}

---

Home Index