---

Step * 1 2 of Lemma prod-Leibniz-type


1. A : Type
2. B : Type
3. s1 : A ⟶ A ⟶ ℙ
4. ∀x,y:A.  ((s1 x y) ⇒ (∀z:A. ((s1 x z) ∨ (s1 y z))))
5. ∀x,y:A.  (x = y ∈ A ⇐⇒ ¬(s1 x y))
6. sep : B ⟶ B ⟶ ℙ
7. ∀x,y:B.  ((sep x y) ⇒ (∀z:B. ((sep x z) ∨ (sep y z))))
8. ∀x,y:B.  (x = y ∈ B ⇐⇒ ¬(sep x y))
9. x1 : A
10. x2 : B
11. y1 : A
12. y2 : B
13. sep x2 y2
14. z1 : A
15. z2 : B
⊢ ((s1 x1 z1) ∨ (sep x2 z2)) ∨ (s1 y1 z1) ∨ (sep y2 z2)
BY
{ ((Assert (sep x2 z2) ∨ (sep y2 z2) BY Auto) THEN ParallelLast THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  s1  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x,y:A.    ((s1  x  y)  {}\mRightarrow{}  (\mforall{}z:A.  ((s1  x  z)  \mvee{}  (s1  y  z))))
5.  \mforall{}x,y:A.    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(s1  x  y))
6.  sep  :  B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
7.  \mforall{}x,y:B.    ((sep  x  y)  {}\mRightarrow{}  (\mforall{}z:B.  ((sep  x  z)  \mvee{}  (sep  y  z))))
8.  \mforall{}x,y:B.    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(sep  x  y))
9.  x1  :  A
10.  x2  :  B
11.  y1  :  A
12.  y2  :  B
13.  sep  x2  y2
14.  z1  :  A
15.  z2  :  B
\mvdash{}  ((s1  x1  z1)  \mvee{}  (sep  x2  z2))  \mvee{}  (s1  y1  z1)  \mvee{}  (sep  y2  z2)


By

---

Latex:
((Assert  (sep  x2  z2)  \mvee{}  (sep  y2  z2)  BY  Auto)  THEN  ParallelLast  THEN  Auto)

---

Home Index