---

Step * of Lemma bag-maximal?-cons

∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x,v:T].  uiff(↑bag-maximal?(v.b;x;R);(↑bag-maximal?(b;x;R)) ∧ (↑(R x v)))
BY
{ ((UnivCD THENA Auto)
   THEN (Subst ⌜v.b ~ {v} + b⌝ 0⋅ THENA (RepUR ``bag-append single-bag cons-bag`` 0 THEN Auto))
   THEN (RWO "bag-maximal?-append" 0 THENA Auto)
   THEN Auto
   THEN Try (Complete ((RWO "bag-maximal?-single" (-2) THEN Auto)))
   THEN Try (Complete ((RWO "bag-maximal?-single" 0 THEN Auto)))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x,v:T].
    uiff(\muparrow{}bag-maximal?(v.b;x;R);(\muparrow{}bag-maximal?(b;x;R))  \mwedge{}  (\muparrow{}(R  x  v)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}v.b  \msim{}  \{v\}  +  b\mkleeneclose{}  0\mcdot{}  THENA  (RepUR  ``bag-append  single-bag  cons-bag``  0  THEN  Auto))
  THEN  (RWO  "bag-maximal?-append"  0  THENA  Auto)
  THEN  Auto
  THEN  Try  (Complete  ((RWO  "bag-maximal?-single"  (-2)  THEN  Auto)))
  THEN  Try  (Complete  ((RWO  "bag-maximal?-single"  0  THEN  Auto))))

---

Home Index