---

Step * of Lemma omral_times_sd_ordered

∀g:OCMon. ∀r:CDRng. ∀ps,qs:(|g| × |r|) List.
  ((↑sd_ordered(map(λz.(fst(z));qs))) ⇒ (↑sd_ordered(map(λz.(fst(z));ps ** qs))))
BY
{ TACTIC:(InductionOnListA THEN Reduce 0 THEN Auto) }

1
1. g : OCMon
2. r : CDRng
3. p : |g| × |r|
4. ps : (|g| × |r|) List
5. ∀qs:(|g| × |r|) List. ((↑sd_ordered(map(λz.(fst(z));qs))) ⇒ (↑sd_ordered(map(λz.(fst(z));ps ** qs))))
6. qs : (|g| × |r|) List
7. ↑sd_ordered(map(λz.(fst(z));qs))
⊢ ↑sd_ordered(map(λz.(fst(z));[p / ps] ** qs))

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}ps,qs:(|g|  \mtimes{}  |r|)  List.
    ((\muparrow{}sd\_ordered(map(\mlambda{}z.(fst(z));qs)))  {}\mRightarrow{}  (\muparrow{}sd\_ordered(map(\mlambda{}z.(fst(z));ps  **  qs))))


By

---

Latex:
TACTIC:(InductionOnListA  THEN  Reduce  0  THEN  Auto)

---

Home Index