---

Step * of Lemma bag-maximal?-iff

∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x:T].  uiff(↑bag-maximal?(b;x;R);∀y:T. (y ↓∈ b ⇒ (↑(R x y))))
BY
{ ((UnivCD THENA Auto)
   THEN D 0
   THEN Auto
   THEN Try (Complete (((FLemma `bag-maximal?-max` [-1;-3] THENA Auto) THEN Auto)))
   THEN (BagToList 2 THENA Auto)
   THEN ListInd 2
   THEN (UnivCD THENA Auto)
   THEN Try (Complete ((RepUR ``bag-maximal? bag-accum`` 0 THEN Auto)))) }

1
1. T : Type
2. R : T ⟶ T ⟶ 𝔹
3. x : T
4. u : T
5. v : T List
6. (∀y:T. (y ↓∈ v ⇒ (↑(R x y)))) ⇒ (↑bag-maximal?(v;x;R))
7. ∀y:T. (y ↓∈ [u / v] ⇒ (↑(R x y)))
⊢ ↑bag-maximal?([u / v];x;R)

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  0
  THEN  Auto
  THEN  Try  (Complete  (((FLemma  `bag-maximal?-max`  [-1;-3]  THENA  Auto)  THEN  Auto)))
  THEN  (BagToList  2  THENA  Auto)
  THEN  ListInd  2
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  (Complete  ((RepUR  ``bag-maximal?  bag-accum``  0  THEN  Auto))))

---

Home Index