---

Step * of Lemma formal-sum-subtype

∀[K:RngSig]. ∀[S,T:Type].  formal-sum(K;S) ⊆r formal-sum(K;T) supposing S ⊆r T
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN EqTypeCD
   THEN Auto
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜x = a ∈ basic-formal-sum(K;S)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜x1 = b ∈ basic-formal-sum(K;S)⌝⋅ THENA Auto)
   THEN ThinVar `x'
   THEN ThinVar `x1'
   THEN (D 0 THENA Auto)) }

1
1. K : RngSig
2. S : Type
3. T : Type
4. S ⊆r T
5. a : basic-formal-sum(K;S)
6. b : basic-formal-sum(K;S)
7. bfs-equiv(K;S;a;b)
⊢ bfs-equiv(K;T;a;b)

---

Latex:

---

Latex:
\mforall{}[K:RngSig].  \mforall{}[S,T:Type].    formal-sum(K;S)  \msubseteq{}r  formal-sum(K;T)  supposing  S  \msubseteq{}r  T


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  EqTypeCD
  THEN  Auto
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}x  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}x1  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `x'
  THEN  ThinVar  `x1'
  THEN  (D  0  THENA  Auto))

---

Home Index