---

Step * of Lemma bag-maximal?-max

∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x,y:T].  (↑(R x y)) supposing ((↑bag-maximal?(b;x;R)) and y ↓∈ b)
BY
{ ((UnivCD THENA Auto)
   THEN (BagToList 2 THENA Auto)
   THEN ListInd 2
   THEN (UnivCD THENA Auto)
   THEN BagMemberD (-2)
   THEN Auto
   THEN Fold `cons-bag` (-1)
   THEN RWO "bag-maximal?-cons" (-1)⋅
   THEN Auto
   THEN RepeatFor 2 ((D (-3) THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x,y:T].
    (\muparrow{}(R  x  y))  supposing  ((\muparrow{}bag-maximal?(b;x;R))  and  y  \mdownarrow{}\mmember{}  b)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (BagToList  2  THENA  Auto)
  THEN  ListInd  2
  THEN  (UnivCD  THENA  Auto)
  THEN  BagMemberD  (-2)
  THEN  Auto
  THEN  Fold  `cons-bag`  (-1)
  THEN  RWO  "bag-maximal?-cons"  (-1)\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  ((D  (-3)  THEN  Auto)))

---

Home Index