---

Step * of Lemma int-product-union-atom-disjoint

∀[T,S,A,B:Type].  (¬ℤ ⋂ (T × S) ⋃ (A + B) ⋃ Atom)
BY
{ (Auto
   THEN (D 0 THEN Auto)
   THEN RenameVar `x' (-1)
   THEN Isect2HD (-1)
   THEN (Assert ↑isint(x) BY
               (GenConclAtAddr [1;1] THEN Reduce 0 THEN Auto))
   THEN MoveToConcl (-1)
   THEN GenConcl ⌜x = z ∈ ((T × S) ⋃ (A + B) ⋃ Atom)⌝⋅
   THEN Auto
   THEN Repeat (OnSomeHyp D_b_union)
   THEN Try (Complete ((DProdsAndUnions THEN AllReduce THEN Auto)))
   THEN Try ((CanonicalTestCases THEN Auto THEN Fold `has-value` 0 THEN Auto))
   THEN MoveToConcl (-1)
   THEN Fold `not` 0
   THEN BLemma `isatom-implies-not-isint`
   THEN Auto
   THEN (Subst ⌜isatom(a1) ~ tt⌝ 0⋅ THENM Auto)
   THEN IsatomReduceTrue
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,S,A,B:Type].    (\mneg{}\mBbbZ{}  \mcap{}  (T  \mtimes{}  S)  \mcup{}  (A  +  B)  \mcup{}  Atom)


By

---

Latex:
(Auto
  THEN  (D  0  THEN  Auto)
  THEN  RenameVar  `x'  (-1)
  THEN  Isect2HD  (-1)
  THEN  (Assert  \muparrow{}isint(x)  BY
                          (GenConclAtAddr  [1;1]  THEN  Reduce  0  THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  GenConcl  \mkleeneopen{}x  =  z\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Repeat  (OnSomeHyp  D\_b\_union)
  THEN  Try  (Complete  ((DProdsAndUnions  THEN  AllReduce  THEN  Auto)))
  THEN  Try  ((CanonicalTestCases  THEN  Auto  THEN  Fold  `has-value`  0  THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  Fold  `not`  0
  THEN  BLemma  `isatom-implies-not-isint`
  THEN  Auto
  THEN  (Subst  \mkleeneopen{}isatom(a1)  \msim{}  tt\mkleeneclose{}  0\mcdot{}  THENM  Auto)
  THEN  IsatomReduceTrue
  THEN  Auto)

---

Home Index