---

Step * 3 of Lemma per-union_wf


1. A : Type
2. B : Type
3. x : Base
4. y : Base
5. z : Base
6. (x)↓
7. (y)↓
8. if x is inl then if y is inl then outl(x) = outl(y) ∈ A
                    else per-void()
   else if x is inr then if y is inr then outr(x) = outr(y) ∈ B
                         else per-void()
        else per-void() 
   supposing uand((x)↓;(y)↓)
9. (y)↓
10. (z)↓
11. if y is inl then if z is inl then outl(y) = outl(z) ∈ A
                     else per-void()
    else if y is inr then if z is inr then outr(y) = outr(z) ∈ B
                          else per-void()
         else per-void() 
    supposing uand((y)↓;(z)↓)
12. uand((x)↓;(z)↓)
⊢ Ax ∈ if x is inl then if z is inl then outl(x) = outl(z) ∈ A
                        else per-void()
       else if x is inr then if z is inr then outr(x) = outr(z) ∈ B
                             else per-void()
            else per-void()
BY
{ (Thin (-1)
   THEN (MoveToConcl (-1) THEN MoveToConcl 8)
   THEN Repeat ((CanonicalTestCases⋅ THENA Auto))
   THEN RepeatFor 2 (((D 0 THENA Auto) THEN (D -1 THENA (DUand 0 THEN Auto))))
   THEN Try (PerVoid)
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  x  :  Base
4.  y  :  Base
5.  z  :  Base
6.  (x)\mdownarrow{}
7.  (y)\mdownarrow{}
8.  if  x  is  inl  then  if  y  is  inl  then  outl(x)  =  outl(y)
                                        else  per-void()
      else  if  x  is  inr  then  if  y  is  inr  then  outr(x)  =  outr(y)
                                                  else  per-void()
                else  per-void() 
      supposing  uand((x)\mdownarrow{};(y)\mdownarrow{})
9.  (y)\mdownarrow{}
10.  (z)\mdownarrow{}
11.  if  y  is  inl  then  if  z  is  inl  then  outl(y)  =  outl(z)
                                          else  per-void()
        else  if  y  is  inr  then  if  z  is  inr  then  outr(y)  =  outr(z)
                                                    else  per-void()
                  else  per-void() 
        supposing  uand((y)\mdownarrow{};(z)\mdownarrow{})
12.  uand((x)\mdownarrow{};(z)\mdownarrow{})
\mvdash{}  Ax  \mmember{}  if  x  is  inl  then  if  z  is  inl  then  outl(x)  =  outl(z)
                                                else  per-void()
              else  if  x  is  inr  then  if  z  is  inr  then  outr(x)  =  outr(z)
                                                          else  per-void()
                        else  per-void()


By

---

Latex:
(Thin  (-1)
  THEN  (MoveToConcl  (-1)  THEN  MoveToConcl  8)
  THEN  Repeat  ((CanonicalTestCases\mcdot{}  THENA  Auto))
  THEN  RepeatFor  2  (((D  0  THENA  Auto)  THEN  (D  -1  THENA  (DUand  0  THEN  Auto))))
  THEN  Try  (PerVoid)
  THEN  Auto)

---

Home Index