---

Step * of Lemma poset-cat-arrow-cases

No Annotations
∀I:Cname List. ∀c1,c2:cat-ob(poset-cat(I)). ∀f:cat-arrow(poset-cat(I)) c1 c2.
  ((c1 = c2 ∈ cat-ob(poset-cat(I)))
  ∨ (∃y:{y:nameset(I)| (c1 y) = 0 ∈ ℕ2} . (c2 = flip(c1;y) ∈ cat-ob(poset-cat(I))))
  ∨ (∃c3:cat-ob(poset-cat(I))
      ∃g:cat-arrow(poset-cat(I)) c1 c3
       ∃h:cat-arrow(poset-cat(I)) c3 c2. ((¬(c1 = c3 ∈ cat-ob(poset-cat(I)))) ∧ (¬(c2 = c3 ∈ cat-ob(poset-cat(I)))))))
BY
{ (InstLemma `poset-cat-ob-cases` []
   THEN RepeatFor 3 (ParallelLast')
   THEN Auto
   THEN ParallelOp -2
   THEN ExRepD
   THEN (InstLemma `poset-cat-arrow-not-equal` [⌜I⌝;⌜y⌝;⌜c1⌝;⌜c2⌝;⌜f⌝]⋅ THENA Auto)
   THEN Decide ⌜c2 = flip(c1;y) ∈ cat-ob(poset-cat(I))⌝⋅
   THEN Auto
   THEN OrRight
   THEN Auto
   THEN InstConcl [⌜flip(c1;y)⌝;⌜λi.Ax⌝;⌜λi.Ax⌝]⋅
   THEN Auto) }

1
.....wf..... 
1. I : Cname List
2. c1 : cat-ob(poset-cat(I))
3. c2 : cat-ob(poset-cat(I))
4. y : nameset(I)
5. c1 y ≠ c2 y
6. f : cat-arrow(poset-cat(I)) c1 c2
7. (c1 y) = 0 ∈ ℕ2
8. (c2 y) = 1 ∈ ℕ2
9. ¬(c2 = flip(c1;y) ∈ cat-ob(poset-cat(I)))
⊢ λi.Ax ∈ cat-arrow(poset-cat(I)) c1 flip(c1;y)

2
.....wf..... 
1. I : Cname List
2. c1 : cat-ob(poset-cat(I))
3. c2 : cat-ob(poset-cat(I))
4. y : nameset(I)
5. c1 y ≠ c2 y
6. f : cat-arrow(poset-cat(I)) c1 c2
7. (c1 y) = 0 ∈ ℕ2
8. (c2 y) = 1 ∈ ℕ2
9. ¬(c2 = flip(c1;y) ∈ cat-ob(poset-cat(I)))
⊢ λi.Ax ∈ cat-arrow(poset-cat(I)) flip(c1;y) c2

3
1. I : Cname List
2. c1 : cat-ob(poset-cat(I))
3. c2 : cat-ob(poset-cat(I))
4. y : nameset(I)
5. c1 y ≠ c2 y
6. f : cat-arrow(poset-cat(I)) c1 c2
7. (c1 y) = 0 ∈ ℕ2
8. (c2 y) = 1 ∈ ℕ2
9. ¬(c2 = flip(c1;y) ∈ cat-ob(poset-cat(I)))
⊢ ¬(c1 = flip(c1;y) ∈ cat-ob(poset-cat(I)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:Cname  List.  \mforall{}c1,c2:cat-ob(poset-cat(I)).  \mforall{}f:cat-arrow(poset-cat(I))  c1  c2.
    ((c1  =  c2)
    \mvee{}  (\mexists{}y:\{y:nameset(I)|  (c1  y)  =  0\}  .  (c2  =  flip(c1;y)))
    \mvee{}  (\mexists{}c3:cat-ob(poset-cat(I))
            \mexists{}g:cat-arrow(poset-cat(I))  c1  c3
              \mexists{}h:cat-arrow(poset-cat(I))  c3  c2.  ((\mneg{}(c1  =  c3))  \mwedge{}  (\mneg{}(c2  =  c3)))))


By

---

Latex:
(InstLemma  `poset-cat-ob-cases`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Auto
  THEN  ParallelOp  -2
  THEN  ExRepD
  THEN  (InstLemma  `poset-cat-arrow-not-equal`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Decide  \mkleeneopen{}c2  =  flip(c1;y)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  OrRight
  THEN  Auto
  THEN  InstConcl  [\mkleeneopen{}flip(c1;y)\mkleeneclose{};\mkleeneopen{}\mlambda{}i.Ax\mkleeneclose{};\mkleeneopen{}\mlambda{}i.Ax\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index