---

Step * of Lemma disjoint-union-classrel

∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E].
  ∀v:A + B. uiff(v ∈ X + Y(e);case v of inl(x) => x ∈ X(e) | inr(x) => x ∈ Y(e) ∧ (∀w:A. (¬w ∈ X(e))))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `disjoint-union-class` 0
   THEN RepUR ``classrel simple-comb-2 simple-comb`` 0
   THEN (Unhide THENA Auto)
   THEN Try (((D (-1) THEN Reduce 0) THEN Complete (Auto)))
   THEN (GenConcl ⌜(X es e) = a ∈ bag(A)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(Y es e) = b ∈ bag(B)⌝⋅ THENA Auto)
   THEN All Thin
   THEN OldAutoSplit
   THEN Try ((HypSubst (-1) 0 THENA Auto))
   THEN DVar `v'
   THEN Reduce 0
   THEN ((RWO "bag-member-map bag-member-empty-iff" 0 THENM Reduce 0) THENA Auto)
   THEN Auto
   THEN SqExRepD
   THEN Auto
   THEN RWW "empty-bag-iff-no-member" (-3)
   THEN Auto
   THEN (Try ((D 0 THEN With ⌜x⌝ (D 0)⋅ THEN Auto))⋅ THEN Try ((D 0 THEN With ⌜y⌝ (D 0)⋅ THEN Auto))⋅)⋅) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    \mforall{}v:A  +  B
        uiff(v  \mmember{}  X  +  Y(e);case  v  of  inl(x)  =>  x  \mmember{}  X(e)  |  inr(x)  =>  x  \mmember{}  Y(e)  \mwedge{}  (\mforall{}w:A.  (\mneg{}w  \mmember{}  X(e))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `disjoint-union-class`  0
  THEN  RepUR  ``classrel  simple-comb-2  simple-comb``  0
  THEN  (Unhide  THENA  Auto)
  THEN  Try  (((D  (-1)  THEN  Reduce  0)  THEN  Complete  (Auto)))
  THEN  (GenConcl  \mkleeneopen{}(X  es  e)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(Y  es  e)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  OldAutoSplit
  THEN  Try  ((HypSubst  (-1)  0  THENA  Auto))
  THEN  DVar  `v'
  THEN  Reduce  0
  THEN  ((RWO  "bag-member-map  bag-member-empty-iff"  0  THENM  Reduce  0)  THENA  Auto)
  THEN  Auto
  THEN  SqExRepD
  THEN  Auto
  THEN  RWW  "empty-bag-iff-no-member"  (-3)
  THEN  Auto
  THEN  (Try  ((D  0  THEN  With  \mkleeneopen{}x\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))\mcdot{}  THEN  Try  ((D  0  THEN  With  \mkleeneopen{}y\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))\mcdot{})
  \mcdot{})

---

Home Index