---

Step * of Lemma union-ss_wf

∀[ss1,ss2:SeparationSpace].  (ss1 + ss2 ∈ SeparationSpace)
BY
{ (Auto
   THEN Unfold `union-ss` 0
   THEN MemCD
   THEN Try ((MemTypeCD THEN Reduce 0 THEN Auto THEN D -1 THEN RepUR ``union-sep`` 0 THEN Auto))
   THEN Reduce 0
   THEN RepeatFor 3 ((MemCD THENA Auto))) }

1
.....subterm..... T:t
1:n
1. ss1 : SeparationSpace
2. ss2 : SeparationSpace
3. x : Point(ss1) + Point(ss2)
4. y : Point(ss1) + Point(ss2)
5. z : Point(ss1) + Point(ss2)
⊢ λsep.case x
        of inl(a) =>
        case y
         of inl(a') =>
         case z of inl(a'') => ss1."#or" a a' a'' sep | inr(_) => inl Ax
         | inr(b') =>
         case z of inl(_) => inr Ax  | inr(_) => inl Ax
        | inr(b) =>
        case y
         of inl(a') =>
         case z of inl(_) => inl Ax | inr(_) => inr Ax 
         | inr(b') =>
         case z of inl(_) => inl Ax | inr(b'') => ss2."#or" b b' b'' sep ∈ union-sep(ss1;ss2;x;y)
  ⇒ (union-sep(ss1;ss2;x;z) ∨ union-sep(ss1;ss2;y;z))

---

Latex:

---

Latex:
\mforall{}[ss1,ss2:SeparationSpace].    (ss1  +  ss2  \mmember{}  SeparationSpace)


By

---

Latex:
(Auto
  THEN  Unfold  `union-ss`  0
  THEN  MemCD
  THEN  Try  ((MemTypeCD  THEN  Reduce  0  THEN  Auto  THEN  D  -1  THEN  RepUR  ``union-sep``  0  THEN  Auto))
  THEN  Reduce  0
  THEN  RepeatFor  3  ((MemCD  THENA  Auto)))

---

Home Index