---

Step * of Lemma bfs-reduce-subtype1

∀[K:RngSig]. ∀[S,T:Type].
  ∀[as,bs:basic-formal-sum(K;S)].  (bfs-reduce(K;S;as;bs) ⇒ bfs-reduce(K;T;as;bs)) supposing S ⊆r T
BY
{ (Auto THEN RepeatFor 8 (ParallelLast)) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepeatFor  8  (ParallelLast))

---

Home Index