---

Step * 2 of Lemma continuous-monotone-co-value


1. T : Type
2. S : Type
3. atomic-values() ⋂ (S × S) ⋃ (S + S)
⊢ False
BY
{ (RenameVar `x' (-1)
   THEN (Assert ↑is-atomic(x) BY
               ((GenConcl ⌜x = v ∈ atomic-values()⌝⋅ THENA Auto) THEN D -2 THEN Unhide THEN Auto))
   THEN MoveToConcl (-1)⋅
   THEN (GenConcl ⌜x = c ∈ ((S × S) ⋃ (S + S))⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. S : Type
2. c : (S × S) ⋃ (S + S)
⊢ (↑is-atomic(c)) ⇒ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  S  :  Type
3.  atomic-values()  \mcap{}  (S  \mtimes{}  S)  \mcup{}  (S  +  S)
\mvdash{}  False


By

---

Latex:
(RenameVar  `x'  (-1)
  THEN  (Assert  \muparrow{}is-atomic(x)  BY
                          ((GenConcl  \mkleeneopen{}x  =  v\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Unhide  THEN  Auto))
  THEN  MoveToConcl  (-1)\mcdot{}
  THEN  (GenConcl  \mkleeneopen{}x  =  c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index