Step * 1 of Lemma product-Leibniz-type


1. Type
2. A ⟶ Type
3. ∀x,y:A.  Dec(x y ∈ A)
4. ∀a:A
     ∃sep:B[a] ⟶ B[a] ⟶ ℙ
      ((∀x,y:B[a].  ((sep y)  (∀z:B[a]. ((sep z) ∨ (sep z))))) ∧ (∀x,y:B[a].  (x y ∈ B[a] ⇐⇒ ¬(sep y))))
5. a:A ⟶ B[a] ⟶ B[a] ⟶ ℙ
6. ∀a:A. ((∀x,y:B[a].  ((s y)  (∀z:B[a]. ((s z) ∨ (s z))))) ∧ (∀x,y:B[a].  (x y ∈ B[a] ⇐⇒ ¬(s y))))
⊢ ∃sep:(a:A × B[a]) ⟶ (a:A × B[a]) ⟶ ℙ
   ((∀x,y:a:A × B[a].  ((sep y)  (∀z:a:A × B[a]. ((sep z) ∨ (sep z)))))
   ∧ (∀x,y:a:A × B[a].  (x y ∈ (a:A × B[a]) ⇐⇒ ¬(sep y))))
BY
((D With ⌜λp,q. (((fst(p)) (fst(q)) ∈ A)  (s (fst(p)) (snd(p)) (snd(q))))⌝  THENW Auto)
   THEN Reduce 0
   THEN 0
   THEN (UnivCD THENA Auto)
   THEN DVar `x'
   THEN DVar `y'
   THEN Try (DVar `z')
   THEN All Reduce) }

1
1. Type
2. A ⟶ Type
3. ∀x,y:A.  Dec(x y ∈ A)
4. ∀a:A
     ∃sep:B[a] ⟶ B[a] ⟶ ℙ
      ((∀x,y:B[a].  ((sep y)  (∀z:B[a]. ((sep z) ∨ (sep z))))) ∧ (∀x,y:B[a].  (x y ∈ B[a] ⇐⇒ ¬(sep y))))
5. a:A ⟶ B[a] ⟶ B[a] ⟶ ℙ
6. ∀a:A. ((∀x,y:B[a].  ((s y)  (∀z:B[a]. ((s z) ∨ (s z))))) ∧ (∀x,y:B[a].  (x y ∈ B[a] ⇐⇒ ¬(s y))))
7. A
8. x1 B[a]
9. a1 A
10. y1 B[a1]
11. (a a1 ∈ A)  (s x1 y1)
12. a2 A
13. z1 B[a2]
⊢ ((a a2 ∈ A)  (s x1 z1)) ∨ ((a1 a2 ∈ A)  (s a1 y1 z1))

2
1. Type
2. A ⟶ Type
3. ∀x,y:A.  Dec(x y ∈ A)
4. ∀a:A
     ∃sep:B[a] ⟶ B[a] ⟶ ℙ
      ((∀x,y:B[a].  ((sep y)  (∀z:B[a]. ((sep z) ∨ (sep z))))) ∧ (∀x,y:B[a].  (x y ∈ B[a] ⇐⇒ ¬(sep y))))
5. a:A ⟶ B[a] ⟶ B[a] ⟶ ℙ
6. ∀a:A. ((∀x,y:B[a].  ((s y)  (∀z:B[a]. ((s z) ∨ (s z))))) ∧ (∀x,y:B[a].  (x y ∈ B[a] ⇐⇒ ¬(s y))))
7. A
8. x1 B[a]
9. a1 A
10. y1 B[a1]
⊢ <a, x1> = <a1, y1> ∈ (a:A × B[a]) ⇐⇒ ¬((a a1 ∈ A)  (s x1 y1))


Latex:


Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  \mforall{}x,y:A.    Dec(x  =  y)
4.  \mforall{}a:A
          \mexists{}sep:B[a]  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbP{}
            ((\mforall{}x,y:B[a].    ((sep  x  y)  {}\mRightarrow{}  (\mforall{}z:B[a].  ((sep  x  z)  \mvee{}  (sep  y  z)))))
            \mwedge{}  (\mforall{}x,y:B[a].    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(sep  x  y))))
5.  s  :  a:A  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}a:A
          ((\mforall{}x,y:B[a].    ((s  a  x  y)  {}\mRightarrow{}  (\mforall{}z:B[a].  ((s  a  x  z)  \mvee{}  (s  a  y  z)))))
          \mwedge{}  (\mforall{}x,y:B[a].    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(s  a  x  y))))
\mvdash{}  \mexists{}sep:(a:A  \mtimes{}  B[a])  {}\mrightarrow{}  (a:A  \mtimes{}  B[a])  {}\mrightarrow{}  \mBbbP{}
      ((\mforall{}x,y:a:A  \mtimes{}  B[a].    ((sep  x  y)  {}\mRightarrow{}  (\mforall{}z:a:A  \mtimes{}  B[a].  ((sep  x  z)  \mvee{}  (sep  y  z)))))
      \mwedge{}  (\mforall{}x,y:a:A  \mtimes{}  B[a].    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(sep  x  y))))


By


Latex:
((D  0  With  \mkleeneopen{}\mlambda{}p,q.  (((fst(p))  =  (fst(q)))  {}\mRightarrow{}  (s  (fst(p))  (snd(p))  (snd(q))))\mkleeneclose{}    THENW  Auto)
  THEN  Reduce  0
  THEN  D  0
  THEN  (UnivCD  THENA  Auto)
  THEN  DVar  `x'
  THEN  DVar  `y'
  THEN  Try  (DVar  `z')
  THEN  All  Reduce)




Home Index