---

Step * of Lemma bfs-reduce-strong-subtype

∀[K:RngSig]. ∀[S,T:Type].
  ∀[as,bs:basic-formal-sum(K;S)].  (bfs-reduce(K;T;as;bs) ⇒ bfs-reduce(K;S;as;bs)) supposing strong-subtype(S;T)
BY
{ (Auto
   THEN (InstLemma `basic-formal-sum-strong-subtype` [⌜K⌝;⌜S⌝;⌜T⌝]⋅ THENA Auto)
   THEN (FLemma `strong-subtype-implies` [-1] THENA Auto)
   THEN RepeatFor 2 (ParallelOp -3)
   THEN ExRepD) }

1
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)))
⊢ ∃s:bag(S). (as = (bs + 0 * s) ∈ 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)))
⊢ ∃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:
\mforall{}[K:RngSig].  \mforall{}[S,T:Type].
    \mforall{}[as,bs:basic-formal-sum(K;S)].    (bfs-reduce(K;T;as;bs)  {}\mRightarrow{}  bfs-reduce(K;S;as;bs)) 
    supposing  strong-subtype(S;T)


By

---

Latex:
(Auto
  THEN  (InstLemma  `basic-formal-sum-strong-subtype`  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (FLemma  `strong-subtype-implies`  [-1]  THENA  Auto)
  THEN  RepeatFor  2  (ParallelOp  -3)
  THEN  ExRepD)

---

Home Index