---

Step * 1 of Lemma comparison-seq-zero


1. T : Type
2. c1 : comparison(T)
3. c2 : ⋂a:T. comparison({b:T| (c1 a b) = 0 ∈ ℤ} )
4. x : T
5. y : T
⊢ uiff(if c1 x y=0  then c2 x y  else (c1 x y) = 0 ∈ ℤ;((c1 x y) = 0 ∈ ℤ) ∧ ((c2 x y) = 0 ∈ ℤ))
BY
{ (AutoSplit
   THEN (Assert c2 x y ∈ ℤ BY
               ((With ⌜x⌝ (D 3)⋅ THEN Auto)
                THEN (GenConcl ⌜c2 = X ∈ comparison({b:T| (c1 x b) = 0 ∈ ℤ} )⌝⋅ THEN Auto)
                THEN MemTypeCD
                THEN Auto
                THEN BLemma `comparison-reflexive`
                THEN Auto))
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  c1  :  comparison(T)
3.  c2  :  \mcap{}a:T.  comparison(\{b:T|  (c1  a  b)  =  0\}  )
4.  x  :  T
5.  y  :  T
\mvdash{}  uiff(if  c1  x  y=0    then  c2  x  y    else  (c1  x  y)  =  0;((c1  x  y)  =  0)  \mwedge{}  ((c2  x  y)  =  0))


By

---

Latex:
(AutoSplit
  THEN  (Assert  c2  x  y  \mmember{}  \mBbbZ{}  BY
                          ((With  \mkleeneopen{}x\mkleeneclose{}  (D  3)\mcdot{}  THEN  Auto)
                            THEN  (GenConcl  \mkleeneopen{}c2  =  X\mkleeneclose{}\mcdot{}  THEN  Auto)
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  BLemma  `comparison-reflexive`
                            THEN  Auto))
  THEN  Auto)

---

Home Index